%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP012^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:07:44 AM UTC 2026
% Result : Theorem 0.62s 0.43s
% Output : Refutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP012^1 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n014.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 19:26:45 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.62/0.43 % (3100153)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.62/0.43 % (3100164)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.62/0.43 % (3100164)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.62/0.43 % (3100160)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2297481636:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.62/0.43 % (3100164)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=1256568234:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.62/0.43 % (3100160)Instruction limit reached!
% 0.62/0.43 % (3100160)------------------------------
% 0.62/0.43 % (3100160)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100160)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100160)Termination reason: Instruction limit
% 0.62/0.43 % (3100160)Termination phase: shuffling
% 0.62/0.43 % (3100160)Time elapsed: 0.003 s
% 0.62/0.43 % (3100160)Peak memory usage: 10 MB
% 0.62/0.43 % (3100160)Instructions burned: 6 (million)
% 0.62/0.43 % (3100161)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=4187909602: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.62/0.43 % (3100162)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1778031063:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.62/0.43 % (3100158)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3526321598:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.62/0.43 % (3100167)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3546255000:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.62/0.43 % (3100159)lrs+10_16_si=on:nwc=1.5:random_seed=1759657271:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.62/0.43 % (3100167)Instruction limit reached!
% 0.62/0.43 % (3100167)------------------------------
% 0.62/0.43 % (3100167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100167)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100167)Termination reason: Instruction limit
% 0.62/0.43 % (3100167)Termination phase: Property scanning
% 0.62/0.43 % (3100167)Time elapsed: 0.001 s
% 0.62/0.43 % (3100167)Peak memory usage: 10 MB
% 0.62/0.43 % (3100167)Instructions burned: 2 (million)
% 0.62/0.43 % (3100163)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1885079937:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.62/0.43 % (3100162)Instruction limit reached!
% 0.62/0.43 % (3100162)------------------------------
% 0.62/0.43 % (3100162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100162)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100162)Termination reason: Instruction limit
% 0.62/0.43 % (3100162)Termination phase: Property scanning
% 0.62/0.43 % (3100162)Time elapsed: 0.011 s
% 0.62/0.43 % (3100162)Peak memory usage: 11 MB
% 0.62/0.43 % (3100162)Instructions burned: 25 (million)
% 0.62/0.43 % (3100175)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.62/0.43 % (3100173)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=933647963:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.62/0.43 % (3100175)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2022225309:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.62/0.43 % (3100159)Instruction limit reached!
% 0.62/0.43 % (3100159)------------------------------
% 0.62/0.43 % (3100159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100159)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100159)Termination reason: Instruction limit
% 0.62/0.43 % (3100159)Termination phase: Property scanning
% 0.62/0.43 % (3100159)Time elapsed: 0.025 s
% 0.62/0.43 % (3100159)Peak memory usage: 10 MB
% 0.62/0.43 % (3100159)Instructions burned: 18 (million)
% 0.62/0.43 % (3100173)Instruction limit reached!
% 0.62/0.43 % (3100173)------------------------------
% 0.62/0.43 % (3100173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100173)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100173)Termination reason: Instruction limit
% 0.62/0.43 % (3100173)Termination phase: Preprocessing 1
% 0.62/0.43 % (3100173)Time elapsed: 0.003 s
% 0.62/0.43 % (3100173)Peak memory usage: 10 MB
% 0.62/0.43 % (3100173)Instructions burned: 6 (million)
% 0.62/0.43 % (3100175)Instruction limit reached!
% 0.62/0.43 % (3100175)------------------------------
% 0.62/0.43 % (3100175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100175)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100175)Termination reason: Instruction limit
% 0.62/0.43 % (3100175)Termination phase: Property scanning
% 0.62/0.43 % (3100175)Time elapsed: 0.004 s
% 0.62/0.43 % (3100175)Peak memory usage: 10 MB
% 0.62/0.43 % (3100175)Instructions burned: 9 (million)
% 0.62/0.43 % (3100179)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.62/0.43 % (3100179)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.62/0.43 % (3100164)Instruction limit reached!
% 0.62/0.43 % (3100164)------------------------------
% 0.62/0.43 % (3100164)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100164)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100164)Termination reason: Instruction limit
% 0.62/0.43 % (3100164)Termination phase: Saturation
% 0.62/0.43 % (3100164)Time elapsed: 0.082 s
% 0.62/0.43 % (3100164)Peak memory usage: 13 MB
% 0.62/0.43 % (3100164)Instructions burned: 158 (million)
% 0.62/0.43 % (3100179)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1156390965:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.62/0.43 % (3100178)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2800796158:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.62/0.43 % (3100181)lrs+10_1_si=on:cs=on:random_seed=2664543242:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 0.62/0.43 % (3100178)Instruction limit reached!
% 0.62/0.43 % (3100178)------------------------------
% 0.62/0.43 % (3100178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100178)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100178)Termination reason: Instruction limit
% 0.62/0.43 % (3100178)Termination phase: Property scanning
% 0.62/0.43 % (3100178)Time elapsed: 0.014 s
% 0.62/0.43 % (3100178)Peak memory usage: 11 MB
% 0.62/0.43 % (3100178)Instructions burned: 14 (million)
% 0.62/0.43 % (3100180)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=663914804:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.62/0.43 % (3100181)Instruction limit reached!
% 0.62/0.43 % (3100181)------------------------------
% 0.62/0.43 % (3100181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100181)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100181)Termination reason: Instruction limit
% 0.62/0.43 % (3100181)Termination phase: Preprocessing 3
% 0.62/0.43 % (3100181)Time elapsed: 0.004 s
% 0.62/0.43 % (3100181)Peak memory usage: 10 MB
% 0.62/0.43 % (3100181)Instructions burned: 9 (million)
% 0.62/0.43 % (3100179)Instruction limit reached!
% 0.62/0.43 % (3100179)------------------------------
% 0.62/0.43 % (3100179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100179)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100179)Termination reason: Instruction limit
% 0.62/0.43 % (3100179)Termination phase: Property scanning
% 0.62/0.43 % (3100179)Time elapsed: 0.020 s
% 0.62/0.43 % (3100179)Peak memory usage: 11 MB
% 0.62/0.43 % (3100179)Instructions burned: 28 (million)
% 0.62/0.43 % (3100161) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3100153-3100161"...
% 0.62/0.43 % (3100161)...printing done.
% 0.62/0.43 % (3100161)Refutation found. Thanks to Tanya!
% 0.62/0.43 % SZS status Theorem for theBenchmark
% 0.62/0.43 % SZS output start Proof for theBenchmark
% 0.62/0.43 thf(type_def_5, type, u: $tType).
% 0.62/0.43 thf(type_def_6, type, d: $tType).
% 0.62/0.43 thf(type_def_7, type, du: $tType).
% 0.62/0.43 thf(type_def_8, type, mono_2Etyop_2Einteger_2Eint: $tType).
% 0.62/0.43 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 0.62/0.43 thf(func_def_0, type, tyop_2Einteger_2Eint: d).
% 0.62/0.43 thf(func_def_1, type, tyop_2Emin_2Ebool: d).
% 0.62/0.43 thf(func_def_2, type, tyop_2Emin_2Efun: (d > d > d)).
% 0.62/0.43 thf(func_def_3, type, s: (d > u > du)).
% 0.62/0.43 thf(func_def_4, type, app_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_5, type, combin_i_2E0: u).
% 0.62/0.43 thf(func_def_6, type, combin_k_2E0: u).
% 0.62/0.43 thf(func_def_7, type, combin_s_2E0: u).
% 0.62/0.43 thf(func_def_8, type, c_2Ebool_2E_21_2E0: u).
% 0.62/0.43 thf(func_def_9, type, c_2Ebool_2E_21_2E1: (du > u)).
% 0.62/0.43 thf(func_def_10, type, c_2Ebool_2E_2F_5C_2E0: u).
% 0.62/0.43 thf(func_def_11, type, c_2Ebool_2E_2F_5C_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_12, type, c_2Emin_2E_3D_2E0: u).
% 0.62/0.43 thf(func_def_13, type, c_2Emin_2E_3D_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_14, type, c_2Emin_2E_3D_3D_3E_2E0: u).
% 0.62/0.43 thf(func_def_15, type, c_2Emin_2E_3D_3D_3E_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_16, type, c_2Ebool_2E_3F_2E0: u).
% 0.62/0.43 thf(func_def_17, type, c_2Ebool_2E_3F_2E1: (du > u)).
% 0.62/0.43 thf(func_def_18, type, c_2Ebool_2EF_2E0: u).
% 0.62/0.43 thf(func_def_19, type, c_2Ebool_2ET_2E0: u).
% 0.62/0.43 thf(func_def_20, type, c_2Ebool_2E_5C_2F_2E0: u).
% 0.62/0.43 thf(func_def_21, type, c_2Ebool_2E_5C_2F_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_22, type, c_2Einteger_2Eint__add_2E0: u).
% 0.62/0.43 thf(func_def_23, type, c_2Einteger_2Eint__add_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_24, type, c_2Einteger_2Eint__divides_2E0: u).
% 0.62/0.43 thf(func_def_25, type, c_2Einteger_2Eint__divides_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_26, type, c_2Einteger_2Eint__neg_2E0: u).
% 0.62/0.43 thf(func_def_27, type, c_2Einteger_2Eint__neg_2E1: (du > u)).
% 0.62/0.43 thf(func_def_28, type, c_2Einteger_2Eint__sub_2E0: u).
% 0.62/0.43 thf(func_def_29, type, c_2Einteger_2Eint__sub_2E2: (du > du > u)).
% 0.62/0.43 thf(func_def_30, type, c_2Ebool_2E_7E_2E0: u).
% 0.62/0.43 thf(func_def_31, type, c_2Ebool_2E_7E_2E1: (du > u)).
% 0.62/0.43 thf(func_def_32, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: (($o > $o) > $o > $o)).
% 0.62/0.43 thf(func_def_33, 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.62/0.43 thf(func_def_34, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Ebool: ((mono_2Etyop_2Einteger_2Eint > $o) > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.62/0.43 thf(func_def_35, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.62/0.43 thf(func_def_36, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_37, type, mono_2Eapp_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Einteger_2Eint: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_38, type, mono_2Ec_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 0.62/0.43 thf(func_def_39, type, mono_2Ec_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 0.62/0.43 thf(func_def_40, type, mono_2Ec_2Ebool_2EF: $o).
% 0.62/0.43 thf(func_def_41, type, mono_2Ec_2Ebool_2ET: $o).
% 0.62/0.43 thf(func_def_42, type, mono_2Ec_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 0.62/0.43 thf(func_def_43, type, mono_2Ec_2Einteger_2Eint__add: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_44, type, mono_2Ec_2Einteger_2Eint__divides: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.62/0.43 thf(func_def_45, type, mono_2Ec_2Einteger_2Eint__neg: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_46, type, mono_2Ec_2Einteger_2Eint__sub: (mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_47, type, mono_2Ec_2Ebool_2E_7E: ($o > $o)).
% 0.62/0.43 thf(func_def_48, type, i_mono_2Etyop_2Emin_2Ebool: ($o > u)).
% 0.62/0.43 thf(func_def_49, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (($o > $o) > u)).
% 0.62/0.43 thf(func_def_50, 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.62/0.43 thf(func_def_51, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: ((mono_2Etyop_2Einteger_2Eint > $o) > u)).
% 0.62/0.43 thf(func_def_52, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o) > u)).
% 0.62/0.43 thf(func_def_53, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > u)).
% 0.62/0.43 thf(func_def_54, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: ((mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint) > u)).
% 0.62/0.43 thf(func_def_55, type, i_mono_2Etyop_2Einteger_2Eint: (mono_2Etyop_2Einteger_2Eint > u)).
% 0.62/0.43 thf(func_def_56, type, j_mono_2Etyop_2Emin_2Ebool: (du > $o)).
% 0.62/0.43 thf(func_def_57, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: (du > $o > $o)).
% 0.62/0.43 thf(func_def_58, 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.62/0.43 thf(func_def_59, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: (du > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.62/0.43 thf(func_def_60, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o)).
% 0.62/0.43 thf(func_def_61, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_62, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: (du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_63, type, j_mono_2Etyop_2Einteger_2Eint: (du > mono_2Etyop_2Einteger_2Eint)).
% 0.62/0.43 thf(func_def_65, type, vNOT: ($o > $o)).
% 0.62/0.43 thf(func_def_68, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.62/0.43 thf(func_def_69, type, db0: !>[X0: $tType]:(X0)).
% 0.62/0.43 thf(func_def_70, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.62/0.43 thf(func_def_71, type, vAND: ($o > $o > $o)).
% 0.62/0.43 thf(func_def_72, type, vOR: ($o > $o > $o)).
% 0.62/0.43 thf(func_def_73, type, sP0: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_74, type, sP1: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_75, type, sP2: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_76, type, sP3: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_77, type, sP4: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_78, type, sP5: ($o > $o > $o > $o)).
% 0.62/0.43 thf(func_def_79, type, sK6: (u > d > u)).
% 0.62/0.43 thf(func_def_80, type, sK7: (u > d > u)).
% 0.62/0.43 thf(func_def_81, type, sK8: (d > d > u > u > u)).
% 0.62/0.43 thf(func_def_82, type, sK9: mono_2Etyop_2Einteger_2Eint).
% 0.62/0.43 thf(func_def_83, type, sK10: mono_2Etyop_2Einteger_2Eint).
% 0.62/0.43 thf(func_def_84, type, sK11: mono_2Etyop_2Einteger_2Eint).
% 0.62/0.43 thf(func_def_85, type, sK12: (d > u > u)).
% 0.62/0.43 thf(func_def_86, type, sK13: (u > d > u)).
% 0.62/0.43 thf(func_def_87, type, sK14: (u > d > u > u)).
% 0.62/0.43 thf(func_def_88, type, sK15: (u > d > u)).
% 0.62/0.43 thf(func_def_89, type, sK16: (u > d > u)).
% 0.62/0.43 thf(f49,axiom,(
% 0.62/0.43 ! [X0 : $o] : (((~ X0) <=> (mono_2Ec_2Ebool_2EF = X0)) & ((~ X0) <=> (X0 = mono_2Ec_2Ebool_2EF)) & ((X0 = mono_2Ec_2Ebool_2ET) <=> X0) & (X0 <=> (mono_2Ec_2Ebool_2ET = X0)))),
% 0.62/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__CLAUSES)).
% 0.62/0.43 thf(f55,axiom,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : (((mono_2Ec_2Einteger_2Eint__sub @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__add @ X0 @ (mono_2Ec_2Einteger_2Eint__neg @ X1))))),
% 0.62/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2Eint__sub)).
% 0.62/0.43 thf(f56,axiom,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__add @ X2 @ X1))) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2))))),
% 0.62/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__DIVIDES__RADD)).
% 0.62/0.43 thf(f57,axiom,(
% 0.62/0.43 ! [X1 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__neg @ X1))) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1))) & (((mono_2Ec_2Einteger_2Eint__divides @ (mono_2Ec_2Einteger_2Eint__neg @ X0) @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1))))),
% 0.62/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__DIVIDES__NEG)).
% 0.62/0.43 thf(f68,conjecture,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__sub @ X2 @ X1))) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2))))),
% 0.62/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__DIVIDES__RSUB)).
% 0.62/0.43 thf(f69,negated_conjecture,(
% 0.62/0.43 ~ ! [X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__sub @ X2 @ X1))) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2))))),
% 0.62/0.43 inference(negated_conjecture,[status(cth)],[f68])).
% 0.62/0.43 thf(f102,plain,(
% 0.62/0.43 ! [X0 : $o] : (((~ X0) <=> (mono_2Ec_2Ebool_2EF = X0)) & ((~ X0) <=> (X0 = mono_2Ec_2Ebool_2EF)) & ((X0 = mono_2Ec_2Ebool_2ET) <=> X0) & (X0 <=> (mono_2Ec_2Ebool_2ET = X0)))),
% 0.62/0.43 inference(rectify,[],[f49])).
% 0.62/0.43 thf(f103,plain,(
% 0.62/0.43 ! [X0 : $o] : ((((mono_2Ec_2Ebool_2EF = $true) <=> ($true = X0)) <=> (((~ X0)) = $true)) & ((((~ X0)) = $true) <=> ((mono_2Ec_2Ebool_2EF = $true) <=> ($true = X0))) & (($true = X0) <=> (($true = X0) <=> (mono_2Ec_2Ebool_2ET = $true))) & (($true = X0) <=> ((mono_2Ec_2Ebool_2ET = $true) <=> ($true = X0))))),
% 0.62/0.43 inference(fool_elimination,[],[f102])).
% 0.62/0.43 thf(f122,plain,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__add @ X1 @ X2)))))),
% 0.62/0.43 inference(rectify,[],[f56])).
% 0.62/0.43 thf(f123,plain,(
% 0.62/0.43 ! [X1 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2)) = $true) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__add @ X1 @ X2)))))),
% 0.62/0.43 inference(fool_elimination,[],[f122])).
% 0.62/0.43 thf(f132,plain,(
% 0.62/0.43 ~ ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__sub @ X1 @ X2)))))),
% 0.62/0.43 inference(rectify,[],[f69])).
% 0.62/0.43 thf(f133,plain,(
% 0.62/0.43 ~ ! [X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2)) = $true) => (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__sub @ X1 @ X2)))))),
% 0.62/0.43 inference(fool_elimination,[],[f132])).
% 0.62/0.43 thf(f156,plain,(
% 0.62/0.43 ? [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2)) = $true) & (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) != ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__sub @ X1 @ X2)))))),
% 0.62/0.43 inference(ennf_transformation,[],[f133])).
% 0.62/0.43 thf(f157,plain,(
% 0.62/0.43 ! [X1 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X2)) != $true) | (((mono_2Ec_2Einteger_2Eint__divides @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__divides @ X0 @ (mono_2Ec_2Einteger_2Eint__add @ X1 @ X2)))))),
% 0.62/0.43 inference(ennf_transformation,[],[f123])).
% 0.62/0.43 thf(f184,plain,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint,X2 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X2)) != $true) | (((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)) = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__add @ X0 @ X2)))))),
% 0.62/0.43 inference(rectify,[],[f157])).
% 0.62/0.43 thf(f188,plain,(
% 0.62/0.43 ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__neg @ X0))) = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0))) & (((mono_2Ec_2Einteger_2Eint__divides @ (mono_2Ec_2Einteger_2Eint__neg @ X1) @ X0)) = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0))))),
% 0.62/0.43 inference(rectify,[],[f57])).
% 0.62/0.43 thf(f205,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $true) & (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) != ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))))),
% 0.62/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11)],[f156])).
% 0.62/0.43 thf(f220,plain,(
% 0.62/0.43 ! [X0 : $o] : ((((((mono_2Ec_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2EF != $true))) | (((~ X0)) != $true)) & ((((~ X0)) = $true) | ((($true != X0) | (mono_2Ec_2Ebool_2EF != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2EF = $true))))) & (((((~ X0)) = $true) | ((($true != X0) | (mono_2Ec_2Ebool_2EF != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2EF = $true)))) & ((((mono_2Ec_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2EF != $true))) | (((~ X0)) != $true))) & ((($true = X0) | (((mono_2Ec_2Ebool_2ET != $true) | ($true != X0)) & ((mono_2Ec_2Ebool_2ET = $true) | ($true = X0)))) & (((($true = X0) | (mono_2Ec_2Ebool_2ET != $true)) & ((mono_2Ec_2Ebool_2ET = $true) | ($true != X0))) | ($true != X0))) & ((($true = X0) | ((($true != X0) | (mono_2Ec_2Ebool_2ET != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2ET = $true)))) & ((((mono_2Ec_2Ebool_2ET = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2ET != $true))) | ($true != X0))))),
% 0.62/0.43 inference(nnf_transformation,[],[f103])).
% 0.62/0.43 thf(f221,plain,(
% 0.62/0.43 ! [X0 : $o] : (((((mono_2Ec_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2EF != $true))) | (((~ X0)) != $true)) & ((((~ X0)) = $true) | ((($true != X0) | (mono_2Ec_2Ebool_2EF != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2EF = $true)))) & ((((~ X0)) = $true) | ((($true != X0) | (mono_2Ec_2Ebool_2EF != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2EF = $true)))) & ((((mono_2Ec_2Ebool_2EF = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2EF != $true))) | (((~ X0)) != $true)) & (($true = X0) | (((mono_2Ec_2Ebool_2ET != $true) | ($true != X0)) & ((mono_2Ec_2Ebool_2ET = $true) | ($true = X0)))) & (((($true = X0) | (mono_2Ec_2Ebool_2ET != $true)) & ((mono_2Ec_2Ebool_2ET = $true) | ($true != X0))) | ($true != X0)) & (($true = X0) | ((($true != X0) | (mono_2Ec_2Ebool_2ET != $true)) & (($true = X0) | (mono_2Ec_2Ebool_2ET = $true)))) & ((((mono_2Ec_2Ebool_2ET = $true) | ($true != X0)) & (($true = X0) | (mono_2Ec_2Ebool_2ET != $true))) | ($true != X0)))),
% 0.62/0.43 inference(flattening,[],[f220])).
% 0.62/0.43 thf(f283,plain,(
% 0.62/0.43 ( ! [X2 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)) = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__add @ X0 @ X2)))) | (((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X2)) != $true)) )),
% 0.62/0.43 inference(cnf_transformation,[],[f184])).
% 0.62/0.43 thf(f290,plain,(
% 0.62/0.43 ( ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__neg @ X0))) = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)))) )),
% 0.62/0.43 inference(cnf_transformation,[],[f188])).
% 0.62/0.43 thf(f322,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) != ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))))),
% 0.62/0.43 inference(cnf_transformation,[],[f205])).
% 0.62/0.43 thf(f323,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $true)),
% 0.62/0.43 inference(cnf_transformation,[],[f205])).
% 0.62/0.43 thf(f370,plain,(
% 0.62/0.43 ( ! [X0 : $o] : ((((~ X0)) = $true) | ($true != X0) | (mono_2Ec_2Ebool_2EF != $true)) )),
% 0.62/0.43 inference(cnf_transformation,[],[f221])).
% 0.62/0.43 thf(f445,plain,(
% 0.62/0.43 ( ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__sub @ X0 @ X1)) = ((mono_2Ec_2Einteger_2Eint__add @ X0 @ (mono_2Ec_2Einteger_2Eint__neg @ X1))))) )),
% 0.62/0.43 inference(cnf_transformation,[],[f55])).
% 0.62/0.43 thf(f529,plain,(
% 0.62/0.43 (((~ $true)) = $true) | (mono_2Ec_2Ebool_2EF != $true)),
% 0.62/0.43 inference(equality_resolution,[],[f370])).
% 0.62/0.43 thf(f653,plain,(
% 0.62/0.43 ( ! [X2 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : (($false = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__add @ X0 @ X2)))) | (((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X2)) != $true) | ($true = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)))) )),
% 0.62/0.43 inference(iff_proxy_clausification,[],[f283])).
% 0.62/0.43 thf(f654,plain,(
% 0.62/0.43 ( ! [X2 : mono_2Etyop_2Einteger_2Eint,X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : (($true = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__add @ X0 @ X2)))) | (((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X2)) != $true) | ($false = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)))) )),
% 0.62/0.43 inference(iff_proxy_clausification,[],[f283])).
% 0.62/0.43 thf(f668,plain,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF != $true) | ($false = $true)),
% 0.62/0.43 inference(not_proxy_clausification,[],[f529])).
% 0.62/0.43 thf(f669,plain,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF != $true)),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f668])).
% 0.62/0.43 thf(f671,plain,(
% 0.62/0.43 ( ! [X0 : mono_2Etyop_2Einteger_2Eint,X1 : mono_2Etyop_2Einteger_2Eint] : ((((mono_2Ec_2Einteger_2Eint__divides @ X1 @ (mono_2Ec_2Einteger_2Eint__neg @ X0))) = $true) | ($false = ((mono_2Ec_2Einteger_2Eint__divides @ X1 @ X0)))) )),
% 0.62/0.43 inference(iff_proxy_clausification,[],[f290])).
% 0.62/0.43 thf(f868,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))) = $true)),
% 0.62/0.43 inference(xor_proxy_clausification,[],[f322])).
% 0.62/0.43 thf(f869,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $false) | ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))))),
% 0.62/0.43 inference(xor_proxy_clausification,[],[f322])).
% 0.62/0.43 thf(f887,definition,(
% 0.62/0.43 spl17_3 <=> (mono_2Ec_2Ebool_2EF = $false)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition])).
% 0.62/0.43 thf(f896,definition,(
% 0.62/0.43 spl17_5 <=> (mono_2Ec_2Ebool_2EF = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_5])],[avatar_definition])).
% 0.62/0.43 thf(f897,plain,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF != $true) | spl17_5),
% 0.62/0.43 inference(avatar_component_clause,[],[f896])).
% 0.62/0.43 thf(f904,plain,(
% 0.62/0.43 ~spl17_5),
% 0.62/0.43 inference(avatar_split_clause,[],[f669,f896])).
% 0.62/0.43 thf(f928,definition,(
% 0.62/0.43 spl17_10 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_10])],[avatar_definition])).
% 0.62/0.43 thf(f931,plain,(
% 0.62/0.43 spl17_10),
% 0.62/0.43 inference(avatar_split_clause,[],[f323,f928])).
% 0.62/0.43 thf(f933,definition,(
% 0.62/0.43 spl17_11 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $false)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_11])],[avatar_definition])).
% 0.62/0.43 thf(f934,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) != $false) | spl17_11),
% 0.62/0.43 inference(avatar_component_clause,[],[f933])).
% 0.62/0.43 thf(f935,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $false) | ~spl17_11),
% 0.62/0.43 inference(avatar_component_clause,[],[f933])).
% 0.62/0.43 thf(f937,definition,(
% 0.62/0.43 spl17_12 <=> ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))))),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_12])],[avatar_definition])).
% 0.62/0.43 thf(f939,plain,(
% 0.62/0.43 ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11)))) | ~spl17_12),
% 0.62/0.43 inference(avatar_component_clause,[],[f937])).
% 0.62/0.43 thf(f940,plain,(
% 0.62/0.43 spl17_11 | spl17_12),
% 0.62/0.43 inference(avatar_split_clause,[],[f869,f937,f933])).
% 0.62/0.43 thf(f942,definition,(
% 0.62/0.43 spl17_13 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_13])],[avatar_definition])).
% 0.62/0.43 thf(f946,definition,(
% 0.62/0.43 spl17_14 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))) = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_14])],[avatar_definition])).
% 0.62/0.43 thf(f948,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__sub @ sK10 @ sK11))) = $true) | ~spl17_14),
% 0.62/0.43 inference(avatar_component_clause,[],[f946])).
% 0.62/0.43 thf(f949,plain,(
% 0.62/0.43 spl17_13 | spl17_14),
% 0.62/0.43 inference(avatar_split_clause,[],[f868,f946,f942])).
% 0.62/0.43 thf(f953,plain,(
% 0.62/0.43 ($true != $true) | (mono_2Ec_2Ebool_2EF = $false) | spl17_5),
% 0.62/0.43 inference(fool_paramodulation,[],[f897])).
% 0.62/0.43 thf(f954,plain,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF = $false) | spl17_5),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f953])).
% 0.62/0.43 thf(f955,plain,(
% 0.62/0.43 spl17_3 | spl17_5),
% 0.62/0.43 inference(avatar_split_clause,[],[f954,f896,f887])).
% 0.62/0.43 thf(f958,definition,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF != $false) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) != $false) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) != $true) | (mono_2Ec_2Ebool_2EF = $true)),
% 0.62/0.43 introduced(theory,[theory_tautology_sat_conflict])).
% 0.62/0.43 thf(f965,plain,(
% 0.62/0.43 ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))))) | ~spl17_12),
% 0.62/0.43 inference(superposition,[],[f939,f445])).
% 0.62/0.43 thf(f967,definition,(
% 0.62/0.43 spl17_15 <=> ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11)))))),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_15])],[avatar_definition])).
% 0.62/0.43 thf(f969,plain,(
% 0.62/0.43 ($false = ((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))))) | ~spl17_15),
% 0.62/0.43 inference(avatar_component_clause,[],[f967])).
% 0.62/0.43 thf(f970,plain,(
% 0.62/0.43 spl17_15 | ~spl17_12),
% 0.62/0.43 inference(avatar_split_clause,[],[f965,f937,f967])).
% 0.62/0.43 thf(f1167,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | ($false = $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $false) | ~spl17_15),
% 0.62/0.43 inference(superposition,[],[f969,f654])).
% 0.62/0.43 thf(f1171,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $false) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | ~spl17_15),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f1167])).
% 0.62/0.43 thf(f1176,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | (spl17_11 | ~spl17_15)),
% 0.62/0.43 inference(forward_subsumption_resolution,[],[f1171,f934])).
% 0.62/0.43 thf(f1179,definition,(
% 0.62/0.43 spl17_20 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_20])],[avatar_definition])).
% 0.62/0.43 thf(f1181,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | spl17_20),
% 0.62/0.43 inference(avatar_component_clause,[],[f1179])).
% 0.62/0.43 thf(f1182,plain,(
% 0.62/0.43 ~spl17_20 | spl17_11 | ~spl17_15),
% 0.62/0.43 inference(avatar_split_clause,[],[f1176,f967,f933,f1179])).
% 0.62/0.43 thf(f1483,plain,(
% 0.62/0.43 ($true != $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $false) | spl17_20),
% 0.62/0.43 inference(superposition,[],[f1181,f671])).
% 0.62/0.43 thf(f1484,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $false) | spl17_20),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f1483])).
% 0.62/0.43 thf(f1486,definition,(
% 0.62/0.43 spl17_33 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) = $false)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_33])],[avatar_definition])).
% 0.62/0.43 thf(f1489,plain,(
% 0.62/0.43 spl17_33 | spl17_20),
% 0.62/0.43 inference(avatar_split_clause,[],[f1484,f1179,f1486])).
% 0.62/0.43 thf(f1490,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11)))) = $true) | ~spl17_14),
% 0.62/0.43 inference(forward_demodulation,[],[f948,f445])).
% 0.62/0.43 thf(f1493,definition,(
% 0.62/0.43 spl17_34 <=> (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11)))) = $true)),
% 0.62/0.43 introduced(definition,[new_symbols(definition,[spl17_34])],[avatar_definition])).
% 0.62/0.43 thf(f1495,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__add @ sK10 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11)))) = $true) | ~spl17_34),
% 0.62/0.43 inference(avatar_component_clause,[],[f1493])).
% 0.62/0.43 thf(f1496,plain,(
% 0.62/0.43 spl17_34 | ~spl17_14),
% 0.62/0.43 inference(avatar_split_clause,[],[f1490,f946,f1493])).
% 0.62/0.43 thf(f1499,plain,(
% 0.62/0.43 ($false = $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | ~spl17_34),
% 0.62/0.43 inference(superposition,[],[f1495,f653])).
% 0.62/0.43 thf(f1501,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK10)) = $true) | ~spl17_34),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f1499])).
% 0.62/0.43 thf(f1503,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | ($false = $true) | (~spl17_11 | ~spl17_34)),
% 0.62/0.43 inference(forward_demodulation,[],[f1501,f935])).
% 0.62/0.43 thf(f1504,plain,(
% 0.62/0.43 (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ (mono_2Ec_2Einteger_2Eint__neg @ sK11))) != $true) | (~spl17_11 | ~spl17_34)),
% 0.62/0.43 inference(trivial_inequality_removal,[],[f1503])).
% 0.62/0.43 thf(f1507,plain,(
% 0.62/0.43 ~spl17_20 | ~spl17_11 | ~spl17_34),
% 0.62/0.43 inference(avatar_split_clause,[],[f1504,f1493,f933,f1179])).
% 0.62/0.43 thf(f1509,definition,(
% 0.62/0.43 (mono_2Ec_2Ebool_2EF != $false) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) != $false) | (((mono_2Ec_2Einteger_2Eint__divides @ sK9 @ sK11)) != $true) | (mono_2Ec_2Ebool_2EF = $true)),
% 0.62/0.43 introduced(theory,[theory_tautology_sat_conflict])).
% 0.62/0.43 cnf(s7, plain, ~spl17_5, inference(sat_conversion,[],[f904])).
% 0.62/0.43 cnf(s23, plain, spl17_10, inference(sat_conversion,[],[f931])).
% 0.62/0.43 cnf(s25, plain, spl17_11 | spl17_12, inference(sat_conversion,[],[f940])).
% 0.62/0.43 cnf(s26, plain, spl17_13 | spl17_14, inference(sat_conversion,[],[f949])).
% 0.62/0.43 cnf(s30, plain, spl17_3 | spl17_5, inference(sat_conversion,[],[f955])).
% 0.62/0.43 cnf(s33, plain, ~spl17_3 | spl17_5 | ~spl17_11 | ~spl17_13, inference(sat_conversion,[],[f958])).
% 0.62/0.43 cnf(s34, plain, ~spl17_12 | spl17_15, inference(sat_conversion,[],[f970])).
% 0.62/0.43 cnf(s37, plain, spl17_11 | ~spl17_15 | ~spl17_20, inference(sat_conversion,[],[f1182])).
% 0.62/0.43 cnf(s48, plain, spl17_20 | spl17_33, inference(sat_conversion,[],[f1489])).
% 0.62/0.43 cnf(s49, plain, ~spl17_14 | spl17_34, inference(sat_conversion,[],[f1496])).
% 0.62/0.43 cnf(s51, plain, ~spl17_11 | ~spl17_20 | ~spl17_34, inference(sat_conversion,[],[f1507])).
% 0.62/0.43 cnf(s54, plain, ~spl17_3 | spl17_5 | ~spl17_10 | ~spl17_33, inference(sat_conversion,[],[f1509])).
% 0.62/0.43 cnf(s55, plain, spl17_3, inference(rat,[],[s30,s7])).
% 0.62/0.43 cnf(s57, plain, ~spl17_33, inference(rat,[],[s54,s7,s23,s55])).
% 0.62/0.43 cnf(s59, plain, spl17_20, inference(rat,[],[s48,s57])).
% 0.62/0.43 cnf(s60, plain, spl17_11, inference(rat,[],[s34,s25,s37,s59])).
% 0.62/0.43 cnf(s61, plain, ~spl17_34, inference(rat,[],[s51,s59,s60])).
% 0.62/0.43 cnf(s62, plain, ~spl17_13, inference(rat,[],[s33,s55,s7,s60])).
% 0.62/0.43 cnf(s63, plain, ~spl17_14, inference(rat,[],[s49,s61])).
% 0.62/0.43 cnf(s64, plain, $false, inference(rat,[],[s26,s63,s62])).
% 0.62/0.43 thf(f1510,plain,(
% 0.62/0.43 $false),
% 0.62/0.43 inference(avatar_sat_refutation,[],[s64])).
% 0.62/0.43 % SZS output end Proof for theBenchmark
% 0.62/0.43 % (3100161)------------------------------
% 0.62/0.43 % (3100161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.43 % (3100161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.43 % (3100161)CaDiCaL version: 2.1.3
% 0.62/0.43 % (3100161)Termination reason: Refutation
% 0.62/0.43 % (3100161)Time elapsed: 0.100 s
% 0.62/0.43 % (3100161)Peak memory usage: 14 MB
% 0.62/0.43 % (3100161)Instructions burned: 123 (million)
% 0.62/0.43 % (3100153)Success in time 0.153 s
% 0.62/0.43 % Vampire exiting
%------------------------------------------------------------------------------