%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP006^3 : 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 : n016.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:38 AM UTC 2026
% Result : Theorem 0.62s 0.38s
% Output : Refutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP006^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n016.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:27:41 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.23 Running higher-order theorem proving
% 0.09/0.25 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.38 % (792250)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.62/0.38 % (792259)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3392788221:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.62/0.38 % (792261)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.38 % (792261)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.38 % (792255)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2620995163:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.62/0.38 % (792256)lrs+10_16_si=on:nwc=1.5:random_seed=1732781239:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.62/0.38 % (792257)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3218802727:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.62/0.38 % (792258)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=295309926: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.38 % (792260)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2719227101:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.62/0.38 % (792261)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=3871429450:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.62/0.38 % (792259)Instruction limit reached!
% 0.62/0.38 % (792259)------------------------------
% 0.62/0.38 % (792259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792259)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792259)Termination reason: Instruction limit
% 0.62/0.38 % (792259)Termination phase: Saturation
% 0.62/0.38 % (792259)Time elapsed: 0.008 s
% 0.62/0.38 % (792259)Peak memory usage: 12 MB
% 0.62/0.38 % (792259)Instructions burned: 27 (million)
% 0.62/0.38 % (792257)Instruction limit reached!
% 0.62/0.38 % (792257)------------------------------
% 0.62/0.38 % (792257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792257)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792257)Termination reason: Instruction limit
% 0.62/0.38 % (792257)Termination phase: Preprocessing 3
% 0.62/0.38 % (792257)Time elapsed: 0.002 s
% 0.62/0.38 % (792257)Peak memory usage: 10 MB
% 0.62/0.38 % (792257)Instructions burned: 3 (million)
% 0.62/0.38 % (792256)Instruction limit reached!
% 0.62/0.38 % (792256)------------------------------
% 0.62/0.38 % (792256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792256)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792256)Termination reason: Instruction limit
% 0.62/0.38 % (792256)Termination phase: Saturation
% 0.62/0.38 % (792256)Time elapsed: 0.010 s
% 0.62/0.38 % (792256)Peak memory usage: 11 MB
% 0.62/0.38 % (792256)Instructions burned: 18 (million)
% 0.62/0.38 % (792269)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2561146205:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.62/0.38 % (792269)Instruction limit reached!
% 0.62/0.38 % (792269)------------------------------
% 0.62/0.38 % (792269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792269)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792269)Termination reason: Instruction limit
% 0.62/0.38 % (792269)Termination phase: Property scanning
% 0.62/0.38 % (792269)Time elapsed: 0.003 s
% 0.62/0.38 % (792269)Peak memory usage: 11 MB
% 0.62/0.38 % (792269)Instructions burned: 11 (million)
% 0.62/0.38 % (792270)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2832657455:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.62/0.38 % (792270)Instruction limit reached!
% 0.62/0.38 % (792270)------------------------------
% 0.62/0.38 % (792270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792270)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792270)Termination reason: Instruction limit
% 0.62/0.38 % (792270)Termination phase: Preprocessing 3
% 0.62/0.38 % (792270)Time elapsed: 0.003 s
% 0.62/0.38 % (792270)Peak memory usage: 10 MB
% 0.62/0.38 % (792270)Instructions burned: 5 (million)
% 0.62/0.38 % (792271)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.38 % (792273)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1667181392:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.62/0.38 % (792271)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3610399484: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.38 % (792273)Instruction limit reached!
% 0.62/0.38 % (792273)------------------------------
% 0.62/0.38 % (792273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792273)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792273)Termination reason: Instruction limit
% 0.62/0.38 % (792273)Termination phase: Property scanning
% 0.62/0.38 % (792273)Time elapsed: 0.003 s
% 0.62/0.38 % (792273)Peak memory usage: 11 MB
% 0.62/0.38 % (792273)Instructions burned: 13 (million)
% 0.62/0.38 % (792271)Instruction limit reached!
% 0.62/0.38 % (792271)------------------------------
% 0.62/0.38 % (792271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792271)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792271)Termination reason: Instruction limit
% 0.62/0.38 % (792271)Termination phase: Function definition elimination
% 0.62/0.38 % (792271)Time elapsed: 0.005 s
% 0.62/0.38 % (792271)Peak memory usage: 10 MB
% 0.62/0.38 % (792271)Instructions burned: 10 (million)
% 0.62/0.38 % (792275)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.38 % (792275)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.38 % (792260)Instruction limit reached!
% 0.62/0.38 % (792260)------------------------------
% 0.62/0.38 % (792260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792260)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792260)Termination reason: Instruction limit
% 0.62/0.38 % (792260)Termination phase: Saturation
% 0.62/0.38 % (792260)Time elapsed: 0.043 s
% 0.62/0.38 % (792260)Peak memory usage: 13 MB
% 0.62/0.38 % (792260)Instructions burned: 77 (million)
% 0.62/0.38 % (792275)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2627126325: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.38 % (792279)lrs+10_1_si=on:cs=on:random_seed=1979091069:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.62/0.38 % (792279)Instruction limit reached!
% 0.62/0.38 % (792279)------------------------------
% 0.62/0.38 % (792279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792279)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792279)Termination reason: Instruction limit
% 0.62/0.38 % (792279)Termination phase: Property scanning
% 0.62/0.38 % (792279)Time elapsed: 0.003 s
% 0.62/0.38 % (792279)Peak memory usage: 10 MB
% 0.62/0.38 % (792279)Instructions burned: 11 (million)
% 0.62/0.38 % (792255)Instruction limit reached!
% 0.62/0.38 % (792255)------------------------------
% 0.62/0.38 % (792255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792255)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792255)Termination reason: Instruction limit
% 0.62/0.38 % (792255)Termination phase: Saturation
% 0.62/0.38 % (792255)Time elapsed: 0.049 s
% 0.62/0.38 % (792255)Peak memory usage: 13 MB
% 0.62/0.38 % (792255)Instructions burned: 87 (million)
% 0.62/0.38 % (792275)Instruction limit reached!
% 0.62/0.38 % (792275)------------------------------
% 0.62/0.38 % (792275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792275)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792275)Termination reason: Instruction limit
% 0.62/0.38 % (792275)Termination phase: Saturation
% 0.62/0.38 % (792275)Time elapsed: 0.013 s
% 0.62/0.38 % (792275)Peak memory usage: 12 MB
% 0.62/0.38 % (792275)Instructions burned: 28 (million)
% 0.62/0.38 % (792280)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.62/0.38 % (792284)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2376651097:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.62/0.38 % (792280)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=2694190680:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.62/0.38 % (792258)Refutation not found, incomplete strategy
% 0.62/0.38 % (792258)------------------------------
% 0.62/0.38 % (792258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792258)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792258)Termination reason: Refutation not found, incomplete strategy
% 0.62/0.38 % (792258)Time elapsed: 0.063 s
% 0.62/0.38 % (792258)Peak memory usage: 13 MB
% 0.62/0.38 % (792258)Instructions burned: 105 (million)
% 0.62/0.38 % (792258)------------------------------
% 0.62/0.38 % (792258)------------------------------
% 0.62/0.38 % (792278)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=3244597846:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.62/0.38 % (792280)Instruction limit reached!
% 0.62/0.38 % (792280)------------------------------
% 0.62/0.38 % (792280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792280)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792280)Termination reason: Instruction limit
% 0.62/0.38 % (792280)Termination phase: Property scanning
% 0.62/0.38 % (792280)Time elapsed: 0.002 s
% 0.62/0.38 % (792280)Peak memory usage: 10 MB
% 0.62/0.38 % (792280)Instructions burned: 4 (million)
% 0.62/0.38 % (792283)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1336052845:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.62/0.38 % (792283)Refutation not found, incomplete strategy
% 0.62/0.38 % (792283)------------------------------
% 0.62/0.38 % (792283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792283)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792283)Termination reason: Refutation not found, incomplete strategy
% 0.62/0.38 % (792283)Time elapsed: 0.002 s
% 0.62/0.38 % (792283)Peak memory usage: 12 MB
% 0.62/0.38 % (792283)Instructions burned: 3 (million)
% 0.62/0.38 % (792283)------------------------------
% 0.62/0.38 % (792283)------------------------------
% 0.62/0.38 % (792284) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-792250-792284"...
% 0.62/0.38 % (792285)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2104846123:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.62/0.38 % (792284)...printing done.
% 0.62/0.38 % (792284)Refutation found. Thanks to Tanya!
% 0.62/0.38 % SZS status Theorem for theBenchmark
% 0.62/0.38 % SZS output start Proof for theBenchmark
% 0.62/0.38 thf(type_def_5, type, tyop_2Emin_2Ebool: $tType).
% 0.62/0.38 thf(type_def_6, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 0.62/0.38 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 0.62/0.38 thf(type_def_8, type, sK8: $tType).
% 0.62/0.38 thf(type_def_9, type, sK9: $tType).
% 0.62/0.38 thf(func_def_0, type, c_2Ebool_2E_21: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.62/0.38 thf(func_def_1, type, c_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 0.62/0.38 thf(func_def_2, type, c_2Emin_2E_3D: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.62/0.38 thf(func_def_3, type, c_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 0.62/0.38 thf(func_def_4, type, c_2Ebool_2E_3F: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.62/0.38 thf(func_def_5, type, c_2Ebool_2EF: $o).
% 0.62/0.38 thf(func_def_6, type, c_2EquantHeuristics_2EGUESS__EXISTS: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_7, type, c_2EquantHeuristics_2EGUESS__EXISTS__GAP: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_8, type, c_2EquantHeuristics_2EGUESS__EXISTS__POINT: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_9, type, c_2EquantHeuristics_2EGUESS__FORALL: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_10, type, c_2EquantHeuristics_2EGUESS__FORALL__GAP: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_11, type, c_2EquantHeuristics_2EGUESS__FORALL__POINT: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X1 > $o) > $o))).
% 0.62/0.38 thf(func_def_12, type, c_2Ebool_2ET: $o).
% 0.62/0.38 thf(func_def_13, type, c_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 0.62/0.38 thf(func_def_14, type, c_2Ebool_2E_7E: ($o > $o)).
% 0.62/0.38 thf(func_def_16, type, vNOT: ($o > $o)).
% 0.62/0.38 thf(func_def_19, type, vOR: ($o > $o > $o)).
% 0.62/0.38 thf(func_def_20, type, vIMP: ($o > $o > $o)).
% 0.62/0.38 thf(func_def_21, type, sP0: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_22, type, sP1: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_23, type, sP2: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_24, type, sP3: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_25, type, sP4: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_26, type, sP5: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_27, type, sP6: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_28, type, sP7: ($o > $o > $o > $o)).
% 0.62/0.38 thf(func_def_29, type, sK10: (sK9 > sK8)).
% 0.62/0.38 thf(func_def_30, type, sK11: (sK8 > $o)).
% 0.62/0.38 thf(func_def_31, type, sK12: (sK8 > $o)).
% 0.62/0.38 thf(func_def_32, type, sK13: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X1 > X0) > X1))).
% 0.62/0.38 thf(func_def_33, type, sK14: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > X1))).
% 0.62/0.38 thf(func_def_34, type, sK15: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > X0))).
% 0.62/0.38 thf(func_def_35, type, sK16: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > X1))).
% 0.62/0.38 thf(func_def_36, type, sK17: !>[X0: $tType, X1: $tType]:((X0 > (X1 > X0) > X1))).
% 0.62/0.38 thf(func_def_37, type, sK18: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X1 > X0) > X0))).
% 0.62/0.38 thf(func_def_38, type, sK19: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > X0))).
% 0.62/0.38 thf(func_def_39, type, sK20: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X0 > $o) > X1))).
% 0.62/0.38 thf(func_def_40, type, sK21: !>[X0: $tType, X1: $tType]:((X0 > (X1 > X0) > X1))).
% 0.62/0.38 thf(func_def_41, type, sK22: !>[X0: $tType, X1: $tType]:(((X0 > $o) > (X1 > X0) > X0))).
% 0.62/0.38 thf(f15,axiom,(
% 0.62/0.38 ! [X0 : $tType,X1 : $tType,X2 : (X0 > X1),X3 : (X1 > $o)] : (! [X8 : (X0 > X1),X9 : (X1 > $o)] : ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X8 @ X9) <=> ! [X10 : X0] : (X9 @ (X8 @ X10))) & ! [X11 : (X0 > X1),X12 : (X1 > $o)] : ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X11 @ X12) <=> ! [X13 : X0] : (~ (X12 @ (X11 @ X13)))) & ! [X15 : (X1 > $o),X14 : (X0 > X1)] : ((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X14 @ X15) <=> ! [X16 : X1] : ((X15 @ X16) => ? [X17 : X0] : (X16 = ((X14 @ X17))))) & ! [X19 : (X1 > $o),X18 : (X0 > X1)] : (! [X20 : X1] : ((~ (X19 @ X20)) => ? [X21 : X0] : (X20 = ((X18 @ X21)))) <=> (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X18 @ X19)) & (! [X4 : X1] : ((X3 @ X4) => ? [X5 : X0] : (X3 @ (X2 @ X5))) <=> (c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) & (! [X6 : X1] : ((~ (X3 @ X6)) => ? [X7 : X0] : (~ (X3 @ (X2 @ X7)))) <=> (c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)))),
% 0.62/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__REWRITES)).
% 0.62/0.38 thf(f27,conjecture,(
% 0.62/0.38 ! [X1 : $tType,X0 : $tType,X3 : (X0 > $o),X4 : (X0 > $o),X2 : (X1 > X0)] : (! [X5 : X0] : ((X4 @ X5) => (X3 @ X5)) => ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X3) => (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X4)))),
% 0.62/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT)).
% 0.62/0.38 thf(f28,negated_conjecture,(
% 0.62/0.38 ~ ! [X1 : $tType,X0 : $tType,X3 : (X0 > $o),X4 : (X0 > $o),X2 : (X1 > X0)] : (! [X5 : X0] : ((X4 @ X5) => (X3 @ X5)) => ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X3) => (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X4)))),
% 0.62/0.38 inference(negated_conjecture,[status(cth)],[f27])).
% 0.62/0.38 thf(f47,plain,(
% 0.62/0.38 ! [X0 : $tType,X1 : $tType,X2 : (X0 > X1),X3 : (X1 > $o)] : (! [X4 : (X0 > X1),X5 : (X1 > $o)] : ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5) <=> ! [X6 : X0] : (X5 @ (X4 @ X6))) & ! [X7 : (X0 > X1),X8 : (X1 > $o)] : ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8) <=> ! [X9 : X0] : (~ (X8 @ (X7 @ X9)))) & ! [X10 : (X1 > $o),X11 : (X0 > X1)] : ((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10) <=> ! [X12 : X1] : ((X10 @ X12) => ? [X13 : X0] : (((X11 @ X13)) = X12))) & ! [X14 : (X1 > $o),X15 : (X0 > X1)] : (! [X16 : X1] : ((~ (X14 @ X16)) => ? [X17 : X0] : (((X15 @ X17)) = X16)) <=> (c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) & (! [X18 : X1] : ((X3 @ X18) => ? [X19 : X0] : (X3 @ (X2 @ X19))) <=> (c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) & (! [X20 : X1] : ((~ (X3 @ X20)) => ? [X21 : X0] : (~ (X3 @ (X2 @ X21)))) <=> (c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)))),
% 0.62/0.38 inference(rectify,[],[f15])).
% 0.62/0.38 thf(f48,plain,(
% 0.62/0.38 ! [X0 : $tType,X1 : $tType,X3 : (X1 > $o),X2 : (X0 > X1)] : (! [X11 : (X0 > X1),X10 : (X1 > $o)] : ((((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) = $true) <=> ! [X12 : X1] : (($true = ((X10 @ X12))) => ? [X13 : X0] : (((X11 @ X13)) = X12))) & (! [X20 : X1] : ((((~ (X3 @ X20))) = $true) => ? [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) = $true)) <=> (((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) = $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) = $true) <=> ! [X18 : X1] : ((((X3 @ X18)) = $true) => ? [X19 : X0] : ($true = ((X3 @ (X2 @ X19)))))) & ! [X4 : (X0 > X1),X5 : (X1 > $o)] : ((((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) = $true) <=> ! [X6 : X0] : (((X5 @ (X4 @ X6))) = $true)) & ! [X15 : (X0 > X1),X14 : (X1 > $o)] : (! [X16 : X1] : ((((~ (X14 @ X16))) = $true) => ? [X17 : X0] : (((X15 @ X17)) = X16)) <=> (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) = $true)) & ! [X8 : (X1 > $o),X7 : (X0 > X1)] : (! [X9 : X0] : ($true = ((~ (X8 @ (X7 @ X9))))) <=> (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) = $true)))),
% 0.62/0.38 inference(fool_elimination,[],[f47])).
% 0.62/0.38 thf(f73,plain,(
% 0.62/0.38 ~ ! [X0 : $tType,X1 : $tType,X2 : (X1 > $o),X3 : (X1 > $o),X4 : (X0 > X1)] : (! [X5 : X1] : ((X3 @ X5) => (X2 @ X5)) => ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X2) => (c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X3)))),
% 0.62/0.38 inference(rectify,[],[f28])).
% 0.62/0.38 thf(f74,plain,(
% 0.62/0.38 ~ ! [X1 : $tType,X0 : $tType,X4 : (X0 > X1),X2 : (X1 > $o),X3 : (X1 > $o)] : (! [X5 : X1] : (($true = ((X3 @ X5))) => (((X2 @ X5)) = $true)) => ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X2)) = $true) => ($true = ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X3)))))),
% 0.62/0.38 inference(fool_elimination,[],[f73])).
% 0.62/0.38 thf(f82,plain,(
% 0.62/0.38 ? [X1 : $tType,X0 : $tType,X4 : (X0 > X1),X2 : (X1 > $o),X3 : (X1 > $o)] : ((($true != ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X3))) & (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X2)) = $true)) & ! [X5 : X1] : ((((X2 @ X5)) = $true) | ($true != ((X3 @ X5)))))),
% 0.62/0.38 inference(ennf_transformation,[],[f74])).
% 0.62/0.38 thf(f83,plain,(
% 0.62/0.38 ? [X1 : $tType,X0 : $tType,X4 : (X0 > X1),X2 : (X1 > $o),X3 : (X1 > $o)] : ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X2)) = $true) & ($true != ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X4 @ X3))) & ! [X5 : X1] : ((((X2 @ X5)) = $true) | ($true != ((X3 @ X5)))))),
% 0.62/0.38 inference(flattening,[],[f82])).
% 0.62/0.38 thf(f85,plain,(
% 0.62/0.38 ! [X1 : $tType,X0 : $tType,X3 : (X1 > $o),X2 : (X0 > X1)] : (! [X4 : (X0 > X1),X5 : (X1 > $o)] : ((((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) = $true) <=> ! [X6 : X0] : (((X5 @ (X4 @ X6))) = $true)) & (! [X18 : X1] : (? [X19 : X0] : ($true = ((X3 @ (X2 @ X19)))) | (((X3 @ X18)) != $true)) <=> (((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) = $true)) & ! [X8 : (X1 > $o),X7 : (X0 > X1)] : (! [X9 : X0] : ($true = ((~ (X8 @ (X7 @ X9))))) <=> (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) = $true)) & ! [X11 : (X0 > X1),X10 : (X1 > $o)] : (! [X12 : X1] : (? [X13 : X0] : (((X11 @ X13)) = X12) | ($true != ((X10 @ X12)))) <=> (((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) = $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) = $true) <=> ! [X20 : X1] : (? [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) = $true) | (((~ (X3 @ X20))) != $true))) & ! [X15 : (X0 > X1),X14 : (X1 > $o)] : (! [X16 : X1] : ((((~ (X14 @ X16))) != $true) | ? [X17 : X0] : (((X15 @ X17)) = X16)) <=> (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) = $true)))),
% 0.62/0.38 inference(ennf_transformation,[],[f48])).
% 0.62/0.38 thf(f135,plain,(
% 0.62/0.38 ? [X0 : $tType,X1 : $tType,X2 : (X1 > X0),X3 : (X0 > $o),X4 : (X0 > $o)] : ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X3)) = $true) & (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X2 @ X4)) != $true) & ! [X5 : X0] : ((((X3 @ X5)) = $true) | (((X4 @ X5)) != $true)))),
% 0.62/0.38 inference(rectify,[],[f83])).
% 0.62/0.38 thf(f136,plain,(
% 0.62/0.38 ($true = ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK11))) & (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK12)) != $true) & ! [X5 : sK8] : (($true = ((sK11 @ X5))) | ($true != ((sK12 @ X5))))),
% 0.62/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK8),skolemize(X1,sK9),skolemize(X2,sK10),skolemize(X3,sK11),skolemize(X4,sK12)],[f135])).
% 0.62/0.38 thf(f137,plain,(
% 0.62/0.38 ! [X1 : $tType,X0 : $tType,X3 : (X1 > $o),X2 : (X0 > X1)] : (! [X4 : (X0 > X1),X5 : (X1 > $o)] : (((((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) = $true) | ? [X6 : X0] : (((X5 @ (X4 @ X6))) != $true)) & (! [X6 : X0] : (((X5 @ (X4 @ X6))) = $true) | (((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) != $true))) & ((! [X18 : X1] : (? [X19 : X0] : ($true = ((X3 @ (X2 @ X19)))) | (((X3 @ X18)) != $true)) | (((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) = $true) | ? [X18 : X1] : (! [X19 : X0] : ($true != ((X3 @ (X2 @ X19)))) & (((X3 @ X18)) = $true)))) & ! [X8 : (X1 > $o),X7 : (X0 > X1)] : ((! [X9 : X0] : ($true = ((~ (X8 @ (X7 @ X9))))) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) = $true) | ? [X9 : X0] : ($true != ((~ (X8 @ (X7 @ X9))))))) & ! [X11 : (X0 > X1),X10 : (X1 > $o)] : ((! [X12 : X1] : (? [X13 : X0] : (((X11 @ X13)) = X12) | ($true != ((X10 @ X12)))) | (((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) = $true) | ? [X12 : X1] : (! [X13 : X0] : (((X11 @ X13)) != X12) & ($true = ((X10 @ X12)))))) & (((((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) = $true) | ? [X20 : X1] : (! [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) != $true) & (((~ (X3 @ X20))) = $true))) & (! [X20 : X1] : (? [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) = $true) | (((~ (X3 @ X20))) != $true)) | (((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) != $true))) & ! [X15 : (X0 > X1),X14 : (X1 > $o)] : ((! [X16 : X1] : ((((~ (X14 @ X16))) != $true) | ? [X17 : X0] : (((X15 @ X17)) = X16)) | (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) = $true) | ? [X16 : X1] : ((((~ (X14 @ X16))) = $true) & ! [X17 : X0] : (((X15 @ X17)) != X16)))))),
% 0.62/0.38 inference(nnf_transformation,[],[f85])).
% 0.62/0.38 thf(f138,plain,(
% 0.62/0.38 ! [X1 : $tType,X0 : $tType,X3 : (X1 > $o),X2 : (X0 > X1)] : (! [X4 : (X0 > X1),X5 : (X1 > $o)] : (((((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) = $true) | ? [X6 : X0] : (((X5 @ (X4 @ X6))) != $true)) & (! [X6 : X0] : (((X5 @ (X4 @ X6))) = $true) | (((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X0 @ X1 @ X4 @ X5)) != $true))) & (! [X18 : X1] : (? [X19 : X0] : ($true = ((X3 @ (X2 @ X19)))) | (((X3 @ X18)) != $true)) | (((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS @ X0 @ X1 @ X2 @ X3)) = $true) | ? [X18 : X1] : (! [X19 : X0] : ($true != ((X3 @ (X2 @ X19)))) & (((X3 @ X18)) = $true))) & ! [X8 : (X1 > $o),X7 : (X0 > X1)] : ((! [X9 : X0] : ($true = ((~ (X8 @ (X7 @ X9))))) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X0 @ X1 @ X7 @ X8)) = $true) | ? [X9 : X0] : ($true != ((~ (X8 @ (X7 @ X9))))))) & ! [X11 : (X0 > X1),X10 : (X1 > $o)] : ((! [X12 : X1] : (? [X13 : X0] : (((X11 @ X13)) = X12) | ($true != ((X10 @ X12)))) | (((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X0 @ X1 @ X11 @ X10)) = $true) | ? [X12 : X1] : (! [X13 : X0] : (((X11 @ X13)) != X12) & ($true = ((X10 @ X12)))))) & ((((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) = $true) | ? [X20 : X1] : (! [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) != $true) & (((~ (X3 @ X20))) = $true))) & (! [X20 : X1] : (? [X21 : X0] : (((~ (X3 @ (X2 @ X21)))) = $true) | (((~ (X3 @ X20))) != $true)) | (((c_2EquantHeuristics_2EGUESS__FORALL @ X0 @ X1 @ X2 @ X3)) != $true)) & ! [X15 : (X0 > X1),X14 : (X1 > $o)] : ((! [X16 : X1] : ((((~ (X14 @ X16))) != $true) | ? [X17 : X0] : (((X15 @ X17)) = X16)) | (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X0 @ X1 @ X15 @ X14)) = $true) | ? [X16 : X1] : ((((~ (X14 @ X16))) = $true) & ! [X17 : X0] : (((X15 @ X17)) != X16)))))),
% 0.62/0.38 inference(flattening,[],[f137])).
% 0.62/0.38 thf(f139,plain,(
% 0.62/0.38 ! [X0 : $tType,X1 : $tType,X2 : (X0 > $o),X3 : (X1 > X0)] : (! [X4 : (X1 > X0),X5 : (X0 > $o)] : ((($true = ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X1 @ X0 @ X4 @ X5))) | ? [X6 : X1] : ($true != ((X5 @ (X4 @ X6))))) & (! [X7 : X1] : (((X5 @ (X4 @ X7))) = $true) | ($true != ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X1 @ X0 @ X4 @ X5))))) & (! [X8 : X0] : (? [X9 : X1] : ($true = ((X2 @ (X3 @ X9)))) | (((X2 @ X8)) != $true)) | (((c_2EquantHeuristics_2EGUESS__EXISTS @ X1 @ X0 @ X3 @ X2)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS @ X1 @ X0 @ X3 @ X2)) = $true) | ? [X10 : X0] : (! [X11 : X1] : (((X2 @ (X3 @ X11))) != $true) & (((X2 @ X10)) = $true))) & ! [X12 : (X0 > $o),X13 : (X1 > X0)] : ((! [X14 : X1] : (((~ (X12 @ (X13 @ X14)))) = $true) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) = $true) | ? [X15 : X1] : (((~ (X12 @ (X13 @ X15)))) != $true))) & ! [X16 : (X1 > X0),X17 : (X0 > $o)] : ((! [X18 : X0] : (? [X19 : X1] : (((X16 @ X19)) = X18) | ($true != ((X17 @ X18)))) | (((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X1 @ X0 @ X16 @ X17)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X1 @ X0 @ X16 @ X17)) = $true) | ? [X20 : X0] : (! [X21 : X1] : (((X16 @ X21)) != X20) & ($true = ((X17 @ X20)))))) & ((((c_2EquantHeuristics_2EGUESS__FORALL @ X1 @ X0 @ X3 @ X2)) = $true) | ? [X22 : X0] : (! [X23 : X1] : (((~ (X2 @ (X3 @ X23)))) != $true) & (((~ (X2 @ X22))) = $true))) & (! [X24 : X0] : (? [X25 : X1] : (((~ (X2 @ (X3 @ X25)))) = $true) | ($true != ((~ (X2 @ X24))))) | (((c_2EquantHeuristics_2EGUESS__FORALL @ X1 @ X0 @ X3 @ X2)) != $true)) & ! [X26 : (X1 > X0),X27 : (X0 > $o)] : ((! [X28 : X0] : ((((~ (X27 @ X28))) != $true) | ? [X29 : X1] : (((X26 @ X29)) = X28)) | (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X1 @ X0 @ X26 @ X27)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X1 @ X0 @ X26 @ X27)) = $true) | ? [X30 : X0] : (($true = ((~ (X27 @ X30)))) & ! [X31 : X1] : (((X26 @ X31)) != X30)))))),
% 0.62/0.38 inference(rectify,[],[f138])).
% 0.62/0.38 thf(f140,plain,(
% 0.62/0.38 ! [X0 : $tType,X1 : $tType,X2 : (X0 > $o),X3 : (X1 > X0)] : (! [X4 : (X1 > X0),X5 : (X0 > $o)] : ((($true = ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X1 @ X0 @ X4 @ X5))) | (((X5 @ (X4 @ (sK13 @ X0 @ X1 @ X5 @ X4)))) != $true)) & (! [X7 : X1] : (((X5 @ (X4 @ X7))) = $true) | ($true != ((c_2EquantHeuristics_2EGUESS__EXISTS__POINT @ X1 @ X0 @ X4 @ X5))))) & (! [X8 : X0] : ((((X2 @ (X3 @ (sK14 @ X0 @ X1 @ X3 @ X2)))) = $true) | (((X2 @ X8)) != $true)) | (((c_2EquantHeuristics_2EGUESS__EXISTS @ X1 @ X0 @ X3 @ X2)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS @ X1 @ X0 @ X3 @ X2)) = $true) | (! [X11 : X1] : (((X2 @ (X3 @ X11))) != $true) & (((X2 @ (sK15 @ X0 @ X1 @ X3 @ X2))) = $true))) & ! [X12 : (X0 > $o),X13 : (X1 > X0)] : ((! [X14 : X1] : (((~ (X12 @ (X13 @ X14)))) = $true) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) = $true) | ($true != ((~ (X12 @ (X13 @ (sK16 @ X0 @ X1 @ X13 @ X12)))))))) & ! [X16 : (X1 > X0),X17 : (X0 > $o)] : ((! [X18 : X0] : ((((X16 @ (sK17 @ X0 @ X1 @ X18 @ X16))) = X18) | ($true != ((X17 @ X18)))) | (((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X1 @ X0 @ X16 @ X17)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__EXISTS__GAP @ X1 @ X0 @ X16 @ X17)) = $true) | (! [X21 : X1] : (((sK18 @ X0 @ X1 @ X17 @ X16)) != ((X16 @ X21))) & (((X17 @ (sK18 @ X0 @ X1 @ X17 @ X16))) = $true)))) & ((((c_2EquantHeuristics_2EGUESS__FORALL @ X1 @ X0 @ X3 @ X2)) = $true) | (! [X23 : X1] : (((~ (X2 @ (X3 @ X23)))) != $true) & (((~ (X2 @ (sK19 @ X0 @ X1 @ X3 @ X2)))) = $true))) & (! [X24 : X0] : ((((~ (X2 @ (X3 @ (sK20 @ X0 @ X1 @ X3 @ X2))))) = $true) | ($true != ((~ (X2 @ X24))))) | (((c_2EquantHeuristics_2EGUESS__FORALL @ X1 @ X0 @ X3 @ X2)) != $true)) & ! [X26 : (X1 > X0),X27 : (X0 > $o)] : ((! [X28 : X0] : ((((~ (X27 @ X28))) != $true) | (((X26 @ (sK21 @ X0 @ X1 @ X28 @ X26))) = X28)) | (((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X1 @ X0 @ X26 @ X27)) != $true)) & ((((c_2EquantHeuristics_2EGUESS__FORALL__GAP @ X1 @ X0 @ X26 @ X27)) = $true) | ((((~ (X27 @ (sK22 @ X0 @ X1 @ X27 @ X26)))) = $true) & ! [X31 : X1] : (((sK22 @ X0 @ X1 @ X27 @ X26)) != ((X26 @ X31)))))))),
% 0.62/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26),skolemize(X30,sK22 @ X0 @ X1 @ X27 @ X26)],[f139])).
% 0.62/0.38 thf(f217,plain,(
% 0.62/0.38 ( ! [X5 : sK8] : (($true = ((sK11 @ X5))) | ($true != ((sK12 @ X5)))) )),
% 0.62/0.38 inference(cnf_transformation,[],[f136])).
% 0.62/0.38 thf(f218,plain,(
% 0.62/0.38 (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK12)) != $true)),
% 0.62/0.38 inference(cnf_transformation,[],[f136])).
% 0.62/0.38 thf(f219,plain,(
% 0.62/0.38 ($true = ((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK11)))),
% 0.62/0.38 inference(cnf_transformation,[],[f136])).
% 0.62/0.38 thf(f229,plain,(
% 0.62/0.38 ( ! [X1 : $tType,X0 : $tType,X12 : (X0 > $o),X13 : (X1 > X0)] : (($true != ((~ (X12 @ (X13 @ (sK16 @ X0 @ X1 @ X13 @ X12)))))) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) = $true)) )),
% 0.62/0.38 inference(cnf_transformation,[],[f140])).
% 0.62/0.38 thf(f230,plain,(
% 0.62/0.38 ( ! [X1 : $tType,X0 : $tType,X14 : X1,X12 : (X0 > $o),X13 : (X1 > X0)] : ((((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ X1 @ X0 @ X13 @ X12)) != $true) | (((~ (X12 @ (X13 @ X14)))) = $true)) )),
% 0.62/0.38 inference(cnf_transformation,[],[f140])).
% 0.62/0.38 thf(f243,definition,(
% 0.62/0.38 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.62/0.38 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.62/0.38 thf(f401,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : ((((~ (sK11 @ (sK10 @ X0)))) = $true) | ($true != $true)) )),
% 0.62/0.38 inference(superposition,[],[f230,f219])).
% 0.62/0.38 thf(f404,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($true != $true) | ($false = ((sK11 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(not_proxy_clausification,[],[f401])).
% 0.62/0.38 thf(f405,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($false = ((sK11 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(trivial_inequality_removal,[],[f404])).
% 0.62/0.38 thf(f452,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($false = $true) | ($true != ((sK12 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(superposition,[],[f405,f217])).
% 0.62/0.38 thf(f471,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($true != ((sK12 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(trivial_inequality_removal,[],[f452])).
% 0.62/0.38 thf(f613,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($true != $true) | ($false = ((sK12 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(superposition,[],[f471,f243])).
% 0.62/0.38 thf(f617,plain,(
% 0.62/0.38 ( ! [X0 : sK9] : (($false = ((sK12 @ (sK10 @ X0))))) )),
% 0.62/0.38 inference(trivial_inequality_removal,[],[f613])).
% 0.62/0.38 thf(f678,plain,(
% 0.62/0.38 (((~ $false)) != $true) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK12)) = $true)),
% 0.62/0.38 inference(superposition,[],[f229,f617])).
% 0.62/0.38 thf(f687,plain,(
% 0.62/0.38 ($false = $true) | (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK12)) = $true)),
% 0.62/0.38 inference(not_proxy_clausification,[],[f678])).
% 0.62/0.38 thf(f688,plain,(
% 0.62/0.38 (((c_2EquantHeuristics_2EGUESS__FORALL__POINT @ sK9 @ sK8 @ sK10 @ sK12)) = $true)),
% 0.62/0.38 inference(trivial_inequality_removal,[],[f687])).
% 0.62/0.38 thf(f692,plain,(
% 0.62/0.38 $false),
% 0.62/0.38 inference(forward_subsumption_resolution,[],[f688,f218])).
% 0.62/0.38 % SZS output end Proof for theBenchmark
% 0.62/0.38 % (792284)------------------------------
% 0.62/0.38 % (792284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.62/0.38 % (792284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.62/0.38 % (792284)CaDiCaL version: 2.1.3
% 0.62/0.38 % (792284)Termination reason: Refutation
% 0.62/0.38 % (792284)Time elapsed: 0.015 s
% 0.62/0.38 % (792284)Peak memory usage: 13 MB
% 0.62/0.38 % (792284)Instructions burned: 48 (million)
% 0.62/0.38 % (792250)Success in time 0.123 s
% 0.62/0.38 % Vampire exiting
%------------------------------------------------------------------------------