%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP001^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 08:07:34 AM UTC 2026
% Result : Theorem 0.45s 0.57s
% Output : Refutation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP001^4 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.29 % Computer : n003.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8046.5625MB
% 0.10/0.29 % OS : Linux 6.8.0-71-generic
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Tue Sep 29 19:19:14 UTC 2026
% 0.10/0.29 % CPUTime :
% 0.10/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.29/0.35 Running higher-order theorem proving
% 0.33/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.45/0.57 % (2935751)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.45/0.57 % (2935756)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=608566410:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.45/0.57 % (2935762)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.45/0.57 % (2935762)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.45/0.57 % (2935757)lrs+10_16_si=on:nwc=1.5:random_seed=3495338819:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.45/0.57 % (2935758)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=678313159:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.45/0.57 % (2935759)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=3409284397:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.45/0.57 % (2935762)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3070834882:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.45/0.57 % (2935760)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2312781731:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.45/0.57 % (2935761)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3325406252:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.45/0.57 % (2935758)Instruction limit reached!
% 0.45/0.57 % (2935758)------------------------------
% 0.45/0.57 % (2935758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935758)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935758)Termination reason: Instruction limit
% 0.45/0.57 % (2935758)Termination phase: shuffling
% 0.45/0.57 % (2935758)Time elapsed: 0.003 s
% 0.45/0.57 % (2935758)Peak memory usage: 10 MB
% 0.45/0.57 % (2935758)Instructions burned: 4 (million)
% 0.45/0.57 % (2935757)Instruction limit reached!
% 0.45/0.57 % (2935757)------------------------------
% 0.45/0.57 % (2935757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935757)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935757)Termination reason: Instruction limit
% 0.45/0.57 % (2935757)Termination phase: Property scanning
% 0.45/0.57 % (2935757)Time elapsed: 0.015 s
% 0.45/0.57 % (2935757)Peak memory usage: 10 MB
% 0.45/0.57 % (2935757)Instructions burned: 19 (million)
% 0.45/0.57 % (2935756)Instruction limit reached!
% 0.45/0.57 % (2935756)------------------------------
% 0.45/0.57 % (2935756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935756)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935756)Termination reason: Instruction limit
% 0.45/0.57 % (2935756)Termination phase: Saturation
% 0.45/0.57 % (2935756)Time elapsed: 0.034 s
% 0.45/0.57 % (2935756)Peak memory usage: 12 MB
% 0.45/0.57 % (2935756)Instructions burned: 88 (million)
% 0.45/0.57 % (2935760)Instruction limit reached!
% 0.45/0.57 % (2935760)------------------------------
% 0.45/0.57 % (2935760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935760)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935760)Termination reason: Instruction limit
% 0.45/0.57 % (2935760)Termination phase: Preprocessing 1
% 0.45/0.57 % (2935760)Time elapsed: 0.019 s
% 0.45/0.57 % (2935760)Peak memory usage: 10 MB
% 0.45/0.57 % (2935760)Instructions burned: 24 (million)
% 0.45/0.57 % (2935772)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.45/0.57 % (2935770)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4171567595:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.45/0.57 % (2935772)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=6644768:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.45/0.57 % (2935770)Instruction limit reached!
% 0.45/0.57 % (2935770)------------------------------
% 0.45/0.57 % (2935770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935770)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935770)Termination reason: Instruction limit
% 0.45/0.57 % (2935770)Termination phase: shuffling
% 0.45/0.57 % (2935770)Time elapsed: 0.002 s
% 0.45/0.57 % (2935770)Peak memory usage: 10 MB
% 0.45/0.57 % (2935770)Instructions burned: 2 (million)
% 0.45/0.57 % (2935772)Instruction limit reached!
% 0.45/0.57 % (2935772)------------------------------
% 0.45/0.57 % (2935772)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935772)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935772)Termination reason: Instruction limit
% 0.45/0.57 % (2935772)Termination phase: shuffling
% 0.45/0.57 % (2935772)Time elapsed: 0.003 s
% 0.45/0.57 % (2935772)Peak memory usage: 10 MB
% 0.45/0.57 % (2935772)Instructions burned: 8 (million)
% 0.45/0.57 % (2935771)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=281478107:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.45/0.57 % (2935771)Instruction limit reached!
% 0.45/0.57 % (2935771)------------------------------
% 0.45/0.57 % (2935771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935771)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935771)Termination reason: Instruction limit
% 0.45/0.57 % (2935771)Termination phase: shuffling
% 0.45/0.57 % (2935771)Time elapsed: 0.005 s
% 0.45/0.57 % (2935771)Peak memory usage: 10 MB
% 0.45/0.57 % (2935771)Instructions burned: 6 (million)
% 0.45/0.57 % (2935773)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1327689370:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.45/0.57 % (2935761)Instruction limit reached!
% 0.45/0.57 % (2935761)------------------------------
% 0.45/0.57 % (2935761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935761)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935761)Termination reason: Instruction limit
% 0.45/0.57 % (2935761)Termination phase: Property scanning
% 0.45/0.57 % (2935761)Time elapsed: 0.058 s
% 0.45/0.57 % (2935761)Peak memory usage: 11 MB
% 0.45/0.57 % (2935761)Instructions burned: 75 (million)
% 0.45/0.57 % (2935777)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2408810458:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 0.45/0.57 % (2935773)Instruction limit reached!
% 0.45/0.57 % (2935773)------------------------------
% 0.45/0.57 % (2935773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.57 % (2935773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.57 % (2935773)CaDiCaL version: 2.1.3
% 0.45/0.57 % (2935773)Termination reason: Instruction limit
% 0.45/0.57 % (2935773)Termination phase: Property scanning
% 0.45/0.57 % (2935773)Time elapsed: 0.010 s
% 0.45/0.57 % (2935773)Peak memory usage: 10 MB
% 0.45/0.57 % (2935773)Instructions burned: 13 (million)
% 0.45/0.57 % (2935776)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.45/0.57 % (2935776)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.45/0.57 % (2935762) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2935751-2935762"...
% 0.45/0.57 % (2935776)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1493346523:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 0.45/0.57 % (2935762)...printing done.
% 0.45/0.57 % (2935762)Refutation found. Thanks to Tanya!
% 0.45/0.57 % SZS status Theorem for theBenchmark
% 0.45/0.57 % SZS output start Proof for theBenchmark
% 0.45/0.57 thf(type_def_5, type, u: $tType).
% 0.45/0.57 thf(type_def_6, type, d: $tType).
% 0.45/0.57 thf(type_def_7, type, du: $tType).
% 0.45/0.57 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 0.45/0.57 thf(type_def_9, type, mono_2Etyop_2Emin_2Eind: $tType).
% 0.45/0.57 thf(func_def_0, type, tyop_2Emin_2Ebool: d).
% 0.45/0.57 thf(func_def_1, type, tyop_2Emin_2Efun: (d > d > d)).
% 0.45/0.57 thf(func_def_2, type, s: (d > u > du)).
% 0.45/0.57 thf(func_def_3, type, app_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_4, type, combin_i_2E0: u).
% 0.45/0.57 thf(func_def_5, type, combin_k_2E0: u).
% 0.45/0.57 thf(func_def_6, type, combin_s_2E0: u).
% 0.45/0.57 thf(func_def_7, type, c_2Ebool_2E_21_2E0: u).
% 0.45/0.57 thf(func_def_8, type, c_2Ebool_2E_21_2E1: (du > u)).
% 0.45/0.57 thf(func_def_9, type, c_2Ebool_2E_2F_5C_2E0: u).
% 0.45/0.57 thf(func_def_10, type, c_2Ebool_2E_2F_5C_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_11, type, c_2Emin_2E_3D_2E0: u).
% 0.45/0.57 thf(func_def_12, type, c_2Emin_2E_3D_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_13, type, c_2Emin_2E_3D_3D_3E_2E0: u).
% 0.45/0.57 thf(func_def_14, type, c_2Emin_2E_3D_3D_3E_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_15, type, c_2Ebool_2E_3F_2E0: u).
% 0.45/0.57 thf(func_def_16, type, c_2Ebool_2E_3F_2E1: (du > u)).
% 0.45/0.57 thf(func_def_17, type, c_2Ebool_2EF_2E0: u).
% 0.45/0.57 thf(func_def_18, type, c_2Ebool_2ET_2E0: u).
% 0.45/0.57 thf(func_def_19, type, c_2Ebool_2E_5C_2F_2E0: u).
% 0.45/0.57 thf(func_def_20, type, c_2Ebool_2E_5C_2F_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_21, type, c_2Ebool_2E_7E_2E0: u).
% 0.45/0.57 thf(func_def_22, type, c_2Ebool_2E_7E_2E1: (du > u)).
% 0.45/0.57 thf(func_def_23, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: (($o > $o) > $o > $o)).
% 0.45/0.57 thf(func_def_24, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o > $o) > $o > $o > $o)).
% 0.45/0.57 thf(func_def_25, type, mono_2Ec_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 0.45/0.57 thf(func_def_26, type, mono_2Ec_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 0.45/0.57 thf(func_def_27, type, mono_2Ec_2Ebool_2EF: $o).
% 0.45/0.57 thf(func_def_28, type, mono_2Ec_2Ebool_2ET: $o).
% 0.45/0.57 thf(func_def_29, type, mono_2Ec_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 0.45/0.57 thf(func_def_30, type, mono_2Ec_2Ebool_2E_7E: ($o > $o)).
% 0.45/0.57 thf(func_def_31, type, i_mono_2Etyop_2Emin_2Ebool: ($o > u)).
% 0.45/0.57 thf(func_def_32, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o) > u)).
% 0.45/0.57 thf(func_def_33, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (($o > $o > $o) > u)).
% 0.45/0.57 thf(func_def_34, type, j_mono_2Etyop_2Emin_2Ebool: (du > $o)).
% 0.45/0.57 thf(func_def_35, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (du > $o > $o)).
% 0.45/0.57 thf(func_def_36, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: (du > $o > $o > $o)).
% 0.45/0.57 thf(func_def_38, type, vNOT: ($o > $o)).
% 0.45/0.57 thf(func_def_39, type, tyop_2Emin_2Eind: d).
% 0.45/0.57 thf(func_def_40, type, c_2Ebool_2E_3F_21_2E0: u).
% 0.45/0.57 thf(func_def_41, type, c_2Ebool_2E_3F_21_2E1: (du > u)).
% 0.45/0.57 thf(func_def_42, type, c_2Emin_2E_40_2E0: u).
% 0.45/0.57 thf(func_def_43, type, c_2Emin_2E_40_2E1: (du > u)).
% 0.45/0.57 thf(func_def_44, type, c_2Ebool_2EBOUNDED_2E0: u).
% 0.45/0.57 thf(func_def_45, type, c_2Ebool_2EBOUNDED_2E1: (du > u)).
% 0.45/0.57 thf(func_def_46, type, c_2Ebool_2ECOND_2E0: u).
% 0.45/0.57 thf(func_def_47, type, c_2Ebool_2ECOND_2E3: (du > du > du > u)).
% 0.45/0.57 thf(func_def_48, type, c_2Ebool_2EDATATYPE_2E0: u).
% 0.45/0.57 thf(func_def_49, type, c_2Ebool_2EDATATYPE_2E1: (du > u)).
% 0.45/0.57 thf(func_def_50, type, c_2Ebool_2EIN_2E0: u).
% 0.45/0.57 thf(func_def_51, type, c_2Ebool_2EIN_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_52, type, c_2Ebool_2ELET_2E0: u).
% 0.45/0.57 thf(func_def_53, type, c_2Ebool_2ELET_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_54, type, c_2Ebool_2EONE__ONE_2E0: u).
% 0.45/0.57 thf(func_def_55, type, c_2Ebool_2EONE__ONE_2E1: (du > u)).
% 0.45/0.57 thf(func_def_56, type, c_2Ebool_2EONTO_2E0: u).
% 0.45/0.57 thf(func_def_57, type, c_2Ebool_2EONTO_2E1: (du > u)).
% 0.45/0.57 thf(func_def_58, type, c_2Ebool_2ERES__EXISTS_2E0: u).
% 0.45/0.57 thf(func_def_59, type, c_2Ebool_2ERES__EXISTS_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_60, type, c_2Ebool_2ERES__EXISTS__UNIQUE_2E0: u).
% 0.45/0.57 thf(func_def_61, type, c_2Ebool_2ERES__EXISTS__UNIQUE_2E2: (du > du > u)).
% 0.45/0.57 thf(func_def_62, type, c_2Ebool_2ERES__FORALL_2E0: u).
% 0.45/0.58 thf(func_def_63, type, c_2Ebool_2ERES__FORALL_2E2: (du > du > u)).
% 0.45/0.58 thf(func_def_64, type, c_2Ebool_2ERES__SELECT_2E0: u).
% 0.45/0.58 thf(func_def_65, type, c_2Ebool_2ERES__SELECT_2E2: (du > du > u)).
% 0.45/0.58 thf(func_def_66, type, c_2Ebool_2ETYPE__DEFINITION_2E0: u).
% 0.45/0.58 thf(func_def_67, type, c_2Ebool_2ETYPE__DEFINITION_2E2: (du > du > u)).
% 0.45/0.58 thf(func_def_68, type, c_2Ebool_2Eliteral__case_2E0: u).
% 0.45/0.58 thf(func_def_69, type, c_2Ebool_2Eliteral__case_2E2: (du > du > u)).
% 0.45/0.58 thf(func_def_70, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_20mono_2Etyop_2Emin_2Ebool: (((mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o) > (mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o)).
% 0.45/0.58 thf(func_def_71, type, mono_2Ec_2Ebool_2EBOUNDED: ($o > $o)).
% 0.45/0.58 thf(func_def_72, type, mono_2Ec_2Ebool_2EONE__ONE_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind: ((mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o)).
% 0.45/0.58 thf(func_def_73, type, mono_2Ec_2Ebool_2EONTO_2Emono_2Etyop_2Emin_2Eind_20mono_2Etyop_2Emin_2Eind: ((mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o)).
% 0.45/0.58 thf(func_def_74, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29: (((mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o) > u)).
% 0.45/0.58 thf(func_def_75, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29: ((mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > u)).
% 0.45/0.58 thf(func_def_76, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29_2Ctyop_2Emin_2Ebool_29: (du > (mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind) > $o)).
% 0.45/0.58 thf(func_def_77, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Eind_2Ctyop_2Emin_2Eind_29: (du > mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind)).
% 0.45/0.58 thf(func_def_80, type, sP0: (u > d > $o)).
% 0.45/0.58 thf(func_def_81, type, sP1: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_82, type, sP2: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_83, type, sP3: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_84, type, sP4: (u > u > d > u > $o)).
% 0.45/0.58 thf(func_def_85, type, sP5: (u > u > u > d > u > $o)).
% 0.45/0.58 thf(func_def_86, type, sP6: (u > d > $o)).
% 0.45/0.58 thf(func_def_87, type, sP7: (u > u > d > $o)).
% 0.45/0.58 thf(func_def_88, type, sP8: (u > u > d > d > $o)).
% 0.45/0.58 thf(func_def_89, type, sP9: (u > d > u > d > $o)).
% 0.45/0.58 thf(func_def_90, type, sP10: (u > u > d > u > $o)).
% 0.45/0.58 thf(func_def_91, type, sP11: (u > d > $o)).
% 0.45/0.58 thf(func_def_92, type, sP12: ($o > $o > $o > $o)).
% 0.45/0.58 thf(func_def_93, type, sP13: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_94, type, sP14: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_95, type, sP15: ($o > u > d > u > $o)).
% 0.45/0.58 thf(func_def_96, type, sP16: (u > $o > u > d > u > $o)).
% 0.45/0.58 thf(func_def_97, type, sP17: (u > d > $o)).
% 0.45/0.58 thf(func_def_98, type, sK18: (u > u > d > d > u)).
% 0.45/0.58 thf(func_def_99, type, sK19: (d > u > d > u > u)).
% 0.45/0.58 thf(func_def_100, type, sK20: (d > u > d > u)).
% 0.45/0.58 thf(func_def_101, type, sK21: (u > d > u > d > u)).
% 0.45/0.58 thf(func_def_102, type, sK22: (u > d > u)).
% 0.45/0.58 thf(func_def_103, type, sK23: (u > d > u)).
% 0.45/0.58 thf(func_def_104, type, sK24: $o).
% 0.45/0.58 thf(func_def_105, type, sK25: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_106, type, sK26: (mono_2Etyop_2Emin_2Eind > mono_2Etyop_2Emin_2Eind)).
% 0.45/0.58 thf(func_def_107, type, sK27: (d > u > u)).
% 0.45/0.58 thf(func_def_108, type, sK28: (u > u > d > u)).
% 0.45/0.58 thf(func_def_109, type, sK29: (u > d > u)).
% 0.45/0.58 thf(func_def_110, type, sK30: (u > d > u)).
% 0.45/0.58 thf(func_def_111, type, sK31: (u > d > u)).
% 0.45/0.58 thf(func_def_112, type, sK32: (u > d > u)).
% 0.45/0.58 thf(func_def_113, type, sK33: (d > u > u > u)).
% 0.45/0.58 thf(func_def_114, type, sK34: (d > u > u > u)).
% 0.45/0.58 thf(func_def_115, type, sK35: (d > u > u > u)).
% 0.45/0.58 thf(func_def_116, type, sK36: (d > u > u)).
% 0.45/0.58 thf(func_def_117, type, sK37: (d > u > u)).
% 0.45/0.58 thf(func_def_118, type, sK38: (d > u > u)).
% 0.45/0.58 thf(func_def_119, type, sK39: (d > u > d > u)).
% 0.45/0.58 thf(func_def_120, type, sK40: (d > u > d > u)).
% 0.45/0.58 thf(func_def_121, type, sK41: (u > u > d > d > u)).
% 0.45/0.58 thf(func_def_122, type, sK42: (u > u > d > d > u)).
% 0.45/0.58 thf(func_def_123, type, sK43: (u > u > d > d > u)).
% 0.45/0.58 thf(func_def_124, type, sK44: (d > u > u > u)).
% 0.45/0.58 thf(func_def_125, type, sK45: (d > u > u)).
% 0.45/0.58 thf(func_def_126, type, sK46: (u > d > u)).
% 0.45/0.58 thf(func_def_127, type, sK47: (u > d > u)).
% 0.45/0.58 thf(func_def_128, type, sK48: (u > d > u)).
% 0.45/0.58 thf(func_def_129, type, sK49: (d > u > u)).
% 0.45/0.58 thf(func_def_130, type, sK50: ($o > $o > $o)).
% 0.45/0.58 thf(func_def_131, type, sK51: (u > d > d > u)).
% 0.45/0.58 thf(func_def_132, type, sK52: (u > d > d > u)).
% 0.45/0.58 thf(func_def_133, type, sK53: (u > d > u)).
% 0.45/0.58 thf(func_def_134, type, sK54: (u > d > $o)).
% 0.45/0.58 thf(func_def_135, type, sK55: (u > d > u)).
% 0.45/0.58 thf(func_def_136, type, sK56: (u > d > u)).
% 0.45/0.58 thf(func_def_137, type, sK57: $o).
% 0.45/0.58 thf(f73,axiom,(
% 0.45/0.58 ! [X0 : $o] : ((X0 = mono_2Ec_2Ebool_2ET) | (X0 = mono_2Ec_2Ebool_2EF))),
% 0.45/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EBOOL__CASES__AX)).
% 0.45/0.58 thf(f83,axiom,(
% 0.45/0.58 ! [X0 : $o] : ((X0 => mono_2Ec_2Ebool_2EF) <=> (~ X0))),
% 0.45/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__DEF)).
% 0.45/0.58 thf(f98,conjecture,(
% 0.45/0.58 mono_2Ec_2Ebool_2ET),
% 0.45/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH)).
% 0.45/0.58 thf(f99,negated_conjecture,(
% 0.45/0.58 ~mono_2Ec_2Ebool_2ET),
% 0.45/0.58 inference(negated_conjecture,[status(cth)],[f98])).
% 0.45/0.58 thf(f130,plain,(
% 0.45/0.58 ! [X0 : $o] : ((X0 => mono_2Ec_2Ebool_2EF) <=> (~ X0))),
% 0.45/0.58 inference(rectify,[],[f83])).
% 0.45/0.58 thf(f131,plain,(
% 0.45/0.58 ! [X0 : $o] : ((((~ X0)) = $true) <=> (($true = X0) => (mono_2Ec_2Ebool_2EF = $true)))),
% 0.45/0.58 inference(fool_elimination,[],[f130])).
% 0.45/0.58 thf(f166,plain,(
% 0.45/0.58 ~mono_2Ec_2Ebool_2ET),
% 0.45/0.58 inference(rectify,[],[f99])).
% 0.45/0.58 thf(f167,plain,(
% 0.45/0.58 ~ (mono_2Ec_2Ebool_2ET = $true)),
% 0.45/0.58 inference(fool_elimination,[],[f166])).
% 0.45/0.58 thf(f198,plain,(
% 0.45/0.58 (mono_2Ec_2Ebool_2ET != $true)),
% 0.45/0.58 inference(flattening,[],[f167])).
% 0.45/0.58 thf(f214,plain,(
% 0.45/0.58 ! [X0 : $o] : ((($true != X0) | (mono_2Ec_2Ebool_2EF = $true)) <=> (((~ X0)) = $true))),
% 0.45/0.58 inference(ennf_transformation,[],[f131])).
% 0.45/0.58 thf(f394,plain,(
% 0.45/0.58 ! [X0 : $o] : (((($true != X0) | (mono_2Ec_2Ebool_2EF = $true)) | (((~ X0)) != $true)) & ((((~ X0)) = $true) | (($true = X0) & (mono_2Ec_2Ebool_2EF != $true))))),
% 0.45/0.58 inference(nnf_transformation,[],[f214])).
% 0.45/0.58 thf(f395,plain,(
% 0.45/0.58 ! [X0 : $o] : ((($true != X0) | (mono_2Ec_2Ebool_2EF = $true) | (((~ X0)) != $true)) & ((((~ X0)) = $true) | (($true = X0) & (mono_2Ec_2Ebool_2EF != $true))))),
% 0.45/0.58 inference(flattening,[],[f394])).
% 0.45/0.58 thf(f495,plain,(
% 0.45/0.58 ( ! [X0 : $o] : ((mono_2Ec_2Ebool_2EF = X0) | (mono_2Ec_2Ebool_2ET = X0)) )),
% 0.45/0.58 inference(cnf_transformation,[],[f73])).
% 0.45/0.58 thf(f524,plain,(
% 0.45/0.58 (mono_2Ec_2Ebool_2ET != $true)),
% 0.45/0.58 inference(cnf_transformation,[],[f198])).
% 0.45/0.58 thf(f585,plain,(
% 0.45/0.58 ( ! [X0 : $o] : ((mono_2Ec_2Ebool_2EF != $true) | (((~ X0)) = $true)) )),
% 0.45/0.58 inference(cnf_transformation,[],[f395])).
% 0.45/0.58 thf(f595,definition,(
% 0.45/0.58 ($true != $false)),
% 0.45/0.58 introduced(theory,[fool_distinctness_axiom])).
% 0.45/0.58 thf(f623,plain,(
% 0.45/0.58 ( ! [X0 : $o] : ((mono_2Ec_2Ebool_2EF != $true) | ($false = X0)) )),
% 0.45/0.58 inference(not_proxy_clausification,[],[f585])).
% 0.45/0.58 thf(f699,plain,(
% 0.45/0.58 ( ! [X0 : $o] : (($false = X0) | (mono_2Ec_2Ebool_2ET = X0) | (mono_2Ec_2Ebool_2EF = $true)) )),
% 0.45/0.58 inference(iff_proxy_clausification,[],[f495])).
% 0.45/0.58 thf(f704,plain,(
% 0.45/0.58 ( ! [X0 : $o] : (($false = X0) | ($false = X0) | (mono_2Ec_2Ebool_2EF = $true) | (mono_2Ec_2Ebool_2ET = $true)) )),
% 0.45/0.58 inference(iff_proxy_clausification,[],[f699])).
% 0.45/0.58 thf(f706,plain,(
% 0.45/0.58 ( ! [X0 : $o] : (($false = X0) | (mono_2Ec_2Ebool_2EF = $true) | (mono_2Ec_2Ebool_2ET = $true)) )),
% 0.45/0.58 inference(duplicate_literal_removal,[],[f704])).
% 0.45/0.58 thf(f708,definition,(
% 0.45/0.58 spl58_1 <=> ! [X0 : $o] : ($false = X0)),
% 0.45/0.58 introduced(definition,[new_symbols(definition,[spl58_1])],[avatar_definition])).
% 0.45/0.58 thf(f709,plain,(
% 0.45/0.58 ( ! [X0 : $o] : (($false = X0)) ) | ~spl58_1),
% 0.45/0.58 inference(avatar_component_clause,[],[f708])).
% 0.45/0.58 thf(f711,definition,(
% 0.45/0.58 spl58_2 <=> (mono_2Ec_2Ebool_2EF = $true)),
% 0.45/0.58 introduced(definition,[new_symbols(definition,[spl58_2])],[avatar_definition])).
% 0.45/0.58 thf(f714,plain,(
% 0.45/0.58 spl58_1 | ~spl58_2),
% 0.45/0.58 inference(avatar_split_clause,[],[f623,f711,f708])).
% 0.45/0.58 thf(f719,definition,(
% 0.45/0.58 spl58_4 <=> (mono_2Ec_2Ebool_2ET = $true)),
% 0.45/0.58 introduced(definition,[new_symbols(definition,[spl58_4])],[avatar_definition])).
% 0.45/0.58 thf(f783,plain,(
% 0.45/0.58 ~spl58_4),
% 0.45/0.58 inference(avatar_split_clause,[],[f524,f719])).
% 0.45/0.58 thf(f805,plain,(
% 0.45/0.58 spl58_4 | spl58_1 | spl58_2),
% 0.45/0.58 inference(avatar_split_clause,[],[f706,f711,f708,f719])).
% 0.45/0.58 thf(f807,plain,(
% 0.45/0.58 ($false != $false) | ~spl58_1),
% 0.45/0.58 inference(constrained_superposition,[],[f595,f709])).
% 0.45/0.58 thf(f810,plain,(
% 0.45/0.58 $false | ~spl58_1),
% 0.45/0.58 inference(trivial_inequality_removal,[],[f807])).
% 0.45/0.58 thf(f811,plain,(
% 0.45/0.58 ~spl58_1),
% 0.45/0.58 inference(avatar_contradiction_clause,[],[f810])).
% 0.45/0.58 cnf(s1, plain, spl58_1 | ~spl58_2, inference(sat_conversion,[],[f714])).
% 0.45/0.58 cnf(s18, plain, ~spl58_4, inference(sat_conversion,[],[f783])).
% 0.45/0.58 cnf(s28, plain, spl58_1 | spl58_2 | spl58_4, inference(sat_conversion,[],[f805])).
% 0.45/0.58 cnf(s29, plain, ~spl58_1, inference(sat_conversion,[],[f811])).
% 0.45/0.58 cnf(s30, plain, spl58_2 | spl58_4, inference(rat,[],[s28,s29])).
% 0.45/0.58 cnf(s31, plain, spl58_2, inference(rat,[],[s30,s18])).
% 0.45/0.58 cnf(s40, plain, $false, inference(rat,[],[s1,s31,s29])).
% 0.45/0.58 thf(f812,plain,(
% 0.45/0.58 $false),
% 0.45/0.58 inference(avatar_sat_refutation,[],[s40])).
% 0.45/0.58 % SZS output end Proof for theBenchmark
% 0.45/0.58 % (2935762)------------------------------
% 0.45/0.58 % (2935762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.45/0.58 % (2935762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.45/0.58 % (2935762)CaDiCaL version: 2.1.3
% 0.45/0.58 % (2935762)Termination reason: Refutation
% 0.45/0.58 % (2935762)Time elapsed: 0.071 s
% 0.45/0.58 % (2935762)Peak memory usage: 13 MB
% 0.45/0.58 % (2935762)Instructions burned: 90 (million)
% 0.45/0.58 % (2935751)Success in time 0.146 s
% 0.45/0.58 % Vampire exiting
%------------------------------------------------------------------------------