%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP008^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:40 AM UTC 2026
% Result : Theorem 2.86s 0.77s
% Output : Refutation 2.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP008^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.08/0.19 % Computer : n016.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 19:28:35 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running higher-order theorem proving
% 0.08/0.24 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.20/0.36 % (793104)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.20/0.36 % (793110)lrs+10_16_si=on:nwc=1.5:random_seed=286066389:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.20/0.36 % (793115)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.20/0.36 % (793115)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.20/0.36 % (793110)Instruction limit reached!
% 0.20/0.36 % (793110)------------------------------
% 0.20/0.36 % (793110)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (793110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (793110)CaDiCaL version: 2.1.3
% 0.20/0.36 % (793110)Termination reason: Instruction limit
% 0.20/0.36 % (793110)Termination phase: Saturation
% 0.20/0.36 % (793110)Time elapsed: 0.007 s
% 0.20/0.36 % (793110)Peak memory usage: 12 MB
% 0.20/0.36 % (793110)Instructions burned: 21 (million)
% 0.20/0.36 % (793109)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=3698039661:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.20/0.36 % (793111)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3269908753:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.20/0.36 % (793113)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3347899437:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.20/0.36 % (793112)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=2864243861: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.20/0.36 % (793114)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3889814265:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.20/0.36 % (793115)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=2200710042:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.20/0.36 % (793111)Instruction limit reached!
% 0.20/0.36 % (793111)------------------------------
% 0.20/0.36 % (793111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (793111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (793111)CaDiCaL version: 2.1.3
% 0.20/0.36 % (793111)Termination reason: Instruction limit
% 0.20/0.36 % (793111)Termination phase: Saturation
% 0.20/0.36 % (793111)Time elapsed: 0.003 s
% 0.20/0.36 % (793111)Peak memory usage: 12 MB
% 0.20/0.36 % (793111)Instructions burned: 4 (million)
% 0.20/0.36 % (793117)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=840110428:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.36 % (793117)Instruction limit reached!
% 0.20/0.36 % (793117)------------------------------
% 0.20/0.36 % (793117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (793117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (793117)CaDiCaL version: 2.1.3
% 0.20/0.36 % (793117)Termination reason: Instruction limit
% 0.20/0.36 % (793117)Termination phase: Saturation
% 0.20/0.36 % (793117)Time elapsed: 0.001 s
% 0.20/0.36 % (793117)Peak memory usage: 12 MB
% 0.20/0.36 % (793117)Instructions burned: 4 (million)
% 0.20/0.36 % (793113)Instruction limit reached!
% 0.20/0.36 % (793113)------------------------------
% 0.20/0.36 % (793113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (793113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (793113)CaDiCaL version: 2.1.3
% 0.20/0.36 % (793113)Termination reason: Instruction limit
% 0.20/0.36 % (793113)Termination phase: Saturation
% 0.20/0.36 % (793113)Time elapsed: 0.015 s
% 0.20/0.36 % (793113)Peak memory usage: 12 MB
% 0.20/0.36 % (793113)Instructions burned: 24 (million)
% 0.20/0.36 % (793126)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.20/0.36 % (793126)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1373550581:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.85/0.40 % (793124)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3234722188:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.85/0.40 % (793126)Instruction limit reached!
% 0.85/0.40 % (793126)------------------------------
% 0.85/0.40 % (793126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (793126)CaDiCaL version: 2.1.3
% 0.85/0.40 % (793126)Termination reason: Instruction limit
% 0.85/0.40 % (793126)Termination phase: Saturation
% 0.85/0.40 % (793126)Time elapsed: 0.003 s
% 0.85/0.40 % (793126)Peak memory usage: 12 MB
% 0.85/0.40 % (793126)Instructions burned: 11 (million)
% 0.85/0.40 % (793124)Instruction limit reached!
% 0.85/0.40 % (793124)------------------------------
% 0.85/0.40 % (793124)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (793124)CaDiCaL version: 2.1.3
% 0.85/0.40 % (793124)Termination reason: Instruction limit
% 0.85/0.40 % (793124)Termination phase: Saturation
% 0.85/0.40 % (793124)Time elapsed: 0.004 s
% 0.85/0.40 % (793124)Peak memory usage: 12 MB
% 0.85/0.40 % (793124)Instructions burned: 6 (million)
% 0.85/0.40 % (793130)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.85/0.40 % (793130)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.85/0.40 % (793127)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2016891907:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.85/0.40 % (793130)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2010446675: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.85/0.40 % (793127)Instruction limit reached!
% 0.85/0.40 % (793127)------------------------------
% 0.85/0.40 % (793127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (793127)CaDiCaL version: 2.1.3
% 0.85/0.40 % (793127)Termination reason: Instruction limit
% 0.85/0.40 % (793127)Termination phase: Saturation
% 0.85/0.40 % (793127)Time elapsed: 0.009 s
% 0.85/0.40 % (793127)Peak memory usage: 12 MB
% 0.85/0.40 % (793127)Instructions burned: 13 (million)
% 0.85/0.40 % (793130)Instruction limit reached!
% 0.85/0.40 % (793130)------------------------------
% 0.85/0.40 % (793130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (793130)CaDiCaL version: 2.1.3
% 0.85/0.40 % (793130)Termination reason: Instruction limit
% 0.85/0.40 % (793130)Termination phase: Saturation
% 0.85/0.40 % (793130)Time elapsed: 0.008 s
% 0.85/0.40 % (793130)Peak memory usage: 12 MB
% 0.85/0.40 % (793130)Instructions burned: 31 (million)
% 0.85/0.40 % (793131)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=3973794829:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.85/0.40 % (793114)Instruction limit reached!
% 0.85/0.40 % (793114)------------------------------
% 0.85/0.40 % (793114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.40 % (793114)CaDiCaL version: 2.1.3
% 0.85/0.40 % (793114)Termination reason: Instruction limit
% 0.85/0.40 % (793114)Termination phase: Saturation
% 0.85/0.40 % (793114)Time elapsed: 0.045 s
% 0.85/0.40 % (793114)Peak memory usage: 13 MB
% 0.85/0.40 % (793114)Instructions burned: 76 (million)
% 0.85/0.40 % (793109)Instruction limit reached!
% 0.85/0.40 % (793109)------------------------------
% 0.85/0.40 % (793109)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.40 % (793109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793109)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793109)Termination reason: Instruction limit
% 0.85/0.43 % (793109)Termination phase: Saturation
% 0.85/0.43 % (793109)Time elapsed: 0.051 s
% 0.85/0.43 % (793109)Peak memory usage: 12 MB
% 0.85/0.43 % (793109)Instructions burned: 88 (million)
% 0.85/0.43 % (793135)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.85/0.43 % (793131)Refutation not found, incomplete strategy
% 0.85/0.43 % (793131)------------------------------
% 0.85/0.43 % (793131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (793131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793131)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793131)Termination reason: Refutation not found, incomplete strategy
% 0.85/0.43 % (793131)Time elapsed: 0.008 s
% 0.85/0.43 % (793131)Peak memory usage: 12 MB
% 0.85/0.43 % (793131)Instructions burned: 12 (million)
% 0.85/0.43 % (793131)------------------------------
% 0.85/0.43 % (793131)------------------------------
% 0.85/0.43 % (793135)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=2097044324:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.85/0.43 % (793135)Instruction limit reached!
% 0.85/0.43 % (793135)------------------------------
% 0.85/0.43 % (793135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (793135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793135)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793135)Termination reason: Instruction limit
% 0.85/0.43 % (793135)Termination phase: Saturation
% 0.85/0.43 % (793135)Time elapsed: 0.001 s
% 0.85/0.43 % (793135)Peak memory usage: 11 MB
% 0.85/0.43 % (793135)Instructions burned: 3 (million)
% 0.85/0.43 % (793134)lrs+10_1_si=on:cs=on:random_seed=2293966574:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.85/0.43 % (793137)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=2485315050:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.85/0.43 % (793141)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2365447061:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.85/0.43 % (793134)Instruction limit reached!
% 0.85/0.43 % (793134)------------------------------
% 0.85/0.43 % (793134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (793134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793134)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793134)Termination reason: Instruction limit
% 0.85/0.43 % (793134)Termination phase: Saturation
% 0.85/0.43 % (793134)Time elapsed: 0.005 s
% 0.85/0.43 % (793134)Peak memory usage: 12 MB
% 0.85/0.43 % (793134)Instructions burned: 8 (million)
% 0.85/0.43 % (793138)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=4227485704:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.85/0.43 % (793141)Instruction limit reached!
% 0.85/0.43 % (793141)------------------------------
% 0.85/0.43 % (793141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (793141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793141)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793141)Termination reason: Instruction limit
% 0.85/0.43 % (793141)Termination phase: Saturation
% 0.85/0.43 % (793141)Time elapsed: 0.005 s
% 0.85/0.43 % (793141)Peak memory usage: 12 MB
% 0.85/0.43 % (793141)Instructions burned: 15 (million)
% 0.85/0.43 % (793138)Refutation not found, incomplete strategy
% 0.85/0.43 % (793138)------------------------------
% 0.85/0.43 % (793138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.85/0.43 % (793138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.85/0.43 % (793138)CaDiCaL version: 2.1.3
% 0.85/0.43 % (793138)Termination reason: Refutation not found, incomplete strategy
% 0.85/0.43 % (793138)Time elapsed: 0.002 s
% 0.85/0.43 % (793138)Peak memory usage: 12 MB
% 0.85/0.43 % (793138)Instructions burned: 2 (million)
% 0.85/0.43 % (793138)------------------------------
% 0.85/0.43 % (793138)------------------------------
% 0.85/0.43 % (793140)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1159446368:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 1.77/0.53 % (793147)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1599543971:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.77/0.53 % (793137)Instruction limit reached!
% 1.77/0.53 % (793137)------------------------------
% 1.77/0.53 % (793137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793137)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793137)Termination reason: Instruction limit
% 1.77/0.53 % (793137)Termination phase: Saturation
% 1.77/0.53 % (793137)Time elapsed: 0.020 s
% 1.77/0.53 % (793137)Peak memory usage: 12 MB
% 1.77/0.53 % (793137)Instructions burned: 40 (million)
% 1.77/0.53 % (793145)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=277519722:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.77/0.53 % (793147)Instruction limit reached!
% 1.77/0.53 % (793147)------------------------------
% 1.77/0.53 % (793147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793115)Instruction limit reached!
% 1.77/0.53 % (793115)------------------------------
% 1.77/0.53 % (793115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793147)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793115)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793147)Termination reason: Instruction limit
% 1.77/0.53 % (793147)Termination phase: Saturation
% 1.77/0.53 % (793147)Time elapsed: 0.005 s
% 1.77/0.53 % (793115)Termination reason: Instruction limit
% 1.77/0.53 % (793115)Termination phase: Saturation
% 1.77/0.53 % (793147)Peak memory usage: 12 MB
% 1.77/0.53 % (793115)Time elapsed: 0.087 s
% 1.77/0.53 % (793147)Instructions burned: 16 (million)
% 1.77/0.53 % (793115)Peak memory usage: 13 MB
% 1.77/0.53 % (793115)Instructions burned: 157 (million)
% 1.77/0.53 % (793149)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3053165259:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.77/0.53 % (793140)Instruction limit reached!
% 1.77/0.53 % (793140)------------------------------
% 1.77/0.53 % (793140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793140)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793140)Termination reason: Instruction limit
% 1.77/0.53 % (793140)Termination phase: Saturation
% 1.77/0.53 % (793140)Time elapsed: 0.020 s
% 1.77/0.53 % (793140)Peak memory usage: 12 MB
% 1.77/0.53 % (793140)Instructions burned: 25 (million)
% 1.77/0.53 % (793149)Instruction limit reached!
% 1.77/0.53 % (793149)------------------------------
% 1.77/0.53 % (793149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793149)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793149)Termination reason: Instruction limit
% 1.77/0.53 % (793149)Termination phase: Saturation
% 1.77/0.53 % (793149)Time elapsed: 0.002 s
% 1.77/0.53 % (793149)Peak memory usage: 12 MB
% 1.77/0.53 % (793149)Instructions burned: 2 (million)
% 1.77/0.53 % (793153)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2306758315:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.77/0.53 % (793153)Instruction limit reached!
% 1.77/0.53 % (793153)------------------------------
% 1.77/0.53 % (793153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.53 % (793153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.53 % (793153)CaDiCaL version: 2.1.3
% 1.77/0.53 % (793153)Termination reason: Instruction limit
% 1.77/0.53 % (793153)Termination phase: Saturation
% 1.77/0.53 % (793153)Time elapsed: 0.007 s
% 1.77/0.53 % (793153)Peak memory usage: 11 MB
% 1.77/0.53 % (793153)Instructions burned: 24 (million)
% 1.77/0.53 % (793154)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=810831909:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.77/0.53 % (793151)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1177724746:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.77/0.58 % (793157)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.77/0.58 % (793156)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) 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
% 1.77/0.58 % (793156)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.77/0.58 % (793157)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=2551164971:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.77/0.58 % (793156)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3062616570:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.77/0.58 % (793159)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=2210115446:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.77/0.58 % (793157)Instruction limit reached!
% 1.77/0.58 % (793157)------------------------------
% 1.77/0.58 % (793157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.58 % (793157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.58 % (793157)CaDiCaL version: 2.1.3
% 1.77/0.58 % (793157)Termination reason: Instruction limit
% 1.77/0.58 % (793157)Termination phase: Saturation
% 1.77/0.58 % (793157)Time elapsed: 0.006 s
% 1.77/0.58 % (793157)Peak memory usage: 12 MB
% 1.77/0.58 % (793157)Instructions burned: 8 (million)
% 1.77/0.58 % (793156)Instruction limit reached!
% 1.77/0.58 % (793156)------------------------------
% 1.77/0.58 % (793156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.58 % (793156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.58 % (793156)CaDiCaL version: 2.1.3
% 1.77/0.58 % (793156)Termination reason: Instruction limit
% 1.77/0.58 % (793156)Termination phase: Saturation
% 1.77/0.58 % (793156)Time elapsed: 0.009 s
% 1.77/0.58 % (793156)Peak memory usage: 12 MB
% 1.77/0.58 % (793156)Instructions burned: 15 (million)
% 1.77/0.58 % (793151)Instruction limit reached!
% 1.77/0.58 % (793151)------------------------------
% 1.77/0.58 % (793151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.58 % (793151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.58 % (793151)CaDiCaL version: 2.1.3
% 1.77/0.58 % (793151)Termination reason: Instruction limit
% 1.77/0.58 % (793151)Termination phase: Saturation
% 1.77/0.58 % (793151)Time elapsed: 0.016 s
% 1.77/0.58 % (793151)Peak memory usage: 12 MB
% 1.77/0.58 % (793151)Instructions burned: 26 (million)
% 1.77/0.58 % (793159)Instruction limit reached!
% 1.77/0.58 % (793159)------------------------------
% 1.77/0.58 % (793159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.58 % (793159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.77/0.58 % (793159)CaDiCaL version: 2.1.3
% 1.77/0.58 % (793159)Termination reason: Instruction limit
% 1.77/0.58 % (793159)Termination phase: Saturation
% 1.77/0.58 % (793159)Time elapsed: 0.010 s
% 1.77/0.58 % (793159)Peak memory usage: 12 MB
% 1.77/0.58 % (793159)Instructions burned: 34 (million)
% 1.77/0.58 % (793168)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2921784876:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 1.77/0.58 % (793165)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=3609125566:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.77/0.58 % (793166)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=3351218135:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.77/0.58 % (793165)Instruction limit reached!
% 1.77/0.58 % (793165)------------------------------
% 1.77/0.58 % (793165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.77/0.58 % (793165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793165)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793165)Termination reason: Instruction limit
% 2.40/0.64 % (793165)Termination phase: Saturation
% 2.40/0.64 % (793165)Time elapsed: 0.004 s
% 2.40/0.64 % (793165)Peak memory usage: 12 MB
% 2.40/0.64 % (793165)Instructions burned: 7 (million)
% 2.40/0.64 % (793167)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=4293579716:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.40/0.64 % (793154)Instruction limit reached!
% 2.40/0.64 % (793154)------------------------------
% 2.40/0.64 % (793154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (793154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793154)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793154)Termination reason: Instruction limit
% 2.40/0.64 % (793154)Termination phase: Saturation
% 2.40/0.64 % (793154)Time elapsed: 0.038 s
% 2.40/0.64 % (793154)Peak memory usage: 12 MB
% 2.40/0.64 % (793154)Instructions burned: 60 (million)
% 2.40/0.64 % (793166)Instruction limit reached!
% 2.40/0.64 % (793166)------------------------------
% 2.40/0.64 % (793166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (793166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793166)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793166)Termination reason: Instruction limit
% 2.40/0.64 % (793166)Termination phase: Saturation
% 2.40/0.64 % (793166)Time elapsed: 0.014 s
% 2.40/0.64 % (793166)Peak memory usage: 12 MB
% 2.40/0.64 % (793166)Instructions burned: 24 (million)
% 2.40/0.64 % (793167)Instruction limit reached!
% 2.40/0.64 % (793167)------------------------------
% 2.40/0.64 % (793167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (793167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793167)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793167)Termination reason: Instruction limit
% 2.40/0.64 % (793167)Termination phase: Saturation
% 2.40/0.64 % (793167)Time elapsed: 0.013 s
% 2.40/0.64 % (793167)Peak memory usage: 12 MB
% 2.40/0.64 % (793167)Instructions burned: 21 (million)
% 2.40/0.64 % (793173)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=3680478253:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.40/0.64 % (793174)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=52190940:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.40/0.64 % (793176)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.40/0.64 % (793176)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2426494592:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 2.40/0.64 % (793176)Instruction limit reached!
% 2.40/0.64 % (793176)------------------------------
% 2.40/0.64 % (793176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (793176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793176)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793176)Termination reason: Instruction limit
% 2.40/0.64 % (793176)Termination phase: Saturation
% 2.40/0.64 % (793176)Time elapsed: 0.005 s
% 2.40/0.64 % (793176)Peak memory usage: 12 MB
% 2.40/0.64 % (793176)Instructions burned: 8 (million)
% 2.40/0.64 % (793175)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4022665294:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.40/0.64 % (793180)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=3784953242:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.40/0.64 % (793175)Instruction limit reached!
% 2.40/0.64 % (793175)------------------------------
% 2.40/0.64 % (793175)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.40/0.64 % (793175)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.40/0.64 % (793175)CaDiCaL version: 2.1.3
% 2.40/0.64 % (793175)Termination reason: Instruction limit
% 2.40/0.64 % (793175)Termination phase: Saturation
% 2.40/0.64 % (793175)Time elapsed: 0.044 s
% 2.40/0.64 % (793175)Peak memory usage: 12 MB
% 2.40/0.64 % (793175)Instructions burned: 42 (million)
% 2.40/0.64 % (793173)Instruction limit reached!
% 2.40/0.64 % (793173)------------------------------
% 2.40/0.64 % (793173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793173)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793173)Termination reason: Instruction limit
% 2.86/0.74 % (793173)Termination phase: Saturation
% 2.86/0.74 % (793173)Time elapsed: 0.074 s
% 2.86/0.74 % (793173)Peak memory usage: 13 MB
% 2.86/0.74 % (793173)Instructions burned: 145 (million)
% 2.86/0.74 % (793183)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=1136515863:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.86/0.74 % (793184)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.86/0.74 % (793183)Refutation not found, incomplete strategy
% 2.86/0.74 % (793183)------------------------------
% 2.86/0.74 % (793183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793183)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793183)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.74 % (793183)Time elapsed: 0.002 s
% 2.86/0.74 % (793183)Peak memory usage: 12 MB
% 2.86/0.74 % (793183)Instructions burned: 2 (million)
% 2.86/0.74 % (793183)------------------------------
% 2.86/0.74 % (793183)------------------------------
% 2.86/0.74 % (793184)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=218851833:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.86/0.74 % (793184)Instruction limit reached!
% 2.86/0.74 % (793184)------------------------------
% 2.86/0.74 % (793184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793184)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793184)Termination reason: Instruction limit
% 2.86/0.74 % (793184)Termination phase: Saturation
% 2.86/0.74 % (793184)Time elapsed: 0.005 s
% 2.86/0.74 % (793184)Peak memory usage: 12 MB
% 2.86/0.74 % (793184)Instructions burned: 8 (million)
% 2.86/0.74 % (793145)Instruction limit reached!
% 2.86/0.74 % (793145)------------------------------
% 2.86/0.74 % (793145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793145)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793145)Termination reason: Instruction limit
% 2.86/0.74 % (793145)Termination phase: Saturation
% 2.86/0.74 % (793145)Time elapsed: 0.182 s
% 2.86/0.74 % (793145)Peak memory usage: 14 MB
% 2.86/0.74 % (793145)Instructions burned: 329 (million)
% 2.86/0.74 % (793174)Instruction limit reached!
% 2.86/0.74 % (793174)------------------------------
% 2.86/0.74 % (793174)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793174)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793174)Termination reason: Instruction limit
% 2.86/0.74 % (793174)Termination phase: Saturation
% 2.86/0.74 % (793174)Time elapsed: 0.113 s
% 2.86/0.74 % (793174)Peak memory usage: 14 MB
% 2.86/0.74 % (793174)Instructions burned: 194 (million)
% 2.86/0.74 % (793186)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3594592752:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.86/0.74 % (793188)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=40388273:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.86/0.74 % (793188)Refutation not found, incomplete strategy
% 2.86/0.74 % (793188)------------------------------
% 2.86/0.74 % (793188)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.74 % (793188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.74 % (793188)CaDiCaL version: 2.1.3
% 2.86/0.74 % (793188)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.74 % (793188)Time elapsed: 0.003 s
% 2.86/0.74 % (793188)Peak memory usage: 12 MB
% 2.86/0.74 % (793188)Instructions burned: 4 (million)
% 2.86/0.74 % (793188)------------------------------
% 2.86/0.74 % (793188)------------------------------
% 2.86/0.74 % (793189)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3478347321:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 2.86/0.77 % (793190)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=3239636735:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 2.86/0.77 % (793186)Instruction limit reached!
% 2.86/0.77 % (793186)------------------------------
% 2.86/0.77 % (793186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793186)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793186)Termination reason: Instruction limit
% 2.86/0.77 % (793186)Termination phase: Saturation
% 2.86/0.77 % (793186)Time elapsed: 0.019 s
% 2.86/0.77 % (793186)Peak memory usage: 12 MB
% 2.86/0.77 % (793186)Instructions burned: 23 (million)
% 2.86/0.77 % (793180)Instruction limit reached!
% 2.86/0.77 % (793180)------------------------------
% 2.86/0.77 % (793180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793180)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793180)Termination reason: Instruction limit
% 2.86/0.77 % (793180)Termination phase: Saturation
% 2.86/0.77 % (793180)Time elapsed: 0.100 s
% 2.86/0.77 % (793180)Peak memory usage: 14 MB
% 2.86/0.77 % (793180)Instructions burned: 182 (million)
% 2.86/0.77 % (793193)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=827456989:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 2.86/0.77 % (793197)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1284831568:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.86/0.77 % (793196)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3142879135:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.86/0.77 % (793193)Instruction limit reached!
% 2.86/0.77 % (793193)------------------------------
% 2.86/0.77 % (793193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793193)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793193)Termination reason: Instruction limit
% 2.86/0.77 % (793193)Termination phase: Saturation
% 2.86/0.77 % (793193)Time elapsed: 0.029 s
% 2.86/0.77 % (793193)Peak memory usage: 12 MB
% 2.86/0.77 % (793193)Instructions burned: 45 (million)
% 2.86/0.77 % (793197)Instruction limit reached!
% 2.86/0.77 % (793197)------------------------------
% 2.86/0.77 % (793197)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793197)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793197)Termination reason: Instruction limit
% 2.86/0.77 % (793197)Termination phase: Saturation
% 2.86/0.77 % (793197)Time elapsed: 0.015 s
% 2.86/0.77 % (793197)Peak memory usage: 12 MB
% 2.86/0.77 % (793197)Instructions burned: 22 (million)
% 2.86/0.77 % (793196)Refutation not found, incomplete strategy
% 2.86/0.77 % (793196)------------------------------
% 2.86/0.77 % (793196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793196)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793196)Termination reason: Refutation not found, incomplete strategy
% 2.86/0.77 % (793196)Time elapsed: 0.005 s
% 2.86/0.77 % (793196)Peak memory usage: 12 MB
% 2.86/0.77 % (793196)Instructions burned: 3 (million)
% 2.86/0.77 % (793196)------------------------------
% 2.86/0.77 % (793196)------------------------------
% 2.86/0.77 % (793201)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.86/0.77 % (793201)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=997120833:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.86/0.77 % (793202)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3088577670:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 2.86/0.77 % (793203)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1826255039:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 2.86/0.77 % (793202)Instruction limit reached!
% 2.86/0.77 % (793202)------------------------------
% 2.86/0.77 % (793202)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793202)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793202)Termination reason: Instruction limit
% 2.86/0.77 % (793202)Termination phase: Saturation
% 2.86/0.77 % (793202)Time elapsed: 0.008 s
% 2.86/0.77 % (793202)Peak memory usage: 12 MB
% 2.86/0.77 % (793202)Instructions burned: 13 (million)
% 2.86/0.77 % (793207)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=890364964:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 2.86/0.77 % (793112)Instruction limit reached!
% 2.86/0.77 % (793112)------------------------------
% 2.86/0.77 % (793112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793112)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793112)Termination reason: Instruction limit
% 2.86/0.77 % (793112)Termination phase: Saturation
% 2.86/0.77 % (793112)Time elapsed: 0.398 s
% 2.86/0.77 % (793112)Peak memory usage: 16 MB
% 2.86/0.77 % (793112)Instructions burned: 636 (million)
% 2.86/0.77 % (793203)Instruction limit reached!
% 2.86/0.77 % (793203)------------------------------
% 2.86/0.77 % (793203)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793203)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793203)Termination reason: Instruction limit
% 2.86/0.77 % (793203)Termination phase: Saturation
% 2.86/0.77 % (793203)Time elapsed: 0.042 s
% 2.86/0.77 % (793203)Peak memory usage: 13 MB
% 2.86/0.77 % (793203)Instructions burned: 67 (million)
% 2.86/0.77 % (793207)Instruction limit reached!
% 2.86/0.77 % (793207)------------------------------
% 2.86/0.77 % (793207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793207)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793207)Termination reason: Instruction limit
% 2.86/0.77 % (793207)Termination phase: Saturation
% 2.86/0.77 % (793207)Time elapsed: 0.029 s
% 2.86/0.77 % (793207)Peak memory usage: 12 MB
% 2.86/0.77 % (793207)Instructions burned: 52 (million)
% 2.86/0.77 % (793209)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=450438185:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 2.86/0.77 % (793210)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3461575446:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 2.86/0.77 % (793211)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=645783452:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 2.86/0.77 % (793209)Instruction limit reached!
% 2.86/0.77 % (793209)------------------------------
% 2.86/0.77 % (793209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793209)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793209)Termination reason: Instruction limit
% 2.86/0.77 % (793209)Termination phase: Saturation
% 2.86/0.77 % (793209)Time elapsed: 0.019 s
% 2.86/0.77 % (793209)Peak memory usage: 12 MB
% 2.86/0.77 % (793209)Instructions burned: 31 (million)
% 2.86/0.77 % (793211)Instruction limit reached!
% 2.86/0.77 % (793211)------------------------------
% 2.86/0.77 % (793211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793211)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793211)Termination reason: Instruction limit
% 2.86/0.77 % (793211)Termination phase: Saturation
% 2.86/0.77 % (793211)Time elapsed: 0.020 s
% 2.86/0.77 % (793211)Peak memory usage: 12 MB
% 2.86/0.77 % (793211)Instructions burned: 35 (million)
% 2.86/0.77 % (793215)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=4173687822:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 2.86/0.77 % (793201)Instruction limit reached!
% 2.86/0.77 % (793201)------------------------------
% 2.86/0.77 % (793201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793201)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793201)Termination reason: Instruction limit
% 2.86/0.77 % (793201)Termination phase: Saturation
% 2.86/0.77 % (793201)Time elapsed: 0.105 s
% 2.86/0.77 % (793201)Peak memory usage: 13 MB
% 2.86/0.77 % (793201)Instructions burned: 201 (million)
% 2.86/0.77 % (793216)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 2.86/0.77 % (793216)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=3038667192:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 2.86/0.77 % (793215) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-793104-793215"...
% 2.86/0.77 % (793218)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1901503445:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 2.86/0.77 % (793189)Instruction limit reached!
% 2.86/0.77 % (793189)------------------------------
% 2.86/0.77 % (793189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793189)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793189)Termination reason: Instruction limit
% 2.86/0.77 % (793189)Termination phase: Saturation
% 2.86/0.77 % (793189)Time elapsed: 0.191 s
% 2.86/0.77 % (793189)Peak memory usage: 15 MB
% 2.86/0.77 % (793189)Instructions burned: 316 (million)
% 2.86/0.77 % (793215)...printing done.
% 2.86/0.77 % (793215)Refutation found. Thanks to Tanya!
% 2.86/0.77 % SZS status Theorem for theBenchmark
% 2.86/0.77 % SZS output start Proof for theBenchmark
% 2.86/0.77 thf(type_def_5, type, tyop_2Emin_2Ebool: $tType).
% 2.86/0.77 thf(type_def_6, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 2.86/0.77 thf(type_def_7, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 2.86/0.77 thf(type_def_8, type, tyop_2Ewellorder_2Ewellorder: $tType > $tType).
% 2.86/0.77 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 2.86/0.77 thf(type_def_10, type, sK0: $tType).
% 2.86/0.77 thf(func_def_0, type, c_2Ebool_2E_21: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.86/0.77 thf(func_def_1, type, c_2Epair_2E_2C: !>[X0: $tType, X1: $tType]:((X0 > X1 > tyop_2Epair_2Eprod @ X0 @ X1))).
% 2.86/0.77 thf(func_def_2, type, c_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 2.86/0.77 thf(func_def_3, type, c_2Emin_2E_3D: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.86/0.77 thf(func_def_4, type, c_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 2.86/0.77 thf(func_def_5, type, c_2Ebool_2E_3F: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.86/0.77 thf(func_def_6, type, c_2Epair_2ECURRY: !>[X0: $tType, X1: $tType, X2: $tType]:(((tyop_2Epair_2Eprod @ X0 @ X1 > X2) > X0 > X1 > X2))).
% 2.86/0.77 thf(func_def_7, type, c_2Ebool_2EIN: !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 2.86/0.77 thf(func_def_8, type, c_2Erelation_2EWF: !>[X0: $tType]:(((X0 > X0 > $o) > $o))).
% 2.86/0.77 thf(func_def_9, type, c_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 2.86/0.77 thf(func_def_10, type, c_2Eset__relation_2Estrict: !>[X0: $tType]:(((tyop_2Epair_2Eprod @ X0 @ X0 > $o) > tyop_2Epair_2Eprod @ X0 @ X0 > $o))).
% 2.86/0.77 thf(func_def_11, type, c_2Ewellorder_2Ewellfounded: !>[X0: $tType]:(((tyop_2Epair_2Eprod @ X0 @ X0 > $o) > $o))).
% 2.86/0.77 thf(func_def_12, type, c_2Ewellorder_2Ewellorder__REP: !>[X0: $tType]:((tyop_2Ewellorder_2Ewellorder @ X0 > tyop_2Epair_2Eprod @ X0 @ X0 > $o))).
% 2.86/0.77 thf(func_def_13, type, c_2Ebool_2E_7E: ($o > $o)).
% 2.86/0.77 thf(func_def_15, type, vNOT: ($o > $o)).
% 2.86/0.77 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 2.86/0.77 thf(func_def_19, type, db0: !>[X0: $tType]:(X0)).
% 2.86/0.77 thf(func_def_20, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.86/0.77 thf(func_def_21, type, sK1: tyop_2Ewellorder_2Ewellorder @ sK0).
% 2.86/0.77 thf(func_def_22, type, sK2: !>[X0: $tType]:(((X0 > $o) > X0))).
% 2.86/0.77 thf(func_def_23, type, sK3: !>[X0: $tType]:(((X0 > $o) > X0))).
% 2.86/0.77 thf(func_def_24, type, db2: !>[X0: $tType]:(X0)).
% 2.86/0.77 thf(func_def_25, type, sK4: ((tyop_2Epair_2Eprod @ sK0 @ sK0 > $o) > sK0)).
% 2.86/0.77 thf(func_def_26, type, sK5: ((tyop_2Epair_2Eprod @ sK0 @ sK0 > $o) > sK0)).
% 2.86/0.77 thf(func_def_27, type, sK6: !>[X0: $tType, X1: $tType]:(((tyop_2Epair_2Eprod @ X0 @ X1 > sK0 > sK0 > $o) > X0 > X1 > sK0))).
% 2.86/0.77 thf(func_def_28, type, sK7: !>[X0: $tType, X1: $tType]:((X0 > X1 > (tyop_2Epair_2Eprod @ X0 @ X1 > sK0 > sK0 > $o) > sK0))).
% 2.86/0.77 thf(f9,axiom,(
% 2.86/0.77 ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : (tyop_2Epair_2Eprod @ X0 @ X1 > X2),X4 : X0,X5 : X1] : (((c_2Epair_2ECURRY @ X0 @ X1 @ X2 @ X3 @ X4 @ X5)) = ((X3 @ (c_2Epair_2E_2C @ X0 @ X1 @ X4 @ X5))))),
% 2.86/0.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Epair_2ECURRY__DEF)).
% 2.86/0.77 thf(f10,axiom,(
% 2.86/0.77 ! [X0 : $tType,X1 : (tyop_2Epair_2Eprod @ X0 @ X0 > $o)] : (((c_2Ewellorder_2Ewellfounded @ X0 @ X1)) = ((c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X1))))),
% 2.86/0.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewellorder_2Ewellfounded__WF)).
% 2.86/0.77 thf(f11,axiom,(
% 2.86/0.77 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Ewellorder_2Ewellfounded @ X0 @ (^[X2 : tyop_2Epair_2Eprod @ X0 @ X0] : ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ X2 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))),
% 2.86/0.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewellorder_2EWIN__WF)).
% 2.86/0.77 thf(f12,conjecture,(
% 2.86/0.77 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X2 : X0, X3 : X0] : ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X2 @ X3) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))),
% 2.86/0.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewellorder_2EWIN__WF2)).
% 2.86/0.77 thf(f13,negated_conjecture,(
% 2.86/0.77 ~ ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X2 : X0, X3 : X0] : ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X2 @ X3) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))),
% 2.86/0.77 inference(negated_conjecture,[status(cth)],[f12])).
% 2.86/0.77 thf(f18,plain,(
% 2.86/0.77 ~ ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X2 : X0, X3 : X0] : ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X2 @ X3) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))),
% 2.86/0.77 inference(rectify,[],[f13])).
% 2.86/0.77 thf(f19,plain,(
% 2.86/0.77 ~ ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (((c_2Erelation_2EWF @ X0 @ (^[Y0 : X0]: ((^[Y1 : X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))))) = $true)),
% 2.86/0.77 inference(fool_elimination,[],[f18])).
% 2.86/0.77 thf(f24,plain,(
% 2.86/0.77 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Ewellorder_2Ewellfounded @ X0 @ (^[X2 : tyop_2Epair_2Eprod @ X0 @ X0] : ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ X2 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))),
% 2.86/0.77 inference(rectify,[],[f11])).
% 2.86/0.77 thf(f25,plain,(
% 2.86/0.77 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (((c_2Ewellorder_2Ewellfounded @ X0 @ (^[Y0 : tyop_2Epair_2Eprod @ X0 @ X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ Y0 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))) = $true)),
% 2.86/0.77 inference(fool_elimination,[],[f24])).
% 2.86/0.77 thf(f34,plain,(
% 2.86/0.77 ! [X2 : $tType,X1 : $tType,X0 : $tType,X4 : X1,X3 : (tyop_2Epair_2Eprod @ X1 @ X0 > X2),X5 : X0] : (((X3 @ (c_2Epair_2E_2C @ X1 @ X0 @ X4 @ X5))) = ((c_2Epair_2ECURRY @ X1 @ X0 @ X2 @ X3 @ X4 @ X5)))),
% 2.86/0.77 inference(rectify,[],[f9])).
% 2.86/0.77 thf(f35,plain,(
% 2.86/0.77 ? [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (((c_2Erelation_2EWF @ X0 @ (^[Y0 : X0]: ((^[Y1 : X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))))) != $true)),
% 2.86/0.77 inference(ennf_transformation,[],[f19])).
% 2.86/0.77 thf(f37,plain,(
% 2.86/0.77 (((c_2Erelation_2EWF @ sK0 @ (^[Y0 : sK0]: ((^[Y1 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))))) != $true)),
% 2.86/0.77 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f35])).
% 2.86/0.77 thf(f43,plain,(
% 2.86/0.77 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : X1,X4 : (tyop_2Epair_2Eprod @ X1 @ X2 > X0),X5 : X2] : (((X4 @ (c_2Epair_2E_2C @ X1 @ X2 @ X3 @ X5))) = ((c_2Epair_2ECURRY @ X1 @ X2 @ X0 @ X4 @ X3 @ X5)))),
% 2.86/0.77 inference(rectify,[],[f34])).
% 2.86/0.77 thf(f53,plain,(
% 2.86/0.77 (((c_2Erelation_2EWF @ sK0 @ (^[Y0 : sK0]: ((^[Y1 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))))) != $true)),
% 2.86/0.77 inference(cnf_transformation,[],[f37])).
% 2.86/0.77 thf(f59,plain,(
% 2.86/0.77 ( ! [X0 : $tType,X1 : (tyop_2Epair_2Eprod @ X0 @ X0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ X0 @ X1)) = ((c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X1))))) )),
% 2.86/0.77 inference(cnf_transformation,[],[f10])).
% 2.86/0.77 thf(f60,plain,(
% 2.86/0.77 ( ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : X1,X4 : (tyop_2Epair_2Eprod @ X1 @ X2 > X0),X5 : X2] : ((((X4 @ (c_2Epair_2E_2C @ X1 @ X2 @ X3 @ X5))) = ((c_2Epair_2ECURRY @ X1 @ X2 @ X0 @ X4 @ X3 @ X5)))) )),
% 2.86/0.77 inference(cnf_transformation,[],[f43])).
% 2.86/0.77 thf(f69,plain,(
% 2.86/0.77 ( ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : ((((c_2Ewellorder_2Ewellfounded @ X0 @ (^[Y0 : tyop_2Epair_2Eprod @ X0 @ X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ Y0 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))) = $true)) )),
% 2.86/0.77 inference(cnf_transformation,[],[f25])).
% 2.86/0.77 thf(f85,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : (((^[Y0 : sK0]: ((^[Y1 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) != ((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0))) | (((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true)) )),
% 2.86/0.77 inference(constrained_superposition,[],[f53,f59])).
% 2.86/0.77 thf(f86,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true) | (((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0))) != (((^[Y0 : sK0]: ((^[Y1 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) @ (sK4 @ X0))))) )),
% 2.86/0.77 inference(negative_extensionality,[],[f85])).
% 2.86/0.77 thf(f90,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : (((^[Y0 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) != ((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0)))) | (((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true)) )),
% 2.86/0.77 inference(beta-eta_normalization,[],[f86])).
% 2.86/0.77 thf(f91,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true) | (((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0) @ (sK5 @ X0))) != (((^[Y0 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) @ (sK5 @ X0))))) )),
% 2.86/0.77 inference(negative_extensionality,[],[f90])).
% 2.86/0.77 thf(f97,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : (($true = (((^[Y0 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) @ (sK5 @ X0)))) | (((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0) @ (sK5 @ X0))) = $true) | (((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true)) )),
% 2.86/0.77 inference(xor_proxy_clausification,[],[f91])).
% 2.86/0.77 thf(f98,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : (($false = (((^[Y0 : sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) @ (sK5 @ X0)))) | ($false = ((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0) @ (sK5 @ X0)))) | (((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true)) )),
% 2.86/0.77 inference(xor_proxy_clausification,[],[f91])).
% 2.86/0.77 thf(f99,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true) | ($false = ((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0) @ (sK5 @ X0)))) | ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0)) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) )),
% 2.86/0.77 inference(beta-eta_normalization,[],[f98])).
% 2.86/0.77 thf(f100,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0)) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) = $true) | (((c_2Epair_2ECURRY @ sK0 @ sK0 @ $o @ X0 @ (sK4 @ X0) @ (sK5 @ X0))) = $true) | (((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true)) )),
% 2.86/0.77 inference(beta-eta_normalization,[],[f97])).
% 2.86/0.77 thf(f101,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true) | ($false = ((X0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0))))) | ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0)) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) )),
% 2.86/0.77 inference(forward_demodulation,[],[f99,f60])).
% 2.86/0.77 thf(f102,plain,(
% 2.86/0.77 ( ! [X0 : (tyop_2Epair_2Eprod @ sK0 @ sK0 > $o)] : ((((c_2Ewellorder_2Ewellfounded @ sK0 @ X0)) != $true) | (((X0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0)))) = $true) | (((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ X0) @ (sK5 @ X0)) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))) = $true)) )),
% 2.86/0.77 inference(forward_demodulation,[],[f100,f60])).
% 2.86/0.77 thf(f108,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (($true != $true) | ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) | ($false = (((^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))) @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))))))) )),
% 2.86/0.77 inference(constrained_superposition,[],[f101,f69])).
% 2.86/0.77 thf(f110,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) | ($false = (((^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))) @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))))))) )),
% 2.86/0.77 inference(trivial_inequality_removal,[],[f108])).
% 2.86/0.77 thf(f111,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) | ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) )),
% 2.86/0.77 inference(beta-eta_normalization,[],[f110])).
% 2.86/0.77 thf(f126,plain,(
% 2.86/0.77 ($false != $false) | ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))),
% 2.86/0.77 inference(equality_factoring,[],[f111])).
% 2.86/0.77 thf(f130,plain,(
% 2.86/0.77 ($false = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))),
% 2.86/0.77 inference(trivial_inequality_removal,[],[f126])).
% 2.86/0.77 thf(f133,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) | ((((^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))) @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))))) = $true) | ($true != $true)) )),
% 2.86/0.77 inference(constrained_superposition,[],[f102,f69])).
% 2.86/0.77 thf(f135,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (((((^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))) @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))))) = $true) | ($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) )),
% 2.86/0.77 inference(trivial_inequality_removal,[],[f133])).
% 2.86/0.77 thf(f136,plain,(
% 2.86/0.77 ( ! [X0 : tyop_2Ewellorder_2Ewellorder @ sK0] : (($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) | ($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ X0)))))) )),
% 2.86/0.77 inference(beta-eta_normalization,[],[f135])).
% 2.86/0.77 thf(f148,plain,(
% 2.86/0.77 ($true != $true) | ($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))),
% 2.86/0.77 inference(equality_factoring,[],[f136])).
% 2.86/0.77 thf(f151,plain,(
% 2.86/0.77 ($true = ((c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ (c_2Epair_2E_2C @ sK0 @ sK0 @ (sK4 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1))))) @ (sK5 @ (^[Y0 : tyop_2Epair_2Eprod @ sK0 @ sK0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK0 @ sK0 @ Y0 @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))) @ (c_2Eset__relation_2Estrict @ sK0 @ (c_2Ewellorder_2Ewellorder__REP @ sK0 @ sK1)))))),
% 2.86/0.77 inference(trivial_inequality_removal,[],[f148])).
% 2.86/0.77 thf(f161,plain,(
% 2.86/0.77 ($false = $true)),
% 2.86/0.77 inference(forward_demodulation,[],[f151,f130])).
% 2.86/0.77 thf(f162,plain,(
% 2.86/0.77 $false),
% 2.86/0.77 inference(trivial_inequality_removal,[],[f161])).
% 2.86/0.77 % SZS output end Proof for theBenchmark
% 2.86/0.77 % (793215)------------------------------
% 2.86/0.77 % (793215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.77 % (793215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.77 % (793215)CaDiCaL version: 2.1.3
% 2.86/0.77 % (793215)Termination reason: Refutation
% 2.86/0.77 % (793215)Time elapsed: 0.022 s
% 2.86/0.77 % (793215)Peak memory usage: 13 MB
% 2.86/0.77 % (793215)Instructions burned: 38 (million)
% 2.86/0.77 % (793104)Success in time 0.52 s
% 2.86/0.77 % Vampire exiting
%------------------------------------------------------------------------------