%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU558^2 : TPTP v9.3.1. Bugfixed v4.0.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:04 AM UTC 2026
% Result : Theorem 3.52s 0.89s
% Output : Refutation 3.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU558^2 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.18 % Computer : n006.cluster.edu
% 0.10/0.18 % Model : x86_64 x86_64
% 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.18 % Memory : 8046.5625MB
% 0.10/0.18 % OS : Linux 6.8.0-71-generic
% 0.10/0.18 % CPULimit : 300
% 0.10/0.18 % WCLimit : 300
% 0.10/0.18 % DateTime : Tue Sep 29 13:49:54 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 Running higher-order theorem proving
% 0.10/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.21/0.37 % (750550)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.37 % (750558)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=3683937647: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.21/0.37 % (750561)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.37 % (750561)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.21/0.37 % (750556)lrs+10_16_si=on:nwc=1.5:random_seed=100704999:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.37 % (750555)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=257354834:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.37 % (750557)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3065731605:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.37 % (750560)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=2395106878:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.37 % (750559)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=441668738:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.37 % (750561)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=1447155971:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.37 % (750557)Refutation not found, incomplete strategy
% 0.21/0.37 % (750557)------------------------------
% 0.21/0.37 % (750557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (750557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (750557)CaDiCaL version: 2.1.3
% 0.21/0.37 % (750557)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.37 % (750557)Time elapsed: 0.002 s
% 0.21/0.37 % (750557)Peak memory usage: 12 MB
% 0.21/0.37 % (750557)Instructions burned: 4 (million)
% 0.21/0.37 % (750557)------------------------------
% 0.21/0.37 % (750557)------------------------------
% 0.21/0.37 % (750556)Instruction limit reached!
% 0.21/0.37 % (750556)------------------------------
% 0.21/0.37 % (750556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (750556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (750556)CaDiCaL version: 2.1.3
% 0.21/0.37 % (750556)Termination reason: Instruction limit
% 0.21/0.37 % (750556)Termination phase: Saturation
% 0.21/0.37 % (750556)Time elapsed: 0.011 s
% 0.21/0.37 % (750556)Peak memory usage: 12 MB
% 0.21/0.37 % (750556)Instructions burned: 20 (million)
% 0.21/0.37 % (750559)Instruction limit reached!
% 0.21/0.37 % (750559)------------------------------
% 0.21/0.37 % (750559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (750559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (750559)CaDiCaL version: 2.1.3
% 0.21/0.37 % (750559)Termination reason: Instruction limit
% 0.21/0.37 % (750559)Termination phase: Saturation
% 0.21/0.37 % (750559)Time elapsed: 0.014 s
% 0.21/0.37 % (750559)Peak memory usage: 12 MB
% 0.21/0.37 % (750559)Instructions burned: 25 (million)
% 0.21/0.37 % (750569)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1443482121:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.37 % (750569)Instruction limit reached!
% 0.21/0.37 % (750569)------------------------------
% 0.21/0.37 % (750569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.37 % (750569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.37 % (750569)CaDiCaL version: 2.1.3
% 0.21/0.37 % (750569)Termination reason: Instruction limit
% 0.21/0.37 % (750569)Termination phase: Saturation
% 0.21/0.37 % (750569)Time elapsed: 0.002 s
% 0.21/0.37 % (750569)Peak memory usage: 12 MB
% 0.21/0.37 % (750569)Instructions burned: 3 (million)
% 0.21/0.37 % (750571)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.97/0.41 % (750571)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2715232738:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.97/0.41 % (750571)Instruction limit reached!
% 0.97/0.41 % (750571)------------------------------
% 0.97/0.41 % (750571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.41 % (750571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.41 % (750571)CaDiCaL version: 2.1.3
% 0.97/0.41 % (750571)Termination reason: Instruction limit
% 0.97/0.41 % (750571)Termination phase: Saturation
% 0.97/0.41 % (750571)Time elapsed: 0.004 s
% 0.97/0.41 % (750571)Peak memory usage: 12 MB
% 0.97/0.41 % (750571)Instructions burned: 7 (million)
% 0.97/0.41 % (750570)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3137889372:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.97/0.41 % (750560)Instruction limit reached!
% 0.97/0.41 % (750560)------------------------------
% 0.97/0.41 % (750560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.41 % (750560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.41 % (750560)CaDiCaL version: 2.1.3
% 0.97/0.41 % (750560)Termination reason: Instruction limit
% 0.97/0.41 % (750560)Termination phase: Saturation
% 0.97/0.41 % (750560)Time elapsed: 0.040 s
% 0.97/0.41 % (750560)Peak memory usage: 13 MB
% 0.97/0.41 % (750560)Instructions burned: 75 (million)
% 0.97/0.41 % (750555)Instruction limit reached!
% 0.97/0.41 % (750555)------------------------------
% 0.97/0.41 % (750555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.41 % (750555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.41 % (750555)CaDiCaL version: 2.1.3
% 0.97/0.41 % (750555)Termination reason: Instruction limit
% 0.97/0.41 % (750555)Termination phase: Saturation
% 0.97/0.41 % (750555)Time elapsed: 0.045 s
% 0.97/0.41 % (750555)Peak memory usage: 12 MB
% 0.97/0.41 % (750555)Instructions burned: 88 (million)
% 0.97/0.41 % (750570)Instruction limit reached!
% 0.97/0.41 % (750570)------------------------------
% 0.97/0.41 % (750570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.41 % (750570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.41 % (750570)CaDiCaL version: 2.1.3
% 0.97/0.41 % (750570)Termination reason: Instruction limit
% 0.97/0.41 % (750570)Termination phase: Saturation
% 0.97/0.41 % (750570)Time elapsed: 0.005 s
% 0.97/0.41 % (750570)Peak memory usage: 12 MB
% 0.97/0.41 % (750570)Instructions burned: 5 (million)
% 0.97/0.41 % (750573)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2399467915:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.97/0.41 % (750575)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.97/0.41 % (750575)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.97/0.41 % (750573)Instruction limit reached!
% 0.97/0.41 % (750573)------------------------------
% 0.97/0.41 % (750573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.41 % (750573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.41 % (750573)CaDiCaL version: 2.1.3
% 0.97/0.41 % (750573)Termination reason: Instruction limit
% 0.97/0.41 % (750573)Termination phase: Saturation
% 0.97/0.41 % (750573)Time elapsed: 0.007 s
% 0.97/0.41 % (750573)Peak memory usage: 12 MB
% 0.97/0.41 % (750573)Instructions burned: 13 (million)
% 0.97/0.41 % (750575)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=2920209269: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.97/0.41 % (750577)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=1633723368:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.97/0.41 % (750579)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.97/0.41 % (750578)lrs+10_1_si=on:cs=on:random_seed=928611406:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.97/0.45 % (750579)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=3836591256:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.97/0.45 % (750579)Instruction limit reached!
% 0.97/0.45 % (750579)------------------------------
% 0.97/0.45 % (750579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750579)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750579)Termination reason: Instruction limit
% 0.97/0.45 % (750579)Termination phase: Saturation
% 0.97/0.45 % (750579)Time elapsed: 0.002 s
% 0.97/0.45 % (750579)Peak memory usage: 12 MB
% 0.97/0.45 % (750579)Instructions burned: 3 (million)
% 0.97/0.45 % (750578)Instruction limit reached!
% 0.97/0.45 % (750578)------------------------------
% 0.97/0.45 % (750578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750578)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750578)Termination reason: Instruction limit
% 0.97/0.45 % (750578)Termination phase: Saturation
% 0.97/0.45 % (750578)Time elapsed: 0.007 s
% 0.97/0.45 % (750578)Peak memory usage: 12 MB
% 0.97/0.45 % (750578)Instructions burned: 15 (million)
% 0.97/0.45 % (750575)Instruction limit reached!
% 0.97/0.45 % (750575)------------------------------
% 0.97/0.45 % (750575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750575)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750575)Termination reason: Instruction limit
% 0.97/0.45 % (750575)Termination phase: Saturation
% 0.97/0.45 % (750575)Time elapsed: 0.015 s
% 0.97/0.45 % (750575)Peak memory usage: 12 MB
% 0.97/0.45 % (750575)Instructions burned: 29 (million)
% 0.97/0.45 % (750581)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1315865110:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.97/0.45 % (750581)Refutation not found, incomplete strategy
% 0.97/0.45 % (750581)------------------------------
% 0.97/0.45 % (750581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750581)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750581)Termination reason: Refutation not found, incomplete strategy
% 0.97/0.45 % (750581)Time elapsed: 0.003 s
% 0.97/0.45 % (750581)Peak memory usage: 12 MB
% 0.97/0.45 % (750581)Instructions burned: 5 (million)
% 0.97/0.45 % (750581)------------------------------
% 0.97/0.45 % (750581)------------------------------
% 0.97/0.45 % (750577)Refutation not found, incomplete strategy
% 0.97/0.45 % (750577)------------------------------
% 0.97/0.45 % (750577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750577)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750577)Termination reason: Refutation not found, incomplete strategy
% 0.97/0.45 % (750577)Time elapsed: 0.022 s
% 0.97/0.45 % (750577)Peak memory usage: 12 MB
% 0.97/0.45 % (750577)Instructions burned: 41 (million)
% 0.97/0.45 % (750577)------------------------------
% 0.97/0.45 % (750577)------------------------------
% 0.97/0.45 % (750561)Instruction limit reached!
% 0.97/0.45 % (750561)------------------------------
% 0.97/0.45 % (750561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.97/0.45 % (750561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.97/0.45 % (750561)CaDiCaL version: 2.1.3
% 0.97/0.45 % (750561)Termination reason: Instruction limit
% 0.97/0.45 % (750561)Termination phase: Saturation
% 0.97/0.45 % (750561)Time elapsed: 0.081 s
% 0.97/0.45 % (750561)Peak memory usage: 13 MB
% 0.97/0.45 % (750561)Instructions burned: 157 (million)
% 0.97/0.45 % (750588)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=754615:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 0.97/0.45 % (750590)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1690656703:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 0.97/0.45 % (750592)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=438485678:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.49 % (750596)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2217133075:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.52/0.49 % (750592)Instruction limit reached!
% 1.52/0.49 % (750592)------------------------------
% 1.52/0.49 % (750592)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.49 % (750592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.49 % (750592)CaDiCaL version: 2.1.3
% 1.52/0.49 % (750592)Termination reason: Instruction limit
% 1.52/0.49 % (750592)Termination phase: Saturation
% 1.52/0.49 % (750592)Time elapsed: 0.008 s
% 1.52/0.49 % (750592)Peak memory usage: 12 MB
% 1.52/0.49 % (750592)Instructions burned: 14 (million)
% 1.52/0.49 % (750599)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=478594771:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.49 % (750600)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1554235706:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.52/0.49 % (750600)Instruction limit reached!
% 1.52/0.49 % (750600)------------------------------
% 1.52/0.49 % (750600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.49 % (750600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.49 % (750600)CaDiCaL version: 2.1.3
% 1.52/0.49 % (750600)Termination reason: Instruction limit
% 1.52/0.49 % (750600)Termination phase: Saturation
% 1.52/0.49 % (750600)Time elapsed: 0.002 s
% 1.52/0.49 % (750600)Peak memory usage: 12 MB
% 1.52/0.49 % (750600)Instructions burned: 3 (million)
% 1.52/0.49 % (750590)Instruction limit reached!
% 1.52/0.49 % (750590)------------------------------
% 1.52/0.49 % (750590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.49 % (750590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.49 % (750590)CaDiCaL version: 2.1.3
% 1.52/0.49 % (750590)Termination reason: Instruction limit
% 1.52/0.49 % (750590)Termination phase: Saturation
% 1.52/0.49 % (750590)Time elapsed: 0.015 s
% 1.52/0.49 % (750590)Peak memory usage: 12 MB
% 1.52/0.49 % (750590)Instructions burned: 25 (million)
% 1.52/0.49 % (750599)Instruction limit reached!
% 1.52/0.49 % (750599)------------------------------
% 1.52/0.49 % (750599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.49 % (750599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.49 % (750599)CaDiCaL version: 2.1.3
% 1.52/0.49 % (750599)Termination reason: Instruction limit
% 1.52/0.49 % (750599)Termination phase: Saturation
% 1.52/0.49 % (750599)Time elapsed: 0.009 s
% 1.52/0.49 % (750599)Peak memory usage: 12 MB
% 1.52/0.49 % (750599)Instructions burned: 15 (million)
% 1.52/0.49 % (750616)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3302861593:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.52/0.49 % (750617)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=4064819661:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.52/0.49 % (750622)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.52/0.49 % (750622)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.52/0.49 % (750621)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=186716486:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.52/0.49 % (750622)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=4004946696:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.52/0.49 % (750617)Instruction limit reached!
% 1.52/0.49 % (750617)------------------------------
% 1.52/0.49 % (750617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.49 % (750617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750617)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750617)Termination reason: Instruction limit
% 1.52/0.54 % (750617)Termination phase: Saturation
% 1.52/0.54 % (750617)Time elapsed: 0.013 s
% 1.52/0.54 % (750617)Peak memory usage: 12 MB
% 1.52/0.54 % (750617)Instructions burned: 23 (million)
% 1.52/0.54 % (750622)Instruction limit reached!
% 1.52/0.54 % (750622)------------------------------
% 1.52/0.54 % (750622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750622)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750622)Termination reason: Instruction limit
% 1.52/0.54 % (750622)Termination phase: Saturation
% 1.52/0.54 % (750622)Time elapsed: 0.007 s
% 1.52/0.54 % (750622)Peak memory usage: 12 MB
% 1.52/0.54 % (750622)Instructions burned: 14 (million)
% 1.52/0.54 % (750616)Instruction limit reached!
% 1.52/0.54 % (750616)------------------------------
% 1.52/0.54 % (750616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750616)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750616)Termination reason: Instruction limit
% 1.52/0.54 % (750616)Termination phase: Saturation
% 1.52/0.54 % (750616)Time elapsed: 0.015 s
% 1.52/0.54 % (750616)Peak memory usage: 12 MB
% 1.52/0.54 % (750616)Instructions burned: 27 (million)
% 1.52/0.54 % (750639)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 1.52/0.54 % (750639)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=284077219:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.52/0.54 % (750641)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=3286696492:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 1.52/0.54 % (750642)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=99066939:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 1.52/0.54 % (750639)Instruction limit reached!
% 1.52/0.54 % (750639)------------------------------
% 1.52/0.54 % (750639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750639)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750639)Termination reason: Instruction limit
% 1.52/0.54 % (750639)Termination phase: Saturation
% 1.52/0.54 % (750639)Time elapsed: 0.005 s
% 1.52/0.54 % (750639)Peak memory usage: 12 MB
% 1.52/0.54 % (750639)Instructions burned: 8 (million)
% 1.52/0.54 % (750621)Instruction limit reached!
% 1.52/0.54 % (750621)------------------------------
% 1.52/0.54 % (750621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750621)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750621)Termination reason: Instruction limit
% 1.52/0.54 % (750621)Termination phase: Saturation
% 1.52/0.54 % (750621)Time elapsed: 0.034 s
% 1.52/0.54 % (750621)Peak memory usage: 12 MB
% 1.52/0.54 % (750621)Instructions burned: 60 (million)
% 1.52/0.54 % (750642)Instruction limit reached!
% 1.52/0.54 % (750642)------------------------------
% 1.52/0.54 % (750642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750642)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750642)Termination reason: Instruction limit
% 1.52/0.54 % (750642)Termination phase: Saturation
% 1.52/0.54 % (750642)Time elapsed: 0.005 s
% 1.52/0.54 % (750642)Peak memory usage: 12 MB
% 1.52/0.54 % (750642)Instructions burned: 9 (million)
% 1.52/0.54 % (750558)Instruction limit reached!
% 1.52/0.54 % (750558)------------------------------
% 1.52/0.54 % (750558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.52/0.54 % (750558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.52/0.54 % (750558)CaDiCaL version: 2.1.3
% 1.52/0.54 % (750558)Termination reason: Instruction limit
% 1.52/0.54 % (750558)Termination phase: Saturation
% 1.52/0.54 % (750558)Time elapsed: 0.174 s
% 1.52/0.54 % (750558)Peak memory usage: 15 MB
% 1.52/0.54 % (750558)Instructions burned: 634 (million)
% 1.52/0.54 % (750641)Instruction limit reached!
% 2.27/0.62 % (750641)------------------------------
% 2.27/0.62 % (750641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.62 % (750641)CaDiCaL version: 2.1.3
% 2.27/0.62 % (750641)Termination reason: Instruction limit
% 2.27/0.62 % (750641)Termination phase: Saturation
% 2.27/0.62 % (750641)Time elapsed: 0.016 s
% 2.27/0.62 % (750641)Peak memory usage: 12 MB
% 2.27/0.62 % (750641)Instructions burned: 31 (million)
% 2.27/0.62 % (750660)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=2133385156:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.27/0.62 % (750654)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1252704612:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.27/0.62 % (750656)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=2214085801:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.27/0.62 % (750657)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3887528373:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.27/0.62 % (750654)Instruction limit reached!
% 2.27/0.62 % (750654)------------------------------
% 2.27/0.62 % (750654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.62 % (750654)CaDiCaL version: 2.1.3
% 2.27/0.62 % (750654)Termination reason: Instruction limit
% 2.27/0.62 % (750654)Termination phase: Saturation
% 2.27/0.62 % (750654)Time elapsed: 0.009 s
% 2.27/0.62 % (750654)Peak memory usage: 12 MB
% 2.27/0.62 % (750654)Instructions burned: 23 (million)
% 2.27/0.62 % (750663)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1851593104:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.27/0.62 % (750656)Instruction limit reached!
% 2.27/0.62 % (750656)------------------------------
% 2.27/0.62 % (750656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.62 % (750656)CaDiCaL version: 2.1.3
% 2.27/0.62 % (750656)Termination reason: Instruction limit
% 2.27/0.62 % (750656)Termination phase: Saturation
% 2.27/0.62 % (750656)Time elapsed: 0.012 s
% 2.27/0.62 % (750656)Peak memory usage: 12 MB
% 2.27/0.62 % (750656)Instructions burned: 21 (million)
% 2.27/0.62 % (750676)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1881760556:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.27/0.62 % (750680)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.27/0.62 % (750588)Instruction limit reached!
% 2.27/0.62 % (750588)------------------------------
% 2.27/0.62 % (750588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.62 % (750588)CaDiCaL version: 2.1.3
% 2.27/0.62 % (750588)Termination reason: Instruction limit
% 2.27/0.62 % (750588)Termination phase: Saturation
% 2.27/0.62 % (750588)Time elapsed: 0.122 s
% 2.27/0.62 % (750588)Peak memory usage: 13 MB
% 2.27/0.62 % (750588)Instructions burned: 251 (million)
% 2.27/0.62 % (750680)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2116041575:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.27/0.62 % (750680)Instruction limit reached!
% 2.27/0.62 % (750680)------------------------------
% 2.27/0.62 % (750680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.27/0.62 % (750680)CaDiCaL version: 2.1.3
% 2.27/0.62 % (750680)Termination reason: Instruction limit
% 2.27/0.62 % (750680)Termination phase: Saturation
% 2.27/0.62 % (750680)Time elapsed: 0.004 s
% 2.27/0.62 % (750680)Peak memory usage: 12 MB
% 2.27/0.62 % (750680)Instructions burned: 8 (million)
% 2.27/0.62 % (750660)Instruction limit reached!
% 2.27/0.62 % (750660)------------------------------
% 2.27/0.62 % (750660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.27/0.62 % (750660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750660)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750660)Termination reason: Instruction limit
% 2.58/0.69 % (750660)Termination phase: Saturation
% 2.58/0.69 % (750660)Time elapsed: 0.040 s
% 2.58/0.69 % (750660)Peak memory usage: 13 MB
% 2.58/0.69 % (750660)Instructions burned: 143 (million)
% 2.58/0.69 % (750696)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.58/0.69 % (750692)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2259075378:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.58/0.69 % (750696)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=3463871691:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.58/0.69 % (750676)Instruction limit reached!
% 2.58/0.69 % (750676)------------------------------
% 2.58/0.69 % (750676)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.69 % (750676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750676)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750676)Termination reason: Instruction limit
% 2.58/0.69 % (750676)Termination phase: Saturation
% 2.58/0.69 % (750676)Time elapsed: 0.023 s
% 2.58/0.69 % (750676)Peak memory usage: 12 MB
% 2.58/0.69 % (750676)Instructions burned: 43 (million)
% 2.58/0.69 % (750696)Instruction limit reached!
% 2.58/0.69 % (750696)------------------------------
% 2.58/0.69 % (750696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.69 % (750696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750696)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750696)Termination reason: Instruction limit
% 2.58/0.69 % (750696)Termination phase: Saturation
% 2.58/0.69 % (750696)Time elapsed: 0.002 s
% 2.58/0.69 % (750696)Peak memory usage: 12 MB
% 2.58/0.69 % (750696)Instructions burned: 7 (million)
% 2.58/0.69 % (750695)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=1527396818:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.58/0.69 % (750706)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1218303528:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.58/0.69 % (750706)Instruction limit reached!
% 2.58/0.69 % (750706)------------------------------
% 2.58/0.69 % (750706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.69 % (750706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750706)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750706)Termination reason: Instruction limit
% 2.58/0.69 % (750706)Termination phase: Saturation
% 2.58/0.69 % (750706)Time elapsed: 0.006 s
% 2.58/0.69 % (750706)Peak memory usage: 12 MB
% 2.58/0.69 % (750706)Instructions burned: 22 (million)
% 2.58/0.69 % (750705)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=888464922:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.58/0.69 % (750596)Instruction limit reached!
% 2.58/0.69 % (750596)------------------------------
% 2.58/0.69 % (750596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.69 % (750596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750596)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750596)Termination reason: Instruction limit
% 2.58/0.69 % (750596)Termination phase: Saturation
% 2.58/0.69 % (750596)Time elapsed: 0.162 s
% 2.58/0.69 % (750596)Peak memory usage: 13 MB
% 2.58/0.69 % (750596)Instructions burned: 334 (million)
% 2.58/0.69 % (750714)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=2352706339:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.58/0.69 % (750705)Instruction limit reached!
% 2.58/0.69 % (750705)------------------------------
% 2.58/0.69 % (750705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.58/0.69 % (750705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.58/0.69 % (750705)CaDiCaL version: 2.1.3
% 2.58/0.69 % (750705)Termination reason: Instruction limit
% 2.58/0.69 % (750705)Termination phase: Saturation
% 2.86/0.78 % (750705)Time elapsed: 0.013 s
% 2.86/0.78 % (750705)Peak memory usage: 12 MB
% 2.86/0.78 % (750705)Instructions burned: 24 (million)
% 2.86/0.78 % (750721)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=868159384:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 2.86/0.78 % (750724)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=1382652852:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2997 on theBenchmark for (2997ds/45Mi)
% 2.86/0.78 % (750663)Instruction limit reached!
% 2.86/0.78 % (750663)------------------------------
% 2.86/0.78 % (750663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.78 % (750663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.78 % (750663)CaDiCaL version: 2.1.3
% 2.86/0.78 % (750663)Termination reason: Instruction limit
% 2.86/0.78 % (750663)Termination phase: Saturation
% 2.86/0.78 % (750663)Time elapsed: 0.096 s
% 2.86/0.78 % (750663)Peak memory usage: 13 MB
% 2.86/0.78 % (750663)Instructions burned: 194 (million)
% 2.86/0.78 % (750736)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3574853401:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 2.86/0.78 % (750724)Instruction limit reached!
% 2.86/0.78 % (750724)------------------------------
% 2.86/0.78 % (750724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.78 % (750724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.78 % (750724)CaDiCaL version: 2.1.3
% 2.86/0.78 % (750724)Termination reason: Instruction limit
% 2.86/0.78 % (750724)Termination phase: Saturation
% 2.86/0.78 % (750724)Time elapsed: 0.028 s
% 2.86/0.78 % (750724)Peak memory usage: 12 MB
% 2.86/0.78 % (750724)Instructions burned: 46 (million)
% 2.86/0.78 % (750692)Instruction limit reached!
% 2.86/0.78 % (750692)------------------------------
% 2.86/0.78 % (750692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.78 % (750692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.78 % (750692)CaDiCaL version: 2.1.3
% 2.86/0.78 % (750692)Termination reason: Instruction limit
% 2.86/0.78 % (750692)Termination phase: Saturation
% 2.86/0.78 % (750692)Time elapsed: 0.089 s
% 2.86/0.78 % (750692)Peak memory usage: 13 MB
% 2.86/0.78 % (750692)Instructions burned: 181 (million)
% 2.86/0.78 % (750695)Instruction limit reached!
% 2.86/0.78 % (750695)------------------------------
% 2.86/0.78 % (750695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.78 % (750695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.78 % (750695)CaDiCaL version: 2.1.3
% 2.86/0.78 % (750695)Termination reason: Instruction limit
% 2.86/0.78 % (750695)Termination phase: Saturation
% 2.86/0.78 % (750695)Time elapsed: 0.083 s
% 2.86/0.78 % (750695)Peak memory usage: 12 MB
% 2.86/0.78 % (750695)Instructions burned: 169 (million)
% 2.86/0.78 % (750743)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=3785018664:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 2.86/0.78 % (750747)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 2.86/0.78 % (750747)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2482319789:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 2.86/0.78 % (750749)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=1870099711:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 2.86/0.78 % (750743)Instruction limit reached!
% 2.86/0.78 % (750743)------------------------------
% 2.86/0.78 % (750743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.86/0.78 % (750743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.86/0.78 % (750743)CaDiCaL version: 2.1.3
% 2.86/0.78 % (750743)Termination reason: Instruction limit
% 2.86/0.78 % (750743)Termination phase: Saturation
% 2.86/0.78 % (750743)Time elapsed: 0.012 s
% 2.86/0.78 % (750743)Peak memory usage: 12 MB
% 2.86/0.78 % (750743)Instructions burned: 22 (million)
% 2.86/0.78 % (750714)Instruction limit reached!
% 3.52/0.89 % (750714)------------------------------
% 3.52/0.89 % (750714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750714)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750714)Termination reason: Instruction limit
% 3.52/0.89 % (750714)Termination phase: Saturation
% 3.52/0.89 % (750714)Time elapsed: 0.083 s
% 3.52/0.89 % (750714)Peak memory usage: 13 MB
% 3.52/0.89 % (750714)Instructions burned: 320 (million)
% 3.52/0.89 % (750749)Instruction limit reached!
% 3.52/0.89 % (750749)------------------------------
% 3.52/0.89 % (750749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750749)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750749)Termination reason: Instruction limit
% 3.52/0.89 % (750749)Termination phase: Saturation
% 3.52/0.89 % (750749)Time elapsed: 0.007 s
% 3.52/0.89 % (750749)Peak memory usage: 12 MB
% 3.52/0.89 % (750749)Instructions burned: 13 (million)
% 3.52/0.89 % (750762)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=2967251025:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.52/0.89 % (750761)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=1282204690:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.52/0.89 % (750763)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=1799762454:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/31Mi)
% 3.52/0.89 % (750762)Instruction limit reached!
% 3.52/0.89 % (750762)------------------------------
% 3.52/0.89 % (750762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750762)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750762)Termination reason: Instruction limit
% 3.52/0.89 % (750762)Termination phase: Saturation
% 3.52/0.89 % (750762)Time elapsed: 0.015 s
% 3.52/0.89 % (750762)Peak memory usage: 12 MB
% 3.52/0.89 % (750762)Instructions burned: 53 (million)
% 3.52/0.89 % (750777)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=3958193998:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.52/0.89 % (750763)Instruction limit reached!
% 3.52/0.89 % (750763)------------------------------
% 3.52/0.89 % (750763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750763)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750763)Termination reason: Instruction limit
% 3.52/0.89 % (750763)Termination phase: Saturation
% 3.52/0.89 % (750763)Time elapsed: 0.017 s
% 3.52/0.89 % (750763)Peak memory usage: 12 MB
% 3.52/0.89 % (750763)Instructions burned: 32 (million)
% 3.52/0.89 % (750761)Instruction limit reached!
% 3.52/0.89 % (750761)------------------------------
% 3.52/0.89 % (750761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750761)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750761)Termination reason: Instruction limit
% 3.52/0.89 % (750761)Termination phase: Saturation
% 3.52/0.89 % (750761)Time elapsed: 0.029 s
% 3.52/0.89 % (750761)Peak memory usage: 12 MB
% 3.52/0.89 % (750761)Instructions burned: 68 (million)
% 3.52/0.89 % (750788)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=543504329:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.52/0.89 % (750795)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=635117772:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 3.52/0.89 % (750777)Instruction limit reached!
% 3.52/0.89 % (750777)------------------------------
% 3.52/0.89 % (750777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750777)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750777)Termination reason: Instruction limit
% 3.52/0.89 % (750777)Termination phase: Saturation
% 3.52/0.89 % (750777)Time elapsed: 0.040 s
% 3.52/0.89 % (750777)Peak memory usage: 13 MB
% 3.52/0.89 % (750777)Instructions burned: 140 (million)
% 3.52/0.89 % (750788)Instruction limit reached!
% 3.52/0.89 % (750788)------------------------------
% 3.52/0.89 % (750788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750788)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750788)Termination reason: Instruction limit
% 3.52/0.89 % (750788)Termination phase: Saturation
% 3.52/0.89 % (750788)Time elapsed: 0.019 s
% 3.52/0.89 % (750788)Peak memory usage: 12 MB
% 3.52/0.89 % (750788)Instructions burned: 35 (million)
% 3.52/0.89 % (750811)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 3.52/0.89 % (750811)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=615993564:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 3.52/0.89 % (750747)Instruction limit reached!
% 3.52/0.89 % (750747)------------------------------
% 3.52/0.89 % (750747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750747)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750747)Termination reason: Instruction limit
% 3.52/0.89 % (750747)Termination phase: Saturation
% 3.52/0.89 % (750747)Time elapsed: 0.094 s
% 3.52/0.89 % (750747)Peak memory usage: 12 MB
% 3.52/0.89 % (750747)Instructions burned: 201 (million)
% 3.52/0.89 % (750812)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=181222747:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 3.52/0.89 % (750795)Instruction limit reached!
% 3.52/0.89 % (750795)------------------------------
% 3.52/0.89 % (750795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750795)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750795)Termination reason: Instruction limit
% 3.52/0.89 % (750795)Termination phase: Saturation
% 3.52/0.89 % (750795)Time elapsed: 0.036 s
% 3.52/0.89 % (750795)Peak memory usage: 12 MB
% 3.52/0.89 % (750795)Instructions burned: 67 (million)
% 3.52/0.89 % (750818)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=2207551364:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 3.52/0.89 % (750820)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=416686010:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 3.52/0.89 % (750820)Refutation not found, incomplete strategy
% 3.52/0.89 % (750820)------------------------------
% 3.52/0.89 % (750820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750820)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750820)Termination reason: Refutation not found, incomplete strategy
% 3.52/0.89 % (750820)Time elapsed: 0.004 s
% 3.52/0.89 % (750820)Peak memory usage: 12 MB
% 3.52/0.89 % (750820)Instructions burned: 6 (million)
% 3.52/0.89 % (750820)------------------------------
% 3.52/0.89 % (750820)------------------------------
% 3.52/0.89 % (750811)Instruction limit reached!
% 3.52/0.89 % (750811)------------------------------
% 3.52/0.89 % (750811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750811)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750811)Termination reason: Instruction limit
% 3.52/0.89 % (750811)Termination phase: Saturation
% 3.52/0.89 % (750811)Time elapsed: 0.046 s
% 3.52/0.89 % (750811)Peak memory usage: 13 MB
% 3.52/0.89 % (750811)Instructions burned: 183 (million)
% 3.52/0.89 % (750824)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3854707262:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 3.52/0.89 % (750823)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=3326406300:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 3.52/0.89 % (750818)Instruction limit reached!
% 3.52/0.89 % (750818)------------------------------
% 3.52/0.89 % (750818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750818)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750818)Termination reason: Instruction limit
% 3.52/0.89 % (750818)Termination phase: Saturation
% 3.52/0.89 % (750818)Time elapsed: 0.052 s
% 3.52/0.89 % (750818)Peak memory usage: 12 MB
% 3.52/0.89 % (750818)Instructions burned: 96 (million)
% 3.52/0.89 % (750827)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=3997101341:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 3.52/0.89 % (750736)Instruction limit reached!
% 3.52/0.89 % (750736)------------------------------
% 3.52/0.89 % (750736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750736)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750736)Termination reason: Instruction limit
% 3.52/0.89 % (750736)Termination phase: Saturation
% 3.52/0.89 % (750736)Time elapsed: 0.216 s
% 3.52/0.89 % (750736)Peak memory usage: 14 MB
% 3.52/0.89 % (750736)Instructions burned: 482 (million)
% 3.52/0.89 % (750829)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3926697586:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 3.52/0.89 % (750812)Instruction limit reached!
% 3.52/0.89 % (750812)------------------------------
% 3.52/0.89 % (750812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750812)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750812)Termination reason: Instruction limit
% 3.52/0.89 % (750812)Termination phase: Saturation
% 3.52/0.89 % (750812)Time elapsed: 0.125 s
% 3.52/0.89 % (750812)Peak memory usage: 13 MB
% 3.52/0.89 % (750812)Instructions burned: 247 (million)
% 3.52/0.89 % (750829)Instruction limit reached!
% 3.52/0.89 % (750829)------------------------------
% 3.52/0.89 % (750829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750829)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750829)Termination reason: Instruction limit
% 3.52/0.89 % (750829)Termination phase: Saturation
% 3.52/0.89 % (750829)Time elapsed: 0.024 s
% 3.52/0.89 % (750829)Peak memory usage: 12 MB
% 3.52/0.89 % (750829)Instructions burned: 46 (million)
% 3.52/0.89 % (750831)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=2759606041:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 3.52/0.89 % (750832)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=2143653579:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 3.52/0.89 % (750827)Instruction limit reached!
% 3.52/0.89 % (750827)------------------------------
% 3.52/0.89 % (750827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750827)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750827)Termination reason: Instruction limit
% 3.52/0.89 % (750827)Termination phase: Saturation
% 3.52/0.89 % (750827)Time elapsed: 0.066 s
% 3.52/0.89 % (750827)Peak memory usage: 12 MB
% 3.52/0.89 % (750827)Instructions burned: 130 (million)
% 3.52/0.89 % (750831)Refutation not found, incomplete strategy
% 3.52/0.89 % (750831)------------------------------
% 3.52/0.89 % (750831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750831)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750831)Termination reason: Refutation not found, incomplete strategy
% 3.52/0.89 % (750831)Time elapsed: 0.004 s
% 3.52/0.89 % (750831)Peak memory usage: 12 MB
% 3.52/0.89 % (750831)Instructions burned: 7 (million)
% 3.52/0.89 % (750831)------------------------------
% 3.52/0.89 % (750831)------------------------------
% 3.52/0.89 % (750657) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-750550-750657"...
% 3.52/0.89 % (750835)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=8560768:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/95Mi)
% 3.52/0.89 % (750836)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=1936836952:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2993 on theBenchmark for (2993ds/65Mi)
% 3.52/0.89 % (750657)...printing done.
% 3.52/0.89 % (750657)Refutation found. Thanks to Tanya!
% 3.52/0.89 % SZS status Theorem for theBenchmark
% 3.52/0.89 % SZS output start Proof for theBenchmark
% 3.52/0.89 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 3.52/0.89 thf(func_def_0, type, in: ($i > $i > $o)).
% 3.52/0.89 thf(func_def_1, type, dsetconstr: ($i > ($i > $o) > $i)).
% 3.52/0.89 thf(func_def_2, type, dsetconstrI: $o).
% 3.52/0.89 thf(func_def_4, type, dsetconstrEL: $o).
% 3.52/0.89 thf(func_def_5, type, dsetconstrER: $o).
% 3.52/0.89 thf(func_def_6, type, setext: $o).
% 3.52/0.89 thf(func_def_7, type, vNOT: ($o > $o)).
% 3.52/0.89 thf(func_def_8, type, vIMP: ($o > $o > $o)).
% 3.52/0.89 thf(func_def_9, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 3.52/0.89 thf(func_def_10, type, db0: !>[X0: $tType]:(X0)).
% 3.52/0.89 thf(func_def_11, type, db1: !>[X0: $tType]:(X0)).
% 3.52/0.89 thf(func_def_12, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.52/0.89 thf(func_def_13, type, db3: !>[X0: $tType]:(X0)).
% 3.52/0.89 thf(func_def_14, type, db5: !>[X0: $tType]:(X0)).
% 3.52/0.89 thf(func_def_15, type, vIFF: ($o > $o > $o)).
% 3.52/0.89 thf(func_def_16, type, db2: !>[X0: $tType]:(X0)).
% 3.52/0.89 thf(func_def_17, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.52/0.89 thf(func_def_23, type, sK3: ($i > $o)).
% 3.52/0.89 thf(func_def_24, type, sK4: ($i > $o)).
% 3.52/0.89 thf(func_def_25, type, sK5: ($i > $i > $i)).
% 3.52/0.89 thf(f1,axiom,(
% 3.52/0.89 (dsetconstrI = ! [X1 : ($i > $o),X2 : $i,X0 : $i] : ((in @ X2 @ X0) => ((X1 @ X2) => (in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))))))),
% 3.52/0.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p',dsetconstrI)).
% 3.52/0.89 thf(f2,axiom,(
% 3.52/0.89 (! [X0 : $i,X1 : ($i > $o),X2 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X2 @ X0)) = dsetconstrEL)),
% 3.52/0.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p',dsetconstrEL)).
% 3.52/0.89 thf(f3,axiom,(
% 3.52/0.89 (dsetconstrER = ! [X1 : ($i > $o),X2 : $i,X0 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (X1 @ X2)))),
% 3.52/0.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p',dsetconstrER)).
% 3.52/0.89 thf(f4,axiom,(
% 3.52/0.89 (setext = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X2 : $i] : ((in @ X2 @ X1) => (in @ X2 @ X0)) => (X0 = X1))))),
% 3.52/0.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p',setext)).
% 3.52/0.89 thf(f5,conjecture,(
% 3.52/0.89 dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X3 : ($i > $o),X2 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X2 @ X4) <=> (X3 @ X5))))) => (((dsetconstr @ X0 @ (^[X4 : $i] : ((X2 @ X4))))) = ((dsetconstr @ X1 @ (^[X4 : $i] : ((X3 @ X4)))))))))))),
% 3.52/0.89 file('/export/starexec/sandbox/benchmark/theBenchmark.p',dsetconstr__Cong)).
% 3.52/0.89 thf(f6,negated_conjecture,(
% 3.52/0.89 ~(dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X3 : ($i > $o),X2 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X2 @ X4) <=> (X3 @ X5))))) => (((dsetconstr @ X0 @ (^[X4 : $i] : ((X2 @ X4))))) = ((dsetconstr @ X1 @ (^[X4 : $i] : ((X3 @ X4))))))))))))),
% 3.52/0.89 inference(negated_conjecture,[status(cth)],[f5])).
% 3.52/0.89 thf(f7,plain,(
% 3.52/0.89 ~(dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => ! [X0 : $i,X1 : $i] : ((X0 = X1) => ! [X2 : ($i > $o),X3 : ($i > $o)] : (! [X4 : $i] : ((in @ X4 @ X0) => ! [X5 : $i] : ((in @ X5 @ X1) => ((X4 = X5) => ((X3 @ X4) <=> (X2 @ X5))))) => (((dsetconstr @ X0 @ (^[X6 : $i] : ((X3 @ X6))))) = ((dsetconstr @ X1 @ (^[X7 : $i] : ((X2 @ X7))))))))))))),
% 3.52/0.89 inference(rectify,[],[f6])).
% 3.52/0.89 thf(f8,plain,(
% 3.52/0.89 (((~ (dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ (^[Y4 : $i]: (Y2 @ Y4))) = (dsetconstr @ Y0 @ (^[Y4 : $i]: (Y3 @ Y4)))))))))))))))))))) = $true)),
% 3.52/0.89 inference(fool_elimination,[],[f7])).
% 3.52/0.89 thf(f9,plain,(
% 3.52/0.89 (dsetconstrI = ! [X0 : ($i > $o),X1 : $i,X2 : $i] : ((in @ X1 @ X2) => ((X0 @ X1) => (in @ X1 @ (dsetconstr @ X2 @ (^[X3 : $i] : ((X0 @ X3))))))))),
% 3.52/0.89 inference(rectify,[],[f1])).
% 3.52/0.89 thf(f10,plain,(
% 3.52/0.89 (dsetconstrI = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3))))))))))))))),
% 3.52/0.89 inference(fool_elimination,[],[f9])).
% 3.52/0.89 thf(f11,plain,(
% 3.52/0.89 (setext = ! [X0 : $i,X1 : $i] : (! [X2 : $i] : ((in @ X2 @ X0) => (in @ X2 @ X1)) => (! [X3 : $i] : ((in @ X3 @ X1) => (in @ X3 @ X0)) => (X0 = X1))))),
% 3.52/0.89 inference(rectify,[],[f4])).
% 3.52/0.89 thf(f12,plain,(
% 3.52/0.89 (setext = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))))))),
% 3.52/0.89 inference(fool_elimination,[],[f11])).
% 3.52/0.89 thf(f13,plain,(
% 3.52/0.89 (dsetconstrER = ! [X0 : ($i > $o),X1 : $i,X2 : $i] : ((in @ X1 @ (dsetconstr @ X2 @ (^[X3 : $i] : ((X0 @ X3))))) => (X0 @ X1)))),
% 3.52/0.89 inference(rectify,[],[f3])).
% 3.52/0.89 thf(f14,plain,(
% 3.52/0.89 (dsetconstrER = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y1))))))))))),
% 3.52/0.89 inference(fool_elimination,[],[f13])).
% 3.52/0.89 thf(f15,plain,(
% 3.52/0.89 (! [X0 : $i,X1 : ($i > $o),X2 : $i] : ((in @ X2 @ (dsetconstr @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) => (in @ X2 @ X0)) = dsetconstrEL)),
% 3.52/0.89 inference(rectify,[],[f2])).
% 3.52/0.89 thf(f16,plain,(
% 3.52/0.89 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y0 @ Y2))))))))))),
% 3.52/0.89 inference(fool_elimination,[],[f15])).
% 3.52/0.89 thf(f17,plain,(
% 3.52/0.89 (dsetconstrER = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3)))) => (Y2 @ Y1))))))))))),
% 3.52/0.89 inference(cnf_transformation,[],[f14])).
% 3.52/0.89 thf(f18,plain,(
% 3.52/0.89 (setext = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))))))),
% 3.52/0.89 inference(cnf_transformation,[],[f12])).
% 3.52/0.89 thf(f19,plain,(
% 3.52/0.89 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ (^[Y3 : $i]: (Y1 @ Y3)))) => (in @ Y0 @ Y2))))))))))),
% 3.52/0.89 inference(cnf_transformation,[],[f16])).
% 3.52/0.89 thf(f20,plain,(
% 3.52/0.89 (dsetconstrI = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ (^[Y3 : $i]: (Y2 @ Y3))))))))))))))),
% 3.52/0.89 inference(cnf_transformation,[],[f10])).
% 3.52/0.89 thf(f21,plain,(
% 3.52/0.89 (((~ (dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ (^[Y4 : $i]: (Y2 @ Y4))) = (dsetconstr @ Y0 @ (^[Y4 : $i]: (Y3 @ Y4)))))))))))))))))))) = $true)),
% 3.52/0.89 inference(cnf_transformation,[],[f8])).
% 3.52/0.89 thf(f23,definition,(
% 3.52/0.89 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.52/0.89 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.52/0.89 thf(f24,plain,(
% 3.52/0.89 (((~ (dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3)))))))))))))))))) = $true)),
% 3.52/0.89 inference(beta-eta_normalization,[],[f21])).
% 3.52/0.89 thf(f25,plain,(
% 3.52/0.89 (dsetconstrI = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ Y2))))))))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f20])).
% 3.52/0.89 thf(f26,plain,(
% 3.52/0.89 (dsetconstrEL = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ Y1)) => (in @ Y0 @ Y2))))))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f19])).
% 3.52/0.89 thf(f27,plain,(
% 3.52/0.89 (dsetconstrER = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) => (Y2 @ Y1))))))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f17])).
% 3.52/0.89 thf(f29,plain,(
% 3.52/0.89 (setext = $false) | (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))))) = $true)),
% 3.52/0.89 inference(iff_proxy_clausification,[],[f18])).
% 3.52/0.89 thf(f30,plain,(
% 3.52/0.89 ($false = ((dsetconstrI => (dsetconstrEL => (dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3))))))))))))))))))),
% 3.52/0.89 inference(not_proxy_clausification,[],[f24])).
% 3.52/0.89 thf(f32,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ Y2))))))))))) = $true) | (dsetconstrI = $false)),
% 3.52/0.89 inference(iff_proxy_clausification,[],[f25])).
% 3.52/0.89 thf(f34,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ Y1)) => (in @ Y0 @ Y2))))))))) = $true) | (dsetconstrEL = $false)),
% 3.52/0.89 inference(iff_proxy_clausification,[],[f26])).
% 3.52/0.89 thf(f36,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) => (Y2 @ Y1))))))))) = $true) | (dsetconstrER = $false)),
% 3.52/0.89 inference(iff_proxy_clausification,[],[f27])).
% 3.52/0.89 thf(f38,definition,(
% 3.52/0.89 spl0_1 <=> (setext = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 3.52/0.89 thf(f40,plain,(
% 3.52/0.89 (setext = $true) | ~spl0_1),
% 3.52/0.89 inference(avatar_component_clause,[],[f38])).
% 3.52/0.89 thf(f47,definition,(
% 3.52/0.89 spl0_3 <=> (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 3.52/0.89 thf(f49,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))))) = $true) | ~spl0_3),
% 3.52/0.89 inference(avatar_component_clause,[],[f47])).
% 3.52/0.89 thf(f51,definition,(
% 3.52/0.89 spl0_4 <=> (setext = $false)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition])).
% 3.52/0.89 thf(f53,plain,(
% 3.52/0.89 (setext = $false) | ~spl0_4),
% 3.52/0.89 inference(avatar_component_clause,[],[f51])).
% 3.52/0.89 thf(f54,plain,(
% 3.52/0.89 spl0_3 | spl0_4),
% 3.52/0.89 inference(avatar_split_clause,[],[f29,f51,f47])).
% 3.52/0.89 thf(f55,plain,(
% 3.52/0.89 ($false = ((dsetconstrEL => (dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3)))))))))))))))))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f30])).
% 3.52/0.89 thf(f56,plain,(
% 3.52/0.89 (dsetconstrI = $true)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f30])).
% 3.52/0.89 thf(f58,definition,(
% 3.52/0.89 spl0_5 <=> (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ Y2))))))))))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition])).
% 3.52/0.89 thf(f60,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ Y2))))))))))) = $true) | ~spl0_5),
% 3.52/0.89 inference(avatar_component_clause,[],[f58])).
% 3.52/0.89 thf(f62,definition,(
% 3.52/0.89 spl0_6 <=> (dsetconstrI = $false)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 3.52/0.89 thf(f64,plain,(
% 3.52/0.89 (dsetconstrI = $false) | ~spl0_6),
% 3.52/0.89 inference(avatar_component_clause,[],[f62])).
% 3.52/0.89 thf(f65,plain,(
% 3.52/0.89 spl0_5 | spl0_6),
% 3.52/0.89 inference(avatar_split_clause,[],[f32,f62,f58])).
% 3.52/0.89 thf(f71,definition,(
% 3.52/0.89 spl0_8 <=> (dsetconstrI = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 3.52/0.89 thf(f73,plain,(
% 3.52/0.89 (dsetconstrI = $true) | ~spl0_8),
% 3.52/0.89 inference(avatar_component_clause,[],[f71])).
% 3.52/0.89 thf(f76,definition,(
% 3.52/0.89 spl0_9 <=> (dsetconstrEL = $false)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition])).
% 3.52/0.89 thf(f78,plain,(
% 3.52/0.89 (dsetconstrEL = $false) | ~spl0_9),
% 3.52/0.89 inference(avatar_component_clause,[],[f76])).
% 3.52/0.89 thf(f80,definition,(
% 3.52/0.89 spl0_10 <=> (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ Y1)) => (in @ Y0 @ Y2))))))))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition])).
% 3.52/0.89 thf(f82,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ Y1)) => (in @ Y0 @ Y2))))))))) = $true) | ~spl0_10),
% 3.52/0.89 inference(avatar_component_clause,[],[f80])).
% 3.52/0.89 thf(f83,plain,(
% 3.52/0.89 spl0_9 | spl0_10),
% 3.52/0.89 inference(avatar_split_clause,[],[f34,f80,f76])).
% 3.52/0.89 thf(f89,definition,(
% 3.52/0.89 spl0_12 <=> (dsetconstrEL = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition])).
% 3.52/0.89 thf(f91,plain,(
% 3.52/0.89 (dsetconstrEL = $true) | ~spl0_12),
% 3.52/0.89 inference(avatar_component_clause,[],[f89])).
% 3.52/0.89 thf(f94,definition,(
% 3.52/0.89 spl0_13 <=> (dsetconstrER = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition])).
% 3.52/0.89 thf(f96,plain,(
% 3.52/0.89 (dsetconstrER = $true) | ~spl0_13),
% 3.52/0.89 inference(avatar_component_clause,[],[f94])).
% 3.52/0.89 thf(f103,definition,(
% 3.52/0.89 spl0_15 <=> (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) => (Y2 @ Y1))))))))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition])).
% 3.52/0.89 thf(f105,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) => (Y2 @ Y1))))))))) = $true) | ~spl0_15),
% 3.52/0.89 inference(avatar_component_clause,[],[f103])).
% 3.52/0.89 thf(f107,definition,(
% 3.52/0.89 spl0_16 <=> (dsetconstrER = $false)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition])).
% 3.52/0.89 thf(f109,plain,(
% 3.52/0.89 (dsetconstrER = $false) | ~spl0_16),
% 3.52/0.89 inference(avatar_component_clause,[],[f107])).
% 3.52/0.89 thf(f110,plain,(
% 3.52/0.89 spl0_15 | spl0_16),
% 3.52/0.89 inference(avatar_split_clause,[],[f36,f107,f103])).
% 3.52/0.89 thf(f111,plain,(
% 3.52/0.89 spl0_8),
% 3.52/0.89 inference(avatar_split_clause,[],[f56,f71])).
% 3.52/0.89 thf(f112,plain,(
% 3.52/0.89 (((dsetconstrER => (setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3))))))))))))))) = $false)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f55])).
% 3.52/0.89 thf(f113,plain,(
% 3.52/0.89 (dsetconstrEL = $true)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f55])).
% 3.52/0.89 thf(f114,plain,(
% 3.52/0.89 spl0_12),
% 3.52/0.89 inference(avatar_split_clause,[],[f113,f89])).
% 3.52/0.89 thf(f115,plain,(
% 3.52/0.89 ($false = ((setext => (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3)))))))))))))))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f112])).
% 3.52/0.89 thf(f116,plain,(
% 3.52/0.89 (dsetconstrER = $true)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f112])).
% 3.52/0.89 thf(f117,plain,(
% 3.52/0.89 ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3))))))))))))))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f115])).
% 3.52/0.89 thf(f118,plain,(
% 3.52/0.89 (setext = $true)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f115])).
% 3.52/0.89 thf(f119,plain,(
% 3.52/0.89 spl0_13),
% 3.52/0.89 inference(avatar_split_clause,[],[f116,f94])).
% 3.52/0.89 thf(f120,plain,(
% 3.52/0.89 spl0_1),
% 3.52/0.89 inference(avatar_split_clause,[],[f118,f38])).
% 3.52/0.89 thf(f121,plain,(
% 3.52/0.89 ($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((Y1 = Y0) => (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: ((!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ Y1) => (!! @ $i @ (^[Y5 : $i]: ((in @ Y5 @ Y0) => ((Y4 = Y5) => ((Y2 @ Y4) = (Y3 @ Y5))))))))) => ((dsetconstr @ Y1 @ Y2) = (dsetconstr @ Y0 @ Y3))))))))))) @ sK1)))),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f117])).
% 3.52/0.89 thf(f122,plain,(
% 3.52/0.89 ($false = ((!! @ $i @ (^[Y0 : $i]: ((Y0 = sK1) => (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ sK1) => ((Y3 = Y4) => ((Y1 @ Y3) = (Y2 @ Y4))))))))) => ((dsetconstr @ Y0 @ Y1) = (dsetconstr @ sK1 @ Y2))))))))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f121])).
% 3.52/0.89 thf(f123,plain,(
% 3.52/0.89 ($false = (((^[Y0 : $i]: ((Y0 = sK1) => (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ Y0) => (!! @ $i @ (^[Y4 : $i]: ((in @ Y4 @ sK1) => ((Y3 = Y4) => ((Y1 @ Y3) = (Y2 @ Y4))))))))) => ((dsetconstr @ Y0 @ Y1) = (dsetconstr @ sK1 @ Y2))))))))) @ sK2)))),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f122])).
% 3.52/0.89 thf(f124,plain,(
% 3.52/0.89 ($false = (((sK2 = sK1) => (!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ sK2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ sK1) => ((Y2 = Y3) => ((Y0 @ Y2) = (Y1 @ Y3))))))))) => ((dsetconstr @ sK2 @ Y0) = (dsetconstr @ sK1 @ Y1))))))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f123])).
% 3.52/0.89 thf(f125,plain,(
% 3.52/0.89 ($false = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ sK2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ sK1) => ((Y2 = Y3) => ((Y0 @ Y2) = (Y1 @ Y3))))))))) => ((dsetconstr @ sK2 @ Y0) = (dsetconstr @ sK1 @ Y1)))))))))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f124])).
% 3.52/0.89 thf(f126,plain,(
% 3.52/0.89 ($true = ((sK2 = sK1)))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f124])).
% 3.52/0.89 thf(f127,plain,(
% 3.52/0.89 (sK2 = sK1)),
% 3.52/0.89 inference(equality_proxy_clausification,[],[f126])).
% 3.52/0.89 thf(f128,plain,(
% 3.52/0.89 ($false = (((^[Y0 : $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ sK2) => (!! @ $i @ (^[Y3 : $i]: ((in @ Y3 @ sK1) => ((Y2 = Y3) => ((Y0 @ Y2) = (Y1 @ Y3))))))))) => ((dsetconstr @ sK2 @ Y0) = (dsetconstr @ sK1 @ Y1)))))) @ sK3)))),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f125])).
% 3.52/0.89 thf(f129,plain,(
% 3.52/0.89 ($false = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK2) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ sK1) => ((Y1 = Y2) => ((sK3 @ Y1) = (Y0 @ Y2))))))))) => ((dsetconstr @ sK2 @ sK3) = (dsetconstr @ sK1 @ Y0)))))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f128])).
% 3.52/0.89 thf(f143,plain,(
% 3.52/0.89 ($false = (((^[Y0 : $i > $o]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK2) => (!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ sK1) => ((Y1 = Y2) => ((sK3 @ Y1) = (Y0 @ Y2))))))))) => ((dsetconstr @ sK2 @ sK3) = (dsetconstr @ sK1 @ Y0)))) @ sK4)))),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f129])).
% 3.52/0.89 thf(f145,plain,(
% 3.52/0.89 ($false = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK2) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK1) => ((Y0 = Y1) => ((sK3 @ Y0) = (sK4 @ Y1))))))))) => ((dsetconstr @ sK2 @ sK3) = (dsetconstr @ sK1 @ sK4)))))),
% 3.52/0.89 inference(beta-eta_normalization,[],[f143])).
% 3.52/0.89 thf(f147,plain,(
% 3.52/0.89 ($false = (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK1) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK1) => ((Y0 = Y1) => ((sK3 @ Y0) = (sK4 @ Y1))))))))) => ((dsetconstr @ sK1 @ sK3) = (dsetconstr @ sK1 @ sK4)))))),
% 3.52/0.89 inference(forward_demodulation,[],[f145,f127])).
% 3.52/0.89 thf(f148,plain,(
% 3.52/0.89 ($false = (((dsetconstr @ sK1 @ sK3) = (dsetconstr @ sK1 @ sK4))))),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f147])).
% 3.52/0.89 thf(f149,plain,(
% 3.52/0.89 (((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK1) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK1) => ((Y0 = Y1) => ((sK3 @ Y0) = (sK4 @ Y1)))))))))) = $true)),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f147])).
% 3.52/0.89 thf(f150,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) != ((dsetconstr @ sK1 @ sK4)))),
% 3.52/0.89 inference(equality_proxy_clausification,[],[f148])).
% 3.52/0.89 thf(f151,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((in @ Y0 @ sK1) => (!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ sK1) => ((Y0 = Y1) => ((sK3 @ Y0) = (sK4 @ Y1)))))))) @ X1)) = $true)) )),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f149])).
% 3.52/0.89 thf(f152,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (((((in @ X1 @ sK1) => (!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK1) => ((X1 = Y0) => ((sK3 @ X1) = (sK4 @ Y0)))))))) = $true)) )),
% 3.52/0.89 inference(beta-eta_normalization,[],[f151])).
% 3.52/0.89 thf(f153,plain,(
% 3.52/0.89 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ sK1) => ((X1 = Y0) => ((sK3 @ X1) = (sK4 @ Y0))))))) = $true) | ($false = ((in @ X1 @ sK1)))) )),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f152])).
% 3.52/0.89 thf(f156,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((in @ Y0 @ sK1) => ((X1 = Y0) => ((sK3 @ X1) = (sK4 @ Y0))))) @ X2)) = $true) | ($false = ((in @ X1 @ sK1)))) )),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f153])).
% 3.52/0.89 thf(f157,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | ((((in @ X2 @ sK1) => ((X1 = X2) => ((sK3 @ X1) = (sK4 @ X2))))) = $true)) )),
% 3.52/0.89 inference(beta-eta_normalization,[],[f156])).
% 3.52/0.89 thf(f158,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | ((((X1 = X2) => ((sK3 @ X1) = (sK4 @ X2)))) = $true) | ($false = ((in @ X2 @ sK1)))) )),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f157])).
% 3.52/0.89 thf(f159,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | ($false = ((X1 = X2))) | ($false = ((in @ X2 @ sK1))) | ((((sK3 @ X1) = (sK4 @ X2))) = $true)) )),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f158])).
% 3.52/0.89 thf(f160,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((sK3 @ X1) = (sK4 @ X2))) = $true) | ($false = ((in @ X2 @ sK1))) | ($false = ((in @ X1 @ sK1))) | (X1 != X2)) )),
% 3.52/0.89 inference(equality_proxy_clausification,[],[f159])).
% 3.52/0.89 thf(f161,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_9 | ~spl0_12)),
% 3.52/0.89 inference(forward_demodulation,[],[f91,f78])).
% 3.52/0.89 thf(f162,plain,(
% 3.52/0.89 $false | (~spl0_9 | ~spl0_12)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f161])).
% 3.52/0.89 thf(f163,plain,(
% 3.52/0.89 ~spl0_9 | ~spl0_12),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f162])).
% 3.52/0.89 thf(f164,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | ($false = ((in @ X0 @ sK1))) | ($false = ((sK4 @ X1))) | ((((sK3 @ X0) = $true)) = $true) | (X0 != X1)) )),
% 3.52/0.89 inference(superposition,[],[f160,f23])).
% 3.52/0.89 thf(f165,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : $i] : (($false = ((in @ X0 @ sK1))) | (X0 != X1) | ($false = ((sK3 @ X0))) | ((($true = (sK4 @ X1))) = $true) | ($false = ((in @ X1 @ sK1)))) )),
% 3.52/0.89 inference(superposition,[],[f160,f23])).
% 3.52/0.89 thf(f166,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | (((sK3 @ X0)) = $true) | ($false = ((in @ X0 @ sK1))) | ($false = ((sK4 @ X1))) | (X0 != X1)) )),
% 3.52/0.89 inference(boolean_simplification,[],[f164])).
% 3.52/0.89 thf(f167,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : $i] : (($false = ((in @ X1 @ sK1))) | ($false = ((in @ X0 @ sK1))) | (((sK4 @ X1)) = $true) | ($false = ((sK3 @ X0))) | (X0 != X1)) )),
% 3.52/0.89 inference(boolean_simplification,[],[f165])).
% 3.52/0.89 thf(f170,plain,(
% 3.52/0.89 ( ! [X0 : $i] : (($false != $false) | (((sK3 @ X0)) = $true) | ($false = ((in @ X0 @ sK1))) | (X0 != X0) | ($false = ((sK4 @ X0)))) )),
% 3.52/0.89 inference(equality_factoring,[],[f166])).
% 3.52/0.89 thf(f171,plain,(
% 3.52/0.89 ( ! [X0 : $i] : (($false = ((in @ X0 @ sK1))) | (((sK3 @ X0)) = $true) | ($false = ((sK4 @ X0)))) )),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f170])).
% 3.52/0.89 thf(f175,plain,(
% 3.52/0.89 ( ! [X0 : $i] : (($false = ((sK3 @ X0))) | ($false != $false) | ($false = ((in @ X0 @ sK1))) | (((sK4 @ X0)) = $true) | (X0 != X0)) )),
% 3.52/0.89 inference(equality_factoring,[],[f167])).
% 3.52/0.89 thf(f176,plain,(
% 3.52/0.89 ( ! [X0 : $i] : (($false = ((in @ X0 @ sK1))) | (((sK4 @ X0)) = $true) | ($false = ((sK3 @ X0)))) )),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f175])).
% 3.52/0.89 thf(f182,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ (dsetconstr @ Y0 @ Y2)) => (Y2 @ Y1))))))) @ X1)) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f105])).
% 3.52/0.89 thf(f183,plain,(
% 3.52/0.89 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ (dsetconstr @ X1 @ Y1)) => (Y1 @ Y0))))))) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(beta-eta_normalization,[],[f182])).
% 3.52/0.89 thf(f184,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ (dsetconstr @ X1 @ Y1)) => (Y1 @ Y0))))) @ X2)) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f183])).
% 3.52/0.89 thf(f185,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((in @ X2 @ (dsetconstr @ X1 @ Y0)) => (Y0 @ X2))))))) ) | ~spl0_15),
% 3.52/0.89 inference(beta-eta_normalization,[],[f184])).
% 3.52/0.89 thf(f186,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (((((^[Y0 : $i > $o]: ((in @ X2 @ (dsetconstr @ X1 @ Y0)) => (Y0 @ X2))) @ X3)) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f185])).
% 3.52/0.89 thf(f187,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (((((in @ X2 @ (dsetconstr @ X1 @ X3)) => (X3 @ X2))) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(beta-eta_normalization,[],[f186])).
% 3.52/0.89 thf(f188,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : ((((in @ X2 @ (dsetconstr @ X1 @ X3))) = $false) | (((X3 @ X2)) = $true)) ) | ~spl0_15),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f187])).
% 3.52/0.89 thf(f191,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((in @ Y0 @ (dsetconstr @ Y2 @ Y1)) => (in @ Y0 @ Y2))))))) @ X1)) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f82])).
% 3.52/0.89 thf(f192,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ X1 @ (dsetconstr @ Y1 @ Y0)) => (in @ X1 @ Y1))))))))) ) | ~spl0_10),
% 3.52/0.89 inference(beta-eta_normalization,[],[f191])).
% 3.52/0.89 thf(f193,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X1 : $i] : (((((^[Y0 : $i > $o]: (!! @ $i @ (^[Y1 : $i]: ((in @ X1 @ (dsetconstr @ Y1 @ Y0)) => (in @ X1 @ Y1))))) @ X2)) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f192])).
% 3.52/0.89 thf(f194,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((in @ X1 @ (dsetconstr @ Y0 @ X2)) => (in @ X1 @ Y0))))) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(beta-eta_normalization,[],[f193])).
% 3.52/0.89 thf(f195,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (((((^[Y0 : $i]: ((in @ X1 @ (dsetconstr @ Y0 @ X2)) => (in @ X1 @ Y0))) @ X3)) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f194])).
% 3.52/0.89 thf(f196,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : (((((in @ X1 @ (dsetconstr @ X3 @ X2)) => (in @ X1 @ X3))) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(beta-eta_normalization,[],[f195])).
% 3.52/0.89 thf(f197,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X3 : $i,X1 : $i] : ((((in @ X1 @ (dsetconstr @ X3 @ X2))) = $false) | (((in @ X1 @ X3)) = $true)) ) | ~spl0_10),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f196])).
% 3.52/0.89 thf(f200,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (((((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: ((in @ Y1 @ Y0) => ((Y2 @ Y1) => (in @ Y1 @ (dsetconstr @ Y0 @ Y2))))))))) @ X1)) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f60])).
% 3.52/0.89 thf(f201,plain,(
% 3.52/0.89 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ X1) => ((Y1 @ Y0) => (in @ Y0 @ (dsetconstr @ X1 @ Y1))))))))) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(beta-eta_normalization,[],[f200])).
% 3.52/0.89 thf(f202,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: ((in @ Y0 @ X1) => ((Y1 @ Y0) => (in @ Y0 @ (dsetconstr @ X1 @ Y1))))))) @ X2)) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f201])).
% 3.52/0.89 thf(f203,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : ((((!! @ ($i > $o) @ (^[Y0 : $i > $o]: ((in @ X2 @ X1) => ((Y0 @ X2) => (in @ X2 @ (dsetconstr @ X1 @ Y0))))))) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(beta-eta_normalization,[],[f202])).
% 3.52/0.89 thf(f204,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (($true = (((^[Y0 : $i > $o]: ((in @ X2 @ X1) => ((Y0 @ X2) => (in @ X2 @ (dsetconstr @ X1 @ Y0))))) @ X3)))) ) | ~spl0_5),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f203])).
% 3.52/0.89 thf(f205,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : (((((in @ X2 @ X1) => ((X3 @ X2) => (in @ X2 @ (dsetconstr @ X1 @ X3))))) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(beta-eta_normalization,[],[f204])).
% 3.52/0.89 thf(f206,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : ((((in @ X2 @ X1)) = $false) | ((((X3 @ X2) => (in @ X2 @ (dsetconstr @ X1 @ X3)))) = $true)) ) | ~spl0_5),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f205])).
% 3.52/0.89 thf(f207,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X1 : $i] : ((((in @ X2 @ (dsetconstr @ X1 @ X3))) = $true) | (((in @ X2 @ X1)) = $false) | ($false = ((X3 @ X2)))) ) | ~spl0_5),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f206])).
% 3.52/0.89 thf(f216,plain,(
% 3.52/0.89 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y1) => (in @ Y2 @ Y0)))) => ((!! @ $i @ (^[Y2 : $i]: ((in @ Y2 @ Y0) => (in @ Y2 @ Y1)))) => (Y1 = Y0)))))) @ X1)))) ) | ~spl0_3),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f49])).
% 3.52/0.89 thf(f217,plain,(
% 3.52/0.89 ( ! [X1 : $i] : ((((!! @ $i @ (^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ Y1 @ X1)))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (in @ Y1 @ Y0)))) => (Y0 = X1)))))) = $true)) ) | ~spl0_3),
% 3.52/0.89 inference(beta-eta_normalization,[],[f216])).
% 3.52/0.89 thf(f218,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ Y0) => (in @ Y1 @ X1)))) => ((!! @ $i @ (^[Y1 : $i]: ((in @ Y1 @ X1) => (in @ Y1 @ Y0)))) => (Y0 = X1)))) @ X2)) = $true)) ) | ~spl0_3),
% 3.52/0.89 inference(pi_proxy_clausification,[],[f217])).
% 3.52/0.89 thf(f219,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1)))) => ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))) => (X2 = X1)))) = $true)) ) | ~spl0_3),
% 3.52/0.89 inference(beta-eta_normalization,[],[f218])).
% 3.52/0.89 thf(f220,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (((((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))) => (X2 = X1))) = $true) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))))))) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f219])).
% 3.52/0.89 thf(f221,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))))) | (((X2 = X1)) = $true) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))))))) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f220])).
% 3.52/0.89 thf(f222,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1)))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))))) | (X1 = X2)) ) | ~spl0_3),
% 3.52/0.89 inference(equality_proxy_clausification,[],[f221])).
% 3.52/0.89 thf(f223,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : ((X1 = X2) | ($false = (((^[Y0 : $i]: ((in @ Y0 @ X2) => (in @ Y0 @ X1))) @ (sK5 @ X1 @ X2)))) | ($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))))))) ) | ~spl0_3),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f222])).
% 3.52/0.89 thf(f225,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))))) | (X1 = X2) | ($false = (((in @ (sK5 @ X1 @ X2) @ X2) => (in @ (sK5 @ X1 @ X2) @ X1))))) ) | ~spl0_3),
% 3.52/0.89 inference(beta-eta_normalization,[],[f223])).
% 3.52/0.89 thf(f227,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))))) | ($false = ((in @ (sK5 @ X1 @ X2) @ X1))) | (X1 = X2)) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f225])).
% 3.52/0.89 thf(f228,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2)))))) | (X1 = X2) | (((in @ (sK5 @ X1 @ X2) @ X2)) = $true)) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f225])).
% 3.52/0.89 thf(f229,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK5 @ X2 @ X1)))) | ($false = ((in @ (sK5 @ X1 @ X2) @ X1))) | (X1 = X2)) ) | ~spl0_3),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f227])).
% 3.52/0.89 thf(f231,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = (((in @ (sK5 @ X2 @ X1) @ X1) => (in @ (sK5 @ X2 @ X1) @ X2)))) | (X1 = X2) | ($false = ((in @ (sK5 @ X1 @ X2) @ X1)))) ) | ~spl0_3),
% 3.52/0.89 inference(beta-eta_normalization,[],[f229])).
% 3.52/0.89 thf(f233,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ (sK5 @ X2 @ X1) @ X2))) | (X1 = X2) | ($false = ((in @ (sK5 @ X1 @ X2) @ X1)))) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f231])).
% 3.52/0.89 thf(f234,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = ((in @ (sK5 @ X1 @ X2) @ X1))) | (((in @ (sK5 @ X2 @ X1) @ X1)) = $true) | (X1 = X2)) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f231])).
% 3.52/0.89 thf(f235,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((in @ Y0 @ X1) => (in @ Y0 @ X2))) @ (sK5 @ X2 @ X1)))) | (((in @ (sK5 @ X1 @ X2) @ X2)) = $true) | (X1 = X2)) ) | ~spl0_3),
% 3.52/0.89 inference(sigma_proxy_clausification,[],[f228])).
% 3.52/0.89 thf(f237,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK5 @ X1 @ X2) @ X2)) = $true) | (X1 = X2) | ($false = (((in @ (sK5 @ X2 @ X1) @ X1) => (in @ (sK5 @ X2 @ X1) @ X2))))) ) | ~spl0_3),
% 3.52/0.89 inference(beta-eta_normalization,[],[f235])).
% 3.52/0.89 thf(f240,plain,(
% 3.52/0.89 ( ! [X2 : $i,X1 : $i] : ((((in @ (sK5 @ X2 @ X1) @ X1)) = $true) | (X1 = X2) | (((in @ (sK5 @ X1 @ X2) @ X2)) = $true)) ) | ~spl0_3),
% 3.52/0.89 inference(imp_proxy_clausification,[],[f237])).
% 3.52/0.89 thf(f243,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ X2 @ (dsetconstr @ X0 @ X1)) @ X2))) | ($false = $true) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2) @ X0))) | (((dsetconstr @ X0 @ X1)) = X2) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2))))) ) | (~spl0_3 | ~spl0_5)),
% 3.52/0.89 inference(superposition,[],[f207,f233])).
% 3.52/0.89 thf(f245,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2) @ X0))) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2)))) | ($false = ((in @ (sK5 @ X2 @ (dsetconstr @ X0 @ X1)) @ X2))) | (((dsetconstr @ X0 @ X1)) = X2)) ) | (~spl0_3 | ~spl0_5)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f243])).
% 3.52/0.89 thf(f248,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ X2 @ (dsetconstr @ X0 @ X1)) @ (dsetconstr @ X0 @ X1))) = $true) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2) @ X0))) | ($false = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2)))) | (((dsetconstr @ X0 @ X1)) = X2)) ) | (~spl0_3 | ~spl0_5)),
% 3.52/0.89 inference(superposition,[],[f234,f207])).
% 3.52/0.89 thf(f252,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ X2 @ (dsetconstr @ X0 @ X1)) @ (dsetconstr @ X0 @ X1))) = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2)))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ X2) @ X0))) | (((dsetconstr @ X0 @ X1)) = X2)) ) | (~spl0_3 | ~spl0_5)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f248])).
% 3.52/0.89 thf(f259,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : ((((in @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)) @ X1)) = $true) | ($false = $true) | (((dsetconstr @ X1 @ X2)) = X0) | (((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X0)) = $true)) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(superposition,[],[f240,f197])).
% 3.52/0.89 thf(f260,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : ((((X2 @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)))) = $true) | (((dsetconstr @ X1 @ X2)) = X0) | (((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X0)) = $true) | ($false = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f240,f188])).
% 3.52/0.89 thf(f272,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : ((((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X0)) = $true) | (((in @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)) @ X1)) = $true) | (((dsetconstr @ X1 @ X2)) = X0)) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f259])).
% 3.52/0.89 thf(f276,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : ((((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X0)) = $true) | (((dsetconstr @ X1 @ X2)) = X0) | (((X2 @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)))) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f260])).
% 3.52/0.89 thf(f284,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((X1 @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)) @ X2)) = $true) | ($false = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3)))) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f276,f197])).
% 3.52/0.89 thf(f287,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((X3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)))) = $true) | ($false = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3))) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)))) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f188,f276])).
% 3.52/0.89 thf(f293,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)) @ X2)) = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3))) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)))) = $true)) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f284])).
% 3.52/0.89 thf(f297,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((X3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)))) = $true) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3)))) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f287])).
% 3.52/0.89 thf(f328,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)) @ X2)) = $true) | ($false = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3))) | (((in @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true)) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(superposition,[],[f272,f197])).
% 3.52/0.89 thf(f338,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ X2 @ X3) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ X3)) @ X2)) = $true) | (((dsetconstr @ X0 @ X1)) = ((dsetconstr @ X2 @ X3)))) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f328])).
% 3.52/0.89 thf(f380,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((X2 @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0)))) | (((in @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)) @ X1)) = $true) | ($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X1))) | ($false = $true) | (((dsetconstr @ X1 @ X2)) = X0)) ) | (~spl0_3 | ~spl0_5 | ~spl0_10)),
% 3.52/0.89 inference(superposition,[],[f252,f197])).
% 3.52/0.89 thf(f383,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X1))) | (((X2 @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)))) = $true) | ($false = ((X2 @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0)))) | ($false = $true) | (((dsetconstr @ X1 @ X2)) = X0)) ) | (~spl0_3 | ~spl0_5 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f188,f252])).
% 3.52/0.89 thf(f385,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X1))) | (((dsetconstr @ X1 @ X2)) = X0) | (((in @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)) @ X1)) = $true) | ($false = ((X2 @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f380])).
% 3.52/0.89 thf(f386,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0) @ X1))) | (((dsetconstr @ X1 @ X2)) = X0) | ($false = ((X2 @ (sK5 @ (dsetconstr @ X1 @ X2) @ X0)))) | (((X2 @ (sK5 @ X0 @ (dsetconstr @ X1 @ X2)))) = $true)) ) | (~spl0_3 | ~spl0_5 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f383])).
% 3.52/0.89 thf(f443,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X3 : $i,X0 : $i,X1 : $i] : ((((X2 @ (sK5 @ (dsetconstr @ X3 @ sK4) @ (dsetconstr @ X1 @ X2)))) = $true) | (((sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X3 @ sK4))) != X0) | (((dsetconstr @ X3 @ sK4)) = ((dsetconstr @ X1 @ X2))) | ($false = ((in @ X0 @ sK1))) | ($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X3 @ sK4)) @ sK1))) | ((((sK3 @ X0) = $true)) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f160,f297])).
% 3.52/0.89 thf(f444,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $o)] : ((((X1 @ (sK5 @ (dsetconstr @ X2 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | ($false = ((in @ X3 @ sK1))) | ((($true = (sK4 @ X3))) = $true) | (((sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3))) != X3) | (((dsetconstr @ X2 @ sK3)) = ((dsetconstr @ X0 @ X1))) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)) @ sK1)) = $false)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f160,f297])).
% 3.52/0.89 thf(f449,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X3 : $i,X0 : $i,X1 : $i] : ((((sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X3 @ sK4))) != X0) | ($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X3 @ sK4)) @ sK1))) | (((X2 @ (sK5 @ (dsetconstr @ X3 @ sK4) @ (dsetconstr @ X1 @ X2)))) = $true) | ($false = ((in @ X0 @ sK1))) | (((dsetconstr @ X3 @ sK4)) = ((dsetconstr @ X1 @ X2))) | (((sK3 @ X0)) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(boolean_simplification,[],[f443])).
% 3.52/0.89 thf(f451,plain,(
% 3.52/0.89 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : ($i > $o)] : ((((sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3))) != X3) | ($false = ((in @ X3 @ sK1))) | (((sK4 @ X3)) = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)) @ sK1)) = $false) | (((dsetconstr @ X2 @ sK3)) = ((dsetconstr @ X0 @ X1))) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(boolean_simplification,[],[f444])).
% 3.52/0.89 thf(f454,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((X1 @ (sK5 @ (dsetconstr @ X2 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK4)) @ sK1))) | (((dsetconstr @ X2 @ sK4)) = ((dsetconstr @ X0 @ X1))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK4)) @ sK1))) | ($true = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK4)))))) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(equality_resolution,[],[f449])).
% 3.52/0.89 thf(f455,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK4)) @ sK1))) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ X2 @ sK4)) = ((dsetconstr @ X0 @ X1))) | ($true = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK4)))))) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f454])).
% 3.52/0.89 thf(f457,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)))) = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)) @ sK1)) = $false) | (((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)) @ sK1)) = $false) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ X2 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(equality_resolution,[],[f451])).
% 3.52/0.89 thf(f458,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)) @ sK1)) = $false) | (((dsetconstr @ X2 @ sK3)) = ((dsetconstr @ X0 @ X1))) | (((X1 @ (sK5 @ (dsetconstr @ X2 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X2 @ sK3)))) = $true)) ) | (~spl0_3 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f457])).
% 3.52/0.89 thf(f579,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ X0 @ X1))) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f293,f458])).
% 3.52/0.89 thf(f593,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($true = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1))))) | ($false = $true) | ($true = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1))))) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f386,f293])).
% 3.52/0.89 thf(f600,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ($false = $true) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ X0 @ X1))) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f455,f293])).
% 3.52/0.89 thf(f606,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : (($true = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1))))) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($false = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f593])).
% 3.52/0.89 thf(f607,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : (($true = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1))))) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f606])).
% 3.52/0.89 thf(f614,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ X0 @ X1))) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK3)))) = $true)) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f579])).
% 3.52/0.89 thf(f615,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f614])).
% 3.52/0.89 thf(f628,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ X0 @ X1))) | (((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ($false = $true) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true)) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f600])).
% 3.52/0.89 thf(f629,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : ((((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((X1 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ X0 @ X1)))) = $true) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f628])).
% 3.52/0.89 thf(f668,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($false = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | (((in @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2))))) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10)),
% 3.52/0.89 inference(superposition,[],[f385,f338])).
% 3.52/0.89 thf(f688,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : (($false = $true) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1))) | (((in @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f668])).
% 3.52/0.89 thf(f689,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ X0 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | ($false = ((X1 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ X2))))) | (((dsetconstr @ X0 @ X2)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f688])).
% 3.52/0.89 thf(f963,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_6 | ~spl0_8)),
% 3.52/0.89 inference(superposition,[],[f64,f73])).
% 3.52/0.89 thf(f969,plain,(
% 3.52/0.89 $false | (~spl0_6 | ~spl0_8)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f963])).
% 3.52/0.89 thf(f970,plain,(
% 3.52/0.89 ~spl0_6 | ~spl0_8),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f969])).
% 3.52/0.89 thf(f984,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_1 | ~spl0_4)),
% 3.52/0.89 inference(superposition,[],[f53,f40])).
% 3.52/0.89 thf(f990,plain,(
% 3.52/0.89 $false | (~spl0_1 | ~spl0_4)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f984])).
% 3.52/0.89 thf(f991,plain,(
% 3.52/0.89 ~spl0_1 | ~spl0_4),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f990])).
% 3.52/0.89 thf(f1128,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_13 | ~spl0_16)),
% 3.52/0.89 inference(superposition,[],[f109,f96])).
% 3.52/0.89 thf(f1134,plain,(
% 3.52/0.89 $false | (~spl0_13 | ~spl0_16)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f1128])).
% 3.52/0.89 thf(f1135,plain,(
% 3.52/0.89 ~spl0_13 | ~spl0_16),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f1134])).
% 3.52/0.89 thf(f3000,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((dsetconstr @ sK1 @ X2)) = ((dsetconstr @ X0 @ X1))) | ($false = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ X2))))) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ X2)))) = $true) | (((in @ (sK5 @ (dsetconstr @ sK1 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true)) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(superposition,[],[f338,f176])).
% 3.52/0.89 thf(f3024,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : ($i > $o)] : ((((in @ (sK5 @ (dsetconstr @ sK1 @ X2) @ (dsetconstr @ X0 @ X1)) @ X0)) = $true) | (((dsetconstr @ sK1 @ X2)) = ((dsetconstr @ X0 @ X1))) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ X2)))) = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ sK1 @ X2)))))) ) | (~spl0_3 | ~spl0_10)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f3000])).
% 3.52/0.89 thf(f5000,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : (($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X1 @ sK4)) @ sK1))) | (((sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X1 @ sK4))) != X0) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ X1 @ sK4) @ (dsetconstr @ X1 @ X2))))) | ((((sK3 @ X0) = $true)) = $true) | (((dsetconstr @ X1 @ X2)) = ((dsetconstr @ X1 @ sK4))) | ($false = ((in @ X0 @ sK1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f160,f607])).
% 3.52/0.89 thf(f5001,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : (((($true = (sK4 @ X2))) = $true) | ($false = ((in @ X2 @ sK1))) | (((sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3))) != X2) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ sK3) @ (dsetconstr @ X0 @ X1))))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)) @ sK1))) | (((dsetconstr @ X0 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f160,f607])).
% 3.52/0.89 thf(f5009,plain,(
% 3.52/0.89 ( ! [X2 : ($i > $o),X0 : $i,X1 : $i] : ((((sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X1 @ sK4))) != X0) | (((sK3 @ X0)) = $true) | ($false = ((in @ X0 @ sK1))) | (((dsetconstr @ X1 @ X2)) = ((dsetconstr @ X1 @ sK4))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ X1 @ sK4) @ (dsetconstr @ X1 @ X2))))) | ($false = ((in @ (sK5 @ (dsetconstr @ X1 @ X2) @ (dsetconstr @ X1 @ sK4)) @ sK1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(boolean_simplification,[],[f5000])).
% 3.52/0.89 thf(f5011,plain,(
% 3.52/0.89 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3))) != X2) | (((sK4 @ X2)) = $true) | (((dsetconstr @ X0 @ sK3)) = ((dsetconstr @ X0 @ X1))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ sK3) @ (dsetconstr @ X0 @ X1))))) | ($false = ((in @ X2 @ sK1))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)) @ sK1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(boolean_simplification,[],[f5001])).
% 3.52/0.89 thf(f5104,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK4)) @ sK1))) | (((dsetconstr @ X0 @ sK4)) = ((dsetconstr @ X0 @ X1))) | (((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK4)))) = $true) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ X0 @ sK4) @ (dsetconstr @ X0 @ X1))))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK4)) @ sK1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(equality_resolution,[],[f5009])).
% 3.52/0.89 thf(f5105,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK4)) @ sK1))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ X0 @ sK4) @ (dsetconstr @ X0 @ X1))))) | (((sK3 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK4)))) = $true) | (((dsetconstr @ X0 @ sK4)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5104])).
% 3.52/0.89 thf(f5107,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)) @ sK1))) | ($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)) @ sK1))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ sK3) @ (dsetconstr @ X0 @ X1))))) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)))) = $true) | (((dsetconstr @ X0 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(equality_resolution,[],[f5011])).
% 3.52/0.89 thf(f5108,plain,(
% 3.52/0.89 ( ! [X0 : $i,X1 : ($i > $o)] : (($false = ((in @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)) @ sK1))) | (((sK4 @ (sK5 @ (dsetconstr @ X0 @ X1) @ (dsetconstr @ X0 @ sK3)))) = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ X0 @ sK3) @ (dsetconstr @ X0 @ X1))))) | (((dsetconstr @ X0 @ sK3)) = ((dsetconstr @ X0 @ X1)))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5107])).
% 3.52/0.89 thf(f5407,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : ((((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ sK1 @ X0))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ X0))))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ sK1 @ X0))) | ($false = $true) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ X0)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f689,f5105])).
% 3.52/0.89 thf(f5408,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : ((((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ X0))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ X0))))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ X0))) | ($false = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ X0))))) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK3)))) = $true)) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f689,f5108])).
% 3.52/0.89 thf(f5438,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : (($false = $true) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ sK1 @ X0))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ X0)))))) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5407])).
% 3.52/0.89 thf(f5439,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : (($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ X0))))) | (((dsetconstr @ sK1 @ sK4)) = ((dsetconstr @ sK1 @ X0))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK4)))) = $true)) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5438])).
% 3.52/0.89 thf(f5440,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : ((((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ X0))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ X0))))) | ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK3)))) = $true)) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5408])).
% 3.52/0.89 thf(f5441,plain,(
% 3.52/0.89 ( ! [X0 : ($i > $o)] : (($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ X0))))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ X0))) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ X0) @ (dsetconstr @ sK1 @ sK3)))) = $true)) ) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5440])).
% 3.52/0.89 thf(f5514,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f615,f5439])).
% 3.52/0.89 thf(f5519,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5514])).
% 3.52/0.89 thf(f5520,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5519])).
% 3.52/0.89 thf(f5524,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5520,f150])).
% 3.52/0.89 thf(f5526,definition,(
% 3.52/0.89 spl0_108 <=> (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition])).
% 3.52/0.89 thf(f5528,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ~spl0_108),
% 3.52/0.89 inference(avatar_component_clause,[],[f5526])).
% 3.52/0.89 thf(f5530,definition,(
% 3.52/0.89 spl0_109 <=> (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition])).
% 3.52/0.89 thf(f5532,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ~spl0_109),
% 3.52/0.89 inference(avatar_component_clause,[],[f5530])).
% 3.52/0.89 thf(f5534,plain,(
% 3.52/0.89 spl0_108 | spl0_109 | ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15),
% 3.52/0.89 inference(avatar_split_clause,[],[f5524,f103,f80,f58,f47,f5530,f5526])).
% 3.52/0.89 thf(f5542,definition,(
% 3.52/0.89 spl0_110 <=> ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)) @ sK1)))),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition])).
% 3.52/0.89 thf(f5543,plain,(
% 3.52/0.89 ($false != ((in @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)) @ sK1))) | spl0_110),
% 3.52/0.89 inference(avatar_component_clause,[],[f5542])).
% 3.52/0.89 thf(f5544,plain,(
% 3.52/0.89 ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)) @ sK1))) | ~spl0_110),
% 3.52/0.89 inference(avatar_component_clause,[],[f5542])).
% 3.52/0.89 thf(f5554,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(superposition,[],[f629,f5441])).
% 3.52/0.89 thf(f5560,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ($false = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(duplicate_literal_removal,[],[f5554])).
% 3.52/0.89 thf(f5561,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5560])).
% 3.52/0.89 thf(f5564,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5561,f150])).
% 3.52/0.89 thf(f5566,definition,(
% 3.52/0.89 spl0_112 <=> (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition])).
% 3.52/0.89 thf(f5568,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ~spl0_112),
% 3.52/0.89 inference(avatar_component_clause,[],[f5566])).
% 3.52/0.89 thf(f5570,definition,(
% 3.52/0.89 spl0_113 <=> (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true)),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition])).
% 3.52/0.89 thf(f5572,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ~spl0_113),
% 3.52/0.89 inference(avatar_component_clause,[],[f5570])).
% 3.52/0.89 thf(f5574,plain,(
% 3.52/0.89 spl0_112 | spl0_113 | ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15),
% 3.52/0.89 inference(avatar_split_clause,[],[f5564,f103,f80,f58,f47,f5570,f5566])).
% 3.52/0.89 thf(f5582,definition,(
% 3.52/0.89 spl0_114 <=> ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ sK1)))),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition])).
% 3.52/0.89 thf(f5583,plain,(
% 3.52/0.89 ($false != ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ sK1))) | spl0_114),
% 3.52/0.89 inference(avatar_component_clause,[],[f5582])).
% 3.52/0.89 thf(f5584,plain,(
% 3.52/0.89 ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ sK1))) | ~spl0_114),
% 3.52/0.89 inference(avatar_component_clause,[],[f5582])).
% 3.52/0.89 thf(f5790,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | ($false = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(superposition,[],[f5544,f689])).
% 3.52/0.89 thf(f5799,plain,(
% 3.52/0.89 ($false = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_3 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(superposition,[],[f3024,f5544])).
% 3.52/0.89 thf(f5802,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5790])).
% 3.52/0.89 thf(f5812,plain,(
% 3.52/0.89 ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5799])).
% 3.52/0.89 thf(f5815,plain,(
% 3.52/0.89 ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5802,f150])).
% 3.52/0.89 thf(f5819,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_3 | ~spl0_10 | ~spl0_110)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5812,f150])).
% 3.52/0.89 thf(f5821,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | ($false = $true) | (~spl0_3 | ~spl0_10 | ~spl0_110 | ~spl0_112)),
% 3.52/0.89 inference(forward_demodulation,[],[f5819,f5568])).
% 3.52/0.89 thf(f5822,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_10 | ~spl0_110 | ~spl0_112)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5821])).
% 3.52/0.89 thf(f5825,plain,(
% 3.52/0.89 spl0_113 | ~spl0_3 | ~spl0_10 | ~spl0_110 | ~spl0_112),
% 3.52/0.89 inference(avatar_split_clause,[],[f5822,f5566,f5542,f80,f47,f5570])).
% 3.52/0.89 thf(f5846,plain,(
% 3.52/0.89 ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ (dsetconstr @ sK1 @ sK4)))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | ($false != $false) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (~spl0_3 | ~spl0_5 | spl0_110)),
% 3.52/0.89 inference(superposition,[],[f5543,f245])).
% 3.52/0.89 thf(f5848,plain,(
% 3.52/0.89 ($false != $false) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | spl0_110),
% 3.52/0.89 inference(superposition,[],[f5543,f171])).
% 3.52/0.89 thf(f5853,plain,(
% 3.52/0.89 ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ (dsetconstr @ sK1 @ sK4)))) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (~spl0_3 | ~spl0_5 | spl0_110)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5846])).
% 3.52/0.89 thf(f5854,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | spl0_110),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5848])).
% 3.52/0.89 thf(f5861,plain,(
% 3.52/0.89 ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ (dsetconstr @ sK1 @ sK4)))) | (~spl0_3 | ~spl0_5 | spl0_110)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5853,f150])).
% 3.52/0.89 thf(f5862,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | ($false = $true) | (~spl0_109 | spl0_110)),
% 3.52/0.89 inference(forward_demodulation,[],[f5854,f5532])).
% 3.52/0.89 thf(f5863,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_109 | spl0_110)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5862])).
% 3.52/0.89 thf(f5867,definition,(
% 3.52/0.89 spl0_124 <=> ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))))),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition])).
% 3.52/0.89 thf(f5869,plain,(
% 3.52/0.89 ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | ~spl0_124),
% 3.52/0.89 inference(avatar_component_clause,[],[f5867])).
% 3.52/0.89 thf(f5871,definition,(
% 3.52/0.89 spl0_125 <=> ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ (dsetconstr @ sK1 @ sK4))))),
% 3.52/0.89 introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition])).
% 3.52/0.89 thf(f5873,plain,(
% 3.52/0.89 ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ (dsetconstr @ sK1 @ sK4)))) | ~spl0_125),
% 3.52/0.89 inference(avatar_component_clause,[],[f5871])).
% 3.52/0.89 thf(f5874,plain,(
% 3.52/0.89 spl0_124 | spl0_125 | ~spl0_3 | ~spl0_5 | spl0_110),
% 3.52/0.89 inference(avatar_split_clause,[],[f5861,f5542,f58,f47,f5871,f5867])).
% 3.52/0.89 thf(f5875,plain,(
% 3.52/0.89 spl0_108 | ~spl0_109 | spl0_110),
% 3.52/0.89 inference(avatar_split_clause,[],[f5863,f5542,f5530,f5526])).
% 3.52/0.89 thf(f5880,plain,(
% 3.52/0.89 ($false = $true) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_108)),
% 3.52/0.89 inference(superposition,[],[f5441,f5528])).
% 3.52/0.89 thf(f5888,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_108)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5880])).
% 3.52/0.89 thf(f5892,plain,(
% 3.52/0.89 (((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_108)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5888,f150])).
% 3.52/0.89 thf(f5894,plain,(
% 3.52/0.89 spl0_113 | ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_108),
% 3.52/0.89 inference(avatar_split_clause,[],[f5892,f5526,f103,f80,f58,f47,f5570])).
% 3.52/0.89 thf(f5898,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_113)),
% 3.52/0.89 inference(superposition,[],[f5439,f5572])).
% 3.52/0.89 thf(f5904,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_113)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5898])).
% 3.52/0.89 thf(f5976,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_108 | ~spl0_124)),
% 3.52/0.89 inference(superposition,[],[f5528,f5869])).
% 3.52/0.89 thf(f5985,plain,(
% 3.52/0.89 $false | (~spl0_108 | ~spl0_124)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5976])).
% 3.52/0.89 thf(f5986,plain,(
% 3.52/0.89 ~spl0_108 | ~spl0_124),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f5985])).
% 3.52/0.89 thf(f5998,plain,(
% 3.52/0.89 (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | ($false = $true) | ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_114)),
% 3.52/0.89 inference(superposition,[],[f689,f5584])).
% 3.52/0.89 thf(f6005,plain,(
% 3.52/0.89 ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | (((dsetconstr @ sK1 @ sK3)) = ((dsetconstr @ sK1 @ sK4))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_114)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f5998])).
% 3.52/0.89 thf(f6018,plain,(
% 3.52/0.89 ($false = ((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4))))) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_114)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f6005,f150])).
% 3.52/0.89 thf(f6020,plain,(
% 3.52/0.89 spl0_124 | ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_114),
% 3.52/0.89 inference(avatar_split_clause,[],[f6018,f5582,f80,f58,f47,f5867])).
% 3.52/0.89 thf(f6040,plain,(
% 3.52/0.89 (((sK3 @ (sK5 @ (dsetconstr @ sK1 @ sK3) @ (dsetconstr @ sK1 @ sK4)))) = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_113)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f5904,f150])).
% 3.52/0.89 thf(f6053,plain,(
% 3.52/0.89 spl0_108 | ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_113),
% 3.52/0.89 inference(avatar_split_clause,[],[f6040,f5570,f103,f80,f58,f47,f5526])).
% 3.52/0.89 thf(f6216,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110 | ~spl0_113)),
% 3.52/0.89 inference(superposition,[],[f5815,f5572])).
% 3.52/0.89 thf(f6225,plain,(
% 3.52/0.89 $false | (~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110 | ~spl0_113)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f6216])).
% 3.52/0.89 thf(f6226,plain,(
% 3.52/0.89 ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110 | ~spl0_113),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f6225])).
% 3.52/0.89 thf(f7790,plain,(
% 3.52/0.89 ($false = $true) | ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ sK1))) | ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_5 | ~spl0_125)),
% 3.52/0.89 inference(superposition,[],[f207,f5873])).
% 3.52/0.89 thf(f7791,plain,(
% 3.52/0.89 ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | ($false = ((in @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3)) @ sK1))) | (~spl0_5 | ~spl0_125)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f7790])).
% 3.52/0.89 thf(f7794,plain,(
% 3.52/0.89 ($false = ((sK4 @ (sK5 @ (dsetconstr @ sK1 @ sK4) @ (dsetconstr @ sK1 @ sK3))))) | (~spl0_5 | spl0_114 | ~spl0_125)),
% 3.52/0.89 inference(forward_subsumption_resolution,[],[f7791,f5583])).
% 3.52/0.89 thf(f7816,plain,(
% 3.52/0.89 ($false = $true) | (~spl0_5 | ~spl0_113 | spl0_114 | ~spl0_125)),
% 3.52/0.89 inference(superposition,[],[f5572,f7794])).
% 3.52/0.89 thf(f7824,plain,(
% 3.52/0.89 $false | (~spl0_5 | ~spl0_113 | spl0_114 | ~spl0_125)),
% 3.52/0.89 inference(trivial_inequality_removal,[],[f7816])).
% 3.52/0.89 thf(f7825,plain,(
% 3.52/0.89 ~spl0_5 | ~spl0_113 | spl0_114 | ~spl0_125),
% 3.52/0.89 inference(avatar_contradiction_clause,[],[f7824])).
% 3.52/0.89 cnf(s2, plain, spl0_3 | spl0_4, inference(sat_conversion,[],[f54])).
% 3.52/0.89 cnf(s3, plain, spl0_5 | spl0_6, inference(sat_conversion,[],[f65])).
% 3.52/0.89 cnf(s5, plain, spl0_9 | spl0_10, inference(sat_conversion,[],[f83])).
% 3.52/0.89 cnf(s8, plain, spl0_15 | spl0_16, inference(sat_conversion,[],[f110])).
% 3.52/0.89 cnf(s9, plain, spl0_8, inference(sat_conversion,[],[f111])).
% 3.52/0.89 cnf(s10, plain, spl0_12, inference(sat_conversion,[],[f114])).
% 3.52/0.89 cnf(s11, plain, spl0_13, inference(sat_conversion,[],[f119])).
% 3.52/0.89 cnf(s12, plain, spl0_1, inference(sat_conversion,[],[f120])).
% 3.52/0.89 cnf(s13, plain, ~spl0_9 | ~spl0_12, inference(sat_conversion,[],[f163])).
% 3.52/0.89 cnf(s19, plain, ~spl0_6 | ~spl0_8, inference(sat_conversion,[],[f970])).
% 3.52/0.89 cnf(s21, plain, ~spl0_1 | ~spl0_4, inference(sat_conversion,[],[f991])).
% 3.52/0.89 cnf(s23, plain, ~spl0_13 | ~spl0_16, inference(sat_conversion,[],[f1135])).
% 3.52/0.89 cnf(s318, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | spl0_108 | spl0_109, inference(sat_conversion,[],[f5534])).
% 3.52/0.89 cnf(s321, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | spl0_112 | spl0_113, inference(sat_conversion,[],[f5574])).
% 3.52/0.89 cnf(s329, plain, ~spl0_3 | ~spl0_10 | ~spl0_110 | ~spl0_112 | spl0_113, inference(sat_conversion,[],[f5825])).
% 3.52/0.89 cnf(s332, plain, ~spl0_3 | ~spl0_5 | spl0_110 | spl0_124 | spl0_125, inference(sat_conversion,[],[f5874])).
% 3.52/0.89 cnf(s333, plain, spl0_108 | ~spl0_109 | spl0_110, inference(sat_conversion,[],[f5875])).
% 3.52/0.89 cnf(s335, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | ~spl0_108 | spl0_113, inference(sat_conversion,[],[f5894])).
% 3.52/0.89 cnf(s339, plain, ~spl0_108 | ~spl0_124, inference(sat_conversion,[],[f5986])).
% 3.52/0.89 cnf(s340, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_114 | spl0_124, inference(sat_conversion,[],[f6020])).
% 3.52/0.89 cnf(s344, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_15 | spl0_108 | ~spl0_113, inference(sat_conversion,[],[f6053])).
% 3.52/0.89 cnf(s352, plain, ~spl0_3 | ~spl0_5 | ~spl0_10 | ~spl0_110 | ~spl0_113, inference(sat_conversion,[],[f6226])).
% 3.52/0.89 cnf(s393, plain, ~spl0_5 | ~spl0_113 | spl0_114 | ~spl0_125, inference(sat_conversion,[],[f7825])).
% 3.52/0.89 cnf(s395, plain, ~spl0_4, inference(rat,[],[s21,s12])).
% 3.52/0.89 cnf(s396, plain, ~spl0_16, inference(rat,[],[s23,s11])).
% 3.52/0.89 cnf(s397, plain, ~spl0_9, inference(rat,[],[s13,s10])).
% 3.52/0.89 cnf(s398, plain, ~spl0_6, inference(rat,[],[s19,s9])).
% 3.52/0.89 cnf(s399, plain, spl0_15, inference(rat,[],[s8,s396])).
% 3.52/0.89 cnf(s400, plain, spl0_10, inference(rat,[],[s5,s397])).
% 3.52/0.89 cnf(s401, plain, spl0_5, inference(rat,[],[s3,s398])).
% 3.52/0.89 cnf(s402, plain, spl0_3, inference(rat,[],[s2,s395])).
% 3.52/0.89 cnf(s407, plain, spl0_108, inference(rat,[],[s329,s333,s321,s318,s344,s400,s402,s399,s401])).
% 3.52/0.89 cnf(s408, plain, ~spl0_124, inference(rat,[],[s339,s407])).
% 3.52/0.89 cnf(s409, plain, spl0_113, inference(rat,[],[s335,s402,s401,s399,s400,s407])).
% 3.52/0.89 cnf(s410, plain, ~spl0_114, inference(rat,[],[s340,s402,s401,s400,s408])).
% 3.52/0.89 cnf(s411, plain, ~spl0_110, inference(rat,[],[s352,s402,s401,s400,s409])).
% 3.52/0.89 cnf(s413, plain, ~spl0_125, inference(rat,[],[s393,s409,s401,s410])).
% 3.52/0.89 cnf(s415, plain, $false, inference(rat,[],[s332,s408,s402,s401,s413,s411])).
% 3.52/0.89 thf(f7830,plain,(
% 3.52/0.89 $false),
% 3.52/0.89 inference(avatar_sat_refutation,[],[s415])).
% 3.52/0.89 % SZS output end Proof for theBenchmark
% 3.52/0.89 % (750657)------------------------------
% 3.52/0.89 % (750657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.52/0.89 % (750657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.52/0.89 % (750657)CaDiCaL version: 2.1.3
% 3.52/0.89 % (750657)Termination reason: Refutation
% 3.52/0.89 % (750657)Time elapsed: 0.428 s
% 3.52/0.89 % (750657)Peak memory usage: 16 MB
% 3.52/0.89 % (750657)Instructions burned: 839 (million)
% 3.52/0.89 % (750550)Success in time 0.651 s
% 3.52/0.89 % Vampire exiting
%------------------------------------------------------------------------------