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