%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ALG254^2 : TPTP v9.3.1. Bugfixed v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 : Wed Sep 30 07:45:25 AM UTC 2026
% Result : Theorem 1.53s 0.53s
% Output : Refutation 1.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG254^2 : TPTP v9.3.1. Bugfixed v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n009.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 17:34:00 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.53/0.53 % (116127)Will run a generic schedule for satisfiability detection.
% 1.53/0.53 % (116134)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1780781362:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.53/0.53 % (116133)% WARNING: option uhcvi not known.
% 1.53/0.53 % (116133)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3316618775:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.53/0.53 % (116132)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1550504207_2999 on theBenchmark for (2999ds/0Mi)
% 1.53/0.53 % (116135)dis+10_1_sil=32000:sp=arity:random_seed=743754846:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.53/0.53 % (116137)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1359767353:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.53/0.53 % (116136)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3867475644:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.53/0.53 % (116138)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2744936487:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.53/0.53 % (116133)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.53/0.53 % (116136)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.53/0.53 % Exception at run slice level
% 1.53/0.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.53/0.53 % (116133)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.53/0.53 % (116135)Instruction limit reached!
% 1.53/0.53 % (116135)------------------------------
% 1.53/0.53 % (116135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116135)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116135)Termination reason: Instruction limit
% 1.53/0.53 % (116135)Termination phase: Saturation
% 1.53/0.53 % (116135)Time elapsed: 0.043 s
% 1.53/0.53 % (116135)Peak memory usage: 12 MB
% 1.53/0.53 % (116135)Instructions burned: 105 (million)
% 1.53/0.53 % (116136)Instruction limit reached!
% 1.53/0.53 % (116136)------------------------------
% 1.53/0.53 % (116136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116136)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116136)Termination reason: Instruction limit
% 1.53/0.53 % (116136)Termination phase: Saturation
% 1.53/0.53 % (116136)Time elapsed: 0.048 s
% 1.53/0.53 % (116136)Peak memory usage: 12 MB
% 1.53/0.53 % (116136)Instructions burned: 117 (million)
% 1.53/0.53 % (116146)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3328958309:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.53/0.53 % (116137)Instruction limit reached!
% 1.53/0.53 % (116137)------------------------------
% 1.53/0.53 % (116137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116137)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116137)Termination reason: Instruction limit
% 1.53/0.53 % (116137)Termination phase: Saturation
% 1.53/0.53 % (116137)Time elapsed: 0.058 s
% 1.53/0.53 % (116137)Peak memory usage: 13 MB
% 1.53/0.53 % (116137)Instructions burned: 140 (million)
% 1.53/0.53 % (116147)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=150695607:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.53/0.53 % (116138)Instruction limit reached!
% 1.53/0.53 % (116138)------------------------------
% 1.53/0.53 % (116138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116138)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116138)Termination reason: Instruction limit
% 1.53/0.53 % (116138)Termination phase: Saturation
% 1.53/0.53 % (116138)Time elapsed: 0.066 s
% 1.53/0.53 % (116138)Peak memory usage: 13 MB
% 1.53/0.53 % (116138)Instructions burned: 160 (million)
% 1.53/0.53 % (116148)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3017421607:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.53/0.53 % (116150)ott-21_1_sil=16000:fs=off:random_seed=621895522:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.53/0.53 % (116153)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1672201042:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.53/0.53 % Exception at run slice level
% 1.53/0.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.53/0.53 % (116148)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.53/0.53 % (116148)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.53/0.53 % (116156)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2233091984:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.53/0.53 % (116147)Instruction limit reached!
% 1.53/0.53 % (116147)------------------------------
% 1.53/0.53 % (116147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116147)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116147)Termination reason: Instruction limit
% 1.53/0.53 % (116147)Termination phase: Saturation
% 1.53/0.53 % (116147)Time elapsed: 0.055 s
% 1.53/0.53 % (116147)Peak memory usage: 13 MB
% 1.53/0.53 % (116147)Instructions burned: 133 (million)
% 1.53/0.53 % (116158)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1049499363:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.53/0.53 % Exception at run slice level
% 1.53/0.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.53/0.53 % (116150)Instruction limit reached!
% 1.53/0.53 % (116150)------------------------------
% 1.53/0.53 % (116150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.53 % (116150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.53 % (116150)CaDiCaL version: 2.1.3
% 1.53/0.53 % (116150)Termination reason: Instruction limit
% 1.53/0.53 % (116150)Termination phase: Saturation
% 1.53/0.53 % (116150)Time elapsed: 0.075 s
% 1.53/0.53 % (116150)Peak memory usage: 13 MB
% 1.53/0.53 % (116150)Instructions burned: 180 (million)
% 1.53/0.53 % (116160)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3453419906:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.53/0.53 % (116161)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1804434041:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 1.53/0.53 % (116161)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.53/0.53 % Exception at run slice level
% 1.53/0.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.53/0.53 % (116164)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=36872157:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 1.53/0.53 % (116164)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.53/0.53 % (116153) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-116127-116153"...
% 1.53/0.53 % (116153)...printing done.
% 1.53/0.53 % (116153)Refutation found. Thanks to Tanya!
% 1.53/0.53 % SZS status Theorem for theBenchmark
% 1.53/0.53 % SZS output start Proof for theBenchmark
% 1.53/0.53 thf(type_def_5, type, term: $tType).
% 1.53/0.53 thf(type_def_6, type, subst: $tType).
% 1.53/0.53 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 1.53/0.53 thf(func_def_0, type, one: term).
% 1.53/0.53 thf(func_def_1, type, ap: (term > term > term)).
% 1.53/0.53 thf(func_def_2, type, lam: (term > term)).
% 1.53/0.53 thf(func_def_3, type, sub: (term > subst > term)).
% 1.53/0.53 thf(func_def_4, type, id: subst).
% 1.53/0.53 thf(func_def_5, type, sh: subst).
% 1.53/0.53 thf(func_def_6, type, push: (term > subst > subst)).
% 1.53/0.53 thf(func_def_7, type, comp: (subst > subst > subst)).
% 1.53/0.53 thf(func_def_8, type, var: (term > $o)).
% 1.53/0.53 thf(func_def_9, type, pushprop_lem1v2: $o).
% 1.53/0.53 thf(func_def_10, type, pushprop_lem1_gthm: $o).
% 1.53/0.53 thf(func_def_11, type, axmap: $o).
% 1.53/0.53 thf(func_def_12, type, pushprop_lem0_gthm: $o).
% 1.53/0.53 thf(func_def_13, type, shinj: $o).
% 1.53/0.53 thf(func_def_14, type, hoasinduction_lem1v2: $o).
% 1.53/0.53 thf(func_def_15, type, hoasinduction_lem1v2_gthm: $o).
% 1.53/0.53 thf(func_def_16, type, hoasap: (subst > term > subst > term > term)).
% 1.53/0.53 thf(func_def_17, type, induction2lem: $o).
% 1.53/0.53 thf(func_def_18, type, hoasinduction_lem3v2_f: $o).
% 1.53/0.53 thf(func_def_19, type, axvarshift: $o).
% 1.53/0.53 thf(func_def_20, type, hoasapinj2: $o).
% 1.53/0.53 thf(func_def_21, type, hoasapnotvar_gthm: $o).
% 1.53/0.53 thf(func_def_22, type, hoasapinj1: $o).
% 1.53/0.53 thf(func_def_23, type, ulamvar1: $o).
% 1.53/0.53 thf(func_def_24, type, induction2lem_lthm: $o).
% 1.53/0.53 thf(func_def_25, type, hoasinduction_lem3v2_gthm: $o).
% 1.53/0.53 thf(func_def_26, type, apnotvar: $o).
% 1.53/0.53 thf(func_def_27, type, pushprop_lthm_orig: $o).
% 1.53/0.53 thf(func_def_28, type, hoasinduction_lem3v2_f_lthm: $o).
% 1.53/0.53 thf(func_def_29, type, hoasinduction_lthm: $o).
% 1.53/0.53 thf(func_def_30, type, hoasinduction_no_psi_cond_lthm: $o).
% 1.53/0.53 thf(func_def_31, type, hoaslaminj: $o).
% 1.53/0.53 thf(func_def_32, type, hoasinduction_lem3aaa: $o).
% 1.53/0.53 thf(func_def_33, type, induction2lem_gthm: $o).
% 1.53/0.53 thf(func_def_34, type, hoasinduction_lem3aa_lthm: $o).
% 1.53/0.53 thf(func_def_35, type, hoasinduction_lem3: $o).
% 1.53/0.53 thf(func_def_36, type, hoasinduction_lem2: $o).
% 1.53/0.53 thf(func_def_37, type, termmset_lthm: $o).
% 1.53/0.53 thf(func_def_38, type, hoasinduction_lem1: $o).
% 1.53/0.53 thf(func_def_39, type, hoaslamnotap_lthm: $o).
% 1.53/0.53 thf(func_def_40, type, pushprop_lem1v2_lthm: $o).
% 1.53/0.53 thf(func_def_41, type, hoasapnotvar: $o).
% 1.53/0.53 thf(func_def_42, type, hoasinduction_lem0: $o).
% 1.53/0.53 thf(func_def_43, type, hoasinduction: $o).
% 1.53/0.53 thf(func_def_44, type, hoasinduction_gthm: $o).
% 1.53/0.53 thf(func_def_45, type, axapp: $o).
% 1.53/0.53 thf(func_def_46, type, hoaslamnotvar_lthm: $o).
% 1.53/0.53 thf(func_def_47, type, pushprop_lem3v2_lthm: $o).
% 1.53/0.53 thf(func_def_48, type, hoasinduction_lem3b_lthm: $o).
% 1.53/0.53 thf(func_def_49, type, ulamvarind: $o).
% 1.53/0.53 thf(func_def_50, type, induction: $o).
% 1.53/0.53 thf(func_def_51, type, hoasinduction_lem3a_lthm: $o).
% 1.53/0.53 thf(func_def_52, type, termmset_gthm: $o).
% 1.53/0.53 thf(func_def_53, type, hoasinduction_lem3aa: $o).
% 1.53/0.53 thf(func_def_54, type, pushprop_lem1v2_gthm: $o).
% 1.53/0.53 thf(func_def_55, type, hoaslamnotap_gthm: $o).
% 1.53/0.53 thf(func_def_56, type, hoaslamnotvar_gthm: $o).
% 1.53/0.53 thf(func_def_57, type, hoasinduction_lem3b_gthm: $o).
% 1.53/0.53 thf(func_def_58, type, pushprop_lem2v2: $o).
% 1.53/0.53 thf(func_def_59, type, hoasinduction_lem3a_gthm: $o).
% 1.53/0.53 thf(func_def_60, type, axclos: $o).
% 1.53/0.53 thf(func_def_61, type, axassoc: $o).
% 1.53/0.53 thf(func_def_62, type, hoasinduction_lem2v2: $o).
% 1.53/0.53 thf(func_def_63, type, pushprop_lthm: $o).
% 1.53/0.53 thf(func_def_64, type, apinj2: $o).
% 1.53/0.53 thf(func_def_65, type, apinj1: $o).
% 1.53/0.53 thf(func_def_66, type, hoasapinj2_lthm: $o).
% 1.53/0.53 thf(func_def_67, type, hoasinduction_lem3v2a: $o).
% 1.53/0.53 thf(func_def_68, type, hoasapinj1_lthm: $o).
% 1.53/0.53 thf(func_def_69, type, hoaslaminj_lthm: $o).
% 1.53/0.53 thf(func_def_70, type, axvarcons: $o).
% 1.53/0.53 thf(func_def_71, type, hoaslam: (subst > (subst > term > term) > term)).
% 1.53/0.53 thf(func_def_72, type, axscons: $o).
% 1.53/0.53 thf(func_def_73, type, hoasinduction_lem2v2_gthm: $o).
% 1.53/0.53 thf(func_def_74, type, axidr: $o).
% 1.53/0.53 thf(func_def_75, type, pushprop_lem1: $o).
% 1.53/0.53 thf(func_def_76, type, laminj: $o).
% 1.53/0.53 thf(func_def_77, type, hoasinduction_lem3_lthm: $o).
% 1.53/0.53 thf(func_def_78, type, pushprop_lem0: $o).
% 1.53/0.53 thf(func_def_79, type, pushprop_gthm: $o).
% 1.53/0.53 thf(func_def_80, type, axabs: $o).
% 1.53/0.53 thf(func_def_81, type, hoasinduction_lem3v2a_lthm: $o).
% 1.53/0.53 thf(func_def_82, type, hoasinduction_lem2_lthm: $o).
% 1.53/0.53 thf(func_def_83, type, hoasapinj2_gthm: $o).
% 1.53/0.53 thf(func_def_84, type, hoasinduction_p_and_p_prime: ((subst > term > subst > $o) > (term > $o) > $o)).
% 1.53/0.53 thf(func_def_85, type, hoasinduction_lem1_lthm: $o).
% 1.53/0.53 thf(func_def_86, type, lamnotap: $o).
% 1.53/0.53 thf(func_def_87, type, hoasapinj1_gthm: $o).
% 1.53/0.53 thf(func_def_88, type, hoaslamnotvar: $o).
% 1.53/0.53 thf(func_def_89, type, axidl: $o).
% 1.53/0.53 thf(func_def_90, type, hoaslaminj_gthm: $o).
% 1.53/0.53 thf(func_def_91, type, induction2_lthm: $o).
% 1.53/0.53 thf(func_def_92, type, hoasinduction_lem0_lthm: $o).
% 1.53/0.53 thf(func_def_93, type, substmonoid_lthm: $o).
% 1.53/0.53 thf(func_def_94, type, pushprop: $o).
% 1.53/0.53 thf(func_def_95, type, hoasinduction_lem3_gthm: $o).
% 1.53/0.53 thf(func_def_96, type, hoasinduction_lem2_gthm: $o).
% 1.53/0.53 thf(func_def_97, type, hoasinduction_lem3b: $o).
% 1.53/0.53 thf(func_def_98, type, substmonoid: $o).
% 1.53/0.53 thf(func_def_99, type, lamnotvar: $o).
% 1.53/0.53 thf(func_def_100, type, hoasinduction_lem3a: $o).
% 1.53/0.53 thf(func_def_101, type, hoasinduction_lem1_gthm: $o).
% 1.53/0.53 thf(func_def_102, type, hoasinduction_no_psi_cond: $o).
% 1.53/0.53 thf(func_def_103, type, induction2_gthm: $o).
% 1.53/0.53 thf(func_def_104, type, pushprop_lem2v2_lthm: $o).
% 1.53/0.53 thf(func_def_105, type, hoasvar: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_106, type, hoaslamnotap: $o).
% 1.53/0.53 thf(func_def_107, type, substmonoid_gthm: $o).
% 1.53/0.53 thf(func_def_108, type, ulamvarsh: $o).
% 1.53/0.53 thf(func_def_109, type, induction2: $o).
% 1.53/0.53 thf(func_def_110, type, pushprop_lem3v2: $o).
% 1.53/0.53 thf(func_def_111, type, pushprop_lem2v2_gthm: $o).
% 1.53/0.53 thf(func_def_112, type, pushprop_lem1_lthm: $o).
% 1.53/0.53 thf(func_def_113, type, hoasinduction_lem3v2: $o).
% 1.53/0.53 thf(func_def_114, type, axshiftcons: $o).
% 1.53/0.53 thf(func_def_115, type, termmset: $o).
% 1.53/0.53 thf(func_def_116, type, pushprop_lem0_lthm: $o).
% 1.53/0.53 thf(func_def_117, type, hoasapnotvar_lthm: $o).
% 1.53/0.53 thf(func_def_118, type, hoasinduction_lem3v2_lthm: $o).
% 1.53/0.53 thf(func_def_119, type, pushprop_p_and_p_prime: (term > subst > (term > $o) > (term > $o) > $o)).
% 1.53/0.53 thf(func_def_120, type, axvarid: $o).
% 1.53/0.53 thf(func_def_121, type, hoasinduction_lthm_3: $o).
% 1.53/0.53 thf(func_def_123, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.53/0.53 thf(func_def_124, type, db0: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_125, type, db1: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_126, type, db2: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_127, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.53/0.53 thf(func_def_128, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.53/0.53 thf(func_def_129, type, vIMP: ($o > $o > $o)).
% 1.53/0.53 thf(func_def_130, type, db3: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_131, type, vNOT: ($o > $o)).
% 1.53/0.53 thf(func_def_132, type, vIFF: ($o > $o > $o)).
% 1.53/0.53 thf(func_def_133, type, db4: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_134, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.53/0.53 thf(func_def_135, type, vAND: ($o > $o > $o)).
% 1.53/0.53 thf(func_def_138, type, sK0: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_139, type, sK1: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_140, type, sK2: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_141, type, sK3: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_142, type, sK4: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_143, type, sK5: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_144, type, sK6: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_145, type, sK7: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_146, type, sK8: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_147, type, sK9: term).
% 1.53/0.53 thf(func_def_148, type, sK10: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_149, type, sK11: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_150, type, sK12: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_151, type, sK13: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_152, type, sK14: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_153, type, sK15: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_154, type, sK16: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_155, type, sK17: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_156, type, sK18: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_157, type, sK19: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_158, type, sK20: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_159, type, sK21: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_160, type, sK22: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_161, type, sK23: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_162, type, sK24: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_163, type, sK25: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_164, type, sK26: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_165, type, sK27: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_166, type, sK28: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_167, type, sK29: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_168, type, sK30: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_169, type, sK31: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_170, type, sK32: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_171, type, sK33: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_172, type, sK34: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_173, type, sK35: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_174, type, sK36: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_175, type, sK37: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_176, type, sK38: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_177, type, sK39: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_178, type, sK40: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_179, type, sK41: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_180, type, sK42: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_181, type, sK43: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_182, type, sK44: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_183, type, sK45: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_184, type, sK46: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_185, type, sK47: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_186, type, sK48: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_187, type, sK49: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_188, type, sK50: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_189, type, sK51: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_190, type, sK52: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_191, type, sK53: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_192, type, sK54: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_193, type, sK55: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_194, type, sK56: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_195, type, sK57: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_196, type, sK58: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_197, type, sK59: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_198, type, sK60: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_199, type, sK61: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_200, type, sK62: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_201, type, sK63: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_202, type, sK64: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_203, type, sK65: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_204, type, sK66: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_205, type, sK67: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_206, type, sK68: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_207, type, sK69: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_208, type, sK70: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_209, type, sK71: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_210, type, sK72: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_211, type, sK73: term).
% 1.53/0.53 thf(func_def_212, type, sK74: (term > subst > term > term)).
% 1.53/0.53 thf(func_def_213, type, sK75: term).
% 1.53/0.53 thf(func_def_214, type, sK76: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_215, type, sK77: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_216, type, sK78: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_217, type, sK79: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_218, type, sK80: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_219, type, sK81: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_220, type, sK82: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_221, type, sK83: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_222, type, sK84: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_223, type, sK85: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_224, type, sK86: term).
% 1.53/0.53 thf(func_def_225, type, sK87: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_226, type, sK88: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_227, type, sK89: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_228, type, sK90: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_229, type, sK91: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_230, type, sK92: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_231, type, sK93: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_232, type, sK94: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_233, type, sK95: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_234, type, sK96: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_235, type, sK97: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_236, type, sK98: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_237, type, sK99: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_238, type, sK100: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_239, type, sK101: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_240, type, sK102: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_241, type, sK103: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_242, type, sK104: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_243, type, sK105: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_244, type, sK106: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_245, type, sK107: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_246, type, sK108: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_247, type, sK109: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_248, type, sK110: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_249, type, sK111: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_250, type, sK112: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_251, type, sK113: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_252, type, sK114: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_253, type, sK115: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_254, type, sK116: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_255, type, sK117: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_256, type, sK118: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_257, type, sK119: term).
% 1.53/0.53 thf(func_def_258, type, sK120: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_259, type, sK121: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_260, type, sK122: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_261, type, sK123: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_262, type, sK124: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_263, type, sK125: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_264, type, sK126: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_265, type, sK127: ((subst > term > term) > term > subst)).
% 1.53/0.53 thf(func_def_266, type, sK128: ((subst > term > term) > term > term)).
% 1.53/0.53 thf(func_def_267, type, sK129: ((subst > term > term) > term > subst)).
% 1.53/0.53 thf(func_def_268, type, sK130: ((subst > term > term) > term > term)).
% 1.53/0.53 thf(func_def_269, type, sK131: ((subst > term > term) > term > subst)).
% 1.53/0.53 thf(func_def_270, type, sK132: term).
% 1.53/0.53 thf(func_def_271, type, sK133: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_272, type, sK134: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_273, type, sK135: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_274, type, sK136: ((subst > term > subst > $o) > term > term)).
% 1.53/0.53 thf(func_def_275, type, sK137: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_276, type, sK138: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_277, type, sK139: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_278, type, sK140: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_279, type, sK141: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_280, type, sK142: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_281, type, sK143: term).
% 1.53/0.53 thf(func_def_282, type, sK144: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_283, type, sK145: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_284, type, sK146: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_285, type, sK147: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_286, type, sK148: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_287, type, sK149: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_288, type, sK150: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_289, type, sK151: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_290, type, sK152: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_291, type, sK153: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_292, type, sK154: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_293, type, sK155: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_294, type, sK156: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_295, type, sK157: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_296, type, sK158: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_297, type, sK159: term).
% 1.53/0.53 thf(func_def_298, type, sK160: term).
% 1.53/0.53 thf(func_def_299, type, sK161: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_300, type, sK162: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_301, type, sK163: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_302, type, sK164: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_303, type, sK165: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_304, type, sK166: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_305, type, sK167: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_306, type, sK168: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_307, type, sK169: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_308, type, sK170: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_309, type, sK171: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_310, type, sK172: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_311, type, sK173: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_312, type, sK174: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_313, type, sK175: term).
% 1.53/0.53 thf(func_def_314, type, sK176: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_315, type, sK177: ((term > $o) > (subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_316, type, sK178: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_317, type, sK179: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_318, type, sK180: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_319, type, sK181: (term > $o)).
% 1.53/0.53 thf(func_def_320, type, sK182: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_321, type, sK183: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_322, type, sK184: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_323, type, sK185: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_324, type, sK186: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_325, type, sK187: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_326, type, sK188: term).
% 1.53/0.53 thf(func_def_327, type, sK189: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_328, type, sK190: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_329, type, sK191: ((subst > term > subst > $o) > subst > term > term)).
% 1.53/0.53 thf(func_def_330, type, sK192: ((term > $o) > (subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_331, type, sK193: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_332, type, sK194: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_333, type, sK195: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_334, type, sK196: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_335, type, sK197: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_336, type, sK198: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_337, type, sK199: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_338, type, sK200: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_339, type, sK201: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_340, type, sK202: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_341, type, sK203: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_342, type, sK204: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_343, type, sK205: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_344, type, sK206: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_345, type, sK207: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_346, type, sK208: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_347, type, sK209: (term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_348, type, sK210: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_349, type, sK211: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_350, type, sK212: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_351, type, sK213: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_352, type, sK214: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_353, type, sK215: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_354, type, sK216: (term > $o)).
% 1.53/0.53 thf(func_def_355, type, sK217: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_356, type, sK218: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_357, type, sK219: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_358, type, sK220: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_359, type, sK221: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_360, type, sK222: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_361, type, sK223: term).
% 1.53/0.53 thf(func_def_362, type, sK224: (term > subst > term > term)).
% 1.53/0.53 thf(func_def_363, type, sK225: term).
% 1.53/0.53 thf(func_def_364, type, sK226: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_365, type, sK227: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_366, type, sK228: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_367, type, sK229: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_368, type, sK230: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_369, type, sK231: ((term > $o) > (subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_370, type, sK232: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_371, type, sK233: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_372, type, sK234: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_373, type, sK235: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_374, type, sK236: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_375, type, sK237: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_376, type, sK238: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_377, type, sK239: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_378, type, sK240: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_379, type, sK241: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_380, type, sK242: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_381, type, sK243: (term > $o)).
% 1.53/0.53 thf(func_def_382, type, sK244: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_383, type, sK245: term).
% 1.53/0.53 thf(func_def_384, type, sK246: term).
% 1.53/0.53 thf(func_def_385, type, sK247: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_386, type, sK248: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_387, type, sK249: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_388, type, sK250: ((term > $o) > (subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_389, type, sK251: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_390, type, sK252: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_391, type, sK253: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_392, type, sK254: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_393, type, sK255: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_394, type, sK256: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_395, type, sK257: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_396, type, sK258: ((subst > term > subst > $o) > term)).
% 1.53/0.53 thf(func_def_397, type, sK259: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_398, type, sK260: ((subst > term > subst > $o) > subst)).
% 1.53/0.53 thf(func_def_399, type, sK261: (term > $o)).
% 1.53/0.53 thf(func_def_400, type, sK262: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_401, type, sK263: term).
% 1.53/0.53 thf(func_def_402, type, sK264: ((subst > term > subst > $o) > term > $o)).
% 1.53/0.53 thf(func_def_403, type, sK265: (subst > term > subst > $o)).
% 1.53/0.53 thf(func_def_404, type, sK266: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_405, type, sK267: term).
% 1.53/0.53 thf(func_def_406, type, sK268: term).
% 1.53/0.53 thf(func_def_407, type, sK269: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_408, type, sK270: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_409, type, sK271: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_410, type, sK272: (subst > term > term)).
% 1.53/0.53 thf(func_def_411, type, sK273: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_412, type, sK274: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_413, type, sK275: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_414, type, sK276: (subst > term > term)).
% 1.53/0.53 thf(func_def_415, type, sK277: term).
% 1.53/0.53 thf(func_def_416, type, sK278: term).
% 1.53/0.53 thf(func_def_417, type, sK279: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_418, type, sK280: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_419, type, sK281: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_420, type, sK282: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_421, type, sK283: ((subst > term > term) > term)).
% 1.53/0.53 thf(func_def_422, type, sK284: ((subst > term > term) > subst)).
% 1.53/0.53 thf(func_def_423, type, sK285: (subst > term > term)).
% 1.53/0.53 thf(func_def_424, type, sK286: (subst > term > term)).
% 1.53/0.53 thf(func_def_425, type, sK287: term).
% 1.53/0.53 thf(func_def_426, type, sK288: subst).
% 1.53/0.53 thf(func_def_427, type, sK289: term).
% 1.53/0.53 thf(func_def_428, type, sK290: term).
% 1.53/0.53 thf(func_def_429, type, sK291: term).
% 1.53/0.53 thf(func_def_430, type, sK292: term).
% 1.53/0.53 thf(func_def_431, type, sK293: term).
% 1.53/0.53 thf(func_def_432, type, sK294: term).
% 1.53/0.53 thf(func_def_433, type, sK295: term).
% 1.53/0.53 thf(func_def_434, type, sK296: term).
% 1.53/0.53 thf(func_def_435, type, sK297: term).
% 1.53/0.53 thf(func_def_436, type, sK298: subst).
% 1.53/0.53 thf(func_def_437, type, sK299: subst).
% 1.53/0.53 thf(func_def_438, type, sK300: term).
% 1.53/0.53 thf(func_def_439, type, sK301: subst).
% 1.53/0.53 thf(func_def_440, type, sK302: subst).
% 1.53/0.53 thf(func_def_441, type, sK303: subst).
% 1.53/0.53 thf(func_def_442, type, sK304: subst).
% 1.53/0.53 thf(func_def_443, type, sK305: subst).
% 1.53/0.53 thf(func_def_444, type, sK306: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_445, type, sK307: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_446, type, sK308: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_447, type, sK309: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_448, type, sK310: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_449, type, sK311: (term > $o)).
% 1.53/0.53 thf(func_def_450, type, sK312: (term > term)).
% 1.53/0.53 thf(func_def_451, type, sK313: term).
% 1.53/0.53 thf(func_def_452, type, sK314: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_453, type, sK315: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_454, type, sK316: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_455, type, sK317: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_456, type, sK318: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_457, type, sK319: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_458, type, sK320: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_459, type, sK321: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_460, type, sK322: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_461, type, sK323: (term > $o)).
% 1.53/0.53 thf(func_def_462, type, sK324: (term > term)).
% 1.53/0.53 thf(func_def_463, type, sK325: subst).
% 1.53/0.53 thf(func_def_464, type, sK326: term).
% 1.53/0.53 thf(func_def_465, type, sK327: ((term > $o) > subst > term)).
% 1.53/0.53 thf(func_def_466, type, sK328: subst).
% 1.53/0.53 thf(func_def_467, type, sK329: term).
% 1.53/0.53 thf(func_def_468, type, sK330: (term > $o)).
% 1.53/0.53 thf(func_def_469, type, sK331: term).
% 1.53/0.53 thf(func_def_470, type, db6: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_471, type, db5: !>[X0: $tType]:(X0)).
% 1.53/0.53 thf(func_def_472, type, sK332: ((term > $o) > subst > term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_473, type, sK333: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_474, type, sK334: subst).
% 1.53/0.53 thf(func_def_475, type, sK335: term).
% 1.53/0.53 thf(func_def_476, type, sK336: (term > $o)).
% 1.53/0.53 thf(func_def_477, type, sK337: (term > $o)).
% 1.53/0.53 thf(func_def_478, type, sK338: term).
% 1.53/0.53 thf(func_def_479, type, sK339: ((term > $o) > subst > term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_480, type, sK340: (subst > (term > $o) > term)).
% 1.53/0.53 thf(func_def_481, type, sK341: subst).
% 1.53/0.53 thf(func_def_482, type, sK342: term).
% 1.53/0.53 thf(func_def_483, type, sK343: (term > $o)).
% 1.53/0.53 thf(func_def_484, type, sK344: (term > $o)).
% 1.53/0.53 thf(func_def_485, type, sK345: term).
% 1.53/0.53 thf(func_def_486, type, sK346: ((term > $o) > subst > term > (term > $o) > term)).
% 1.53/0.53 thf(func_def_487, type, sK347: subst).
% 1.53/0.53 thf(func_def_488, type, sK348: term).
% 1.53/0.53 thf(func_def_489, type, sK349: (term > $o)).
% 1.53/0.53 thf(func_def_490, type, sK350: (term > $o)).
% 1.53/0.53 thf(func_def_491, type, sK351: term).
% 1.53/0.53 thf(func_def_492, type, sK352: subst).
% 1.53/0.53 thf(func_def_493, type, sK353: term).
% 1.53/0.53 thf(func_def_494, type, sK354: (term > $o)).
% 1.53/0.53 thf(func_def_495, type, sK355: (term > $o)).
% 1.53/0.53 thf(func_def_496, type, sK356: ((term > $o) > subst > term > term > $o)).
% 1.53/0.53 thf(func_def_497, type, sK357: subst).
% 1.53/0.53 thf(func_def_498, type, sK358: term).
% 1.53/0.53 thf(func_def_499, type, sK359: (term > $o)).
% 1.53/0.53 thf(func_def_500, type, sK360: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_501, type, sK361: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_502, type, sK362: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_503, type, sK363: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_504, type, sK364: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_505, type, sK365: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_506, type, sK366: (term > $o)).
% 1.53/0.53 thf(func_def_507, type, sK367: term).
% 1.53/0.53 thf(func_def_508, type, sK368: term).
% 1.53/0.53 thf(func_def_509, type, sK369: term).
% 1.53/0.53 thf(func_def_510, type, sK370: term).
% 1.53/0.53 thf(func_def_511, type, sK371: term).
% 1.53/0.53 thf(func_def_512, type, sK372: term).
% 1.53/0.53 thf(func_def_513, type, sK373: term).
% 1.53/0.53 thf(func_def_514, type, sK374: term).
% 1.53/0.53 thf(func_def_515, type, sK375: term).
% 1.53/0.53 thf(func_def_516, type, sK376: term).
% 1.53/0.53 thf(func_def_517, type, sK377: term).
% 1.53/0.53 thf(func_def_518, type, sK378: term).
% 1.53/0.53 thf(func_def_519, type, sK379: term).
% 1.53/0.53 thf(func_def_520, type, sK380: term).
% 1.53/0.53 thf(func_def_521, type, sK381: term).
% 1.53/0.53 thf(func_def_522, type, sK382: term).
% 1.53/0.53 thf(func_def_523, type, sK383: term).
% 1.53/0.53 thf(func_def_524, type, sK384: term).
% 1.53/0.53 thf(func_def_525, type, sK385: term).
% 1.53/0.53 thf(func_def_526, type, sK386: ((term > $o) > term)).
% 1.53/0.53 thf(func_def_527, type, sK387: (term > $o)).
% 1.53/0.53 thf(func_def_528, type, sK388: term).
% 1.53/0.53 thf(func_def_529, type, sK389: term).
% 1.53/0.53 thf(func_def_530, type, sK390: subst).
% 1.53/0.53 thf(func_def_531, type, sK391: subst).
% 1.53/0.53 thf(func_def_532, type, sK392: subst).
% 1.53/0.53 thf(func_def_533, type, sK393: subst).
% 1.53/0.53 thf(func_def_534, type, sK394: term).
% 1.53/0.53 thf(func_def_535, type, sK395: subst).
% 1.53/0.53 thf(func_def_536, type, sK396: subst).
% 1.53/0.53 thf(func_def_537, type, sK397: subst).
% 1.53/0.53 thf(func_def_538, type, sK398: subst).
% 1.53/0.53 thf(func_def_539, type, sK399: term).
% 1.53/0.53 thf(func_def_540, type, sK400: subst).
% 1.53/0.53 thf(func_def_541, type, sK401: subst).
% 1.53/0.53 thf(func_def_542, type, sK402: subst).
% 1.53/0.53 thf(func_def_543, type, sK403: term).
% 1.53/0.53 thf(func_def_544, type, sK404: subst).
% 1.53/0.53 thf(func_def_545, type, sK405: term).
% 1.53/0.53 thf(func_def_546, type, sK406: term).
% 1.53/0.53 thf(func_def_547, type, sK407: subst).
% 1.53/0.53 thf(func_def_548, type, sK408: term).
% 1.53/0.53 thf(func_def_549, type, sK409: subst).
% 1.53/0.53 thf(func_def_550, type, sK410: term).
% 1.53/0.53 thf(func_def_551, type, sK411: term).
% 1.53/0.53 thf(f6,axiom,(
% 1.53/0.53 (axidl = ! [X0 : subst] : (((comp @ id @ X0)) = X0))),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',axidl)).
% 1.53/0.53 thf(f8,axiom,(
% 1.53/0.53 (axassoc = ! [X0 : subst,X1 : subst,X2 : subst] : (((comp @ (comp @ X0 @ X1) @ X2)) = ((comp @ X0 @ (comp @ X1 @ X2)))))),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',axassoc)).
% 1.53/0.53 thf(f10,axiom,(
% 1.53/0.53 (axidr = ! [X0 : subst] : (((comp @ X0 @ id)) = X0))),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',axidr)).
% 1.53/0.53 thf(f49,axiom,(
% 1.53/0.53 (substmonoid = ! [X0 : subst] : (((comp @ X0 @ id)) = X0) & ! [X0 : subst] : (((comp @ id @ X0)) = X0) & ! [X0 : subst,X1 : subst,X2 : subst] : (((comp @ (comp @ X0 @ X1) @ X2)) = ((comp @ X0 @ (comp @ X1 @ X2)))))),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',substmonoid)).
% 1.53/0.53 thf(f51,axiom,(
% 1.53/0.53 (substmonoid_lthm = axidl => (axassoc => (axidr => substmonoid)))),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/Axioms/ALG003^0.ax',substmonoid_lthm)).
% 1.53/0.53 thf(f114,conjecture,(
% 1.53/0.53 substmonoid_lthm),
% 1.53/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm)).
% 1.53/0.53 thf(f115,negated_conjecture,(
% 1.53/0.53 ~substmonoid_lthm),
% 1.53/0.53 inference(negated_conjecture,[status(cth)],[f114])).
% 1.53/0.53 thf(f121,plain,(
% 1.53/0.53 (axidl = ((!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))))),
% 1.53/0.53 inference(fool_elimination,[],[f6])).
% 1.53/0.53 thf(f123,plain,(
% 1.53/0.53 (axassoc = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))))))),
% 1.53/0.53 inference(fool_elimination,[],[f8])).
% 1.53/0.53 thf(f125,plain,(
% 1.53/0.53 (axidr = ((!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)))))),
% 1.53/0.53 inference(fool_elimination,[],[f10])).
% 1.53/0.53 thf(f189,plain,(
% 1.53/0.53 (substmonoid = ! [X0 : subst] : (((comp @ X0 @ id)) = X0) & ! [X1 : subst] : (((comp @ id @ X1)) = X1) & ! [X2 : subst,X3 : subst,X4 : subst] : (((comp @ (comp @ X2 @ X3) @ X4)) = ((comp @ X2 @ (comp @ X3 @ X4)))))),
% 1.53/0.53 inference(rectify,[],[f49])).
% 1.53/0.53 thf(f190,plain,(
% 1.53/0.53 (substmonoid = ((((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0))))))))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0))))))),
% 1.53/0.53 inference(fool_elimination,[],[f189])).
% 1.53/0.53 thf(f193,plain,(
% 1.53/0.53 (substmonoid_lthm = axidl => (axassoc => (axidr => substmonoid)))),
% 1.53/0.53 inference(rectify,[],[f51])).
% 1.53/0.53 thf(f194,plain,(
% 1.53/0.53 (substmonoid_lthm = ((axidl => (axassoc => (axidr => substmonoid)))))),
% 1.53/0.53 inference(fool_elimination,[],[f193])).
% 1.53/0.53 thf(f306,plain,(
% 1.53/0.53 ~substmonoid_lthm),
% 1.53/0.53 inference(rectify,[],[f115])).
% 1.53/0.53 thf(f307,plain,(
% 1.53/0.53 ~ (substmonoid_lthm = $true)),
% 1.53/0.53 inference(fool_elimination,[],[f306])).
% 1.53/0.53 thf(f308,plain,(
% 1.53/0.53 (substmonoid_lthm != $true)),
% 1.53/0.53 inference(flattening,[],[f307])).
% 1.53/0.53 thf(f314,plain,(
% 1.53/0.53 (axidl = ((!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))))),
% 1.53/0.53 inference(cnf_transformation,[],[f121])).
% 1.53/0.53 thf(f316,plain,(
% 1.53/0.53 (axassoc = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))))))),
% 1.53/0.53 inference(cnf_transformation,[],[f123])).
% 1.53/0.53 thf(f318,plain,(
% 1.53/0.53 (axidr = ((!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)))))),
% 1.53/0.53 inference(cnf_transformation,[],[f125])).
% 1.53/0.53 thf(f357,plain,(
% 1.53/0.53 (substmonoid = ((((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0))))))))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0))))))),
% 1.53/0.53 inference(cnf_transformation,[],[f190])).
% 1.53/0.53 thf(f359,plain,(
% 1.53/0.53 (substmonoid_lthm = ((axidl => (axassoc => (axidr => substmonoid)))))),
% 1.53/0.53 inference(cnf_transformation,[],[f194])).
% 1.53/0.53 thf(f422,plain,(
% 1.53/0.53 (substmonoid_lthm != $true)),
% 1.53/0.53 inference(cnf_transformation,[],[f308])).
% 1.53/0.53 thf(f424,definition,(
% 1.53/0.53 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.53/0.53 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.53/0.53 thf(f4288,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (((axidl => (axassoc => (axidr => substmonoid)))) = $false)),
% 1.53/0.53 inference(iff_proxy_clausification,[],[f359])).
% 1.53/0.53 thf(f4293,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (((axassoc => (axidr => substmonoid))) = $false)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4288])).
% 1.53/0.53 thf(f4294,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (axidl = $true)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4288])).
% 1.53/0.53 thf(f4295,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (((axidr => substmonoid)) = $false)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4293])).
% 1.53/0.53 thf(f4296,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (axassoc = $true)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4293])).
% 1.53/0.53 thf(f4297,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (substmonoid = $false)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4295])).
% 1.53/0.53 thf(f4298,plain,(
% 1.53/0.53 (substmonoid_lthm = $true) | (axidr = $true)),
% 1.53/0.53 inference(imp_proxy_clausification,[],[f4295])).
% 1.53/0.53 thf(f4379,plain,(
% 1.53/0.53 (substmonoid = $true) | (((((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0))))))))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0))))) = $false)),
% 1.53/0.53 inference(iff_proxy_clausification,[],[f357])).
% 1.53/0.53 thf(f4398,plain,(
% 1.53/0.53 (substmonoid = $true) | (((!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)))) = $false) | ((((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0))))))))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0))))) = $false)),
% 1.53/0.53 inference(and_proxy_clausification,[],[f4379])).
% 1.53/0.53 thf(f4399,plain,(
% 1.53/0.53 (substmonoid = $true) | ($false = (((^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)) @ sK301))) | ((((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0))))))))) & (!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0))))) = $false)),
% 1.53/0.53 inference(sigma_proxy_clausification,[],[f4398])).
% 1.53/0.53 thf(f4400,plain,(
% 1.53/0.53 (substmonoid = $true) | ($false = (((^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)) @ sK301))) | (((!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))) = $false) | (((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))))) = $false)),
% 1.53/0.53 inference(and_proxy_clausification,[],[f4399])).
% 1.53/0.53 thf(f4401,plain,(
% 1.53/0.53 (substmonoid = $true) | ($false = (((^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)) @ sK301))) | ($false = (((^[Y0 : subst]: ((comp @ id @ Y0) = Y0)) @ sK302))) | (((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))))) = $false)),
% 1.53/0.53 inference(sigma_proxy_clausification,[],[f4400])).
% 1.53/0.53 thf(f4402,plain,(
% 1.53/0.53 (substmonoid = $true) | ($false = (((^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)) @ sK301))) | ($false = (((^[Y0 : subst]: ((comp @ id @ Y0) = Y0)) @ sK302))) | ($false = (((^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))) @ sK303)))),
% 1.53/0.53 inference(sigma_proxy_clausification,[],[f4401])).
% 1.53/0.53 thf(f4403,plain,(
% 1.53/0.53 (substmonoid = $true) | ($false = (((comp @ sK301 @ id) = sK301))) | ($false = (((comp @ id @ sK302) = sK302))) | ($false = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ sK303) = (comp @ Y1 @ (comp @ Y0 @ sK303)))))))))),
% 1.53/0.53 inference(beta-eta_normalization,[],[f4402])).
% 1.53/0.53 thf(f4404,plain,(
% 1.53/0.53 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | ($false = (((comp @ id @ sK302) = sK302))) | ($false = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ sK303) = (comp @ Y1 @ (comp @ Y0 @ sK303)))))))))),
% 1.53/0.53 inference(equality_proxy_clausification,[],[f4403])).
% 1.53/0.53 thf(f4405,plain,(
% 1.53/0.53 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | ($false = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ sK303) = (comp @ Y1 @ (comp @ Y0 @ sK303)))))))))),
% 1.53/0.53 inference(equality_proxy_clausification,[],[f4404])).
% 1.53/0.53 thf(f4406,plain,(
% 1.53/0.53 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | ($false = (((^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ sK303) = (comp @ Y1 @ (comp @ Y0 @ sK303)))))) @ sK304)))),
% 1.53/0.54 inference(sigma_proxy_clausification,[],[f4405])).
% 1.53/0.54 thf(f4407,plain,(
% 1.53/0.54 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | ($false = ((!! @ subst @ (^[Y0 : subst]: ((comp @ (comp @ Y0 @ sK304) @ sK303) = (comp @ Y0 @ (comp @ sK304 @ sK303)))))))),
% 1.53/0.54 inference(beta-eta_normalization,[],[f4406])).
% 1.53/0.54 thf(f4408,plain,(
% 1.53/0.54 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | ($false = (((^[Y0 : subst]: ((comp @ (comp @ Y0 @ sK304) @ sK303) = (comp @ Y0 @ (comp @ sK304 @ sK303)))) @ sK305)))),
% 1.53/0.54 inference(sigma_proxy_clausification,[],[f4407])).
% 1.53/0.54 thf(f4409,plain,(
% 1.53/0.54 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | ($false = (((comp @ (comp @ sK305 @ sK304) @ sK303) = (comp @ sK305 @ (comp @ sK304 @ sK303)))))),
% 1.53/0.54 inference(beta-eta_normalization,[],[f4408])).
% 1.53/0.54 thf(f4410,plain,(
% 1.53/0.54 (substmonoid = $true) | (sK301 != ((comp @ sK301 @ id))) | (sK302 != ((comp @ id @ sK302))) | (((comp @ (comp @ sK305 @ sK304) @ sK303)) != ((comp @ sK305 @ (comp @ sK304 @ sK303))))),
% 1.53/0.54 inference(equality_proxy_clausification,[],[f4409])).
% 1.53/0.54 thf(f5643,plain,(
% 1.53/0.54 (axidr = $false) | (((!! @ subst @ (^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)))) = $true)),
% 1.53/0.54 inference(iff_proxy_clausification,[],[f318])).
% 1.53/0.54 thf(f5644,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidr = $false) | ($true = (((^[Y0 : subst]: ((comp @ Y0 @ id) = Y0)) @ X1)))) )),
% 1.53/0.54 inference(pi_proxy_clausification,[],[f5643])).
% 1.53/0.54 thf(f5645,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidr = $false) | ($true = (((comp @ X1 @ id) = X1)))) )),
% 1.53/0.54 inference(beta-eta_normalization,[],[f5644])).
% 1.53/0.54 thf(f5646,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidr = $false) | (((comp @ X1 @ id)) = X1)) )),
% 1.53/0.54 inference(equality_proxy_clausification,[],[f5645])).
% 1.53/0.54 thf(f5667,plain,(
% 1.53/0.54 (axassoc = $false) | (((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))))) = $true)),
% 1.53/0.54 inference(iff_proxy_clausification,[],[f316])).
% 1.53/0.54 thf(f5668,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axassoc = $false) | ($true = (((^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: (!! @ subst @ (^[Y2 : subst]: ((comp @ (comp @ Y2 @ Y1) @ Y0) = (comp @ Y2 @ (comp @ Y1 @ Y0)))))))) @ X1)))) )),
% 1.53/0.54 inference(pi_proxy_clausification,[],[f5667])).
% 1.53/0.54 thf(f5669,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axassoc = $false) | ($true = ((!! @ subst @ (^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ X1) = (comp @ Y1 @ (comp @ Y0 @ X1)))))))))) )),
% 1.53/0.54 inference(beta-eta_normalization,[],[f5668])).
% 1.53/0.54 thf(f5670,plain,(
% 1.53/0.54 ( ! [X2 : subst,X1 : subst] : ((axassoc = $false) | ($true = (((^[Y0 : subst]: (!! @ subst @ (^[Y1 : subst]: ((comp @ (comp @ Y1 @ Y0) @ X1) = (comp @ Y1 @ (comp @ Y0 @ X1)))))) @ X2)))) )),
% 1.53/0.54 inference(pi_proxy_clausification,[],[f5669])).
% 1.53/0.54 thf(f5671,plain,(
% 1.53/0.54 ( ! [X2 : subst,X1 : subst] : ((axassoc = $false) | ($true = ((!! @ subst @ (^[Y0 : subst]: ((comp @ (comp @ Y0 @ X2) @ X1) = (comp @ Y0 @ (comp @ X2 @ X1)))))))) )),
% 1.53/0.54 inference(beta-eta_normalization,[],[f5670])).
% 1.53/0.54 thf(f5672,plain,(
% 1.53/0.54 ( ! [X2 : subst,X3 : subst,X1 : subst] : ((axassoc = $false) | ($true = (((^[Y0 : subst]: ((comp @ (comp @ Y0 @ X2) @ X1) = (comp @ Y0 @ (comp @ X2 @ X1)))) @ X3)))) )),
% 1.53/0.54 inference(pi_proxy_clausification,[],[f5671])).
% 1.53/0.54 thf(f5673,plain,(
% 1.53/0.54 ( ! [X2 : subst,X3 : subst,X1 : subst] : ((axassoc = $false) | ($true = (((comp @ (comp @ X3 @ X2) @ X1) = (comp @ X3 @ (comp @ X2 @ X1)))))) )),
% 1.53/0.54 inference(beta-eta_normalization,[],[f5672])).
% 1.53/0.54 thf(f5674,plain,(
% 1.53/0.54 ( ! [X2 : subst,X3 : subst,X1 : subst] : ((axassoc = $false) | (((comp @ (comp @ X3 @ X2) @ X1)) = ((comp @ X3 @ (comp @ X2 @ X1))))) )),
% 1.53/0.54 inference(equality_proxy_clausification,[],[f5673])).
% 1.53/0.54 thf(f5695,plain,(
% 1.53/0.54 (axidl = $false) | (((!! @ subst @ (^[Y0 : subst]: ((comp @ id @ Y0) = Y0)))) = $true)),
% 1.53/0.54 inference(iff_proxy_clausification,[],[f314])).
% 1.53/0.54 thf(f5696,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidl = $false) | ($true = (((^[Y0 : subst]: ((comp @ id @ Y0) = Y0)) @ X1)))) )),
% 1.53/0.54 inference(pi_proxy_clausification,[],[f5695])).
% 1.53/0.54 thf(f5697,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidl = $false) | ($true = (((comp @ id @ X1) = X1)))) )),
% 1.53/0.54 inference(beta-eta_normalization,[],[f5696])).
% 1.53/0.54 thf(f5698,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((axidl = $false) | (((comp @ id @ X1)) = X1)) )),
% 1.53/0.54 inference(equality_proxy_clausification,[],[f5697])).
% 1.53/0.54 thf(f5774,plain,(
% 1.53/0.54 ($true != $true) | (substmonoid_lthm = $false)),
% 1.53/0.54 inference(constrained_superposition,[],[f422,f424])).
% 1.53/0.54 thf(f5776,plain,(
% 1.53/0.54 (substmonoid_lthm = $false)),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f5774])).
% 1.53/0.54 thf(f6025,plain,(
% 1.53/0.54 ($true = $false) | (axidl = $true)),
% 1.53/0.54 inference(forward_demodulation,[],[f4294,f5776])).
% 1.53/0.54 thf(f6026,plain,(
% 1.53/0.54 (axidl = $true)),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f6025])).
% 1.53/0.54 thf(f6144,definition,(
% 1.53/0.54 spl412_57 <=> ! [X1 : subst] : (((comp @ X1 @ id)) = X1)),
% 1.53/0.54 introduced(definition,[new_symbols(definition,[spl412_57])],[avatar_definition])).
% 1.53/0.54 thf(f6145,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((((comp @ X1 @ id)) = X1)) ) | ~spl412_57),
% 1.53/0.54 inference(avatar_component_clause,[],[f6144])).
% 1.53/0.54 thf(f6147,definition,(
% 1.53/0.54 spl412_58 <=> (axidr = $false)),
% 1.53/0.54 introduced(definition,[new_symbols(definition,[spl412_58])],[avatar_definition])).
% 1.53/0.54 thf(f6149,plain,(
% 1.53/0.54 (axidr = $false) | ~spl412_58),
% 1.53/0.54 inference(avatar_component_clause,[],[f6147])).
% 1.53/0.54 thf(f6150,plain,(
% 1.53/0.54 spl412_57 | spl412_58),
% 1.53/0.54 inference(avatar_split_clause,[],[f5646,f6147,f6144])).
% 1.53/0.54 thf(f6162,plain,(
% 1.53/0.54 ( ! [X1 : subst] : (($true = $false) | (((comp @ id @ X1)) = X1)) )),
% 1.53/0.54 inference(forward_demodulation,[],[f5698,f6026])).
% 1.53/0.54 thf(f6163,plain,(
% 1.53/0.54 ( ! [X1 : subst] : ((((comp @ id @ X1)) = X1)) )),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f6162])).
% 1.53/0.54 thf(f6344,plain,(
% 1.53/0.54 ($true = $false) | (axassoc = $true)),
% 1.53/0.54 inference(forward_demodulation,[],[f4296,f5776])).
% 1.53/0.54 thf(f6345,plain,(
% 1.53/0.54 (axassoc = $true)),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f6344])).
% 1.53/0.54 thf(f6490,plain,(
% 1.53/0.54 ($true = $false) | (substmonoid = $false)),
% 1.53/0.54 inference(forward_demodulation,[],[f4297,f5776])).
% 1.53/0.54 thf(f6491,plain,(
% 1.53/0.54 (substmonoid = $false)),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f6490])).
% 1.53/0.54 thf(f7254,plain,(
% 1.53/0.54 ( ! [X2 : subst,X3 : subst,X1 : subst] : (($true = $false) | (((comp @ (comp @ X3 @ X2) @ X1)) = ((comp @ X3 @ (comp @ X2 @ X1))))) )),
% 1.53/0.54 inference(forward_demodulation,[],[f5674,f6345])).
% 1.53/0.54 thf(f7255,plain,(
% 1.53/0.54 ( ! [X2 : subst,X3 : subst,X1 : subst] : ((((comp @ (comp @ X3 @ X2) @ X1)) = ((comp @ X3 @ (comp @ X2 @ X1))))) )),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f7254])).
% 1.53/0.54 thf(f7681,plain,(
% 1.53/0.54 (substmonoid = $true) | (sK302 != ((comp @ id @ sK302))) | (((comp @ (comp @ sK305 @ sK304) @ sK303)) != ((comp @ sK305 @ (comp @ sK304 @ sK303)))) | ~spl412_57),
% 1.53/0.54 inference(forward_subsumption_resolution,[],[f4410,f6145])).
% 1.53/0.54 thf(f7682,plain,(
% 1.53/0.54 (substmonoid = $true) | (((comp @ (comp @ sK305 @ sK304) @ sK303)) != ((comp @ sK305 @ (comp @ sK304 @ sK303)))) | ~spl412_57),
% 1.53/0.54 inference(forward_subsumption_resolution,[],[f7681,f6163])).
% 1.53/0.54 thf(f7683,plain,(
% 1.53/0.54 (substmonoid = $true) | ~spl412_57),
% 1.53/0.54 inference(forward_subsumption_resolution,[],[f7682,f7255])).
% 1.53/0.54 thf(f7684,plain,(
% 1.53/0.54 ($true = $false) | ~spl412_57),
% 1.53/0.54 inference(forward_demodulation,[],[f7683,f6491])).
% 1.53/0.54 thf(f7685,plain,(
% 1.53/0.54 $false | ~spl412_57),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f7684])).
% 1.53/0.54 thf(f7686,plain,(
% 1.53/0.54 ~spl412_57),
% 1.53/0.54 inference(avatar_contradiction_clause,[],[f7685])).
% 1.53/0.54 thf(f7687,plain,(
% 1.53/0.54 ($true = $false) | (axidr = $true)),
% 1.53/0.54 inference(forward_demodulation,[],[f4298,f5776])).
% 1.53/0.54 thf(f7688,plain,(
% 1.53/0.54 (axidr = $true)),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f7687])).
% 1.53/0.54 thf(f7693,plain,(
% 1.53/0.54 ($true = $false) | ~spl412_58),
% 1.53/0.54 inference(backward_demodulation,[],[f7688,f6149])).
% 1.53/0.54 thf(f7696,plain,(
% 1.53/0.54 $false | ~spl412_58),
% 1.53/0.54 inference(trivial_inequality_removal,[],[f7693])).
% 1.53/0.54 thf(f7697,plain,(
% 1.53/0.54 ~spl412_58),
% 1.53/0.54 inference(avatar_contradiction_clause,[],[f7696])).
% 1.53/0.54 cnf(s32, plain, spl412_57 | spl412_58, inference(sat_conversion,[],[f6150])).
% 1.53/0.54 cnf(s218, plain, ~spl412_57, inference(sat_conversion,[],[f7686])).
% 1.53/0.54 cnf(s219, plain, ~spl412_58, inference(sat_conversion,[],[f7697])).
% 1.53/0.54 cnf(s222, plain, $false, inference(rat,[],[s32,s219,s218])).
% 1.53/0.54 thf(f7698,plain,(
% 1.53/0.54 $false),
% 1.53/0.54 inference(avatar_sat_refutation,[],[s222])).
% 1.53/0.54 % SZS output end Proof for theBenchmark
% 1.53/0.54 % (116153)------------------------------
% 1.53/0.54 % (116153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.53/0.54 % (116153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.53/0.54 % (116153)CaDiCaL version: 2.1.3
% 1.53/0.54 % (116153)Termination reason: Refutation
% 1.53/0.54 % (116153)Time elapsed: 0.167 s
% 1.53/0.54 % (116153)Peak memory usage: 17 MB
% 1.53/0.54 % (116153)Instructions burned: 357 (million)
% 1.53/0.54 % (116127)Success in time 0.305 s
% 1.53/0.54 % Vampire exiting
%------------------------------------------------------------------------------