%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU708^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:30:53 AM UTC 2026
% Result : Theorem 2.65s 0.67s
% Output : Refutation 2.65s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU708^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n006.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 14:12:55 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.23 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.32 % (780953)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.20/0.32 % (780961)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=3151631888: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.32 % (780961)Refutation not found, incomplete strategy
% 0.20/0.32 % (780961)------------------------------
% 0.20/0.32 % (780961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (780961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (780961)CaDiCaL version: 2.1.3
% 0.20/0.32 % (780961)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.32 % (780961)Time elapsed: 0.004 s
% 0.20/0.32 % (780961)Peak memory usage: 12 MB
% 0.20/0.32 % (780961)Instructions burned: 10 (million)
% 0.20/0.32 % (780964)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.32 % (780964)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.32 % (780961)------------------------------
% 0.20/0.32 % (780961)------------------------------
% 0.20/0.32 % (780958)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=493370911:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.20/0.32 % (780959)lrs+10_16_si=on:nwc=1.5:random_seed=2236286190:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.20/0.32 % (780960)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2312487620:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.20/0.32 % (780963)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3096179845:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.20/0.32 % (780962)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1792807898:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.20/0.32 % (780964)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=2831951205:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.20/0.32 % (780960)Instruction limit reached!
% 0.20/0.32 % (780960)------------------------------
% 0.20/0.32 % (780960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (780960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (780960)CaDiCaL version: 2.1.3
% 0.20/0.32 % (780960)Termination reason: Instruction limit
% 0.20/0.32 % (780960)Termination phase: Saturation
% 0.20/0.32 % (780960)Time elapsed: 0.002 s
% 0.20/0.32 % (780960)Peak memory usage: 11 MB
% 0.20/0.32 % (780960)Instructions burned: 3 (million)
% 0.20/0.32 % (780962)Refutation not found, incomplete strategy
% 0.20/0.32 % (780962)------------------------------
% 0.20/0.32 % (780962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (780962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (780962)CaDiCaL version: 2.1.3
% 0.20/0.32 % (780962)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.32 % (780962)Time elapsed: 0.005 s
% 0.20/0.32 % (780962)Peak memory usage: 12 MB
% 0.20/0.32 % (780962)Instructions burned: 8 (million)
% 0.20/0.32 % (780962)------------------------------
% 0.20/0.32 % (780962)------------------------------
% 0.20/0.32 % (780966)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3463042153:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.32 % (780958)Refutation not found, incomplete strategy
% 0.20/0.32 % (780958)------------------------------
% 0.20/0.32 % (780958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.32 % (780958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.32 % (780958)CaDiCaL version: 2.1.3
% 0.20/0.32 % (780958)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.32 % (780958)Time elapsed: 0.008 s
% 0.20/0.32 % (780958)Peak memory usage: 12 MB
% 0.20/0.32 % (780958)Instructions burned: 14 (million)
% 0.20/0.32 % (780964)Refutation not found, incomplete strategy
% 0.20/0.34 % (780964)------------------------------
% 0.20/0.34 % (780964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (780964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (780964)CaDiCaL version: 2.1.3
% 0.20/0.34 % (780964)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.34 % (780964)Time elapsed: 0.008 s
% 0.20/0.34 % (780964)Peak memory usage: 12 MB
% 0.20/0.34 % (780964)Instructions burned: 13 (million)
% 0.20/0.34 % (780958)------------------------------
% 0.20/0.34 % (780958)------------------------------
% 0.20/0.34 % (780966)Instruction limit reached!
% 0.20/0.34 % (780966)------------------------------
% 0.20/0.34 % (780966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (780966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (780966)CaDiCaL version: 2.1.3
% 0.20/0.34 % (780966)Termination reason: Instruction limit
% 0.20/0.34 % (780966)Termination phase: Saturation
% 0.20/0.34 % (780966)Time elapsed: 0.001 s
% 0.20/0.34 % (780966)Peak memory usage: 11 MB
% 0.20/0.34 % (780966)Instructions burned: 3 (million)
% 0.20/0.34 % (780964)------------------------------
% 0.20/0.34 % (780964)------------------------------
% 0.20/0.34 % (780959)Instruction limit reached!
% 0.20/0.34 % (780959)------------------------------
% 0.20/0.34 % (780959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (780959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (780959)CaDiCaL version: 2.1.3
% 0.20/0.34 % (780959)Termination reason: Instruction limit
% 0.20/0.34 % (780959)Termination phase: Saturation
% 0.20/0.34 % (780959)Time elapsed: 0.010 s
% 0.20/0.34 % (780959)Peak memory usage: 12 MB
% 0.20/0.34 % (780959)Instructions burned: 19 (million)
% 0.20/0.34 % (780976)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=3455383810:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.20/0.34 % (780973)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3964976794:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.20/0.34 % (780974)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.34 % (780976)Instruction limit reached!
% 0.20/0.34 % (780976)------------------------------
% 0.20/0.34 % (780976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (780976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (780976)CaDiCaL version: 2.1.3
% 0.20/0.34 % (780976)Termination reason: Instruction limit
% 0.20/0.34 % (780976)Termination phase: Saturation
% 0.20/0.34 % (780976)Time elapsed: 0.004 s
% 0.20/0.34 % (780976)Peak memory usage: 12 MB
% 0.20/0.34 % (780976)Instructions burned: 13 (million)
% 0.20/0.34 % (780973)Instruction limit reached!
% 0.20/0.34 % (780973)------------------------------
% 0.20/0.34 % (780973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.34 % (780973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.34 % (780973)CaDiCaL version: 2.1.3
% 0.20/0.34 % (780973)Termination reason: Instruction limit
% 0.20/0.34 % (780973)Termination phase: Saturation
% 0.20/0.34 % (780973)Time elapsed: 0.003 s
% 0.20/0.34 % (780973)Peak memory usage: 12 MB
% 0.20/0.34 % (780977)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.34 % (780973)Instructions burned: 5 (million)
% 0.20/0.34 % (780977)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.20/0.34 % (780974)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3149685418:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.20/0.34 % (780977)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2576091114: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.20/0.34 % (780978)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=1664025823:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.20/0.36 % (780979)lrs+10_1_si=on:cs=on:random_seed=1763788463:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.20/0.36 % (780974)Instruction limit reached!
% 0.20/0.36 % (780974)------------------------------
% 0.20/0.36 % (780974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780974)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780974)Termination reason: Instruction limit
% 0.20/0.36 % (780974)Termination phase: Saturation
% 0.20/0.36 % (780974)Time elapsed: 0.004 s
% 0.20/0.36 % (780974)Peak memory usage: 12 MB
% 0.20/0.36 % (780974)Instructions burned: 7 (million)
% 0.20/0.36 % (780982)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.20/0.36 % (780979)Instruction limit reached!
% 0.20/0.36 % (780979)------------------------------
% 0.20/0.36 % (780979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780979)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780979)Termination reason: Instruction limit
% 0.20/0.36 % (780979)Termination phase: Saturation
% 0.20/0.36 % (780979)Time elapsed: 0.004 s
% 0.20/0.36 % (780979)Peak memory usage: 11 MB
% 0.20/0.36 % (780979)Instructions burned: 8 (million)
% 0.20/0.36 % (780982)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=2417060933:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.20/0.36 % (780982)Instruction limit reached!
% 0.20/0.36 % (780982)------------------------------
% 0.20/0.36 % (780982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780982)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780982)Termination reason: Instruction limit
% 0.20/0.36 % (780982)Termination phase: Saturation
% 0.20/0.36 % (780982)Time elapsed: 0.001 s
% 0.20/0.36 % (780982)Peak memory usage: 11 MB
% 0.20/0.36 % (780982)Instructions burned: 3 (million)
% 0.20/0.36 % (780977)Refutation not found, incomplete strategy
% 0.20/0.36 % (780977)------------------------------
% 0.20/0.36 % (780977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780977)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780977)Termination reason: Refutation not found, incomplete strategy
% 0.20/0.36 % (780977)Time elapsed: 0.010 s
% 0.20/0.36 % (780977)Peak memory usage: 12 MB
% 0.20/0.36 % (780977)Instructions burned: 20 (million)
% 0.20/0.36 % (780963)Instruction limit reached!
% 0.20/0.36 % (780963)------------------------------
% 0.20/0.36 % (780963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780963)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780963)Termination reason: Instruction limit
% 0.20/0.36 % (780963)Termination phase: Saturation
% 0.20/0.36 % (780963)Time elapsed: 0.040 s
% 0.20/0.36 % (780963)Peak memory usage: 12 MB
% 0.20/0.36 % (780963)Instructions burned: 77 (million)
% 0.20/0.36 % (780977)------------------------------
% 0.20/0.36 % (780977)------------------------------
% 0.20/0.36 % (780983)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1698560161:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.20/0.36 % (780991)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3362129496:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.20/0.36 % (780988)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1678598603:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.20/0.36 % (780991)Instruction limit reached!
% 0.20/0.36 % (780991)------------------------------
% 0.20/0.36 % (780991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.20/0.36 % (780991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/0.36 % (780991)CaDiCaL version: 2.1.3
% 0.20/0.36 % (780991)Termination reason: Instruction limit
% 0.20/0.36 % (780991)Termination phase: Saturation
% 0.89/0.38 % (780991)Time elapsed: 0.005 s
% 0.89/0.38 % (780991)Peak memory usage: 12 MB
% 0.89/0.38 % (780991)Instructions burned: 17 (million)
% 0.89/0.38 % (780989)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1068099835:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.89/0.38 % (780988)Refutation not found, incomplete strategy
% 0.89/0.38 % (780988)------------------------------
% 0.89/0.38 % (780988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780988)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780988)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.38 % (780988)Time elapsed: 0.005 s
% 0.89/0.38 % (780988)Peak memory usage: 12 MB
% 0.89/0.38 % (780988)Instructions burned: 8 (million)
% 0.89/0.38 % (780983)Refutation not found, incomplete strategy
% 0.89/0.38 % (780983)------------------------------
% 0.89/0.38 % (780983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780983)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780983)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.38 % (780983)Time elapsed: 0.010 s
% 0.89/0.38 % (780983)Peak memory usage: 12 MB
% 0.89/0.38 % (780983)Instructions burned: 18 (million)
% 0.89/0.38 % (780988)------------------------------
% 0.89/0.38 % (780988)------------------------------
% 0.89/0.38 % (780983)------------------------------
% 0.89/0.38 % (780983)------------------------------
% 0.89/0.38 % (780989)Refutation not found, incomplete strategy
% 0.89/0.38 % (780989)------------------------------
% 0.89/0.38 % (780989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780992)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1265000904:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.89/0.38 % (780989)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780989)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.38 % (780989)Time elapsed: 0.005 s
% 0.89/0.38 % (780989)Peak memory usage: 12 MB
% 0.89/0.38 % (780989)Instructions burned: 8 (million)
% 0.89/0.38 % (780993)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=406093569:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/14Mi)
% 0.89/0.38 % (780989)------------------------------
% 0.89/0.38 % (780989)------------------------------
% 0.89/0.38 % (780992)Refutation not found, incomplete strategy
% 0.89/0.38 % (780992)------------------------------
% 0.89/0.38 % (780992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780992)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780992)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.38 % (780992)Time elapsed: 0.005 s
% 0.89/0.38 % (780992)Peak memory usage: 12 MB
% 0.89/0.38 % (780992)Instructions burned: 8 (million)
% 0.89/0.38 % (780992)------------------------------
% 0.89/0.38 % (780992)------------------------------
% 0.89/0.38 % (780998)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=2082238099:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.89/0.38 % (780993)Instruction limit reached!
% 0.89/0.38 % (780993)------------------------------
% 0.89/0.38 % (780993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780993)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780993)Termination reason: Instruction limit
% 0.89/0.38 % (780993)Termination phase: Saturation
% 0.89/0.38 % (780993)Time elapsed: 0.010 s
% 0.89/0.38 % (780993)Peak memory usage: 12 MB
% 0.89/0.38 % (780993)Instructions burned: 20 (million)
% 0.89/0.38 % (780998)Instruction limit reached!
% 0.89/0.38 % (780998)------------------------------
% 0.89/0.38 % (780998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.38 % (780998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.38 % (780998)CaDiCaL version: 2.1.3
% 0.89/0.38 % (780998)Termination reason: Instruction limit
% 0.89/0.38 % (780998)Termination phase: Saturation
% 0.89/0.41 % (780998)Time elapsed: 0.001 s
% 0.89/0.41 % (780998)Peak memory usage: 11 MB
% 0.89/0.41 % (780998)Instructions burned: 5 (million)
% 0.89/0.41 % (780978)Instruction limit reached!
% 0.89/0.41 % (780978)------------------------------
% 0.89/0.41 % (780978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (780978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (780978)CaDiCaL version: 2.1.3
% 0.89/0.41 % (780978)Termination reason: Instruction limit
% 0.89/0.41 % (780978)Termination phase: Saturation
% 0.89/0.41 % (780978)Time elapsed: 0.043 s
% 0.89/0.41 % (780978)Peak memory usage: 13 MB
% 0.89/0.41 % (780978)Instructions burned: 88 (million)
% 0.89/0.41 % (780999)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=67988880:i=26:ep=R:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/26Mi)
% 0.89/0.41 % (781000)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=73829293:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/23Mi)
% 0.89/0.41 % (781003)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=13340567:cond=on:i=60:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/60Mi)
% 0.89/0.41 % (781007)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=1758951647:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 0.89/0.41 % (781004)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
% 0.89/0.41 % (781004)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 0.89/0.41 % (781003)Refutation not found, incomplete strategy
% 0.89/0.41 % (781003)------------------------------
% 0.89/0.41 % (781003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (781003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (781003)CaDiCaL version: 2.1.3
% 0.89/0.41 % (781003)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.41 % (781003)Time elapsed: 0.006 s
% 0.89/0.41 % (781003)Peak memory usage: 12 MB
% 0.89/0.41 % (781003)Instructions burned: 10 (million)
% 0.89/0.41 % (781003)------------------------------
% 0.89/0.41 % (781003)------------------------------
% 0.89/0.41 % (781000)Instruction limit reached!
% 0.89/0.41 % (781000)------------------------------
% 0.89/0.41 % (781000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (781000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (781000)CaDiCaL version: 2.1.3
% 0.89/0.41 % (781000)Termination reason: Instruction limit
% 0.89/0.41 % (781000)Termination phase: Saturation
% 0.89/0.41 % (781000)Time elapsed: 0.012 s
% 0.89/0.41 % (781000)Peak memory usage: 11 MB
% 0.89/0.41 % (781000)Instructions burned: 24 (million)
% 0.89/0.41 % (781004)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=3059861687:i=14:add=off:nm=40:rtra=on:rawr=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.89/0.41 % (780999)Instruction limit reached!
% 0.89/0.41 % (780999)------------------------------
% 0.89/0.41 % (780999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (780999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (780999)CaDiCaL version: 2.1.3
% 0.89/0.41 % (780999)Termination reason: Instruction limit
% 0.89/0.41 % (780999)Termination phase: Saturation
% 0.89/0.41 % (780999)Time elapsed: 0.015 s
% 0.89/0.41 % (780999)Peak memory usage: 12 MB
% 0.89/0.41 % (780999)Instructions burned: 28 (million)
% 0.89/0.41 % (781007)Instruction limit reached!
% 0.89/0.41 % (781007)------------------------------
% 0.89/0.41 % (781007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (781007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (781007)CaDiCaL version: 2.1.3
% 0.89/0.41 % (781007)Termination reason: Instruction limit
% 0.89/0.41 % (781007)Termination phase: Saturation
% 0.89/0.41 % (781007)Time elapsed: 0.009 s
% 0.89/0.41 % (781007)Peak memory usage: 12 MB
% 0.89/0.41 % (781007)Instructions burned: 33 (million)
% 0.89/0.41 % (781008)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2068414631:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 0.89/0.43 % (781006)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 0.89/0.43 % (781004)Instruction limit reached!
% 0.89/0.43 % (781004)------------------------------
% 0.89/0.43 % (781004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.43 % (781004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.43 % (781004)CaDiCaL version: 2.1.3
% 0.89/0.43 % (781004)Termination reason: Instruction limit
% 0.89/0.43 % (781004)Termination phase: Saturation
% 0.89/0.43 % (781004)Time elapsed: 0.008 s
% 0.89/0.43 % (781004)Peak memory usage: 12 MB
% 0.89/0.43 % (781004)Instructions burned: 15 (million)
% 0.89/0.43 % (781008)Instruction limit reached!
% 0.89/0.43 % (781008)------------------------------
% 0.89/0.43 % (781008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.43 % (781008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.43 % (781008)CaDiCaL version: 2.1.3
% 0.89/0.43 % (781008)Termination reason: Instruction limit
% 0.89/0.43 % (781008)Termination phase: Saturation
% 0.89/0.43 % (781008)Time elapsed: 0.004 s
% 0.89/0.43 % (781008)Peak memory usage: 12 MB
% 0.89/0.43 % (781008)Instructions burned: 7 (million)
% 0.89/0.43 % (781006)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=645879500:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.89/0.43 % (781017)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1397390912:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 0.89/0.43 % (781006)Instruction limit reached!
% 0.89/0.43 % (781006)------------------------------
% 0.89/0.43 % (781006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.43 % (781006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.43 % (781006)CaDiCaL version: 2.1.3
% 0.89/0.43 % (781006)Termination reason: Instruction limit
% 0.89/0.43 % (781006)Termination phase: Saturation
% 0.89/0.43 % (781006)Time elapsed: 0.005 s
% 0.89/0.43 % (781006)Peak memory usage: 12 MB
% 0.89/0.43 % (781006)Instructions burned: 8 (million)
% 0.89/0.43 % (781013)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=4041421758:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.89/0.43 % (781015)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1321460990:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 0.89/0.43 % (781016)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2193112015:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 0.89/0.43 % (781019)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=508866229:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 0.89/0.43 % (781020)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4289362026:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 0.89/0.43 % (781013)Instruction limit reached!
% 0.89/0.43 % (781013)------------------------------
% 0.89/0.43 % (781013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.43 % (781013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.43 % (781013)CaDiCaL version: 2.1.3
% 0.89/0.43 % (781013)Termination reason: Instruction limit
% 0.89/0.43 % (781013)Termination phase: Saturation
% 0.89/0.43 % (781013)Time elapsed: 0.011 s
% 0.89/0.43 % (781013)Peak memory usage: 12 MB
% 0.89/0.43 % (781013)Instructions burned: 25 (million)
% 0.89/0.43 % (781015)Instruction limit reached!
% 0.89/0.43 % (781015)------------------------------
% 0.89/0.43 % (781015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.43 % (781015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.43 % (781015)CaDiCaL version: 2.1.3
% 0.89/0.43 % (781015)Termination reason: Instruction limit
% 0.89/0.43 % (781015)Termination phase: Saturation
% 0.89/0.43 % (781015)Time elapsed: 0.012 s
% 0.89/0.43 % (781015)Peak memory usage: 12 MB
% 0.89/0.43 % (781015)Instructions burned: 20 (million)
% 0.89/0.43 % (781023)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.89/0.45 % (781016)Refutation not found, incomplete strategy
% 0.89/0.45 % (781016)------------------------------
% 0.89/0.45 % (781016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (781016)CaDiCaL version: 2.1.3
% 0.89/0.45 % (781016)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.45 % (781016)Time elapsed: 0.011 s
% 0.89/0.45 % (781016)Peak memory usage: 12 MB
% 0.89/0.45 % (781016)Instructions burned: 19 (million)
% 0.89/0.45 % (781019)Refutation not found, incomplete strategy
% 0.89/0.45 % (781019)------------------------------
% 0.89/0.45 % (781019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (781016)------------------------------
% 0.89/0.45 % (781016)------------------------------
% 0.89/0.45 % (781019)CaDiCaL version: 2.1.3
% 0.89/0.45 % (781019)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.45 % (781019)Time elapsed: 0.006 s
% 0.89/0.45 % (781019)Peak memory usage: 12 MB
% 0.89/0.45 % (781019)Instructions burned: 9 (million)
% 0.89/0.45 % (781019)------------------------------
% 0.89/0.45 % (781019)------------------------------
% 0.89/0.45 % (781023)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1612367376:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2998 on theBenchmark for (2998ds/7Mi)
% 0.89/0.45 % (781023)Instruction limit reached!
% 0.89/0.45 % (781023)------------------------------
% 0.89/0.45 % (781023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (781023)CaDiCaL version: 2.1.3
% 0.89/0.45 % (781023)Termination reason: Instruction limit
% 0.89/0.45 % (781023)Termination phase: Saturation
% 0.89/0.45 % (781023)Time elapsed: 0.004 s
% 0.89/0.45 % (781023)Peak memory usage: 12 MB
% 0.89/0.45 % (781023)Instructions burned: 8 (million)
% 0.89/0.45 % (781029)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2643829475:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/181Mi)
% 0.89/0.45 % (781031)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 0.89/0.45 % (781030)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=3914137982:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/169Mi)
% 0.89/0.45 % (781017)Instruction limit reached!
% 0.89/0.45 % (781017)------------------------------
% 0.89/0.45 % (781017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (781017)CaDiCaL version: 2.1.3
% 0.89/0.45 % (781017)Termination reason: Instruction limit
% 0.89/0.45 % (781017)Termination phase: Saturation
% 0.89/0.45 % (781017)Time elapsed: 0.037 s
% 0.89/0.45 % (781017)Peak memory usage: 13 MB
% 0.89/0.45 % (781017)Instructions burned: 144 (million)
% 0.89/0.45 % (781020)Instruction limit reached!
% 0.89/0.45 % (781020)------------------------------
% 0.89/0.45 % (781020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (781020)CaDiCaL version: 2.1.3
% 0.89/0.45 % (781020)Termination reason: Instruction limit
% 0.89/0.45 % (781020)Termination phase: Saturation
% 0.89/0.45 % (781020)Time elapsed: 0.022 s
% 0.89/0.45 % (781020)Peak memory usage: 12 MB
% 0.89/0.45 % (781020)Instructions burned: 44 (million)
% 0.89/0.45 % (781031)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2921275483:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2998 on theBenchmark for (2998ds/6Mi)
% 0.89/0.45 % (781030)Refutation not found, incomplete strategy
% 0.89/0.45 % (781030)------------------------------
% 0.89/0.45 % (781030)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (781030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.48 % (781030)CaDiCaL version: 2.1.3
% 1.60/0.48 % (781030)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.48 % (781030)Time elapsed: 0.005 s
% 1.60/0.48 % (781030)Peak memory usage: 13 MB
% 1.60/0.48 % (781030)Instructions burned: 8 (million)
% 1.60/0.48 % (781030)------------------------------
% 1.60/0.48 % (781030)------------------------------
% 1.60/0.48 % (781033)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1874415594:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2998 on theBenchmark for (2998ds/22Mi)
% 1.60/0.48 % (781031)Instruction limit reached!
% 1.60/0.48 % (781031)------------------------------
% 1.60/0.48 % (781031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.48 % (781031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.48 % (781031)CaDiCaL version: 2.1.3
% 1.60/0.48 % (781031)Termination reason: Instruction limit
% 1.60/0.48 % (781031)Termination phase: Saturation
% 1.60/0.48 % (781031)Time elapsed: 0.003 s
% 1.60/0.48 % (781031)Peak memory usage: 11 MB
% 1.60/0.48 % (781031)Instructions burned: 6 (million)
% 1.60/0.48 % (781034)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1465619006:i=19:add=on:rtra=on_2998 on theBenchmark for (2998ds/19Mi)
% 1.60/0.48 % (781037)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=1433956127:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/316Mi)
% 1.60/0.48 % (781034)Refutation not found, incomplete strategy
% 1.60/0.48 % (781034)------------------------------
% 1.60/0.48 % (781034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.48 % (781034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.48 % (781034)CaDiCaL version: 2.1.3
% 1.60/0.48 % (781034)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.48 % (781034)Time elapsed: 0.007 s
% 1.60/0.48 % (781034)Peak memory usage: 12 MB
% 1.60/0.48 % (781034)Instructions burned: 13 (million)
% 1.60/0.48 % (781034)------------------------------
% 1.60/0.48 % (781034)------------------------------
% 1.60/0.48 % (781033)Instruction limit reached!
% 1.60/0.48 % (781033)------------------------------
% 1.60/0.48 % (781033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.48 % (781033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.48 % (781033)CaDiCaL version: 2.1.3
% 1.60/0.48 % (781033)Termination reason: Instruction limit
% 1.60/0.48 % (781033)Termination phase: Saturation
% 1.60/0.48 % (781033)Time elapsed: 0.012 s
% 1.60/0.48 % (781033)Peak memory usage: 12 MB
% 1.60/0.48 % (781033)Instructions burned: 23 (million)
% 1.60/0.48 % (781038)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=1118067928:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2998 on theBenchmark for (2998ds/853Mi)
% 1.60/0.48 % (781037)Refutation not found, incomplete strategy
% 1.60/0.48 % (781037)------------------------------
% 1.60/0.48 % (781037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.48 % (781037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.48 % (781037)CaDiCaL version: 2.1.3
% 1.60/0.48 % (781037)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.48 % (781037)Time elapsed: 0.008 s
% 1.60/0.48 % (781037)Peak memory usage: 12 MB
% 1.60/0.48 % (781037)Instructions burned: 28 (million)
% 1.60/0.48 % (781037)------------------------------
% 1.60/0.48 % (781037)------------------------------
% 1.60/0.48 % (781041)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=2042519715:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2998 on theBenchmark for (2998ds/45Mi)
% 1.60/0.48 % (781042)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2396890963:i=480:rtra=on_2998 on theBenchmark for (2998ds/480Mi)
% 1.60/0.48 % (781042)Refutation not found, incomplete strategy
% 1.60/0.48 % (781042)------------------------------
% 1.60/0.48 % (781042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.48 % (781042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781042)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781042)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.50 % (781042)Time elapsed: 0.004 s
% 1.60/0.50 % (781042)Peak memory usage: 12 MB
% 1.60/0.50 % (781042)Instructions burned: 5 (million)
% 1.60/0.50 % (781042)------------------------------
% 1.60/0.50 % (781042)------------------------------
% 1.60/0.50 % (781029)Refutation not found, incomplete strategy
% 1.60/0.50 % (781029)------------------------------
% 1.60/0.50 % (781029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.50 % (781029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781029)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781029)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.50 % (781029)Time elapsed: 0.036 s
% 1.60/0.50 % (781029)Peak memory usage: 12 MB
% 1.60/0.50 % (781029)Instructions burned: 71 (million)
% 1.60/0.50 % (781046)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 1.60/0.50 % (781029)------------------------------
% 1.60/0.50 % (781029)------------------------------
% 1.60/0.50 % (781045)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=702934490:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2998 on theBenchmark for (2998ds/21Mi)
% 1.60/0.50 % (781048)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2803058919:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/13Mi)
% 1.60/0.50 % (781046)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=3710862580:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/200Mi)
% 1.60/0.50 % (781051)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=465921505:i=66:s2at=3:nm=2:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/66Mi)
% 1.60/0.50 % (781046)Refutation not found, incomplete strategy
% 1.60/0.50 % (781046)------------------------------
% 1.60/0.50 % (781046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.50 % (781046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781046)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781046)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.50 % (781046)Time elapsed: 0.004 s
% 1.60/0.50 % (781046)Peak memory usage: 12 MB
% 1.60/0.50 % (781046)Instructions burned: 8 (million)
% 1.60/0.50 % (781046)------------------------------
% 1.60/0.50 % (781046)------------------------------
% 1.60/0.50 % (781038)Refutation not found, incomplete strategy
% 1.60/0.50 % (781038)------------------------------
% 1.60/0.50 % (781038)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.50 % (781038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781038)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781038)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.50 % (781038)Time elapsed: 0.024 s
% 1.60/0.50 % (781038)Peak memory usage: 13 MB
% 1.60/0.50 % (781038)Instructions burned: 41 (million)
% 1.60/0.50 % (781038)------------------------------
% 1.60/0.50 % (781038)------------------------------
% 1.60/0.50 % (781051)Refutation not found, incomplete strategy
% 1.60/0.50 % (781051)------------------------------
% 1.60/0.50 % (781051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.50 % (781051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781051)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781051)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.50 % (781051)Time elapsed: 0.003 s
% 1.60/0.50 % (781051)Peak memory usage: 13 MB
% 1.60/0.50 % (781051)Instructions burned: 10 (million)
% 1.60/0.50 % (781048)Instruction limit reached!
% 1.60/0.50 % (781048)------------------------------
% 1.60/0.50 % (781048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.50 % (781048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.50 % (781048)CaDiCaL version: 2.1.3
% 1.60/0.50 % (781048)Termination reason: Instruction limit
% 1.60/0.50 % (781048)Termination phase: Saturation
% 1.60/0.50 % (781048)Time elapsed: 0.009 s
% 1.60/0.50 % (781048)Peak memory usage: 12 MB
% 1.60/0.50 % (781048)Instructions burned: 14 (million)
% 1.60/0.50 % (781051)------------------------------
% 1.60/0.50 % (781051)------------------------------
% 1.60/0.54 % (781041)Refutation not found, incomplete strategy
% 1.60/0.54 % (781041)------------------------------
% 1.60/0.54 % (781041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.54 % (781041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.54 % (781041)CaDiCaL version: 2.1.3
% 1.60/0.54 % (781041)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.54 % (781041)Time elapsed: 0.023 s
% 1.60/0.54 % (781041)Peak memory usage: 12 MB
% 1.60/0.54 % (781041)Instructions burned: 41 (million)
% 1.60/0.54 % (781045)Instruction limit reached!
% 1.60/0.54 % (781045)------------------------------
% 1.60/0.54 % (781045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.54 % (781045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.54 % (781045)CaDiCaL version: 2.1.3
% 1.60/0.54 % (781045)Termination reason: Instruction limit
% 1.60/0.54 % (781045)Termination phase: Saturation
% 1.60/0.54 % (781045)Time elapsed: 0.013 s
% 1.60/0.54 % (781045)Peak memory usage: 12 MB
% 1.60/0.54 % (781045)Instructions burned: 24 (million)
% 1.60/0.54 % (781041)------------------------------
% 1.60/0.54 % (781041)------------------------------
% 1.60/0.54 % (781052)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=661979062:i=51:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/51Mi)
% 1.60/0.54 % (781059)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=3365605179:cond=on:i=34:hud=10:nm=10:rtra=on_2997 on theBenchmark for (2997ds/34Mi)
% 1.60/0.54 % (781057)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1793537301:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/31Mi)
% 1.60/0.54 % (781058)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=2929317758:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2997 on theBenchmark for (2997ds/137Mi)
% 1.60/0.54 % (781061)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 1.60/0.54 % (781060)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3729700734:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/67Mi)
% 1.60/0.54 % (781059)Instruction limit reached!
% 1.60/0.54 % (781059)------------------------------
% 1.60/0.54 % (781059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.54 % (781059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.54 % (781059)CaDiCaL version: 2.1.3
% 1.60/0.54 % (781059)Termination reason: Instruction limit
% 1.60/0.54 % (781059)Termination phase: Saturation
% 1.60/0.54 % (781059)Time elapsed: 0.010 s
% 1.60/0.54 % (781059)Peak memory usage: 13 MB
% 1.60/0.54 % (781059)Instructions burned: 36 (million)
% 1.60/0.54 % (781061)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=582432063:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2997 on theBenchmark for (2997ds/180Mi)
% 1.60/0.54 % (781062)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=2572997734:st=2:i=246:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/246Mi)
% 1.60/0.54 % (781058)Refutation not found, incomplete strategy
% 1.60/0.54 % (781058)------------------------------
% 1.60/0.54 % (781058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.54 % (781058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.54 % (781058)CaDiCaL version: 2.1.3
% 1.60/0.54 % (781058)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.54 % (781058)Time elapsed: 0.009 s
% 1.60/0.54 % (781058)Peak memory usage: 12 MB
% 1.60/0.54 % (781058)Instructions burned: 14 (million)
% 1.60/0.54 % (781057)Refutation not found, incomplete strategy
% 1.60/0.54 % (781057)------------------------------
% 1.60/0.54 % (781057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.60/0.54 % (781057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.60/0.54 % (781057)CaDiCaL version: 2.1.3
% 1.60/0.54 % (781057)Termination reason: Refutation not found, incomplete strategy
% 1.60/0.54 % (781057)Time elapsed: 0.010 s
% 1.60/0.54 % (781057)Peak memory usage: 12 MB
% 1.60/0.54 % (781057)Instructions burned: 19 (million)
% 1.60/0.54 % (781062)Refutation not found, incomplete strategy
% 1.60/0.54 % (781062)------------------------------
% 2.23/0.62 % (781062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.62 % (781058)------------------------------
% 2.23/0.62 % (781058)------------------------------
% 2.23/0.62 % (781062)CaDiCaL version: 2.1.3
% 2.23/0.62 % (781062)Termination reason: Refutation not found, incomplete strategy
% 2.23/0.62 % (781062)Time elapsed: 0.005 s
% 2.23/0.62 % (781062)Peak memory usage: 12 MB
% 2.23/0.62 % (781062)Instructions burned: 8 (million)
% 2.23/0.62 % (781057)------------------------------
% 2.23/0.62 % (781057)------------------------------
% 2.23/0.62 % (781062)------------------------------
% 2.23/0.62 % (781062)------------------------------
% 2.23/0.62 % (781068)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=770693180:cond=on:i=96:bd=all:rtra=on_2997 on theBenchmark for (2997ds/96Mi)
% 2.23/0.62 % (781052)Instruction limit reached!
% 2.23/0.62 % (781052)------------------------------
% 2.23/0.62 % (781052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.62 % (781052)CaDiCaL version: 2.1.3
% 2.23/0.62 % (781052)Termination reason: Instruction limit
% 2.23/0.62 % (781052)Termination phase: Saturation
% 2.23/0.62 % (781052)Time elapsed: 0.025 s
% 2.23/0.62 % (781052)Peak memory usage: 12 MB
% 2.23/0.62 % (781052)Instructions burned: 51 (million)
% 2.23/0.62 % (781068)Refutation not found, incomplete strategy
% 2.23/0.62 % (781068)------------------------------
% 2.23/0.62 % (781068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.62 % (781068)CaDiCaL version: 2.1.3
% 2.23/0.62 % (781068)Termination reason: Refutation not found, incomplete strategy
% 2.23/0.62 % (781068)Time elapsed: 0.004 s
% 2.23/0.62 % (781068)Peak memory usage: 12 MB
% 2.23/0.62 % (781068)Instructions burned: 13 (million)
% 2.23/0.62 % (781068)------------------------------
% 2.23/0.62 % (781068)------------------------------
% 2.23/0.62 % (781076)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=879090758:i=44:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/44Mi)
% 2.23/0.62 % (781071)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3342992514:i=427:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/427Mi)
% 2.23/0.62 % (781072)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2544459629:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/874Mi)
% 2.23/0.62 % (781073)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=1130194967:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/515Mi)
% 2.23/0.62 % (781075)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2936003906:st=1.5:i=130:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/130Mi)
% 2.23/0.62 % (781060)Instruction limit reached!
% 2.23/0.62 % (781060)------------------------------
% 2.23/0.62 % (781060)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.62 % (781060)CaDiCaL version: 2.1.3
% 2.23/0.62 % (781060)Termination reason: Instruction limit
% 2.23/0.62 % (781060)Termination phase: Saturation
% 2.23/0.62 % (781060)Time elapsed: 0.033 s
% 2.23/0.62 % (781060)Peak memory usage: 12 MB
% 2.23/0.62 % (781060)Instructions burned: 68 (million)
% 2.23/0.62 % (781072)Refutation not found, incomplete strategy
% 2.23/0.62 % (781072)------------------------------
% 2.23/0.62 % (781072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.23/0.62 % (781072)CaDiCaL version: 2.1.3
% 2.23/0.62 % (781072)Termination reason: Refutation not found, incomplete strategy
% 2.23/0.62 % (781072)Time elapsed: 0.005 s
% 2.23/0.62 % (781072)Peak memory usage: 12 MB
% 2.23/0.62 % (781072)Instructions burned: 9 (million)
% 2.23/0.62 % (781072)------------------------------
% 2.23/0.62 % (781072)------------------------------
% 2.23/0.62 % (781073)Refutation not found, incomplete strategy
% 2.23/0.62 % (781073)------------------------------
% 2.23/0.62 % (781073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.23/0.62 % (781073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781073)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781073)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781073)Time elapsed: 0.006 s
% 2.65/0.67 % (781073)Peak memory usage: 13 MB
% 2.65/0.67 % (781073)Instructions burned: 10 (million)
% 2.65/0.67 % (781073)------------------------------
% 2.65/0.67 % (781073)------------------------------
% 2.65/0.67 % (781076)Instruction limit reached!
% 2.65/0.67 % (781076)------------------------------
% 2.65/0.67 % (781076)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781076)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781076)Termination reason: Instruction limit
% 2.65/0.67 % (781076)Termination phase: Saturation
% 2.65/0.67 % (781076)Time elapsed: 0.013 s
% 2.65/0.67 % (781076)Peak memory usage: 12 MB
% 2.65/0.67 % (781076)Instructions burned: 46 (million)
% 2.65/0.67 % (781075)Refutation not found, incomplete strategy
% 2.65/0.67 % (781075)------------------------------
% 2.65/0.67 % (781075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781075)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781075)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781075)Time elapsed: 0.012 s
% 2.65/0.67 % (781075)Peak memory usage: 12 MB
% 2.65/0.67 % (781075)Instructions burned: 21 (million)
% 2.65/0.67 % (781075)------------------------------
% 2.65/0.67 % (781075)------------------------------
% 2.65/0.67 % (781085)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=3721982530:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2997 on theBenchmark for (2997ds/65Mi)
% 2.65/0.67 % (781082)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1500298626:s2a=on:i=571:nm=16:rtra=on_2997 on theBenchmark for (2997ds/571Mi)
% 2.65/0.67 % (781083)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=3098015665:i=450:rtra=on:ixr=off:ntd=on_2997 on theBenchmark for (2997ds/450Mi)
% 2.65/0.67 % (781084)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=3441357256:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/95Mi)
% 2.65/0.67 % (781084)Refutation not found, incomplete strategy
% 2.65/0.67 % (781084)------------------------------
% 2.65/0.67 % (781084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781084)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781084)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781084)Time elapsed: 0.007 s
% 2.65/0.67 % (781084)Peak memory usage: 12 MB
% 2.65/0.67 % (781084)Instructions burned: 13 (million)
% 2.65/0.67 % (781083)Refutation not found, incomplete strategy
% 2.65/0.67 % (781083)------------------------------
% 2.65/0.67 % (781083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781083)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781083)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781083)Time elapsed: 0.009 s
% 2.65/0.67 % (781083)Peak memory usage: 12 MB
% 2.65/0.67 % (781083)Instructions burned: 12 (million)
% 2.65/0.67 % (781084)------------------------------
% 2.65/0.67 % (781084)------------------------------
% 2.65/0.67 % (781083)------------------------------
% 2.65/0.67 % (781083)------------------------------
% 2.65/0.67 % (781086)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=309459286:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2997 on theBenchmark for (2997ds/105Mi)
% 2.65/0.67 % (781085)Instruction limit reached!
% 2.65/0.67 % (781085)------------------------------
% 2.65/0.67 % (781085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781085)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781085)Termination reason: Instruction limit
% 2.65/0.67 % (781085)Termination phase: Saturation
% 2.65/0.67 % (781085)Time elapsed: 0.017 s
% 2.65/0.67 % (781085)Peak memory usage: 12 MB
% 2.65/0.67 % (781085)Instructions burned: 66 (million)
% 2.65/0.67 % (781094)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=3886698426:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/495Mi)
% 2.65/0.67 % (781091)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=1229702377:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2997 on theBenchmark for (2997ds/5755Mi)
% 2.65/0.67 % (781092)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=740931675:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/375Mi)
% 2.65/0.67 % (781061)Instruction limit reached!
% 2.65/0.67 % (781061)------------------------------
% 2.65/0.67 % (781061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781061)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781061)Termination reason: Instruction limit
% 2.65/0.67 % (781061)Termination phase: Saturation
% 2.65/0.67 % (781061)Time elapsed: 0.083 s
% 2.65/0.67 % (781061)Peak memory usage: 13 MB
% 2.65/0.67 % (781061)Instructions burned: 181 (million)
% 2.65/0.67 % (781086)Refutation not found, incomplete strategy
% 2.65/0.67 % (781086)------------------------------
% 2.65/0.67 % (781086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781086)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781086)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781086)Time elapsed: 0.022 s
% 2.65/0.67 % (781086)Peak memory usage: 12 MB
% 2.65/0.67 % (781086)Instructions burned: 39 (million)
% 2.65/0.67 % (781086)------------------------------
% 2.65/0.67 % (781086)------------------------------
% 2.65/0.67 % (781091)Refutation not found, incomplete strategy
% 2.65/0.67 % (781091)------------------------------
% 2.65/0.67 % (781091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781091)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781091)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781091)Time elapsed: 0.012 s
% 2.65/0.67 % (781091)Peak memory usage: 13 MB
% 2.65/0.67 % (781091)Instructions burned: 19 (million)
% 2.65/0.67 % (781091)------------------------------
% 2.65/0.67 % (781091)------------------------------
% 2.65/0.67 % (781098)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=2918136944:cond=on:i=34:hud=10:nm=10:rtra=on_2996 on theBenchmark for (2996ds/34Mi)
% 2.65/0.67 % (781099)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=481635948:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/91Mi)
% 2.65/0.67 % (781100)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=377613764:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2996 on theBenchmark for (2996ds/66Mi)
% 2.65/0.67 % (781098)Instruction limit reached!
% 2.65/0.67 % (781098)------------------------------
% 2.65/0.67 % (781098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781098)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781098)Termination reason: Instruction limit
% 2.65/0.67 % (781098)Termination phase: Saturation
% 2.65/0.67 % (781098)Time elapsed: 0.019 s
% 2.65/0.67 % (781098)Peak memory usage: 13 MB
% 2.65/0.67 % (781098)Instructions burned: 35 (million)
% 2.65/0.67 % (781104)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=4290975362:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 2.65/0.67 % (781100)Instruction limit reached!
% 2.65/0.67 % (781100)------------------------------
% 2.65/0.67 % (781100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781100)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781100)Termination reason: Instruction limit
% 2.65/0.67 % (781100)Termination phase: Saturation
% 2.65/0.67 % (781100)Time elapsed: 0.036 s
% 2.65/0.67 % (781100)Peak memory usage: 12 MB
% 2.65/0.67 % (781100)Instructions burned: 67 (million)
% 2.65/0.67 % (781099)Instruction limit reached!
% 2.65/0.67 % (781099)------------------------------
% 2.65/0.67 % (781099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781099)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781099)Termination reason: Instruction limit
% 2.65/0.67 % (781099)Termination phase: Saturation
% 2.65/0.67 % (781099)Time elapsed: 0.046 s
% 2.65/0.67 % (781099)Peak memory usage: 12 MB
% 2.65/0.67 % (781099)Instructions burned: 93 (million)
% 2.65/0.67 % (781104)Instruction limit reached!
% 2.65/0.67 % (781104)------------------------------
% 2.65/0.67 % (781104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781104)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781104)Termination reason: Instruction limit
% 2.65/0.67 % (781104)Termination phase: Saturation
% 2.65/0.67 % (781104)Time elapsed: 0.012 s
% 2.65/0.67 % (781104)Peak memory usage: 12 MB
% 2.65/0.67 % (781104)Instructions burned: 22 (million)
% 2.65/0.67 % (781106)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=3431784663:i=338:bd=all:ins=4:rtra=on_2996 on theBenchmark for (2996ds/338Mi)
% 2.65/0.67 % (781108)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 2.65/0.67 % (781107)lrs+10_1_sil=128000:si=on:urr=on:random_seed=573825281:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2996 on theBenchmark for (2996ds/28Mi)
% 2.65/0.67 % (781108)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=398374706:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2996 on theBenchmark for (2996ds/137Mi)
% 2.65/0.67 % (781108)Refutation not found, incomplete strategy
% 2.65/0.67 % (781108)------------------------------
% 2.65/0.67 % (781108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781108)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781108)Termination reason: Refutation not found, incomplete strategy
% 2.65/0.67 % (781108)Time elapsed: 0.008 s
% 2.65/0.67 % (781108)Peak memory usage: 12 MB
% 2.65/0.67 % (781108)Instructions burned: 14 (million)
% 2.65/0.67 % (781108)------------------------------
% 2.65/0.67 % (781108)------------------------------
% 2.65/0.67 % (781107)Instruction limit reached!
% 2.65/0.67 % (781107)------------------------------
% 2.65/0.67 % (781107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781107)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781107)Termination reason: Instruction limit
% 2.65/0.67 % (781107)Termination phase: Saturation
% 2.65/0.67 % (781107)Time elapsed: 0.015 s
% 2.65/0.67 % (781107)Peak memory usage: 12 MB
% 2.65/0.67 % (781107)Instructions burned: 28 (million)
% 2.65/0.67 % (781094) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-780953-781094"...
% 2.65/0.67 % (781094)...printing done.
% 2.65/0.67 % (781094)Refutation found. Thanks to Tanya!
% 2.65/0.67 % SZS status Theorem for theBenchmark
% 2.65/0.67 % SZS output start Proof for theBenchmark
% 2.65/0.67 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.65/0.67 thf(func_def_0, type, in: ($i > $i > $o)).
% 2.65/0.67 thf(func_def_1, type, setunion: ($i > $i)).
% 2.65/0.67 thf(func_def_2, type, dsetconstr: ($i > ($i > $o) > $i)).
% 2.65/0.67 thf(func_def_3, type, singleton: ($i > $o)).
% 2.65/0.67 thf(func_def_4, type, iffalseProp1: $o).
% 2.65/0.67 thf(func_def_6, type, ifSingleton: $o).
% 2.65/0.67 thf(func_def_7, type, if: ($i > $o > $i > $i > $i)).
% 2.65/0.67 thf(func_def_8, type, theeq: $o).
% 2.65/0.67 thf(func_def_11, type, vOR: ($o > $o > $o)).
% 2.65/0.67 thf(func_def_12, type, vAND: ($o > $o > $o)).
% 2.65/0.67 thf(func_def_13, type, db0: !>[X0: $tType]:(X0)).
% 2.65/0.67 thf(func_def_14, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.65/0.67 thf(func_def_15, type, vNOT: ($o > $o)).
% 2.65/0.67 thf(func_def_16, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.65/0.67 thf(func_def_17, type, db3: !>[X0: $tType]:(X0)).
% 2.65/0.67 thf(func_def_18, type, db2: !>[X0: $tType]:(X0)).
% 2.65/0.67 thf(func_def_19, type, db1: !>[X0: $tType]:(X0)).
% 2.65/0.67 thf(func_def_23, type, sK3: $o).
% 2.65/0.67 thf(func_def_26, type, sK6: $o).
% 2.65/0.67 thf(func_def_30, type, sK10: $o).
% 2.65/0.67 thf(func_def_35, type, sK15: ($o > $i)).
% 2.65/0.67 thf(func_def_36, type, sK16: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_37, type, sK17: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_38, type, sK18: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_39, type, sK19: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_40, type, sK20: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_41, type, sK21: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_42, type, sK22: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_43, type, sK23: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_44, type, sK24: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_45, type, sK25: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_46, type, sK26: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_47, type, sK27: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_48, type, sK28: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_49, type, sK29: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_50, type, sK30: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_51, type, sK31: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_52, type, sK32: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_53, type, sK33: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_54, type, sK34: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_55, type, sK35: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_56, type, sK36: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_57, type, sK37: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_58, type, sK38: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_59, type, sK39: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_60, type, sK40: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_61, type, sK41: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_62, type, sK42: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_63, type, sK43: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_64, type, sK44: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_65, type, sK45: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_66, type, sK46: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_67, type, sK47: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_68, type, sK48: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_69, type, sK49: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_70, type, sK50: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_71, type, sK51: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_72, type, sK52: ($o > $i)).
% 2.65/0.67 thf(func_def_73, type, sK53: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_74, type, sK54: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_75, type, sK55: ($o > $o > $i)).
% 2.65/0.67 thf(func_def_76, type, sK56: ($o > $i)).
% 2.65/0.67 thf(f1,axiom,(
% 2.65/0.67 (iffalseProp1 = ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (~X1 => (in @ X3 @ (dsetconstr @ X0 @ (^[X4 : $i] : ((~X1 & (X4 = X3)) | (X1 & (X4 = X2))))))))))),
% 2.65/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',iffalseProp1)).
% 2.65/0.67 thf(f2,axiom,(
% 2.65/0.67 (ifSingleton = ! [X2 : $i,X1 : $o,X0 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (singleton @ (dsetconstr @ X0 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | (X1 & (X4 = X2)))))))))),
% 2.65/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ifSingleton)).
% 2.65/0.67 thf(f3,axiom,(
% 2.65/0.67 (if = (^[X0 : $i, X1 : $o, X2 : $i, X3 : $i] : ((setunion @ (dsetconstr @ X0 @ (^[X4 : $i] : ((~X1 & (X4 = X3)) | ((X4 = X2) & X1))))))))),
% 2.65/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',if)).
% 2.65/0.67 thf(f4,axiom,(
% 2.65/0.67 (theeq = ! [X0 : $i] : ((singleton @ X0) => ! [X1 : $i] : ((in @ X1 @ X0) => (((setunion @ X0)) = X1))))),
% 2.65/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',theeq)).
% 2.65/0.67 thf(f5,conjecture,(
% 2.65/0.67 iffalseProp1 => (ifSingleton => (theeq => ! [X1 : $o,X2 : $i,X0 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (~X1 => (((if @ X0 @ X1 @ X2 @ X3)) = X3))))))),
% 2.65/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p',iffalse)).
% 2.65/0.67 thf(f6,negated_conjecture,(
% 2.65/0.67 ~(iffalseProp1 => (ifSingleton => (theeq => ! [X1 : $o,X2 : $i,X0 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (~X1 => (((if @ X0 @ X1 @ X2 @ X3)) = X3)))))))),
% 2.65/0.67 inference(negated_conjecture,[status(cth)],[f5])).
% 2.65/0.67 thf(f7,plain,(
% 2.65/0.67 (iffalseProp1 = ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X2 @ X0) => ! [X3 : $i] : ((in @ X3 @ X0) => (~X1 => (in @ X3 @ (dsetconstr @ X0 @ (^[X4 : $i] : ((~X1 & (X4 = X3)) | (X1 & (X4 = X2))))))))))),
% 2.65/0.67 inference(rectify,[],[f1])).
% 2.65/0.67 thf(f8,plain,(
% 2.65/0.67 (iffalseProp1 = $true) <=> ! [X0 : $i,X1 : $o,X2 : $i] : ((((in @ X2 @ X0)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => (~ ($true = X1) => ($true = ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))))))),
% 2.65/0.67 inference(fool_elimination,[],[f7])).
% 2.65/0.67 thf(f9,plain,(
% 2.65/0.67 ~(iffalseProp1 => (ifSingleton => (theeq => ! [X0 : $o,X1 : $i,X2 : $i] : ((in @ X1 @ X2) => ! [X3 : $i] : ((in @ X3 @ X2) => (~X0 => (((if @ X2 @ X0 @ X1 @ X3)) = X3)))))))),
% 2.65/0.67 inference(rectify,[],[f6])).
% 2.65/0.67 thf(f10,plain,(
% 2.65/0.67 ~((iffalseProp1 = $true) => ((ifSingleton = $true) => ((theeq = $true) => ! [X0 : $o,X1 : $i,X2 : $i] : ((((in @ X1 @ X2)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X2)) = $true) => (~ ($true = X0) => (((if @ X2 @ X0 @ X1 @ X3)) = X3)))))))),
% 2.65/0.67 inference(fool_elimination,[],[f9])).
% 2.65/0.67 thf(f11,plain,(
% 2.65/0.67 (ifSingleton = ! [X0 : $i,X1 : $o,X2 : $i] : ((in @ X0 @ X2) => ! [X3 : $i] : ((in @ X3 @ X2) => (singleton @ (dsetconstr @ X2 @ (^[X4 : $i] : (((X4 = X3) & ~X1) | (X1 & (X0 = X4)))))))))),
% 2.65/0.67 inference(rectify,[],[f2])).
% 2.65/0.67 thf(f12,plain,(
% 2.65/0.67 ! [X0 : $i,X2 : $i,X1 : $o] : (($true = ((in @ X0 @ X2))) => ! [X3 : $i] : ((((in @ X3 @ X2)) = $true) => (((singleton @ (dsetconstr @ X2 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (X3 = Y0))))))) = $true))) <=> (ifSingleton = $true)),
% 2.65/0.67 inference(fool_elimination,[],[f11])).
% 2.65/0.67 thf(f13,plain,(
% 2.65/0.67 (theeq = ! [X0 : $i] : ((singleton @ X0) => ! [X1 : $i] : ((in @ X1 @ X0) => (((setunion @ X0)) = X1))))),
% 2.65/0.67 inference(rectify,[],[f4])).
% 2.65/0.67 thf(f14,plain,(
% 2.65/0.67 (theeq = $true) <=> ! [X0 : $i] : ((((singleton @ X0)) = $true) => ! [X1 : $i] : ((((in @ X1 @ X0)) = $true) => (((setunion @ X0)) = X1)))),
% 2.65/0.67 inference(fool_elimination,[],[f13])).
% 2.65/0.67 thf(f15,plain,(
% 2.65/0.67 (if = (^[X0 : $i, X1 : $o, X2 : $i, X3 : $i] : ((setunion @ (dsetconstr @ X0 @ (^[X4 : $i] : ((~X1 & (X4 = X3)) | ((X4 = X2) & X1))))))))),
% 2.65/0.67 inference(rectify,[],[f3])).
% 2.65/0.67 thf(f16,plain,(
% 2.65/0.67 (if = (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((Y3 = Y4) & (~ Y1))))))))))))))),
% 2.65/0.67 inference(fool_elimination,[],[f15])).
% 2.65/0.67 thf(f17,plain,(
% 2.65/0.67 (iffalseProp1 = $true) <=> ! [X2 : $i,X0 : $i,X1 : $o] : ((((in @ X2 @ X0)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X0)) = $true) => (($true != X1) => ($true = ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))))))),
% 2.65/0.67 inference(flattening,[],[f8])).
% 2.65/0.67 thf(f18,plain,(
% 2.65/0.67 ~((iffalseProp1 = $true) => ((ifSingleton = $true) => ((theeq = $true) => ! [X1 : $i,X0 : $o,X2 : $i] : ((((in @ X1 @ X2)) = $true) => ! [X3 : $i] : ((((in @ X3 @ X2)) = $true) => (($true != X0) => (((if @ X2 @ X0 @ X1 @ X3)) = X3)))))))),
% 2.65/0.67 inference(flattening,[],[f10])).
% 2.65/0.67 thf(f19,plain,(
% 2.65/0.67 (iffalseProp1 = $true) <=> ! [X2 : $i,X0 : $i,X1 : $o] : (! [X3 : $i] : ((($true = ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))) | ($true = X1)) | (((in @ X3 @ X0)) != $true)) | (((in @ X2 @ X0)) != $true))),
% 2.65/0.67 inference(ennf_transformation,[],[f17])).
% 2.65/0.67 thf(f20,plain,(
% 2.65/0.67 ! [X1 : $o,X0 : $i,X2 : $i] : ((((in @ X2 @ X0)) != $true) | ! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | ($true = X1) | ($true = ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))))) <=> (iffalseProp1 = $true)),
% 2.65/0.67 inference(flattening,[],[f19])).
% 2.65/0.67 thf(f21,plain,(
% 2.65/0.67 ! [X0 : $i] : (! [X1 : $i] : ((((setunion @ X0)) = X1) | (((in @ X1 @ X0)) != $true)) | (((singleton @ X0)) != $true)) <=> (theeq = $true)),
% 2.65/0.67 inference(ennf_transformation,[],[f14])).
% 2.65/0.67 thf(f22,plain,(
% 2.65/0.67 ((? [X1 : $i,X0 : $o,X2 : $i] : (? [X3 : $i] : (((((if @ X2 @ X0 @ X1 @ X3)) != X3) & ($true != X0)) & (((in @ X3 @ X2)) = $true)) & (((in @ X1 @ X2)) = $true)) & (theeq = $true)) & (ifSingleton = $true)) & (iffalseProp1 = $true)),
% 2.65/0.67 inference(ennf_transformation,[],[f18])).
% 2.65/0.67 thf(f23,plain,(
% 2.65/0.67 (iffalseProp1 = $true) & (ifSingleton = $true) & ? [X0 : $o,X2 : $i,X1 : $i] : (? [X3 : $i] : ((((in @ X3 @ X2)) = $true) & ($true != X0) & (((if @ X2 @ X0 @ X1 @ X3)) != X3)) & (((in @ X1 @ X2)) = $true)) & (theeq = $true)),
% 2.65/0.67 inference(flattening,[],[f22])).
% 2.65/0.67 thf(f24,plain,(
% 2.65/0.67 (ifSingleton = $true) <=> ! [X0 : $i,X1 : $o,X2 : $i] : (! [X3 : $i] : ((((singleton @ (dsetconstr @ X2 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (X3 = Y0))))))) = $true) | (((in @ X3 @ X2)) != $true)) | ($true != ((in @ X0 @ X2))))),
% 2.65/0.67 inference(ennf_transformation,[],[f12])).
% 2.65/0.67 thf(f25,plain,(
% 2.65/0.67 (! [X0 : $i] : (! [X1 : $i] : ((((setunion @ X0)) = X1) | (((in @ X1 @ X0)) != $true)) | (((singleton @ X0)) != $true)) | (theeq != $true)) & ((theeq = $true) | ? [X0 : $i] : (? [X1 : $i] : ((((setunion @ X0)) != X1) & (((in @ X1 @ X0)) = $true)) & (((singleton @ X0)) = $true)))),
% 2.65/0.67 inference(nnf_transformation,[],[f21])).
% 2.65/0.67 thf(f26,plain,(
% 2.65/0.67 (! [X0 : $i] : (! [X1 : $i] : ((((setunion @ X0)) = X1) | (((in @ X1 @ X0)) != $true)) | (((singleton @ X0)) != $true)) | (theeq != $true)) & ((theeq = $true) | ? [X2 : $i] : (? [X3 : $i] : ((((setunion @ X2)) != X3) & (((in @ X3 @ X2)) = $true)) & ($true = ((singleton @ X2)))))),
% 2.65/0.67 inference(rectify,[],[f25])).
% 2.65/0.67 thf(f27,plain,(
% 2.65/0.67 (! [X0 : $i] : (! [X1 : $i] : ((((setunion @ X0)) = X1) | (((in @ X1 @ X0)) != $true)) | (((singleton @ X0)) != $true)) | (theeq != $true)) & ((theeq = $true) | (((((setunion @ sK0)) != sK1) & ($true = ((in @ sK1 @ sK0)))) & ($true = ((singleton @ sK0)))))),
% 2.65/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X2,sK0),skolemize(X3,sK1)],[f26])).
% 2.65/0.67 thf(f28,plain,(
% 2.65/0.67 ((ifSingleton = $true) | ? [X0 : $i,X1 : $o,X2 : $i] : (? [X3 : $i] : ((((singleton @ (dsetconstr @ X2 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (X3 = Y0))))))) != $true) & (((in @ X3 @ X2)) = $true)) & ($true = ((in @ X0 @ X2))))) & (! [X0 : $i,X1 : $o,X2 : $i] : (! [X3 : $i] : ((((singleton @ (dsetconstr @ X2 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (X3 = Y0))))))) = $true) | (((in @ X3 @ X2)) != $true)) | ($true != ((in @ X0 @ X2)))) | (ifSingleton != $true))),
% 2.65/0.67 inference(nnf_transformation,[],[f24])).
% 2.65/0.67 thf(f29,plain,(
% 2.65/0.67 ((ifSingleton = $true) | ? [X0 : $i,X1 : $o,X2 : $i] : (? [X3 : $i] : ((((singleton @ (dsetconstr @ X2 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (X3 = Y0))))))) != $true) & (((in @ X3 @ X2)) = $true)) & ($true = ((in @ X0 @ X2))))) & (! [X4 : $i,X5 : $o,X6 : $i] : (! [X7 : $i] : ((((singleton @ (dsetconstr @ X6 @ (^[Y0 : $i]: (((X4 = Y0) & X5) | ((~ X5) & (X7 = Y0))))))) = $true) | ($true != ((in @ X7 @ X6)))) | ($true != ((in @ X4 @ X6)))) | (ifSingleton != $true))),
% 2.65/0.67 inference(rectify,[],[f28])).
% 2.65/0.67 thf(f30,plain,(
% 2.65/0.67 ((ifSingleton = $true) | ((($true != ((singleton @ (dsetconstr @ sK4 @ (^[Y0 : $i]: (((sK2 = Y0) & sK3) | ((~ sK3) & (sK5 = Y0)))))))) & ($true = ((in @ sK5 @ sK4)))) & ($true = ((in @ sK2 @ sK4))))) & (! [X4 : $i,X5 : $o,X6 : $i] : (! [X7 : $i] : ((((singleton @ (dsetconstr @ X6 @ (^[Y0 : $i]: (((X4 = Y0) & X5) | ((~ X5) & (X7 = Y0))))))) = $true) | ($true != ((in @ X7 @ X6)))) | ($true != ((in @ X4 @ X6)))) | (ifSingleton != $true))),
% 2.65/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f29])).
% 2.65/0.67 thf(f31,plain,(
% 2.65/0.67 (! [X1 : $o,X0 : $i,X2 : $i] : ((((in @ X2 @ X0)) != $true) | ! [X3 : $i] : ((((in @ X3 @ X0)) != $true) | ($true = X1) | ($true = ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))))) | (iffalseProp1 != $true)) & ((iffalseProp1 = $true) | ? [X1 : $o,X0 : $i,X2 : $i] : ((((in @ X2 @ X0)) = $true) & ? [X3 : $i] : ((((in @ X3 @ X0)) = $true) & ($true != X1) & ($true != ((in @ X3 @ (dsetconstr @ X0 @ (^[Y0 : $i]: (((X2 = Y0) & X1) | ((X3 = Y0) & (~ X1)))))))))))),
% 2.65/0.67 inference(nnf_transformation,[],[f20])).
% 2.65/0.67 thf(f32,plain,(
% 2.65/0.67 (! [X0 : $o,X1 : $i,X2 : $i] : (($true != ((in @ X2 @ X1))) | ! [X3 : $i] : ((((in @ X3 @ X1)) != $true) | ($true = X0) | ($true = ((in @ X3 @ (dsetconstr @ X1 @ (^[Y0 : $i]: (((X2 = Y0) & X0) | ((X3 = Y0) & (~ X0)))))))))) | (iffalseProp1 != $true)) & ((iffalseProp1 = $true) | ? [X4 : $o,X5 : $i,X6 : $i] : (($true = ((in @ X6 @ X5))) & ? [X7 : $i] : (($true = ((in @ X7 @ X5))) & ($true != X4) & ($true != ((in @ X7 @ (dsetconstr @ X5 @ (^[Y0 : $i]: (((X6 = Y0) & X4) | ((X7 = Y0) & (~ X4)))))))))))),
% 2.65/0.67 inference(rectify,[],[f31])).
% 2.65/0.67 thf(f33,plain,(
% 2.65/0.67 (! [X0 : $o,X1 : $i,X2 : $i] : (($true != ((in @ X2 @ X1))) | ! [X3 : $i] : ((((in @ X3 @ X1)) != $true) | ($true = X0) | ($true = ((in @ X3 @ (dsetconstr @ X1 @ (^[Y0 : $i]: (((X2 = Y0) & X0) | ((X3 = Y0) & (~ X0)))))))))) | (iffalseProp1 != $true)) & ((iffalseProp1 = $true) | ((((in @ sK8 @ sK7)) = $true) & (($true = ((in @ sK9 @ sK7))) & ($true != sK6) & ($true != ((in @ sK9 @ (dsetconstr @ sK7 @ (^[Y0 : $i]: (((sK8 = Y0) & sK6) | ((sK9 = Y0) & (~ sK6)))))))))))),
% 2.65/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK8,sK9]),skolemize(X4,sK6),skolemize(X5,sK7),skolemize(X6,sK8),skolemize(X7,sK9)],[f32])).
% 2.65/0.67 thf(f34,plain,(
% 2.65/0.67 (iffalseProp1 = $true) & (ifSingleton = $true) & ? [X0 : $o,X1 : $i,X2 : $i] : (? [X3 : $i] : ((((in @ X3 @ X1)) = $true) & ($true != X0) & (((if @ X1 @ X0 @ X2 @ X3)) != X3)) & ($true = ((in @ X2 @ X1)))) & (theeq = $true)),
% 2.65/0.67 inference(rectify,[],[f23])).
% 2.65/0.67 thf(f35,plain,(
% 2.65/0.67 (iffalseProp1 = $true) & (ifSingleton = $true) & (((((in @ sK13 @ sK11)) = $true) & (sK10 != $true) & (((if @ sK11 @ sK10 @ sK12 @ sK13)) != sK13)) & (((in @ sK12 @ sK11)) = $true)) & (theeq = $true)),
% 2.65/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK10,sK11,sK12,sK13]),skolemize(X0,sK10),skolemize(X1,sK11),skolemize(X2,sK12),skolemize(X3,sK13)],[f34])).
% 2.65/0.67 thf(f39,plain,(
% 2.65/0.67 ( ! [X0 : $i,X1 : $i] : ((((setunion @ X0)) = X1) | (((in @ X1 @ X0)) != $true) | (((singleton @ X0)) != $true) | (theeq != $true)) )),
% 2.65/0.67 inference(cnf_transformation,[],[f27])).
% 2.65/0.67 thf(f40,plain,(
% 2.65/0.67 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $o] : ((((singleton @ (dsetconstr @ X6 @ (^[Y0 : $i]: (((X4 = Y0) & X5) | ((~ X5) & (X7 = Y0))))))) = $true) | ($true != ((in @ X7 @ X6))) | ($true != ((in @ X4 @ X6))) | (ifSingleton != $true)) )),
% 2.65/0.67 inference(cnf_transformation,[],[f30])).
% 2.65/0.67 thf(f48,plain,(
% 2.65/0.67 ( ! [X2 : $i,X3 : $i,X0 : $o,X1 : $i] : (($true != ((in @ X2 @ X1))) | (((in @ X3 @ X1)) != $true) | ($true = X0) | ($true = ((in @ X3 @ (dsetconstr @ X1 @ (^[Y0 : $i]: (((X2 = Y0) & X0) | ((X3 = Y0) & (~ X0)))))))) | (iffalseProp1 != $true)) )),
% 2.65/0.67 inference(cnf_transformation,[],[f33])).
% 2.65/0.67 thf(f49,plain,(
% 2.65/0.67 (theeq = $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f50,plain,(
% 2.65/0.67 (((in @ sK12 @ sK11)) = $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f51,plain,(
% 2.65/0.67 (((if @ sK11 @ sK10 @ sK12 @ sK13)) != sK13)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f52,plain,(
% 2.65/0.67 (sK10 != $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f53,plain,(
% 2.65/0.67 (((in @ sK13 @ sK11)) = $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f54,plain,(
% 2.65/0.67 (ifSingleton = $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f55,plain,(
% 2.65/0.67 (iffalseProp1 = $true)),
% 2.65/0.67 inference(cnf_transformation,[],[f35])).
% 2.65/0.67 thf(f56,plain,(
% 2.65/0.67 (if = (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((Y3 = Y4) & (~ Y1))))))))))))))),
% 2.65/0.67 inference(cnf_transformation,[],[f16])).
% 2.65/0.67 thf(f58,definition,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.65/0.67 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.65/0.67 thf(f59,plain,(
% 2.65/0.67 ( ! [X0 : $i,X1 : $i] : (($true != $true) | (((singleton @ X0)) != $true) | (((in @ X1 @ X0)) != $true) | (((setunion @ X0)) = X1)) )),
% 2.65/0.67 inference(definition_unfolding,[],[f39,f49])).
% 2.65/0.67 thf(f66,plain,(
% 2.65/0.67 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $o] : (($true != $true) | ($true != ((in @ X7 @ X6))) | ($true != ((in @ X4 @ X6))) | (((singleton @ (dsetconstr @ X6 @ (^[Y0 : $i]: (((X4 = Y0) & X5) | ((~ X5) & (X7 = Y0))))))) = $true)) )),
% 2.65/0.67 inference(definition_unfolding,[],[f40,f54])).
% 2.65/0.67 thf(f67,plain,(
% 2.65/0.67 ( ! [X2 : $i,X3 : $i,X0 : $o,X1 : $i] : (($true != $true) | (((in @ X3 @ X1)) != $true) | ($true = ((in @ X3 @ (dsetconstr @ X1 @ (^[Y0 : $i]: (((X2 = Y0) & X0) | ((X3 = Y0) & (~ X0)))))))) | ($true = X0) | ($true != ((in @ X2 @ X1)))) )),
% 2.65/0.67 inference(definition_unfolding,[],[f48,f55])).
% 2.65/0.67 thf(f72,plain,(
% 2.65/0.67 (sK13 != (((^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $i]: ((^[Y3 : $i]: (setunion @ (dsetconstr @ Y0 @ (^[Y4 : $i]: ((Y1 & (Y2 = Y4)) | ((Y3 = Y4) & (~ Y1))))))))))))) @ sK11 @ sK10 @ sK12 @ sK13)))),
% 2.65/0.67 inference(definition_unfolding,[],[f51,f56])).
% 2.65/0.67 thf(f73,plain,(
% 2.65/0.67 ( ! [X6 : $i,X7 : $i,X4 : $i,X5 : $o] : (($true != ((in @ X7 @ X6))) | (((singleton @ (dsetconstr @ X6 @ (^[Y0 : $i]: (((X4 = Y0) & X5) | ((~ X5) & (X7 = Y0))))))) = $true) | ($true != ((in @ X4 @ X6)))) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f66])).
% 2.65/0.67 thf(f74,plain,(
% 2.65/0.67 ( ! [X2 : $i,X3 : $i,X0 : $o,X1 : $i] : (($true != ((in @ X2 @ X1))) | ($true = X0) | (((in @ X3 @ X1)) != $true) | ($true = ((in @ X3 @ (dsetconstr @ X1 @ (^[Y0 : $i]: (((X2 = Y0) & X0) | ((X3 = Y0) & (~ X0))))))))) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f67])).
% 2.65/0.67 thf(f75,plain,(
% 2.65/0.67 ( ! [X0 : $i,X1 : $i] : ((((in @ X1 @ X0)) != $true) | (((singleton @ X0)) != $true) | (((setunion @ X0)) = X1)) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f59])).
% 2.65/0.67 thf(f76,plain,(
% 2.65/0.67 (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10))))))) != sK13)),
% 2.65/0.67 inference(beta-eta_normalization,[],[f72])).
% 2.65/0.67 thf(f92,plain,(
% 2.65/0.67 ( ! [X0 : $i,X1 : $o] : (($true != $true) | (((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (sK12 = Y0))))))) = $true) | ($true != ((in @ X0 @ sK11)))) )),
% 2.65/0.67 inference(constrained_superposition,[],[f73,f50])).
% 2.65/0.67 thf(f94,plain,(
% 2.65/0.67 ( ! [X0 : $i,X1 : $o] : (($true != ((in @ X0 @ sK11))) | (((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((X0 = Y0) & X1) | ((~ X1) & (sK12 = Y0))))))) = $true)) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f92])).
% 2.65/0.67 thf(f101,plain,(
% 2.65/0.67 (sK10 = $false) | ($true != $true)),
% 2.65/0.67 inference(constrained_superposition,[],[f52,f58])).
% 2.65/0.67 thf(f104,plain,(
% 2.65/0.67 (sK10 = $false)),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f101])).
% 2.65/0.67 thf(f113,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $i] : (($true != $true) | ($true = X0) | (((in @ X1 @ sK11)) != $true) | ($true = ((in @ X1 @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((X1 = Y0) & (~ X0))))))))) )),
% 2.65/0.67 inference(constrained_superposition,[],[f74,f50])).
% 2.65/0.67 thf(f116,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $i] : ((((in @ X1 @ sK11)) != $true) | ($true = X0) | ($true = ((in @ X1 @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((X1 = Y0) & (~ X0))))))))) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f113])).
% 2.65/0.67 thf(f123,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = ((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK13 = Y0) & X0) | ((~ X0) & (sK12 = Y0)))))))) | ($true != $true)) )),
% 2.65/0.67 inference(constrained_superposition,[],[f94,f53])).
% 2.65/0.67 thf(f126,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = ((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK13 = Y0) & X0) | ((~ X0) & (sK12 = Y0))))))))) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f123])).
% 2.65/0.67 thf(f140,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = ((in @ sK13 @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))))))) | ($true != $true) | ($true = X0)) )),
% 2.65/0.67 inference(constrained_superposition,[],[f116,f53])).
% 2.65/0.67 thf(f141,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = ((in @ sK13 @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))))))) | ($true = X0)) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f140])).
% 2.65/0.67 thf(f243,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ($true != $true) | ($true != ((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))))))) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(constrained_superposition,[],[f75,f141])).
% 2.65/0.67 thf(f246,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true != ((singleton @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))))))) | ($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f243])).
% 2.65/0.67 thf(f325,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true != $true) | ($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ((^[Y0 : $i]: (((sK13 = Y0) & X1) | ((~ X1) & (sK12 = Y0)))) != (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))))) )),
% 2.65/0.67 inference(constrained_superposition,[],[f246,f126])).
% 2.65/0.67 thf(f330,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (((^[Y0 : $i]: (((sK13 = Y0) & X1) | ((~ X1) & (sK12 = Y0)))) != (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))) | ($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f325])).
% 2.65/0.67 thf(f871,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ((((^[Y0 : $i]: (((sK13 = Y0) & X1) | ((~ X1) & (sK12 = Y0)))) @ (sK16 @ X1 @ X0))) != (((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK16 @ X1 @ X0))))) )),
% 2.65/0.67 inference(negative_extensionality,[],[f330])).
% 2.65/0.67 thf(f872,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = (((^[Y0 : $i]: (((sK13 = Y0) & X1) | ((~ X1) & (sK12 = Y0)))) @ (sK16 @ X1 @ X0)))) | ($true = (((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK16 @ X1 @ X0))))) )),
% 2.65/0.67 inference(xor_proxy_clausification,[],[f871])).
% 2.65/0.67 thf(f873,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ((((^[Y0 : $i]: (((sK13 = Y0) & X1) | ((~ X1) & (sK12 = Y0)))) @ (sK16 @ X1 @ X0))) = $false) | ($true = X0) | ((((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK16 @ X1 @ X0))) = $false)) )),
% 2.65/0.67 inference(xor_proxy_clausification,[],[f871])).
% 2.65/0.67 thf(f874,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | (((((sK13 = (sK16 @ X1 @ X0)) & X1) | ((~ X1) & (sK12 = (sK16 @ X1 @ X0))))) = $false) | ($true = X0) | (((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0)))) = $false)) )),
% 2.65/0.67 inference(beta-eta_normalization,[],[f873])).
% 2.65/0.67 thf(f876,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (((((sK13 = (sK16 @ X1 @ X0)) & X1)) = $false) | ($true = X0) | (((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0)))) = $false) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(or_proxy_clausification,[],[f874])).
% 2.65/0.67 thf(f877,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($false = X1) | (((sK13 = (sK16 @ X1 @ X0))) = $false) | ($true = X0) | (((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0)))) = $false) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f876])).
% 2.65/0.67 thf(f878,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | (((sK16 @ X1 @ X0)) != sK13) | ($false = X1) | (((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0)))) = $false)) )),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f877])).
% 2.65/0.67 thf(f879,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | (((sK16 @ X1 @ X0)) != sK13) | ((((sK13 = (sK16 @ X1 @ X0)) & (~ X0))) = $false) | ($false = X1)) )),
% 2.65/0.67 inference(or_proxy_clausification,[],[f878])).
% 2.65/0.67 thf(f883,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) != sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($false = X1) | (((sK13 = (sK16 @ X1 @ X0))) = $false) | (((~ X0)) = $false) | ($true = X0)) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f879])).
% 2.65/0.67 thf(f884,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((~ X0)) = $false) | (((sK16 @ X1 @ X0)) != sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0) | (((sK16 @ X1 @ X0)) != sK13) | ($false = X1)) )),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f883])).
% 2.65/0.67 thf(f885,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) != sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | (((sK16 @ X1 @ X0)) != sK13) | ($true = X0) | ($true = X0) | ($false = X1)) )),
% 2.65/0.67 inference(not_proxy_clausification,[],[f884])).
% 2.65/0.67 thf(f886,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) != sK13) | ($false = X1) | ($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(duplicate_literal_removal,[],[f885])).
% 2.65/0.67 thf(f902,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = ((((sK13 = (sK16 @ X1 @ X0)) & X1) | ((~ X1) & (sK12 = (sK16 @ X1 @ X0)))))) | ($true = ((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0)))))) )),
% 2.65/0.67 inference(beta-eta_normalization,[],[f872])).
% 2.65/0.67 thf(f903,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = ((((sK12 = (sK16 @ X1 @ X0)) & X0) | ((sK13 = (sK16 @ X1 @ X0)) & (~ X0))))) | ($true = X0) | ((((sK13 = (sK16 @ X1 @ X0)) & X1)) = $true) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0))))) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(or_proxy_clausification,[],[f902])).
% 2.65/0.67 thf(f904,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = (((sK12 = (sK16 @ X1 @ X0)) & X0))) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0))))) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ((((sK13 = (sK16 @ X1 @ X0)) & (~ X0))) = $true) | ($true = X0) | ((((sK13 = (sK16 @ X1 @ X0)) & X1)) = $true)) )),
% 2.65/0.67 inference(or_proxy_clausification,[],[f903])).
% 2.65/0.67 thf(f905,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (((((sK13 = (sK16 @ X1 @ X0)) & X1)) = $true) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0) | ($true = X0) | ((((sK13 = (sK16 @ X1 @ X0)) & (~ X0))) = $true) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0)))))) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f904])).
% 2.65/0.67 thf(f943,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (((((sK13 = (sK16 @ X1 @ X0)) & (~ X0))) = $true) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0) | ($true = X0) | (((sK13 = (sK16 @ X1 @ X0))) = $true) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0)))))) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f905])).
% 2.65/0.67 thf(f945,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | (((sK13 = (sK16 @ X1 @ X0))) = $true) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0))))) | ($true = X0) | (((sK13 = (sK16 @ X1 @ X0))) = $true)) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f943])).
% 2.65/0.67 thf(f946,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) = sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = (((~ X1) & (sK12 = (sK16 @ X1 @ X0))))) | ($true = X0) | (((sK16 @ X1 @ X0)) = sK13) | ($true = X0)) )),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f945])).
% 2.65/0.67 thf(f948,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) = sK13) | (((~ X1)) = $true) | ($true = X0) | (((sK16 @ X1 @ X0)) = sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0)) )),
% 2.65/0.67 inference(and_proxy_clausification,[],[f946])).
% 2.65/0.67 thf(f949,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : ((((sK16 @ X1 @ X0)) = sK13) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0) | ($false = X1) | ($true = X0) | (((sK16 @ X1 @ X0)) = sK13)) )),
% 2.65/0.67 inference(not_proxy_clausification,[],[f948])).
% 2.65/0.67 thf(f950,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($false = X1) | (((sK16 @ X1 @ X0)) = sK13) | ($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13)) )),
% 2.65/0.67 inference(duplicate_literal_removal,[],[f949])).
% 2.65/0.67 thf(f981,plain,(
% 2.65/0.67 ( ! [X0 : $o,X1 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($false = X1)) )),
% 2.65/0.67 inference(forward_subsumption_resolution,[],[f950,f886])).
% 2.65/0.67 thf(f984,definition,(
% 2.65/0.67 spl14_6 <=> ! [X1 : $o] : ($false = X1)),
% 2.65/0.67 introduced(definition,[new_symbols(definition,[spl14_6])],[avatar_definition])).
% 2.65/0.67 thf(f985,plain,(
% 2.65/0.67 ( ! [X1 : $o] : (($false = X1)) ) | ~spl14_6),
% 2.65/0.67 inference(avatar_component_clause,[],[f984])).
% 2.65/0.67 thf(f987,definition,(
% 2.65/0.67 spl14_7 <=> ! [X0 : $o] : (($true = X0) | (((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13))),
% 2.65/0.67 introduced(definition,[new_symbols(definition,[spl14_7])],[avatar_definition])).
% 2.65/0.67 thf(f988,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((setunion @ (dsetconstr @ sK11 @ (^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0))))))) = sK13) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(avatar_component_clause,[],[f987])).
% 2.65/0.67 thf(f989,plain,(
% 2.65/0.67 spl14_6 | spl14_7),
% 2.65/0.67 inference(avatar_split_clause,[],[f981,f987,f984])).
% 2.65/0.67 thf(f991,plain,(
% 2.65/0.67 ($true = $false) | ~spl14_6),
% 2.65/0.67 inference(constrained_superposition,[],[f50,f985])).
% 2.65/0.67 thf(f1055,plain,(
% 2.65/0.67 $false | ~spl14_6),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f991])).
% 2.65/0.67 thf(f1056,plain,(
% 2.65/0.67 ~spl14_6),
% 2.65/0.67 inference(avatar_contradiction_clause,[],[f1055])).
% 2.65/0.67 thf(f1608,definition,(
% 2.65/0.67 spl14_11 <=> ! [X1 : $o] : ($true = X1)),
% 2.65/0.67 introduced(definition,[new_symbols(definition,[spl14_11])],[avatar_definition])).
% 2.65/0.67 thf(f1609,plain,(
% 2.65/0.67 ( ! [X1 : $o] : (($true = X1)) ) | ~spl14_11),
% 2.65/0.67 inference(avatar_component_clause,[],[f1608])).
% 2.65/0.67 thf(f1727,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) != (^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10))))) | (sK13 != sK13) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(constrained_superposition,[],[f76,f988])).
% 2.65/0.67 thf(f1729,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) != (^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10))))) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f1727])).
% 2.65/0.67 thf(f1993,plain,(
% 2.65/0.67 ($true = $false) | ~spl14_11),
% 2.65/0.67 inference(constrained_superposition,[],[f104,f1609])).
% 2.65/0.67 thf(f2012,plain,(
% 2.65/0.67 $false | ~spl14_11),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f1993])).
% 2.65/0.67 thf(f2013,plain,(
% 2.65/0.67 ~spl14_11),
% 2.65/0.67 inference(avatar_contradiction_clause,[],[f2012])).
% 2.65/0.67 thf(f5811,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK56 @ X0))) != (((^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10)))) @ (sK56 @ X0)))) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(negative_extensionality,[],[f1729])).
% 2.65/0.67 thf(f5812,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ((((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK56 @ X0))) = $true) | ($true = (((^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10)))) @ (sK56 @ X0))))) ) | ~spl14_7),
% 2.65/0.67 inference(xor_proxy_clausification,[],[f5811])).
% 2.65/0.67 thf(f5813,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((((^[Y0 : $i]: ((sK10 & (sK12 = Y0)) | ((sK13 = Y0) & (~ sK10)))) @ (sK56 @ X0))) = $false) | ((((^[Y0 : $i]: (((sK12 = Y0) & X0) | ((sK13 = Y0) & (~ X0)))) @ (sK56 @ X0))) = $false) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(xor_proxy_clausification,[],[f5811])).
% 2.65/0.67 thf(f5814,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((((sK10 & (sK12 = (sK56 @ X0))) | ((sK13 = (sK56 @ X0)) & (~ sK10)))) = $false) | ($true = X0) | (((((sK12 = (sK56 @ X0)) & X0) | ((sK13 = (sK56 @ X0)) & (~ X0)))) = $false)) ) | ~spl14_7),
% 2.65/0.67 inference(beta-eta_normalization,[],[f5813])).
% 2.65/0.67 thf(f5815,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((((sK12 = (sK56 @ X0)) & X0) | ((sK13 = (sK56 @ X0)) & (~ X0)))) = $false) | ((((sK13 = (sK56 @ X0)) & (~ sK10))) = $false) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(or_proxy_clausification,[],[f5814])).
% 2.65/0.67 thf(f5830,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((((sK13 = (sK56 @ X0)) & (~ X0))) = $false) | ($true = X0) | ((((sK13 = (sK56 @ X0)) & (~ sK10))) = $false)) ) | ~spl14_7),
% 2.65/0.67 inference(or_proxy_clausification,[],[f5815])).
% 2.65/0.67 thf(f5837,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($false = ((sK13 = (sK56 @ X0)))) | (((~ X0)) = $false) | ($true = X0) | ((((sK13 = (sK56 @ X0)) & (~ sK10))) = $false)) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5830])).
% 2.65/0.67 thf(f5838,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((sK56 @ X0)) != sK13) | ((((sK13 = (sK56 @ X0)) & (~ sK10))) = $false) | (((~ X0)) = $false) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f5837])).
% 2.65/0.67 thf(f5839,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($false = ((sK13 = (sK56 @ X0)))) | (((~ X0)) = $false) | (((~ sK10)) = $false) | ($true = X0) | (((sK56 @ X0)) != sK13)) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5838])).
% 2.65/0.67 thf(f5840,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | (((sK56 @ X0)) != sK13) | (((~ X0)) = $false) | (((~ sK10)) = $false) | (((sK56 @ X0)) != sK13)) ) | ~spl14_7),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f5839])).
% 2.65/0.67 thf(f5841,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((sK56 @ X0)) != sK13) | (((sK56 @ X0)) != sK13) | ($true = X0) | ($true = X0) | (((~ sK10)) = $false)) ) | ~spl14_7),
% 2.65/0.67 inference(not_proxy_clausification,[],[f5840])).
% 2.65/0.67 thf(f5842,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((sK10 = $true) | ($true = X0) | ($true = X0) | (((sK56 @ X0)) != sK13) | (((sK56 @ X0)) != sK13)) ) | ~spl14_7),
% 2.65/0.67 inference(not_proxy_clausification,[],[f5841])).
% 2.65/0.67 thf(f5843,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((sK10 = $true) | (((sK56 @ X0)) != sK13) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(duplicate_literal_removal,[],[f5842])).
% 2.65/0.67 thf(f5844,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | (((((sK12 = (sK56 @ X0)) & X0) | ((sK13 = (sK56 @ X0)) & (~ X0)))) = $true) | ((((sK10 & (sK12 = (sK56 @ X0))) | ((sK13 = (sK56 @ X0)) & (~ sK10)))) = $true)) ) | ~spl14_7),
% 2.65/0.67 inference(beta-eta_normalization,[],[f5812])).
% 2.65/0.67 thf(f5845,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ($true = (((sK12 = (sK56 @ X0)) & X0))) | ((((sK13 = (sK56 @ X0)) & (~ X0))) = $true) | ((((sK10 & (sK12 = (sK56 @ X0))) | ((sK13 = (sK56 @ X0)) & (~ sK10)))) = $true)) ) | ~spl14_7),
% 2.65/0.67 inference(or_proxy_clausification,[],[f5844])).
% 2.65/0.67 thf(f5846,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ($true = X0) | ((((sK13 = (sK56 @ X0)) & (~ X0))) = $true) | ((((sK10 & (sK12 = (sK56 @ X0))) | ((sK13 = (sK56 @ X0)) & (~ sK10)))) = $true)) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5845])).
% 2.65/0.67 thf(f5886,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (((((sK10 & (sK12 = (sK56 @ X0))) | ((sK13 = (sK56 @ X0)) & (~ sK10)))) = $true) | ($true = ((sK13 = (sK56 @ X0)))) | ($true = X0) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5846])).
% 2.65/0.67 thf(f5887,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | (((sK10 & (sK12 = (sK56 @ X0)))) = $true) | ($true = ((sK13 = (sK56 @ X0)))) | ($true = X0) | ($true = (((sK13 = (sK56 @ X0)) & (~ sK10))))) ) | ~spl14_7),
% 2.65/0.67 inference(or_proxy_clausification,[],[f5886])).
% 2.65/0.67 thf(f5889,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((sK10 = $true) | ($true = X0) | ($true = X0) | ($true = ((sK13 = (sK56 @ X0)))) | ($true = (((sK13 = (sK56 @ X0)) & (~ sK10))))) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5887])).
% 2.65/0.67 thf(f5890,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((sK10 = $true) | ($true = X0) | ($true = X0) | (((sK56 @ X0)) = sK13) | ($true = (((sK13 = (sK56 @ X0)) & (~ sK10))))) ) | ~spl14_7),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f5889])).
% 2.65/0.67 thf(f5892,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | ($true = ((sK13 = (sK56 @ X0)))) | (((sK56 @ X0)) = sK13) | ($true = X0) | (sK10 = $true)) ) | ~spl14_7),
% 2.65/0.67 inference(and_proxy_clausification,[],[f5890])).
% 2.65/0.67 thf(f5893,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((sK10 = $true) | (((sK56 @ X0)) = sK13) | ($true = X0) | ($true = X0) | (((sK56 @ X0)) = sK13)) ) | ~spl14_7),
% 2.65/0.67 inference(equality_proxy_clausification,[],[f5892])).
% 2.65/0.67 thf(f5894,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((sK56 @ X0)) = sK13) | ($true = X0) | (sK10 = $true)) ) | ~spl14_7),
% 2.65/0.67 inference(duplicate_literal_removal,[],[f5893])).
% 2.65/0.67 thf(f5924,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = $false) | (((sK56 @ X0)) != sK13) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(forward_demodulation,[],[f5843,f104])).
% 2.65/0.67 thf(f5925,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0) | (((sK56 @ X0)) != sK13)) ) | ~spl14_7),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f5924])).
% 2.65/0.67 thf(f5928,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((sK56 @ X0)) = sK13) | ($true = X0) | ($true = $false)) ) | ~spl14_7),
% 2.65/0.67 inference(forward_demodulation,[],[f5894,f104])).
% 2.65/0.67 thf(f5929,plain,(
% 2.65/0.67 ( ! [X0 : $o] : ((((sK56 @ X0)) = sK13) | ($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(trivial_inequality_removal,[],[f5928])).
% 2.65/0.67 thf(f5930,plain,(
% 2.65/0.67 ( ! [X0 : $o] : (($true = X0)) ) | ~spl14_7),
% 2.65/0.67 inference(forward_subsumption_resolution,[],[f5929,f5925])).
% 2.65/0.67 thf(f5931,plain,(
% 2.65/0.67 spl14_11 | ~spl14_7),
% 2.65/0.67 inference(avatar_split_clause,[],[f5930,f987,f1608])).
% 2.65/0.67 cnf(s4, plain, spl14_6 | spl14_7, inference(sat_conversion,[],[f989])).
% 2.65/0.67 cnf(s11, plain, ~spl14_6, inference(sat_conversion,[],[f1056])).
% 2.65/0.67 cnf(s18, plain, ~spl14_11, inference(sat_conversion,[],[f2013])).
% 2.65/0.67 cnf(s37, plain, ~spl14_7 | spl14_11, inference(sat_conversion,[],[f5931])).
% 2.65/0.67 cnf(s38, plain, ~spl14_7, inference(rat,[],[s37,s18])).
% 2.65/0.67 cnf(s49, plain, $false, inference(rat,[],[s4,s38,s11])).
% 2.65/0.67 thf(f5932,plain,(
% 2.65/0.67 $false),
% 2.65/0.67 inference(avatar_sat_refutation,[],[s49])).
% 2.65/0.67 % SZS output end Proof for theBenchmark
% 2.65/0.67 % (781094)------------------------------
% 2.65/0.67 % (781094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.65/0.67 % (781094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.65/0.67 % (781094)CaDiCaL version: 2.1.3
% 2.65/0.67 % (781094)Termination reason: Refutation
% 2.65/0.67 % (781094)Time elapsed: 0.116 s
% 2.65/0.67 % (781094)Peak memory usage: 15 MB
% 2.65/0.67 % (781094)Instructions burned: 461 (million)
% 2.65/0.67 % (780953)Success in time 0.43 s
% 2.65/0.67 % Vampire exiting
%------------------------------------------------------------------------------