%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP179^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:08:41 AM UTC 2026
% Result : Theorem 7.99s 1.64s
% Output : Refutation 7.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP179^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 20:07:01 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running higher-order theorem proving
% 0.20/0.29 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.28/0.49 % (577036)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.28/0.49 % (577044)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=3623333301: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.28/0.49 % (577043)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=291173481:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.28/0.49 % (577041)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=90767489:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.28/0.49 % (577042)lrs+10_16_si=on:nwc=1.5:random_seed=3713759166:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.28/0.49 % (577045)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2016551698:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.28/0.49 % (577043)Instruction limit reached!
% 0.28/0.49 % (577043)------------------------------
% 0.28/0.49 % (577043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.49 % (577043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.49 % (577043)CaDiCaL version: 2.1.3
% 0.28/0.49 % (577043)Termination reason: Instruction limit
% 0.28/0.49 % (577043)Termination phase: shuffling
% 0.28/0.49 % (577043)Time elapsed: 0.003 s
% 0.28/0.49 % (577043)Peak memory usage: 10 MB
% 0.28/0.49 % (577043)Instructions burned: 3 (million)
% 0.28/0.49 % (577047)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.28/0.49 % (577047)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.28/0.49 % (577047)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=218632850:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.28/0.49 % (577042)Instruction limit reached!
% 0.28/0.49 % (577042)------------------------------
% 0.28/0.49 % (577042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.49 % (577042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.49 % (577042)CaDiCaL version: 2.1.3
% 0.28/0.49 % (577042)Termination reason: Instruction limit
% 0.28/0.49 % (577042)Termination phase: shuffling
% 0.28/0.49 % (577042)Time elapsed: 0.016 s
% 0.28/0.49 % (577042)Peak memory usage: 10 MB
% 0.28/0.49 % (577042)Instructions burned: 18 (million)
% 0.28/0.49 % (577046)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1928054721:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.28/0.49 % (577045)Instruction limit reached!
% 0.28/0.49 % (577045)------------------------------
% 0.28/0.49 % (577045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.49 % (577045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.49 % (577045)CaDiCaL version: 2.1.3
% 0.28/0.49 % (577045)Termination reason: Instruction limit
% 0.28/0.49 % (577045)Termination phase: shuffling
% 0.28/0.49 % (577045)Time elapsed: 0.020 s
% 0.28/0.49 % (577045)Peak memory usage: 10 MB
% 0.28/0.49 % (577045)Instructions burned: 24 (million)
% 0.28/0.49 % (577053)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3475715060:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.28/0.49 % (577053)Instruction limit reached!
% 0.28/0.49 % (577053)------------------------------
% 0.28/0.49 % (577053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.28/0.49 % (577053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.28/0.49 % (577053)CaDiCaL version: 2.1.3
% 0.28/0.49 % (577053)Termination reason: Instruction limit
% 0.28/0.49 % (577053)Termination phase: shuffling
% 0.28/0.49 % (577053)Time elapsed: 0.002 s
% 0.28/0.49 % (577053)Peak memory usage: 10 MB
% 0.28/0.49 % (577053)Instructions burned: 2 (million)
% 0.28/0.49 % (577057)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.28/0.49 % (577055)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3806240115:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 1.15/0.52 % (577059)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1104265808:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.15/0.52 % (577057)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4154862383:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.15/0.52 % (577055)Instruction limit reached!
% 1.15/0.52 % (577055)------------------------------
% 1.15/0.52 % (577055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.52 % (577055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.52 % (577055)CaDiCaL version: 2.1.3
% 1.15/0.52 % (577055)Termination reason: Instruction limit
% 1.15/0.52 % (577055)Termination phase: shuffling
% 1.15/0.52 % (577055)Time elapsed: 0.005 s
% 1.15/0.52 % (577055)Peak memory usage: 10 MB
% 1.15/0.52 % (577055)Instructions burned: 5 (million)
% 1.15/0.52 % (577059)Instruction limit reached!
% 1.15/0.52 % (577059)------------------------------
% 1.15/0.52 % (577059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.52 % (577059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.52 % (577059)CaDiCaL version: 2.1.3
% 1.15/0.52 % (577059)Termination reason: Instruction limit
% 1.15/0.52 % (577059)Termination phase: shuffling
% 1.15/0.52 % (577059)Time elapsed: 0.007 s
% 1.15/0.52 % (577059)Peak memory usage: 10 MB
% 1.15/0.52 % (577059)Instructions burned: 12 (million)
% 1.15/0.52 % (577057)Instruction limit reached!
% 1.15/0.52 % (577057)------------------------------
% 1.15/0.52 % (577057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.52 % (577057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.52 % (577057)CaDiCaL version: 2.1.3
% 1.15/0.52 % (577057)Termination reason: Instruction limit
% 1.15/0.52 % (577057)Termination phase: shuffling
% 1.15/0.52 % (577057)Time elapsed: 0.005 s
% 1.15/0.52 % (577057)Peak memory usage: 10 MB
% 1.15/0.52 % (577057)Instructions burned: 7 (million)
% 1.15/0.52 % (577041)Instruction limit reached!
% 1.15/0.52 % (577041)------------------------------
% 1.15/0.52 % (577041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.52 % (577041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.52 % (577041)CaDiCaL version: 2.1.3
% 1.15/0.52 % (577041)Termination reason: Instruction limit
% 1.15/0.52 % (577041)Termination phase: Function definition elimination
% 1.15/0.52 % (577041)Time elapsed: 0.067 s
% 1.15/0.52 % (577041)Peak memory usage: 12 MB
% 1.15/0.52 % (577041)Instructions burned: 87 (million)
% 1.15/0.52 % (577063)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
% 1.15/0.52 % (577063)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.15/0.52 % (577046)Instruction limit reached!
% 1.15/0.52 % (577046)------------------------------
% 1.15/0.52 % (577046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.52 % (577046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.52 % (577046)CaDiCaL version: 2.1.3
% 1.15/0.52 % (577046)Termination reason: Instruction limit
% 1.15/0.52 % (577046)Termination phase: Property scanning
% 1.15/0.52 % (577046)Time elapsed: 0.053 s
% 1.15/0.52 % (577046)Peak memory usage: 12 MB
% 1.15/0.52 % (577046)Instructions burned: 77 (million)
% 1.15/0.52 % (577063)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=439612014:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2998 on theBenchmark for (2998ds/28Mi)
% 1.15/0.52 % (577064)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=1240436982:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.15/0.52 % (577065)lrs+10_1_si=on:cs=on:random_seed=228513242:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.15/0.52 % (577066)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.15/0.57 % (577065)Instruction limit reached!
% 1.15/0.57 % (577065)------------------------------
% 1.15/0.57 % (577065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577065)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577065)Termination reason: Instruction limit
% 1.15/0.57 % (577065)Termination phase: shuffling
% 1.15/0.57 % (577065)Time elapsed: 0.005 s
% 1.15/0.57 % (577065)Peak memory usage: 10 MB
% 1.15/0.57 % (577065)Instructions burned: 10 (million)
% 1.15/0.57 % (577066)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=2296942408:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.15/0.57 % (577066)Instruction limit reached!
% 1.15/0.57 % (577066)------------------------------
% 1.15/0.57 % (577066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577066)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577066)Termination reason: Instruction limit
% 1.15/0.57 % (577066)Termination phase: shuffling
% 1.15/0.57 % (577066)Time elapsed: 0.002 s
% 1.15/0.57 % (577066)Peak memory usage: 10 MB
% 1.15/0.57 % (577066)Instructions burned: 3 (million)
% 1.15/0.57 % (577067)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1245853031:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.15/0.57 % (577063)Instruction limit reached!
% 1.15/0.57 % (577063)------------------------------
% 1.15/0.57 % (577063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577063)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577063)Termination reason: Instruction limit
% 1.15/0.57 % (577063)Termination phase: shuffling
% 1.15/0.57 % (577063)Time elapsed: 0.023 s
% 1.15/0.57 % (577063)Peak memory usage: 10 MB
% 1.15/0.57 % (577063)Instructions burned: 29 (million)
% 1.15/0.57 % (577071)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1932166961:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.15/0.57 % (577073)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=287780309:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.15/0.57 % (577067)Instruction limit reached!
% 1.15/0.57 % (577067)------------------------------
% 1.15/0.57 % (577067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577067)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577067)Termination reason: Instruction limit
% 1.15/0.57 % (577067)Termination phase: SInE selection
% 1.15/0.57 % (577067)Time elapsed: 0.018 s
% 1.15/0.57 % (577067)Peak memory usage: 11 MB
% 1.15/0.57 % (577067)Instructions burned: 38 (million)
% 1.15/0.57 % (577064)Instruction limit reached!
% 1.15/0.57 % (577064)------------------------------
% 1.15/0.57 % (577064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577064)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577064)Termination reason: Instruction limit
% 1.15/0.57 % (577064)Termination phase: Preprocessing 3
% 1.15/0.57 % (577064)Time elapsed: 0.039 s
% 1.15/0.57 % (577064)Peak memory usage: 11 MB
% 1.15/0.57 % (577064)Instructions burned: 86 (million)
% 1.15/0.57 % (577075)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=2273974891:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.15/0.57 % (577073)Instruction limit reached!
% 1.15/0.57 % (577073)------------------------------
% 1.15/0.57 % (577073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.15/0.57 % (577073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/0.57 % (577073)CaDiCaL version: 2.1.3
% 1.15/0.57 % (577073)Termination reason: Instruction limit
% 1.15/0.57 % (577073)Termination phase: Property scanning
% 1.15/0.57 % (577073)Time elapsed: 0.015 s
% 1.15/0.57 % (577073)Peak memory usage: 10 MB
% 1.15/0.57 % (577073)Instructions burned: 31 (million)
% 1.15/0.57 % (577075)Instruction limit reached!
% 1.15/0.57 % (577075)------------------------------
% 1.93/0.61 % (577075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.61 % (577075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.61 % (577075)CaDiCaL version: 2.1.3
% 1.93/0.61 % (577075)Termination reason: Instruction limit
% 1.93/0.61 % (577075)Termination phase: shuffling
% 1.93/0.61 % (577075)Time elapsed: 0.008 s
% 1.93/0.61 % (577075)Peak memory usage: 10 MB
% 1.93/0.61 % (577075)Instructions burned: 14 (million)
% 1.93/0.61 % (577078)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2032319434:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 1.93/0.61 % (577079)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=362011893:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.93/0.61 % (577081)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3640759516: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.93/0.61 % (577081)Instruction limit reached!
% 1.93/0.61 % (577081)------------------------------
% 1.93/0.61 % (577081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.61 % (577081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.61 % (577081)CaDiCaL version: 2.1.3
% 1.93/0.61 % (577081)Termination reason: Instruction limit
% 1.93/0.61 % (577081)Termination phase: shuffling
% 1.93/0.61 % (577081)Time elapsed: 0.002 s
% 1.93/0.61 % (577081)Peak memory usage: 10 MB
% 1.93/0.61 % (577081)Instructions burned: 3 (million)
% 1.93/0.61 % (577079)Instruction limit reached!
% 1.93/0.61 % (577079)------------------------------
% 1.93/0.61 % (577079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.61 % (577079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.61 % (577079)CaDiCaL version: 2.1.3
% 1.93/0.61 % (577079)Termination reason: Instruction limit
% 1.93/0.61 % (577079)Termination phase: shuffling
% 1.93/0.61 % (577079)Time elapsed: 0.008 s
% 1.93/0.61 % (577079)Peak memory usage: 10 MB
% 1.93/0.61 % (577079)Instructions burned: 16 (million)
% 1.93/0.61 % (577047)Instruction limit reached!
% 1.93/0.61 % (577047)------------------------------
% 1.93/0.61 % (577047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.61 % (577047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.61 % (577047)CaDiCaL version: 2.1.3
% 1.93/0.61 % (577047)Termination reason: Instruction limit
% 1.93/0.61 % (577047)Termination phase: Saturation
% 1.93/0.61 % (577047)Time elapsed: 0.131 s
% 1.93/0.61 % (577047)Peak memory usage: 14 MB
% 1.93/0.61 % (577047)Instructions burned: 158 (million)
% 1.93/0.61 % (577082)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1775281222:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.93/0.61 % (577082)Instruction limit reached!
% 1.93/0.61 % (577082)------------------------------
% 1.93/0.61 % (577082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.93/0.61 % (577082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.93/0.61 % (577082)CaDiCaL version: 2.1.3
% 1.93/0.61 % (577082)Termination reason: Instruction limit
% 1.93/0.61 % (577082)Termination phase: shuffling
% 1.93/0.61 % (577082)Time elapsed: 0.013 s
% 1.93/0.61 % (577082)Peak memory usage: 11 MB
% 1.93/0.61 % (577082)Instructions burned: 26 (million)
% 1.93/0.61 % (577086)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=105743686:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.93/0.61 % (577088)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.93/0.61 % (577088)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 1.93/0.61 % (577087)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3573276793:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 1.93/0.61 % (577088)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=1168728884:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.19/0.67 % (577088)Instruction limit reached!
% 2.19/0.67 % (577088)------------------------------
% 2.19/0.67 % (577088)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577088)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577088)Termination reason: Instruction limit
% 2.19/0.67 % (577088)Termination phase: shuffling
% 2.19/0.67 % (577088)Time elapsed: 0.007 s
% 2.19/0.67 % (577088)Peak memory usage: 10 MB
% 2.19/0.67 % (577088)Instructions burned: 14 (million)
% 2.19/0.67 % (577086)Instruction limit reached!
% 2.19/0.67 % (577086)------------------------------
% 2.19/0.67 % (577086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577086)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577086)Termination reason: Instruction limit
% 2.19/0.67 % (577086)Termination phase: shuffling
% 2.19/0.67 % (577086)Time elapsed: 0.012 s
% 2.19/0.67 % (577086)Peak memory usage: 10 MB
% 2.19/0.67 % (577086)Instructions burned: 25 (million)
% 2.19/0.67 % (577090)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.19/0.67 % (577090)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=692130213:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.19/0.67 % (577090)Instruction limit reached!
% 2.19/0.67 % (577090)------------------------------
% 2.19/0.67 % (577090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577090)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577090)Termination reason: Instruction limit
% 2.19/0.67 % (577090)Termination phase: shuffling
% 2.19/0.67 % (577090)Time elapsed: 0.005 s
% 2.19/0.67 % (577090)Peak memory usage: 10 MB
% 2.19/0.67 % (577090)Instructions burned: 10 (million)
% 2.19/0.67 % (577095)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=1867644505:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.19/0.67 % (577094)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=2482918686:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.19/0.67 % (577087)Instruction limit reached!
% 2.19/0.67 % (577087)------------------------------
% 2.19/0.67 % (577087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577087)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577087)Termination reason: Instruction limit
% 2.19/0.67 % (577087)Termination phase: Clausification
% 2.19/0.67 % (577087)Time elapsed: 0.029 s
% 2.19/0.67 % (577087)Peak memory usage: 12 MB
% 2.19/0.67 % (577087)Instructions burned: 60 (million)
% 2.19/0.67 % (577095)Instruction limit reached!
% 2.19/0.67 % (577095)------------------------------
% 2.19/0.67 % (577095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577095)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577095)Termination reason: Instruction limit
% 2.19/0.67 % (577095)Termination phase: shuffling
% 2.19/0.67 % (577095)Time elapsed: 0.004 s
% 2.19/0.67 % (577095)Peak memory usage: 10 MB
% 2.19/0.67 % (577095)Instructions burned: 8 (million)
% 2.19/0.67 % (577097)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=919945537:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.19/0.67 % (577094)Instruction limit reached!
% 2.19/0.67 % (577094)------------------------------
% 2.19/0.67 % (577094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.19/0.67 % (577094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.19/0.67 % (577094)CaDiCaL version: 2.1.3
% 2.19/0.67 % (577094)Termination reason: Instruction limit
% 2.19/0.67 % (577094)Termination phase: shuffling
% 2.19/0.67 % (577094)Time elapsed: 0.015 s
% 2.19/0.67 % (577094)Peak memory usage: 10 MB
% 2.19/0.67 % (577094)Instructions burned: 32 (million)
% 2.19/0.67 % (577044)Instruction limit reached!
% 2.19/0.67 % (577044)------------------------------
% 2.41/0.74 % (577044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577044)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577044)Termination reason: Instruction limit
% 2.41/0.74 % (577044)Termination phase: Saturation
% 2.41/0.74 % (577044)Time elapsed: 0.220 s
% 2.41/0.74 % (577044)Peak memory usage: 16 MB
% 2.41/0.74 % (577044)Instructions burned: 637 (million)
% 2.41/0.74 % (577097)Instruction limit reached!
% 2.41/0.74 % (577097)------------------------------
% 2.41/0.74 % (577097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577097)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577097)Termination reason: Instruction limit
% 2.41/0.74 % (577097)Termination phase: shuffling
% 2.41/0.74 % (577097)Time elapsed: 0.011 s
% 2.41/0.74 % (577097)Peak memory usage: 10 MB
% 2.41/0.74 % (577097)Instructions burned: 24 (million)
% 2.41/0.74 % (577101)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2072111045:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.41/0.74 % (577104)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=439191575:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/193Mi)
% 2.41/0.74 % (577100)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3824458133:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.41/0.74 % (577103)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=104943291:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2997 on theBenchmark for (2997ds/143Mi)
% 2.41/0.74 % (577071)Instruction limit reached!
% 2.41/0.74 % (577071)------------------------------
% 2.41/0.74 % (577071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577071)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577071)Termination reason: Instruction limit
% 2.41/0.74 % (577071)Termination phase: Saturation
% 2.41/0.74 % (577071)Time elapsed: 0.129 s
% 2.41/0.74 % (577071)Peak memory usage: 15 MB
% 2.41/0.74 % (577071)Instructions burned: 251 (million)
% 2.41/0.74 % (577106)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1825968701:i=42:hud=10:rtra=on_2997 on theBenchmark for (2997ds/42Mi)
% 2.41/0.74 % (577100)Instruction limit reached!
% 2.41/0.74 % (577100)------------------------------
% 2.41/0.74 % (577100)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577100)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577100)Termination reason: Instruction limit
% 2.41/0.74 % (577100)Termination phase: shuffling
% 2.41/0.74 % (577100)Time elapsed: 0.019 s
% 2.41/0.74 % (577100)Peak memory usage: 10 MB
% 2.41/0.74 % (577100)Instructions burned: 20 (million)
% 2.41/0.74 % (577111)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.41/0.74 % (577111)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3843360764:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.41/0.74 % (577106)Instruction limit reached!
% 2.41/0.74 % (577106)------------------------------
% 2.41/0.74 % (577106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577106)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577106)Termination reason: Instruction limit
% 2.41/0.74 % (577106)Termination phase: Preprocessing 1
% 2.41/0.74 % (577106)Time elapsed: 0.020 s
% 2.41/0.74 % (577106)Peak memory usage: 10 MB
% 2.41/0.74 % (577106)Instructions burned: 42 (million)
% 2.41/0.74 % (577111)Instruction limit reached!
% 2.41/0.74 % (577111)------------------------------
% 2.41/0.74 % (577111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.41/0.74 % (577111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.41/0.74 % (577111)CaDiCaL version: 2.1.3
% 2.41/0.74 % (577111)Termination reason: Instruction limit
% 2.41/0.74 % (577111)Termination phase: shuffling
% 2.41/0.74 % (577111)Time elapsed: 0.004 s
% 3.06/0.83 % (577111)Peak memory usage: 10 MB
% 3.06/0.83 % (577111)Instructions burned: 7 (million)
% 3.06/0.83 % (577112)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=512076391:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 3.06/0.83 % (577115)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 3.06/0.83 % (577114)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=638096438:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 3.06/0.83 % (577115)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=140965647:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2996 on theBenchmark for (2996ds/6Mi)
% 3.06/0.83 % (577104)Instruction limit reached!
% 3.06/0.83 % (577104)------------------------------
% 3.06/0.83 % (577104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/0.83 % (577104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/0.83 % (577104)CaDiCaL version: 2.1.3
% 3.06/0.83 % (577104)Termination reason: Instruction limit
% 3.06/0.83 % (577104)Termination phase: Saturation
% 3.06/0.83 % (577104)Time elapsed: 0.053 s
% 3.06/0.83 % (577104)Peak memory usage: 14 MB
% 3.06/0.83 % (577104)Instructions burned: 196 (million)
% 3.06/0.83 % (577115)Instruction limit reached!
% 3.06/0.83 % (577115)------------------------------
% 3.06/0.83 % (577115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/0.83 % (577115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/0.83 % (577115)CaDiCaL version: 2.1.3
% 3.06/0.83 % (577115)Termination reason: Instruction limit
% 3.06/0.83 % (577115)Termination phase: shuffling
% 3.06/0.83 % (577115)Time elapsed: 0.004 s
% 3.06/0.83 % (577115)Peak memory usage: 10 MB
% 3.06/0.83 % (577115)Instructions burned: 8 (million)
% 3.06/0.83 % (577119)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3820590906:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2996 on theBenchmark for (2996ds/22Mi)
% 3.06/0.83 % (577119)Instruction limit reached!
% 3.06/0.83 % (577119)------------------------------
% 3.06/0.83 % (577119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/0.83 % (577119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/0.83 % (577119)CaDiCaL version: 2.1.3
% 3.06/0.83 % (577119)Termination reason: Instruction limit
% 3.06/0.83 % (577119)Termination phase: Property scanning
% 3.06/0.83 % (577119)Time elapsed: 0.006 s
% 3.06/0.83 % (577119)Peak memory usage: 11 MB
% 3.06/0.83 % (577119)Instructions burned: 25 (million)
% 3.06/0.83 % (577103)Instruction limit reached!
% 3.06/0.83 % (577103)------------------------------
% 3.06/0.83 % (577103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/0.83 % (577103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/0.83 % (577103)CaDiCaL version: 2.1.3
% 3.06/0.83 % (577103)Termination reason: Instruction limit
% 3.06/0.83 % (577103)Termination phase: Saturation
% 3.06/0.83 % (577103)Time elapsed: 0.067 s
% 3.06/0.83 % (577103)Peak memory usage: 13 MB
% 3.06/0.83 % (577103)Instructions burned: 144 (million)
% 3.06/0.83 % (577120)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3582097842:i=19:add=on:rtra=on_2996 on theBenchmark for (2996ds/19Mi)
% 3.06/0.83 % (577122)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=2779383815:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/316Mi)
% 3.06/0.83 % (577078)Instruction limit reached!
% 3.06/0.83 % (577078)------------------------------
% 3.06/0.83 % (577078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.06/0.83 % (577078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.06/0.83 % (577078)CaDiCaL version: 2.1.3
% 3.06/0.83 % (577078)Termination reason: Instruction limit
% 3.06/0.83 % (577078)Termination phase: Saturation
% 3.06/0.83 % (577078)Time elapsed: 0.177 s
% 3.06/0.83 % (577078)Peak memory usage: 15 MB
% 3.06/0.83 % (577078)Instructions burned: 329 (million)
% 3.06/0.83 % (577120)Instruction limit reached!
% 3.06/0.83 % (577120)------------------------------
% 3.06/0.83 % (577120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/0.93 % (577120)CaDiCaL version: 2.1.3
% 3.49/0.93 % (577120)Termination reason: Instruction limit
% 3.49/0.93 % (577120)Termination phase: shuffling
% 3.49/0.93 % (577120)Time elapsed: 0.010 s
% 3.49/0.93 % (577120)Peak memory usage: 10 MB
% 3.49/0.93 % (577120)Instructions burned: 20 (million)
% 3.49/0.93 % (577123)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=271070626:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2996 on theBenchmark for (2996ds/853Mi)
% 3.49/0.93 % (577126)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=472763199:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.49/0.93 % (577127)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=3640654980:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.49/0.93 % (577126)Instruction limit reached!
% 3.49/0.93 % (577126)------------------------------
% 3.49/0.93 % (577126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/0.93 % (577126)CaDiCaL version: 2.1.3
% 3.49/0.93 % (577126)Termination reason: Instruction limit
% 3.49/0.93 % (577126)Termination phase: shuffling
% 3.49/0.93 % (577126)Time elapsed: 0.021 s
% 3.49/0.93 % (577126)Peak memory usage: 10 MB
% 3.49/0.93 % (577126)Instructions burned: 46 (million)
% 3.49/0.93 % (577114)Instruction limit reached!
% 3.49/0.93 % (577114)------------------------------
% 3.49/0.93 % (577114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/0.93 % (577114)CaDiCaL version: 2.1.3
% 3.49/0.93 % (577114)Termination reason: Instruction limit
% 3.49/0.93 % (577114)Termination phase: Saturation
% 3.49/0.93 % (577114)Time elapsed: 0.082 s
% 3.49/0.93 % (577114)Peak memory usage: 14 MB
% 3.49/0.93 % (577114)Instructions burned: 171 (million)
% 3.49/0.93 % (577112)Instruction limit reached!
% 3.49/0.93 % (577112)------------------------------
% 3.49/0.93 % (577112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/0.93 % (577112)CaDiCaL version: 2.1.3
% 3.49/0.93 % (577112)Termination reason: Instruction limit
% 3.49/0.93 % (577112)Termination phase: Saturation
% 3.49/0.93 % (577112)Time elapsed: 0.094 s
% 3.49/0.93 % (577112)Peak memory usage: 15 MB
% 3.49/0.93 % (577112)Instructions burned: 181 (million)
% 3.49/0.93 % (577131)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1556373465:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2995 on theBenchmark for (2995ds/21Mi)
% 3.49/0.93 % (577132)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.49/0.93 % (577132)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=2278569722:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/200Mi)
% 3.49/0.93 % (577133)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=644904139:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2995 on theBenchmark for (2995ds/13Mi)
% 3.49/0.93 % (577131)Instruction limit reached!
% 3.49/0.93 % (577131)------------------------------
% 3.49/0.93 % (577131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.49/0.93 % (577131)CaDiCaL version: 2.1.3
% 3.49/0.93 % (577131)Termination reason: Instruction limit
% 3.49/0.93 % (577131)Termination phase: shuffling
% 3.49/0.93 % (577131)Time elapsed: 0.011 s
% 3.49/0.93 % (577131)Peak memory usage: 10 MB
% 3.49/0.93 % (577131)Instructions burned: 23 (million)
% 3.49/0.93 % (577133)Instruction limit reached!
% 3.49/0.93 % (577133)------------------------------
% 3.49/0.93 % (577133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.49/0.93 % (577133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577133)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577133)Termination reason: Instruction limit
% 5.02/1.10 % (577133)Termination phase: shuffling
% 5.02/1.10 % (577133)Time elapsed: 0.006 s
% 5.02/1.10 % (577133)Peak memory usage: 10 MB
% 5.02/1.10 % (577133)Instructions burned: 13 (million)
% 5.02/1.10 % (577122)Instruction limit reached!
% 5.02/1.10 % (577122)------------------------------
% 5.02/1.10 % (577122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.02/1.10 % (577122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577122)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577122)Termination reason: Instruction limit
% 5.02/1.10 % (577122)Termination phase: Saturation
% 5.02/1.10 % (577122)Time elapsed: 0.092 s
% 5.02/1.10 % (577122)Peak memory usage: 17 MB
% 5.02/1.10 % (577122)Instructions burned: 316 (million)
% 5.02/1.10 % (577137)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=3107373430:i=66:s2at=3:nm=2:rtra=on:rawr=on_2995 on theBenchmark for (2995ds/66Mi)
% 5.02/1.10 % (577138)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=3465317299:i=51:fsr=off:rtra=on_2995 on theBenchmark for (2995ds/51Mi)
% 5.02/1.10 % (577139)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3032047303:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 5.02/1.10 % (577139)Instruction limit reached!
% 5.02/1.10 % (577139)------------------------------
% 5.02/1.10 % (577139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.02/1.10 % (577139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577139)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577139)Termination reason: Instruction limit
% 5.02/1.10 % (577139)Termination phase: shuffling
% 5.02/1.10 % (577139)Time elapsed: 0.009 s
% 5.02/1.10 % (577139)Peak memory usage: 10 MB
% 5.02/1.10 % (577139)Instructions burned: 34 (million)
% 5.02/1.10 % (577138)Instruction limit reached!
% 5.02/1.10 % (577138)------------------------------
% 5.02/1.10 % (577138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.02/1.10 % (577138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577138)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577138)Termination reason: Instruction limit
% 5.02/1.10 % (577138)Termination phase: Preprocessing 3
% 5.02/1.10 % (577138)Time elapsed: 0.025 s
% 5.02/1.10 % (577138)Peak memory usage: 11 MB
% 5.02/1.10 % (577138)Instructions burned: 52 (million)
% 5.02/1.10 % (577137)Instruction limit reached!
% 5.02/1.10 % (577137)------------------------------
% 5.02/1.10 % (577137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.02/1.10 % (577137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577137)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577137)Termination reason: Instruction limit
% 5.02/1.10 % (577137)Termination phase: SInE selection
% 5.02/1.10 % (577137)Time elapsed: 0.031 s
% 5.02/1.10 % (577137)Peak memory usage: 11 MB
% 5.02/1.10 % (577137)Instructions burned: 67 (million)
% 5.02/1.10 % (577143)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=4060839713:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 5.02/1.10 % (577144)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=3464399413:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 5.02/1.10 % (577145)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=2965675662:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.02/1.10 % (577144)Instruction limit reached!
% 5.02/1.10 % (577144)------------------------------
% 5.02/1.10 % (577144)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.02/1.10 % (577144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.02/1.10 % (577144)CaDiCaL version: 2.1.3
% 5.02/1.10 % (577144)Termination reason: Instruction limit
% 5.02/1.10 % (577144)Termination phase: Property scanning
% 5.02/1.10 % (577144)Time elapsed: 0.016 s
% 5.02/1.10 % (577144)Peak memory usage: 10 MB
% 5.02/1.10 % (577144)Instructions burned: 35 (million)
% 5.02/1.10 % (577143)Instruction limit reached!
% 5.02/1.10 % (577143)------------------------------
% 5.02/1.10 % (577143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577143)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577143)Termination reason: Instruction limit
% 5.86/1.28 % (577143)Termination phase: Saturation
% 5.86/1.28 % (577143)Time elapsed: 0.036 s
% 5.86/1.28 % (577143)Peak memory usage: 14 MB
% 5.86/1.28 % (577143)Instructions burned: 138 (million)
% 5.86/1.28 % (577132)Instruction limit reached!
% 5.86/1.28 % (577132)------------------------------
% 5.86/1.28 % (577132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577132)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577132)Termination reason: Instruction limit
% 5.86/1.28 % (577132)Termination phase: Saturation
% 5.86/1.28 % (577132)Time elapsed: 0.100 s
% 5.86/1.28 % (577132)Peak memory usage: 14 MB
% 5.86/1.28 % (577132)Instructions burned: 200 (million)
% 5.86/1.28 % (577150)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=1744305796:st=2:i=246:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/246Mi)
% 5.86/1.28 % (577149)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.86/1.28 % (577145)Instruction limit reached!
% 5.86/1.28 % (577145)------------------------------
% 5.86/1.28 % (577145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577145)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577145)Termination reason: Instruction limit
% 5.86/1.28 % (577145)Termination phase: Property scanning
% 5.86/1.28 % (577145)Time elapsed: 0.032 s
% 5.86/1.28 % (577145)Peak memory usage: 11 MB
% 5.86/1.28 % (577145)Instructions burned: 67 (million)
% 5.86/1.28 % (577149)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=758841789:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2994 on theBenchmark for (2994ds/180Mi)
% 5.86/1.28 % (577151)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1309193124:cond=on:i=96:bd=all:rtra=on_2994 on theBenchmark for (2994ds/96Mi)
% 5.86/1.28 % (577153)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=2651578726:i=427:sd=1:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/427Mi)
% 5.86/1.28 % (577151)Instruction limit reached!
% 5.86/1.28 % (577151)------------------------------
% 5.86/1.28 % (577151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577151)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577151)Termination reason: Instruction limit
% 5.86/1.28 % (577151)Termination phase: Property scanning
% 5.86/1.28 % (577151)Time elapsed: 0.045 s
% 5.86/1.28 % (577151)Peak memory usage: 12 MB
% 5.86/1.28 % (577151)Instructions burned: 97 (million)
% 5.86/1.28 % (577150)Instruction limit reached!
% 5.86/1.28 % (577150)------------------------------
% 5.86/1.28 % (577150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577150)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577150)Termination reason: Instruction limit
% 5.86/1.28 % (577150)Termination phase: Saturation
% 5.86/1.28 % (577150)Time elapsed: 0.067 s
% 5.86/1.28 % (577150)Peak memory usage: 15 MB
% 5.86/1.28 % (577150)Instructions burned: 247 (million)
% 5.86/1.28 % (577158)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=3989835525:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/515Mi)
% 5.86/1.28 % (577157)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=375973155:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/874Mi)
% 5.86/1.28 % (577149)Instruction limit reached!
% 5.86/1.28 % (577149)------------------------------
% 5.86/1.28 % (577149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.86/1.28 % (577149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.86/1.28 % (577149)CaDiCaL version: 2.1.3
% 5.86/1.28 % (577149)Termination reason: Instruction limit
% 5.86/1.28 % (577149)Termination phase: Saturation
% 5.86/1.28 % (577149)Time elapsed: 0.081 s
% 5.86/1.28 % (577149)Peak memory usage: 13 MB
% 5.86/1.28 % (577149)Instructions burned: 180 (million)
% 5.86/1.28 % (577127)Instruction limit reached!
% 6.58/1.33 % (577127)------------------------------
% 6.58/1.33 % (577127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577127)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577127)Termination reason: Instruction limit
% 6.58/1.33 % (577127)Termination phase: Saturation
% 6.58/1.33 % (577127)Time elapsed: 0.240 s
% 6.58/1.33 % (577127)Peak memory usage: 16 MB
% 6.58/1.33 % (577127)Instructions burned: 480 (million)
% 6.58/1.33 % (577161)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=2421868436:st=1.5:i=130:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/130Mi)
% 6.58/1.33 % (577162)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=2638625218:i=44:ep=R:rtra=on:ntd=on_2993 on theBenchmark for (2993ds/44Mi)
% 6.58/1.33 % (577162)Instruction limit reached!
% 6.58/1.33 % (577162)------------------------------
% 6.58/1.33 % (577162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577162)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577162)Termination reason: Instruction limit
% 6.58/1.33 % (577162)Termination phase: Property scanning
% 6.58/1.33 % (577162)Time elapsed: 0.020 s
% 6.58/1.33 % (577162)Peak memory usage: 10 MB
% 6.58/1.33 % (577162)Instructions burned: 45 (million)
% 6.58/1.33 % (577165)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=3682259190:s2a=on:i=571:nm=16:rtra=on_2993 on theBenchmark for (2993ds/571Mi)
% 6.58/1.33 % (577161)Instruction limit reached!
% 6.58/1.33 % (577161)------------------------------
% 6.58/1.33 % (577161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577161)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577161)Termination reason: Instruction limit
% 6.58/1.33 % (577161)Termination phase: Saturation
% 6.58/1.33 % (577161)Time elapsed: 0.063 s
% 6.58/1.33 % (577161)Peak memory usage: 13 MB
% 6.58/1.33 % (577161)Instructions burned: 130 (million)
% 6.58/1.33 % (577167)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=4098246865:i=450:rtra=on:ixr=off:ntd=on_2992 on theBenchmark for (2992ds/450Mi)
% 6.58/1.33 % (577158)Instruction limit reached!
% 6.58/1.33 % (577158)------------------------------
% 6.58/1.33 % (577158)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577158)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577158)Termination reason: Instruction limit
% 6.58/1.33 % (577158)Termination phase: Saturation
% 6.58/1.33 % (577158)Time elapsed: 0.139 s
% 6.58/1.33 % (577158)Peak memory usage: 16 MB
% 6.58/1.33 % (577158)Instructions burned: 516 (million)
% 6.58/1.33 % (577169)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=2694720861:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 6.58/1.33 % (577153)Instruction limit reached!
% 6.58/1.33 % (577153)------------------------------
% 6.58/1.33 % (577153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577153)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577153)Termination reason: Instruction limit
% 6.58/1.33 % (577153)Termination phase: Saturation
% 6.58/1.33 % (577153)Time elapsed: 0.218 s
% 6.58/1.33 % (577153)Peak memory usage: 16 MB
% 6.58/1.33 % (577153)Instructions burned: 428 (million)
% 6.58/1.33 % (577169)Instruction limit reached!
% 6.58/1.33 % (577169)------------------------------
% 6.58/1.33 % (577169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.58/1.33 % (577169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.58/1.33 % (577169)CaDiCaL version: 2.1.3
% 6.58/1.33 % (577169)Termination reason: Instruction limit
% 6.58/1.33 % (577169)Termination phase: Property scanning
% 6.58/1.33 % (577169)Time elapsed: 0.024 s
% 6.58/1.33 % (577169)Peak memory usage: 12 MB
% 6.58/1.33 % (577169)Instructions burned: 98 (million)
% 6.58/1.33 % (577171)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=571930942:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 7.02/1.42 % (577172)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=15913197:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2992 on theBenchmark for (2992ds/105Mi)
% 7.02/1.42 % (577123)Instruction limit reached!
% 7.02/1.42 % (577123)------------------------------
% 7.02/1.42 % (577123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577123)CaDiCaL version: 2.1.3
% 7.02/1.42 % (577123)Termination reason: Instruction limit
% 7.02/1.42 % (577123)Termination phase: Saturation
% 7.02/1.42 % (577123)Time elapsed: 0.449 s
% 7.02/1.42 % (577123)Peak memory usage: 17 MB
% 7.02/1.42 % (577123)Instructions burned: 854 (million)
% 7.02/1.42 % (577171)Instruction limit reached!
% 7.02/1.42 % (577171)------------------------------
% 7.02/1.42 % (577171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577171)CaDiCaL version: 2.1.3
% 7.02/1.42 % (577171)Termination reason: Instruction limit
% 7.02/1.42 % (577171)Termination phase: SInE selection
% 7.02/1.42 % (577171)Time elapsed: 0.030 s
% 7.02/1.42 % (577171)Peak memory usage: 11 MB
% 7.02/1.42 % (577171)Instructions burned: 65 (million)
% 7.02/1.42 % (577172)Instruction limit reached!
% 7.02/1.42 % (577172)------------------------------
% 7.02/1.42 % (577172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577172)CaDiCaL version: 2.1.3
% 7.02/1.42 % (577172)Termination reason: Instruction limit
% 7.02/1.42 % (577172)Termination phase: Preprocessing 3
% 7.02/1.42 % (577172)Time elapsed: 0.026 s
% 7.02/1.42 % (577172)Peak memory usage: 11 MB
% 7.02/1.42 % (577172)Instructions burned: 108 (million)
% 7.02/1.42 % (577177)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=358645403:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2991 on theBenchmark for (2991ds/495Mi)
% 7.02/1.42 % (577175)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=2718358241:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2991 on theBenchmark for (2991ds/5755Mi)
% 7.02/1.42 % (577176)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=1826788934:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2991 on theBenchmark for (2991ds/375Mi)
% 7.02/1.42 % (577101)Instruction limit reached!
% 7.02/1.42 % (577101)------------------------------
% 7.02/1.42 % (577101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577101)CaDiCaL version: 2.1.3
% 7.02/1.42 % (577101)Termination reason: Instruction limit
% 7.02/1.42 % (577101)Termination phase: Saturation
% 7.02/1.42 % (577101)Time elapsed: 0.666 s
% 7.02/1.42 % (577101)Peak memory usage: 19 MB
% 7.02/1.42 % (577101)Instructions burned: 1242 (million)
% 7.02/1.42 % (577181)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=2988425486:cond=on:i=34:hud=10:nm=10:rtra=on_2990 on theBenchmark for (2990ds/34Mi)
% 7.02/1.42 % (577177)Instruction limit reached!
% 7.02/1.42 % (577177)------------------------------
% 7.02/1.42 % (577177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577177)CaDiCaL version: 2.1.3
% 7.02/1.42 % (577177)Termination reason: Instruction limit
% 7.02/1.42 % (577177)Termination phase: Saturation
% 7.02/1.42 % (577177)Time elapsed: 0.127 s
% 7.02/1.42 % (577177)Peak memory usage: 16 MB
% 7.02/1.42 % (577177)Instructions burned: 496 (million)
% 7.02/1.42 % (577181)Instruction limit reached!
% 7.02/1.42 % (577181)------------------------------
% 7.02/1.42 % (577181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.02/1.42 % (577181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/1.42 % (577181)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577181)Termination reason: Instruction limit
% 7.99/1.60 % (577181)Termination phase: Property scanning
% 7.99/1.60 % (577181)Time elapsed: 0.017 s
% 7.99/1.60 % (577181)Peak memory usage: 10 MB
% 7.99/1.60 % (577181)Instructions burned: 35 (million)
% 7.99/1.60 % (577183)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=2569131350:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2990 on theBenchmark for (2990ds/91Mi)
% 7.99/1.60 % (577167)Instruction limit reached!
% 7.99/1.60 % (577167)------------------------------
% 7.99/1.60 % (577167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577167)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577167)Termination reason: Instruction limit
% 7.99/1.60 % (577167)Termination phase: Saturation
% 7.99/1.60 % (577167)Time elapsed: 0.243 s
% 7.99/1.60 % (577167)Peak memory usage: 16 MB
% 7.99/1.60 % (577167)Instructions burned: 451 (million)
% 7.99/1.60 % (577165)Instruction limit reached!
% 7.99/1.60 % (577165)------------------------------
% 7.99/1.60 % (577165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577165)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577165)Termination reason: Instruction limit
% 7.99/1.60 % (577165)Termination phase: Saturation
% 7.99/1.60 % (577165)Time elapsed: 0.303 s
% 7.99/1.60 % (577165)Peak memory usage: 16 MB
% 7.99/1.60 % (577165)Instructions burned: 572 (million)
% 7.99/1.60 % (577185)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=3742323522:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2990 on theBenchmark for (2990ds/66Mi)
% 7.99/1.60 % (577183)Instruction limit reached!
% 7.99/1.60 % (577183)------------------------------
% 7.99/1.60 % (577183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577183)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577183)Termination reason: Instruction limit
% 7.99/1.60 % (577183)Termination phase: Twee Goal Transformation
% 7.99/1.60 % (577183)Time elapsed: 0.024 s
% 7.99/1.60 % (577183)Peak memory usage: 12 MB
% 7.99/1.60 % (577183)Instructions burned: 93 (million)
% 7.99/1.60 % (577186)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1770388748:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2990 on theBenchmark for (2990ds/22Mi)
% 7.99/1.60 % (577187)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=1060069922:i=338:bd=all:ins=4:rtra=on_2990 on theBenchmark for (2990ds/338Mi)
% 7.99/1.60 % (577189)lrs+10_1_sil=128000:si=on:urr=on:random_seed=1998839069:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2990 on theBenchmark for (2990ds/28Mi)
% 7.99/1.60 % (577186)Instruction limit reached!
% 7.99/1.60 % (577186)------------------------------
% 7.99/1.60 % (577186)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577186)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577186)Termination reason: Instruction limit
% 7.99/1.60 % (577186)Termination phase: shuffling
% 7.99/1.60 % (577186)Time elapsed: 0.010 s
% 7.99/1.60 % (577186)Peak memory usage: 10 MB
% 7.99/1.60 % (577186)Instructions burned: 22 (million)
% 7.99/1.60 % (577189)Instruction limit reached!
% 7.99/1.60 % (577189)------------------------------
% 7.99/1.60 % (577189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577189)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577189)Termination reason: Instruction limit
% 7.99/1.60 % (577189)Termination phase: SInE selection
% 7.99/1.60 % (577189)Time elapsed: 0.009 s
% 7.99/1.60 % (577189)Peak memory usage: 11 MB
% 7.99/1.60 % (577189)Instructions burned: 40 (million)
% 7.99/1.60 % (577185)Instruction limit reached!
% 7.99/1.60 % (577185)------------------------------
% 7.99/1.60 % (577185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.60 % (577185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.60 % (577185)CaDiCaL version: 2.1.3
% 7.99/1.60 % (577185)Termination reason: Instruction limit
% 7.99/1.60 % (577185)Termination phase: Property scanning
% 7.99/1.64 % (577185)Time elapsed: 0.032 s
% 7.99/1.64 % (577185)Peak memory usage: 12 MB
% 7.99/1.64 % (577185)Instructions burned: 68 (million)
% 7.99/1.64 % (577194)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=2546265193:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2989 on theBenchmark for (2989ds/340Mi)
% 7.99/1.64 % (577193)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 7.99/1.64 % (577193)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=1751240552:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/137Mi)
% 7.99/1.64 % (577176)Instruction limit reached!
% 7.99/1.64 % (577176)------------------------------
% 7.99/1.64 % (577176)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577176)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577176)Termination reason: Instruction limit
% 7.99/1.64 % (577176)Termination phase: Saturation
% 7.99/1.64 % (577176)Time elapsed: 0.193 s
% 7.99/1.64 % (577176)Peak memory usage: 15 MB
% 7.99/1.64 % (577176)Instructions burned: 375 (million)
% 7.99/1.64 % (577195)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=3876354388:i=227:sd=1:bd=all:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/227Mi)
% 7.99/1.64 % (577198)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.99/1.64 % (577198)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=2234571439:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/373Mi)
% 7.99/1.64 % (577157)Instruction limit reached!
% 7.99/1.64 % (577157)------------------------------
% 7.99/1.64 % (577157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577157)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577157)Termination reason: Instruction limit
% 7.99/1.64 % (577157)Termination phase: Saturation
% 7.99/1.64 % (577157)Time elapsed: 0.462 s
% 7.99/1.64 % (577157)Peak memory usage: 18 MB
% 7.99/1.64 % (577157)Instructions burned: 874 (million)
% 7.99/1.64 % (577193)Instruction limit reached!
% 7.99/1.64 % (577193)------------------------------
% 7.99/1.64 % (577193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577193)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577193)Termination reason: Instruction limit
% 7.99/1.64 % (577193)Termination phase: Saturation
% 7.99/1.64 % (577193)Time elapsed: 0.062 s
% 7.99/1.64 % (577193)Peak memory usage: 13 MB
% 7.99/1.64 % (577193)Instructions burned: 138 (million)
% 7.99/1.64 % (577201)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=2076065267:i=116:ep=RSTC:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/116Mi)
% 7.99/1.64 % (577195)Refutation not found, incomplete strategy
% 7.99/1.64 % (577195)------------------------------
% 7.99/1.64 % (577195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577195)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577195)Termination reason: Refutation not found, incomplete strategy
% 7.99/1.64 % (577195)Time elapsed: 0.052 s
% 7.99/1.64 % (577195)Peak memory usage: 14 MB
% 7.99/1.64 % (577195)Instructions burned: 105 (million)
% 7.99/1.64 % (577195)------------------------------
% 7.99/1.64 % (577195)------------------------------
% 7.99/1.64 % (577203)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=1670879659:i=575:rtra=on_2989 on theBenchmark for (2989ds/575Mi)
% 7.99/1.64 % (577204)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=184857987:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 7.99/1.64 % (577194)Instruction limit reached!
% 7.99/1.64 % (577194)------------------------------
% 7.99/1.64 % (577194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577194)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577194)Termination reason: Instruction limit
% 7.99/1.64 % (577194)Termination phase: Saturation
% 7.99/1.64 % (577194)Time elapsed: 0.093 s
% 7.99/1.64 % (577194)Peak memory usage: 15 MB
% 7.99/1.64 % (577194)Instructions burned: 342 (million)
% 7.99/1.64 % (577207)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=4242515129:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2988 on theBenchmark for (2988ds/9840Mi)
% 7.99/1.64 % (577201)Instruction limit reached!
% 7.99/1.64 % (577201)------------------------------
% 7.99/1.64 % (577201)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577201)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577201)Termination reason: Instruction limit
% 7.99/1.64 % (577201)Termination phase: Property scanning
% 7.99/1.64 % (577201)Time elapsed: 0.054 s
% 7.99/1.64 % (577201)Peak memory usage: 12 MB
% 7.99/1.64 % (577201)Instructions burned: 118 (million)
% 7.99/1.64 % (577209)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=1340955260:i=421:rtra=on:ss=axioms_2988 on theBenchmark for (2988ds/421Mi)
% 7.99/1.64 % (577187)Instruction limit reached!
% 7.99/1.64 % (577187)------------------------------
% 7.99/1.64 % (577187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577187)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577187)Termination reason: Instruction limit
% 7.99/1.64 % (577187)Termination phase: Saturation
% 7.99/1.64 % (577187)Time elapsed: 0.177 s
% 7.99/1.64 % (577187)Peak memory usage: 17 MB
% 7.99/1.64 % (577187)Instructions burned: 339 (million)
% 7.99/1.64 % (577211)WARNING Broken Constraint: if sine_to_age_tolerance(3) 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
% 7.99/1.64 % (577211)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=3742532060:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2988 on theBenchmark for (2988ds/270Mi)
% 7.99/1.64 % (577198)Instruction limit reached!
% 7.99/1.64 % (577198)------------------------------
% 7.99/1.64 % (577198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577198)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577198)Termination reason: Instruction limit
% 7.99/1.64 % (577198)Termination phase: Saturation
% 7.99/1.64 % (577198)Time elapsed: 0.193 s
% 7.99/1.64 % (577198)Peak memory usage: 14 MB
% 7.99/1.64 % (577198)Instructions burned: 374 (million)
% 7.99/1.64 % (577213)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=50248622:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/31Mi)
% 7.99/1.64 % (577204)Instruction limit reached!
% 7.99/1.64 % (577204)------------------------------
% 7.99/1.64 % (577204)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577204)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577204)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577204)Termination reason: Instruction limit
% 7.99/1.64 % (577204)Termination phase: Saturation
% 7.99/1.64 % (577204)Time elapsed: 0.163 s
% 7.99/1.64 % (577204)Peak memory usage: 14 MB
% 7.99/1.64 % (577204)Instructions burned: 270 (million)
% 7.99/1.64 % (577213)Instruction limit reached!
% 7.99/1.64 % (577213)------------------------------
% 7.99/1.64 % (577213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577213)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577213)Termination reason: Instruction limit
% 7.99/1.64 % (577213)Termination phase: shuffling
% 7.99/1.64 % (577213)Time elapsed: 0.015 s
% 7.99/1.64 % (577213)Peak memory usage: 10 MB
% 7.99/1.64 % (577213)Instructions burned: 31 (million)
% 7.99/1.64 % (577215)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 7.99/1.64 % (577215)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
% 7.99/1.64 % (577215)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=4076942622:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2987 on theBenchmark for (2987ds/1440Mi)
% 7.99/1.64 % (577216)dis+10_2_sil=128000:si=on:random_seed=3156889837:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2987 on theBenchmark for (2987ds/339Mi)
% 7.99/1.64 % (577207) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-577036-577207"...
% 7.99/1.64 % (577207)...printing done.
% 7.99/1.64 % (577207)Refutation found. Thanks to Tanya!
% 7.99/1.64 % SZS status Theorem for theBenchmark
% 7.99/1.64 % SZS output start Proof for theBenchmark
% 7.99/1.64 thf(type_def_5, type, standard_Constant: $tType > $tType).
% 7.99/1.64 thf(type_def_6, type, labeled_graph: ($tType * $tType) > $tType).
% 7.99/1.64 thf(type_def_7, type, product_prod: ($tType * $tType) > $tType).
% 7.99/1.64 thf(type_def_8, type, sum_sum: ($tType * $tType) > $tType).
% 7.99/1.64 thf(type_def_9, type, set: $tType > $tType).
% 7.99/1.64 thf(type_def_10, type, nat: $tType).
% 7.99/1.64 thf(type_def_11, type, b: $tType).
% 7.99/1.64 thf(type_def_12, type, a: $tType).
% 7.99/1.64 thf(type_def_13, type, sTfun: ($tType * $tType) > $tType).
% 7.99/1.64 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_1, type, one: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_2, type, zero: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_3, type, bot: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_4, type, ord: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_5, type, order: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_6, type, linorder: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_7, type, preorder: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_8, type, zero_neq_one: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_9, type, order_bot: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_10, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_11, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 7.99/1.64 thf(func_def_12, type, equiv_equiv: !>[X0: $tType]:((set @ X0 > set @ product_prod @ X0 @ X0 > $o))).
% 7.99/1.64 thf(func_def_13, type, one_one: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_14, type, zero_zero: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_15, type, standard_S_Bot: !>[X0: $tType]:(standard_Constant @ X0)).
% 7.99/1.64 thf(func_def_16, type, standard_S_Idt: !>[X0: $tType]:(standard_Constant @ X0)).
% 7.99/1.64 thf(func_def_17, type, getRel: !>[X0: $tType, X1: $tType]:((X0 > labeled_graph @ X0 @ X1 > set @ product_prod @ X1 @ X1))).
% 7.99/1.64 thf(func_def_18, type, edge_preserving: !>[X0: $tType, X1: $tType, X2: $tType]:((set @ product_prod @ X0 @ X1 > set @ product_prod @ X2 @ product_prod @ X0 @ X0 > set @ product_prod @ X2 @ product_prod @ X1 @ X1 > $o))).
% 7.99/1.64 thf(func_def_19, type, graph_homomorphism: !>[X0: $tType, X1: $tType, X2: $tType]:((labeled_graph @ X0 @ X1 > labeled_graph @ X0 @ X2 > set @ product_prod @ X1 @ X2 > $o))).
% 7.99/1.64 thf(func_def_20, type, graph_union: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > labeled_graph @ X0 @ X1 > labeled_graph @ X0 @ X1))).
% 7.99/1.64 thf(func_def_21, type, labeled_LG: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ product_prod @ X1 @ X1 > set @ X1 > labeled_graph @ X0 @ X1))).
% 7.99/1.64 thf(func_def_22, type, labeled_edges: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > set @ product_prod @ X0 @ product_prod @ X1 @ X1))).
% 7.99/1.64 thf(func_def_23, type, labeled_vertices: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > set @ X1))).
% 7.99/1.64 thf(func_def_24, type, map_graph: !>[X0: $tType, X1: $tType, X2: $tType]:((set @ product_prod @ X0 @ X1 > labeled_graph @ X2 @ X0 > labeled_graph @ X2 @ X1))).
% 7.99/1.64 thf(func_def_25, type, on_triple: !>[X0: $tType, X1: $tType, X2: $tType]:((set @ product_prod @ X0 @ X1 > set @ product_prod @ product_prod @ X2 @ product_prod @ X0 @ X0 @ product_prod @ X2 @ product_prod @ X1 @ X1))).
% 7.99/1.64 thf(func_def_26, type, restrict: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > labeled_graph @ X0 @ X1))).
% 7.99/1.64 thf(func_def_27, type, univalent: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > $o))).
% 7.99/1.64 thf(func_def_28, type, bot_bot: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_29, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.99/1.64 thf(func_def_30, type, product_Pair: !>[X0: $tType, X1: $tType]:((X0 > X1 > product_prod @ X0 @ X1))).
% 7.99/1.64 thf(func_def_31, type, product_rec_prod: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > product_prod @ X0 @ X1 > X2))).
% 7.99/1.64 thf(func_def_32, type, domain: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > set @ X0))).
% 7.99/1.64 thf(func_def_33, type, id_on: !>[X0: $tType]:((set @ X0 > set @ product_prod @ X0 @ X0))).
% 7.99/1.64 thf(func_def_34, type, image: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > set @ X0 > set @ X1))).
% 7.99/1.64 thf(func_def_35, type, maintained: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ labeled_graph @ X0 @ X1 @ labeled_graph @ X0 @ X1 > labeled_graph @ X0 @ X2 > $o))).
% 7.99/1.64 thf(func_def_36, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 7.99/1.64 thf(func_def_37, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 7.99/1.64 thf(func_def_38, type, is_singleton: !>[X0: $tType]:((set @ X0 > $o))).
% 7.99/1.64 thf(func_def_39, type, the_elem: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_40, type, standa1068660421e_rule: !>[X0: $tType]:((X0 > X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_41, type, standa244753842y_rule: !>[X0: $tType]:(product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat)).
% 7.99/1.64 thf(func_def_42, type, standa245363227y_rule: !>[X0: $tType]:((X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_43, type, standa1805702094y_rule: !>[X0: $tType]:((X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_44, type, standa400804411p_rule: !>[X0: $tType]:((X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_45, type, standa2114124375e_rule: !>[X0: $tType]:((X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_46, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 7.99/1.64 thf(func_def_47, type, g: labeled_graph @ standard_Constant @ a @ sum_sum @ a @ b).
% 7.99/1.64 thf(func_def_48, type, f: set @ product_prod @ nat @ sum_sum @ a @ b).
% 7.99/1.64 thf(func_def_49, type, l: standard_Constant @ a).
% 7.99/1.64 thf(func_def_50, type, v: sum_sum @ a @ b).
% 7.99/1.64 thf(func_def_54, type, vAND: ($o > $o > $o)).
% 7.99/1.64 thf(func_def_55, type, db0: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_56, type, db2: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_57, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.99/1.64 thf(func_def_58, type, db1: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_59, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.99/1.64 thf(func_def_60, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.99/1.64 thf(func_def_61, type, vIMP: ($o > $o > $o)).
% 7.99/1.64 thf(func_def_62, type, db3: !>[X0: $tType]:(X0)).
% 7.99/1.64 thf(func_def_63, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.99/1.64 thf(func_def_64, type, sP0: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 7.99/1.64 thf(func_def_65, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 7.99/1.64 thf(func_def_66, type, sK2: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X1 @ X0 > X1 > X0))).
% 7.99/1.64 thf(func_def_67, type, sK3: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X5))).
% 7.99/1.64 thf(func_def_68, type, sK4: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X2))).
% 7.99/1.64 thf(func_def_69, type, sK5: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X6))).
% 7.99/1.64 thf(func_def_70, type, sK6: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X0))).
% 7.99/1.64 thf(func_def_71, type, sK7: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X1))).
% 7.99/1.64 thf(func_def_72, type, sK8: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X4))).
% 7.99/1.64 thf(func_def_73, type, sK9: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X6 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X1 @ X2 > X3))).
% 7.99/1.64 thf(func_def_74, type, sK10: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_75, type, sK11: (nat > (nat > $o) > nat)).
% 7.99/1.64 thf(func_def_76, type, sK12: ((nat > $o) > nat)).
% 7.99/1.64 thf(func_def_77, type, sK13: !>[X0: $tType]:((set @ X0 > X0 > set @ X0))).
% 7.99/1.64 thf(func_def_78, type, sK14: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_79, type, sK15: !>[X0: $tType, X1: $tType]:((set @ X1 > set @ product_prod @ X1 @ X0 > X0 > X1))).
% 7.99/1.64 thf(func_def_80, type, sK16: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_81, type, sK17: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_82, type, sK18: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_83, type, sK19: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X1))).
% 7.99/1.64 thf(func_def_84, type, sK20: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X2))).
% 7.99/1.64 thf(func_def_85, type, sK21: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X0))).
% 7.99/1.64 thf(func_def_86, type, sK22: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X4))).
% 7.99/1.64 thf(func_def_87, type, sK23: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X3))).
% 7.99/1.64 thf(func_def_88, type, sK24: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X5 @ product_prod @ X3 @ product_prod @ X1 @ X2 > X5))).
% 7.99/1.64 thf(func_def_89, type, sK25: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_90, type, sK26: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_91, type, sK27: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_92, type, sK28: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_93, type, sK29: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_94, type, sK30: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_95, type, sK31: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X2 @ product_prod @ X1 @ product_prod @ X3 @ X0 > X2))).
% 7.99/1.64 thf(func_def_96, type, sK32: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X2 @ product_prod @ X1 @ product_prod @ X3 @ X0 > X1))).
% 7.99/1.64 thf(func_def_97, type, sK33: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X2 @ product_prod @ X1 @ product_prod @ X3 @ X0 > X3))).
% 7.99/1.64 thf(func_def_98, type, sK34: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X2 @ product_prod @ X1 @ product_prod @ X3 @ X0 > X0))).
% 7.99/1.64 thf(func_def_99, type, sK35: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_100, type, sK36: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X1))).
% 7.99/1.64 thf(func_def_101, type, sK37: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X1 @ product_prod @ X2 @ X0 > $o) > X2))).
% 7.99/1.64 thf(func_def_102, type, sK38: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_103, type, sK39: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_104, type, sK40: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 7.99/1.64 thf(func_def_105, type, sK41: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X1 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ X4 > X3))).
% 7.99/1.64 thf(func_def_106, type, sK42: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X1 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ X4 > X0))).
% 7.99/1.64 thf(func_def_107, type, sK43: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X1 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ X4 > X2))).
% 7.99/1.64 thf(func_def_108, type, sK44: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X1 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ X4 > X1))).
% 7.99/1.64 thf(func_def_109, type, sK45: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X1 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X2 @ X4 > X4))).
% 7.99/1.64 thf(func_def_110, type, sK46: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X1 @ X0 > X1 > X0))).
% 7.99/1.64 thf(func_def_111, type, sK47: sum_sum @ a @ b).
% 7.99/1.64 thf(func_def_112, type, sK48: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_113, type, sK49: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > set @ product_prod @ X0 @ product_prod @ X1 @ X1))).
% 7.99/1.64 thf(func_def_114, type, sK50: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > set @ X1))).
% 7.99/1.64 thf(func_def_115, type, sK51: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ X1 > $o) > X0))).
% 7.99/1.64 thf(func_def_116, type, sK52: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ X1 > $o) > X1))).
% 7.99/1.64 thf(func_def_117, type, sK53: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ X1 > $o) > X3))).
% 7.99/1.64 thf(func_def_118, type, sK54: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ X1 > $o) > X2))).
% 7.99/1.64 thf(func_def_119, type, sK55: !>[X0: $tType, X1: $tType]:((X1 > set @ product_prod @ X1 @ X0 > X0))).
% 7.99/1.64 thf(func_def_120, type, sK56: !>[X0: $tType, X1: $tType]:((X1 > set @ product_prod @ X1 @ X0 > X0))).
% 7.99/1.64 thf(func_def_121, type, sK57: !>[X0: $tType, X1: $tType]:((labeled_graph @ X0 @ X1 > X0 > product_prod @ labeled_graph @ X0 @ nat @ labeled_graph @ X0 @ nat))).
% 7.99/1.64 thf(func_def_122, type, sK58: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X1 @ product_prod @ X0 @ X2 > X1))).
% 7.99/1.64 thf(func_def_123, type, sK59: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X1 @ product_prod @ X0 @ X2 > X0))).
% 7.99/1.64 thf(func_def_124, type, sK60: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X1 @ product_prod @ X0 @ X2 > X2))).
% 7.99/1.64 thf(func_def_125, type, sK61: !>[X0: $tType, X1: $tType]:(((X0 > X1) > (X0 > X1) > X0))).
% 7.99/1.64 thf(func_def_126, type, sK62: !>[X0: $tType]:(((X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_127, type, sK63: !>[X0: $tType, X1: $tType, X2: $tType]:((labeled_graph @ X2 @ X1 > labeled_graph @ X2 @ X0 > set @ product_prod @ X1 @ X0 > set @ product_prod @ X1 @ X0))).
% 7.99/1.64 thf(func_def_128, type, sK64: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_129, type, sK65: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_130, type, sK66: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X2))).
% 7.99/1.64 thf(func_def_131, type, sK67: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X6))).
% 7.99/1.64 thf(func_def_132, type, sK68: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X1))).
% 7.99/1.64 thf(func_def_133, type, sK69: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X3))).
% 7.99/1.64 thf(func_def_134, type, sK70: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X5))).
% 7.99/1.64 thf(func_def_135, type, sK71: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X4))).
% 7.99/1.64 thf(func_def_136, type, sK72: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X1 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X0 @ X6 > $o) > X0))).
% 7.99/1.64 thf(func_def_137, type, sK73: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X4))).
% 7.99/1.64 thf(func_def_138, type, sK74: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X2))).
% 7.99/1.64 thf(func_def_139, type, sK75: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X3))).
% 7.99/1.64 thf(func_def_140, type, sK76: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X0))).
% 7.99/1.64 thf(func_def_141, type, sK77: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X5))).
% 7.99/1.64 thf(func_def_142, type, sK78: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X4 @ product_prod @ X2 @ product_prod @ X0 @ product_prod @ X3 @ product_prod @ X5 @ X1 > $o) > X1))).
% 7.99/1.64 thf(func_def_143, type, sK79: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_144, type, sK80: !>[X0: $tType]:((product_prod @ X0 @ X0 > set @ X0 > X0))).
% 7.99/1.64 thf(func_def_145, type, sK81: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 7.99/1.64 thf(func_def_146, type, sK82: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 7.99/1.64 thf(func_def_147, type, sK83: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_148, type, sK84: !>[X0: $tType]:((X0 > set @ X0 > X0 > set @ X0 > set @ X0))).
% 7.99/1.64 thf(func_def_149, type, sK85: !>[X0: $tType]:((set @ X0 > X0))).
% 7.99/1.64 thf(func_def_150, type, sK86: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 7.99/1.64 thf(func_def_151, type, sK87: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_152, type, sK88: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 7.99/1.64 thf(func_def_153, type, sK89: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X1 @ X0 > set @ product_prod @ X1 @ X0 > X0))).
% 7.99/1.64 thf(func_def_154, type, sK90: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X1 @ X0 > set @ product_prod @ X1 @ X0 > X1))).
% 7.99/1.64 thf(func_def_155, type, sK91: !>[X0: $tType, X1: $tType]:(((labeled_graph @ X0 @ X1 > $o) > set @ X1))).
% 7.99/1.64 thf(func_def_156, type, sK92: !>[X0: $tType, X1: $tType]:(((labeled_graph @ X0 @ X1 > $o) > set @ product_prod @ X0 @ product_prod @ X1 @ X1))).
% 7.99/1.64 thf(func_def_157, type, sK93: !>[X0: $tType, X1: $tType]:(((product_prod @ X0 @ X1 > $o) > X1))).
% 7.99/1.64 thf(func_def_158, type, sK94: !>[X0: $tType, X1: $tType]:(((product_prod @ X0 @ X1 > $o) > X0))).
% 7.99/1.64 thf(func_def_159, type, sK95: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 7.99/1.64 thf(func_def_160, type, sK96: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 7.99/1.64 thf(func_def_161, type, sK97: !>[X0: $tType]:(((X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_162, type, sK98: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X0))).
% 7.99/1.64 thf(func_def_163, type, sK99: !>[X0: $tType, X1: $tType]:((product_prod @ X1 @ X0 > X1))).
% 7.99/1.64 thf(func_def_164, type, sK100: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > (X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_165, type, sK101: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > (X0 > $o) > X1))).
% 7.99/1.64 thf(func_def_166, type, sK102: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X1))).
% 7.99/1.64 thf(func_def_167, type, sK103: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X0))).
% 7.99/1.64 thf(func_def_168, type, sK104: !>[X0: $tType, X1: $tType]:((X1 > set @ product_prod @ X1 @ X0 > X0))).
% 7.99/1.64 thf(func_def_169, type, sK105: !>[X0: $tType, X1: $tType]:((X1 > set @ product_prod @ X1 @ X0 > X1))).
% 7.99/1.64 thf(func_def_170, type, sK106: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X3))).
% 7.99/1.64 thf(func_def_171, type, sK107: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X1))).
% 7.99/1.64 thf(func_def_172, type, sK108: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X4))).
% 7.99/1.64 thf(func_def_173, type, sK109: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X2))).
% 7.99/1.64 thf(func_def_174, type, sK110: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X0 @ product_prod @ X4 @ product_prod @ X2 @ product_prod @ X3 @ X1 > $o) > X0))).
% 7.99/1.64 thf(func_def_175, type, sK111: !>[X0: $tType, X1: $tType]:((set @ product_prod @ X0 @ X1 > X1 > set @ X0 > X0))).
% 7.99/1.64 thf(func_def_176, type, vNOT: ($o > $o)).
% 7.99/1.64 thf(f1,axiom,(
% 7.99/1.64 (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g)))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_g)).
% 7.99/1.64 thf(f3,axiom,(
% 7.99/1.64 ! [X0 : $tType] : (zero @ X0 => (edge_preserving @ X0 @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ X0 @ sum_sum @ a @ b @ (product_Pair @ X0 @ sum_sum @ a @ b @ zero_zero @ X0 @ v) @ bot_bot @ set @ product_prod @ X0 @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0 @ (product_Pair @ standard_Constant @ a @ product_prod @ X0 @ X0 @ standard_S_Idt @ a @ (product_Pair @ X0 @ X0 @ zero_zero @ X0 @ zero_zero @ X0)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g)))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__092_060open_062edge__preserving_A_123_I0_058_058_063_Hc1_M_Av_J_125_A_123_IS__Idt_M_A0_058_058_063_Hc1_M_A0_058_058_063_Hc1_J_125_A_Iedges_AG_J_092_060close_062)).
% 7.99/1.64 thf(f4,axiom,(
% 7.99/1.64 (ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_r)).
% 7.99/1.64 thf(f5,axiom,(
% 7.99/1.64 (f = ((insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_f)).
% 7.99/1.64 thf(f6,axiom,(
% 7.99/1.64 (((domain @ nat @ sum_sum @ a @ b @ f)) = ((insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_d)).
% 7.99/1.64 thf(f7,axiom,(
% 7.99/1.64 ! [X1 : $tType,X0 : $tType,X4 : X1,X3 : X1,X2 : X0] : (((labeled_LG @ X0 @ X1 @ (insert @ product_prod @ X0 @ product_prod @ X1 @ X1 @ (product_Pair @ X0 @ product_prod @ X1 @ X1 @ X2 @ (product_Pair @ X1 @ X1 @ X3 @ X4)) @ bot_bot @ set @ product_prod @ X0 @ product_prod @ X1 @ X1) @ (insert @ X1 @ X3 @ (insert @ X1 @ X4 @ bot_bot @ set @ X1)))) = ((restrict @ X0 @ X1 @ (labeled_LG @ X0 @ X1 @ (insert @ product_prod @ X0 @ product_prod @ X1 @ X1 @ (product_Pair @ X0 @ product_prod @ X1 @ X1 @ X2 @ (product_Pair @ X1 @ X1 @ X3 @ X4)) @ bot_bot @ set @ product_prod @ X0 @ product_prod @ X1 @ X1) @ (insert @ X1 @ X3 @ (insert @ X1 @ X4 @ bot_bot @ set @ X1))))))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_graph__single)).
% 7.99/1.64 thf(f9,axiom,(
% 7.99/1.64 (univalent @ nat @ sum_sum @ a @ b @ f)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_u)).
% 7.99/1.64 thf(f10,axiom,(
% 7.99/1.64 ! [X1 : $tType,X0 : $tType,X4 : set @ product_prod @ X1 @ X0,X2 : X1,X3 : X0] : (((domain @ X1 @ X0 @ (insert @ product_prod @ X1 @ X0 @ (product_Pair @ X1 @ X0 @ X2 @ X3) @ X4))) = ((insert @ X1 @ X2 @ (domain @ X1 @ X0 @ X4))))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_Domain__insert)).
% 7.99/1.64 thf(f14,axiom,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType] : (((domain @ X1 @ X0 @ bot_bot @ set @ product_prod @ X1 @ X0)) = bot_bot @ set @ X1)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_Domain__empty)).
% 7.99/1.64 thf(f38,axiom,(
% 7.99/1.64 ! [X1 : $tType,X0 : $tType,X3 : set @ X1,X2 : set @ product_prod @ X0 @ product_prod @ X1 @ X1] : (((labeled_vertices @ X0 @ X1 @ (labeled_LG @ X0 @ X1 @ X2 @ X3))) = X3)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_labeled__graph_Osel_I2_J)).
% 7.99/1.64 thf(f39,axiom,(
% 7.99/1.64 ! [X1 : $tType,X0 : $tType,X3 : set @ X0,X2 : set @ product_prod @ X1 @ product_prod @ X0 @ X0] : (((labeled_edges @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X2 @ X3))) = X2)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_labeled__graph_Osel_I1_J)).
% 7.99/1.64 thf(f43,axiom,(
% 7.99/1.64 ! [X0 : $tType,X1 : X0,X2 : set @ X0,X3 : X0] : ((X1 = X3) & (ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0)) = (((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_singleton__insert__inj__eq_H)).
% 7.99/1.64 thf(f82,axiom,(
% 7.99/1.64 ! [X0 : $tType,X1 : set @ X0] : (ord_less_eq @ set @ X0 @ X1 @ X1)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_subset__refl)).
% 7.99/1.64 thf(f130,axiom,(
% 7.99/1.64 (bot_bot @ nat = zero_zero @ nat)),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_bot__nat__def)).
% 7.99/1.64 thf(f268,axiom,(
% 7.99/1.64 zero @ nat),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero)).
% 7.99/1.64 thf(f281,conjecture,(
% 7.99/1.64 (edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) & (ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)) & (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) = ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) & (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))))),
% 7.99/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 7.99/1.64 thf(f282,negated_conjecture,(
% 7.99/1.64 ~((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) & (ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)) & (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) = ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) & (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))))),
% 7.99/1.64 inference(negated_conjecture,[status(cth)],[f281])).
% 7.99/1.64 thf(f289,plain,(
% 7.99/1.64 ! [X0 : $tType] : (zero @ X0 => (edge_preserving @ X0 @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ X0 @ sum_sum @ a @ b @ (product_Pair @ X0 @ sum_sum @ a @ b @ zero_zero @ X0 @ v) @ bot_bot @ set @ product_prod @ X0 @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0 @ (product_Pair @ standard_Constant @ a @ product_prod @ X0 @ X0 @ standard_S_Idt @ a @ (product_Pair @ X0 @ X0 @ zero_zero @ X0 @ zero_zero @ X0)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g)))),
% 7.99/1.64 inference(rectify,[],[f3])).
% 7.99/1.64 thf(f290,plain,(
% 7.99/1.64 ! [X0 : $tType] : ((zero @ X0 = $true) => (((edge_preserving @ X0 @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ X0 @ sum_sum @ a @ b @ (product_Pair @ X0 @ sum_sum @ a @ b @ zero_zero @ X0 @ v) @ bot_bot @ set @ product_prod @ X0 @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0 @ (product_Pair @ standard_Constant @ a @ product_prod @ X0 @ X0 @ standard_S_Idt @ a @ (product_Pair @ X0 @ X0 @ zero_zero @ X0 @ zero_zero @ X0)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true))),
% 7.99/1.64 inference(fool_elimination,[],[f289])).
% 7.99/1.64 thf(f370,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : set @ X0] : (ord_less_eq @ set @ X0 @ X1 @ X1)),
% 7.99/1.64 inference(rectify,[],[f82])).
% 7.99/1.64 thf(f371,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : set @ X0] : (((ord_less_eq @ set @ X0 @ X1 @ X1)) = $true)),
% 7.99/1.64 inference(fool_elimination,[],[f370])).
% 7.99/1.64 thf(f402,plain,(
% 7.99/1.64 zero @ nat),
% 7.99/1.64 inference(rectify,[],[f268])).
% 7.99/1.64 thf(f403,plain,(
% 7.99/1.64 (zero @ nat = $true)),
% 7.99/1.64 inference(fool_elimination,[],[f402])).
% 7.99/1.64 thf(f495,plain,(
% 7.99/1.64 (univalent @ nat @ sum_sum @ a @ b @ f)),
% 7.99/1.64 inference(rectify,[],[f9])).
% 7.99/1.64 thf(f496,plain,(
% 7.99/1.64 (((univalent @ nat @ sum_sum @ a @ b @ f)) = $true)),
% 7.99/1.64 inference(fool_elimination,[],[f495])).
% 7.99/1.64 thf(f503,plain,(
% 7.99/1.64 (ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))),
% 7.99/1.64 inference(rectify,[],[f4])).
% 7.99/1.64 thf(f504,plain,(
% 7.99/1.64 (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 inference(fool_elimination,[],[f503])).
% 7.99/1.64 thf(f566,plain,(
% 7.99/1.64 ~((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) & (ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g)) & (univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)) & (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) = ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) & (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))))),
% 7.99/1.64 inference(rectify,[],[f282])).
% 7.99/1.64 thf(f567,plain,(
% 7.99/1.64 ~((((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true) & (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))) & (((univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) = $true) & (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) = ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) & (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) & (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true))),
% 7.99/1.64 inference(fool_elimination,[],[f566])).
% 7.99/1.64 thf(f725,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : X0,X2 : set @ X0,X3 : X0] : ((X1 = X3) & (ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0)) = (((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))))),
% 7.99/1.64 inference(rectify,[],[f43])).
% 7.99/1.64 thf(f726,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : X0,X2 : set @ X0,X3 : X0] : (((((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) = $true) & (X1 = X3)) <=> (((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))))),
% 7.99/1.64 inference(fool_elimination,[],[f725])).
% 7.99/1.64 thf(f743,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X4 : X1,X2 : set @ product_prod @ X0 @ X1,X3 : X0] : (((domain @ X0 @ X1 @ (insert @ product_prod @ X0 @ X1 @ (product_Pair @ X0 @ X1 @ X3 @ X4) @ X2))) = ((insert @ X0 @ X3 @ (domain @ X0 @ X1 @ X2))))),
% 7.99/1.64 inference(rectify,[],[f10])).
% 7.99/1.64 thf(f758,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : X0,X4 : X1] : (((restrict @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ (insert @ product_prod @ X1 @ product_prod @ X0 @ X0 @ (product_Pair @ X1 @ product_prod @ X0 @ X0 @ X4 @ (product_Pair @ X0 @ X0 @ X3 @ X2)) @ bot_bot @ set @ product_prod @ X1 @ product_prod @ X0 @ X0) @ (insert @ X0 @ X3 @ (insert @ X0 @ X2 @ bot_bot @ set @ X0))))) = ((labeled_LG @ X1 @ X0 @ (insert @ product_prod @ X1 @ product_prod @ X0 @ X0 @ (product_Pair @ X1 @ product_prod @ X0 @ X0 @ X4 @ (product_Pair @ X0 @ X0 @ X3 @ X2)) @ bot_bot @ set @ product_prod @ X1 @ product_prod @ X0 @ X0) @ (insert @ X0 @ X3 @ (insert @ X0 @ X2 @ bot_bot @ set @ X0)))))),
% 7.99/1.64 inference(rectify,[],[f7])).
% 7.99/1.64 thf(f763,plain,(
% 7.99/1.64 ! [X1 : $tType,X0 : $tType,X2 : set @ X1,X3 : set @ product_prod @ X0 @ product_prod @ X1 @ X1] : (((labeled_edges @ X0 @ X1 @ (labeled_LG @ X0 @ X1 @ X3 @ X2))) = X3)),
% 7.99/1.64 inference(rectify,[],[f39])).
% 7.99/1.64 thf(f766,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X3 : set @ product_prod @ X1 @ product_prod @ X0 @ X0,X2 : set @ X0] : (((labeled_vertices @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X3 @ X2))) = X2)),
% 7.99/1.64 inference(rectify,[],[f38])).
% 7.99/1.64 thf(f917,plain,(
% 7.99/1.64 (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) != ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))) | (((univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) != $true) | (g != ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) | (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) != ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true)),
% 7.99/1.64 inference(ennf_transformation,[],[f567])).
% 7.99/1.64 thf(f942,plain,(
% 7.99/1.64 ! [X0 : $tType] : ((((edge_preserving @ X0 @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ X0 @ sum_sum @ a @ b @ (product_Pair @ X0 @ sum_sum @ a @ b @ zero_zero @ X0 @ v) @ bot_bot @ set @ product_prod @ X0 @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0 @ (product_Pair @ standard_Constant @ a @ product_prod @ X0 @ X0 @ standard_S_Idt @ a @ (product_Pair @ X0 @ X0 @ zero_zero @ X0 @ zero_zero @ X0)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true) | (zero @ X0 != $true))),
% 7.99/1.64 inference(ennf_transformation,[],[f290])).
% 7.99/1.64 thf(f1019,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X2 : set @ product_prod @ X1 @ product_prod @ X0 @ X0,X3 : set @ X0] : (((labeled_vertices @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X2 @ X3))) = X3)),
% 7.99/1.64 inference(rectify,[],[f766])).
% 7.99/1.64 thf(f1169,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : X0,X2 : set @ X0,X3 : X0] : ((((((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) = $true) & (X1 = X3)) | (((insert @ X0 @ X1 @ X2)) != ((insert @ X0 @ X3 @ bot_bot @ set @ X0)))) & ((((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))) | ((((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) != $true) | (X1 != X3))))),
% 7.99/1.64 inference(nnf_transformation,[],[f726])).
% 7.99/1.64 thf(f1170,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : X0,X2 : set @ X0,X3 : X0] : ((((((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) = $true) & (X1 = X3)) | (((insert @ X0 @ X1 @ X2)) != ((insert @ X0 @ X3 @ bot_bot @ set @ X0)))) & ((((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))) | (((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) != $true) | (X1 != X3)))),
% 7.99/1.64 inference(flattening,[],[f1169])).
% 7.99/1.64 thf(f1189,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X2 : set @ X0,X3 : set @ product_prod @ X1 @ product_prod @ X0 @ X0] : (((labeled_edges @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X3 @ X2))) = X3)),
% 7.99/1.64 inference(rectify,[],[f763])).
% 7.99/1.64 thf(f1215,plain,(
% 7.99/1.64 ! [X0 : $tType,X1 : $tType,X2 : X1,X3 : set @ product_prod @ X0 @ X1,X4 : X0] : (((domain @ X0 @ X1 @ (insert @ product_prod @ X0 @ X1 @ (product_Pair @ X0 @ X1 @ X4 @ X2) @ X3))) = ((insert @ X0 @ X4 @ (domain @ X0 @ X1 @ X3))))),
% 7.99/1.64 inference(rectify,[],[f743])).
% 7.99/1.64 thf(f1289,plain,(
% 7.99/1.64 (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g)))),
% 7.99/1.64 inference(cnf_transformation,[],[f1])).
% 7.99/1.64 thf(f1291,plain,(
% 7.99/1.64 ( ! [X1 : $tType,X0 : $tType,X2 : set @ product_prod @ X1 @ product_prod @ X0 @ X0,X3 : set @ X0] : ((((labeled_vertices @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X2 @ X3))) = X3)) )),
% 7.99/1.64 inference(cnf_transformation,[],[f1019])).
% 7.99/1.64 thf(f1323,plain,(
% 7.99/1.64 (zero @ nat = $true)),
% 7.99/1.64 inference(cnf_transformation,[],[f403])).
% 7.99/1.64 thf(f1341,plain,(
% 7.99/1.64 (((insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) = ((domain @ nat @ sum_sum @ a @ b @ f)))),
% 7.99/1.64 inference(cnf_transformation,[],[f6])).
% 7.99/1.64 thf(f1357,plain,(
% 7.99/1.64 (g != ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g))) | (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) != ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) != ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))) | (((univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) != $true) | (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true)),
% 7.99/1.64 inference(cnf_transformation,[],[f917])).
% 7.99/1.64 thf(f1371,plain,(
% 7.99/1.64 (zero_zero @ nat = bot_bot @ nat)),
% 7.99/1.64 inference(cnf_transformation,[],[f130])).
% 7.99/1.64 thf(f1424,plain,(
% 7.99/1.64 (((univalent @ nat @ sum_sum @ a @ b @ f)) = $true)),
% 7.99/1.64 inference(cnf_transformation,[],[f496])).
% 7.99/1.64 thf(f1428,plain,(
% 7.99/1.64 ( ! [X1 : $tType,X0 : $tType,X2 : X0,X3 : X0,X4 : X1] : ((((restrict @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ (insert @ product_prod @ X1 @ product_prod @ X0 @ X0 @ (product_Pair @ X1 @ product_prod @ X0 @ X0 @ X4 @ (product_Pair @ X0 @ X0 @ X3 @ X2)) @ bot_bot @ set @ product_prod @ X1 @ product_prod @ X0 @ X0) @ (insert @ X0 @ X3 @ (insert @ X0 @ X2 @ bot_bot @ set @ X0))))) = ((labeled_LG @ X1 @ X0 @ (insert @ product_prod @ X1 @ product_prod @ X0 @ X0 @ (product_Pair @ X1 @ product_prod @ X0 @ X0 @ X4 @ (product_Pair @ X0 @ X0 @ X3 @ X2)) @ bot_bot @ set @ product_prod @ X1 @ product_prod @ X0 @ X0) @ (insert @ X0 @ X3 @ (insert @ X0 @ X2 @ bot_bot @ set @ X0)))))) )),
% 7.99/1.64 inference(cnf_transformation,[],[f758])).
% 7.99/1.64 thf(f1442,plain,(
% 7.99/1.64 (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 inference(cnf_transformation,[],[f504])).
% 7.99/1.64 thf(f1485,plain,(
% 7.99/1.64 ( ! [X0 : $tType] : ((((edge_preserving @ X0 @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ X0 @ sum_sum @ a @ b @ (product_Pair @ X0 @ sum_sum @ a @ b @ zero_zero @ X0 @ v) @ bot_bot @ set @ product_prod @ X0 @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0 @ (product_Pair @ standard_Constant @ a @ product_prod @ X0 @ X0 @ standard_S_Idt @ a @ (product_Pair @ X0 @ X0 @ zero_zero @ X0 @ zero_zero @ X0)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ X0 @ X0) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true) | (zero @ X0 != $true)) )),
% 7.99/1.64 inference(cnf_transformation,[],[f942])).
% 7.99/1.64 thf(f1537,plain,(
% 7.99/1.64 ( ! [X0 : $tType,X2 : set @ X0,X3 : X0,X1 : X0] : ((((insert @ X0 @ X1 @ X2)) = ((insert @ X0 @ X3 @ bot_bot @ set @ X0))) | (((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) != $true) | (X1 != X3)) )),
% 7.99/1.64 inference(cnf_transformation,[],[f1170])).
% 7.99/1.64 thf(f1552,plain,(
% 7.99/1.64 ( ! [X1 : $tType,X0 : $tType] : ((bot_bot @ set @ X1 = ((domain @ X1 @ X0 @ bot_bot @ set @ product_prod @ X1 @ X0)))) )),
% 7.99/1.64 inference(cnf_transformation,[],[f14])).
% 7.99/1.64 thf(f1569,plain,(
% 7.99/1.64 (f = ((insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))),
% 7.99/1.64 inference(cnf_transformation,[],[f5])).
% 7.99/1.64 thf(f1573,plain,(
% 7.99/1.64 ( ! [X1 : $tType,X0 : $tType,X2 : set @ X0,X3 : set @ product_prod @ X1 @ product_prod @ X0 @ X0] : ((((labeled_edges @ X1 @ X0 @ (labeled_LG @ X1 @ X0 @ X3 @ X2))) = X3)) )),
% 7.99/1.64 inference(cnf_transformation,[],[f1189])).
% 7.99/1.64 thf(f1614,plain,(
% 7.99/1.64 ( ! [X1 : $tType,X0 : $tType,X2 : X1,X3 : set @ product_prod @ X0 @ X1,X4 : X0] : ((((domain @ X0 @ X1 @ (insert @ product_prod @ X0 @ X1 @ (product_Pair @ X0 @ X1 @ X4 @ X2) @ X3))) = ((insert @ X0 @ X4 @ (domain @ X0 @ X1 @ X3))))) )),
% 7.99/1.64 inference(cnf_transformation,[],[f1215])).
% 7.99/1.64 thf(f1631,plain,(
% 7.99/1.64 ( ! [X0 : $tType,X1 : set @ X0] : ((((ord_less_eq @ set @ X0 @ X1 @ X1)) = $true)) )),
% 7.99/1.64 inference(cnf_transformation,[],[f371])).
% 7.99/1.64 thf(f1686,plain,(
% 7.99/1.64 ( ! [X0 : $tType,X2 : set @ X0,X3 : X0] : ((((insert @ X0 @ X3 @ bot_bot @ set @ X0)) = ((insert @ X0 @ X3 @ X2))) | (((ord_less_eq @ set @ X0 @ X2 @ (insert @ X0 @ X3 @ bot_bot @ set @ X0))) != $true)) )),
% 7.99/1.64 inference(equality_resolution,[],[f1537])).
% 7.99/1.64 thf(f1722,definition,(
% 7.99/1.64 spl112_1 <=> (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_1])],[avatar_definition])).
% 7.99/1.64 thf(f1724,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | spl112_1),
% 7.99/1.64 inference(avatar_component_clause,[],[f1722])).
% 7.99/1.64 thf(f1726,definition,(
% 7.99/1.64 spl112_2 <=> (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) = ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_2])],[avatar_definition])).
% 7.99/1.64 thf(f1728,plain,(
% 7.99/1.64 (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) != ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | spl112_2),
% 7.99/1.64 inference(avatar_component_clause,[],[f1726])).
% 7.99/1.64 thf(f1730,definition,(
% 7.99/1.64 spl112_3 <=> (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_3])],[avatar_definition])).
% 7.99/1.64 thf(f1732,plain,(
% 7.99/1.64 (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))) != ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat))))) | spl112_3),
% 7.99/1.64 inference(avatar_component_clause,[],[f1730])).
% 7.99/1.64 thf(f1734,definition,(
% 7.99/1.64 spl112_4 <=> (((univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_4])],[avatar_definition])).
% 7.99/1.64 thf(f1738,definition,(
% 7.99/1.64 spl112_5 <=> (g = ((restrict @ standard_Constant @ a @ sum_sum @ a @ b @ g)))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_5])],[avatar_definition])).
% 7.99/1.64 thf(f1742,definition,(
% 7.99/1.64 spl112_6 <=> (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_6])],[avatar_definition])).
% 7.99/1.64 thf(f1745,plain,(
% 7.99/1.64 ~spl112_1 | ~spl112_2 | ~spl112_3 | ~spl112_4 | ~spl112_5 | ~spl112_6),
% 7.99/1.64 inference(avatar_split_clause,[],[f1357,f1742,f1738,f1734,f1730,f1726,f1722])).
% 7.99/1.64 thf(f1757,definition,(
% 7.99/1.64 spl112_9 <=> (zero @ nat = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_9])],[avatar_definition])).
% 7.99/1.64 thf(f1759,plain,(
% 7.99/1.64 (zero @ nat = $true) | ~spl112_9),
% 7.99/1.64 inference(avatar_component_clause,[],[f1757])).
% 7.99/1.64 thf(f1760,plain,(
% 7.99/1.64 spl112_9),
% 7.99/1.64 inference(avatar_split_clause,[],[f1323,f1757])).
% 7.99/1.64 thf(f1777,definition,(
% 7.99/1.64 spl112_13 <=> (zero_zero @ nat = bot_bot @ nat)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_13])],[avatar_definition])).
% 7.99/1.64 thf(f1779,plain,(
% 7.99/1.64 (zero_zero @ nat = bot_bot @ nat) | ~spl112_13),
% 7.99/1.64 inference(avatar_component_clause,[],[f1777])).
% 7.99/1.64 thf(f1780,plain,(
% 7.99/1.64 spl112_13),
% 7.99/1.64 inference(avatar_split_clause,[],[f1371,f1777])).
% 7.99/1.64 thf(f1802,definition,(
% 7.99/1.64 spl112_18 <=> (((univalent @ nat @ sum_sum @ a @ b @ f)) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_18])],[avatar_definition])).
% 7.99/1.64 thf(f1805,plain,(
% 7.99/1.64 spl112_18),
% 7.99/1.64 inference(avatar_split_clause,[],[f1424,f1802])).
% 7.99/1.64 thf(f1807,definition,(
% 7.99/1.64 spl112_19 <=> (((insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) = ((domain @ nat @ sum_sum @ a @ b @ f)))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_19])],[avatar_definition])).
% 7.99/1.64 thf(f1810,plain,(
% 7.99/1.64 spl112_19),
% 7.99/1.64 inference(avatar_split_clause,[],[f1341,f1807])).
% 7.99/1.64 thf(f1877,definition,(
% 7.99/1.64 spl112_33 <=> (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_33])],[avatar_definition])).
% 7.99/1.64 thf(f1880,plain,(
% 7.99/1.64 spl112_33),
% 7.99/1.64 inference(avatar_split_clause,[],[f1442,f1877])).
% 7.99/1.64 thf(f1896,plain,(
% 7.99/1.64 spl112_5),
% 7.99/1.64 inference(avatar_split_clause,[],[f1289,f1738])).
% 7.99/1.64 thf(f1903,definition,(
% 7.99/1.64 spl112_38 <=> (f = ((insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_38])],[avatar_definition])).
% 7.99/1.64 thf(f1906,plain,(
% 7.99/1.64 spl112_38),
% 7.99/1.64 inference(avatar_split_clause,[],[f1569,f1903])).
% 7.99/1.64 thf(f1911,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | (spl112_1 | ~spl112_13)),
% 7.99/1.64 inference(forward_demodulation,[],[f1724,f1779])).
% 7.99/1.64 thf(f1913,definition,(
% 7.99/1.64 spl112_39 <=> (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_39])],[avatar_definition])).
% 7.99/1.64 thf(f1915,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_edges @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | spl112_39),
% 7.99/1.64 inference(avatar_component_clause,[],[f1913])).
% 7.99/1.64 thf(f1916,plain,(
% 7.99/1.64 ~spl112_39 | spl112_1 | ~spl112_13),
% 7.99/1.64 inference(avatar_split_clause,[],[f1911,f1777,f1722,f1913])).
% 7.99/1.64 thf(f2072,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | spl112_39),
% 7.99/1.64 inference(superposition,[],[f1915,f1573])).
% 7.99/1.64 thf(f2074,definition,(
% 7.99/1.64 spl112_43 <=> (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_43])],[avatar_definition])).
% 7.99/1.64 thf(f2077,plain,(
% 7.99/1.64 ~spl112_43 | spl112_39),
% 7.99/1.64 inference(avatar_split_clause,[],[f2072,f1913,f2074])).
% 7.99/1.64 thf(f4019,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true) | (zero @ nat != $true) | ~spl112_13),
% 7.99/1.64 inference(superposition,[],[f1485,f1779])).
% 7.99/1.64 thf(f4028,plain,(
% 7.99/1.64 (((edge_preserving @ nat @ sum_sum @ a @ b @ standard_Constant @ a @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ bot_bot @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (labeled_edges @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true) | (~spl112_9 | ~spl112_13)),
% 7.99/1.64 inference(forward_subsumption_resolution,[],[f4019,f1759])).
% 7.99/1.64 thf(f4029,plain,(
% 7.99/1.64 (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) != ((insert @ nat @ zero_zero @ nat @ (domain @ nat @ sum_sum @ a @ b @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | spl112_2),
% 7.99/1.64 inference(forward_demodulation,[],[f1728,f1614])).
% 7.99/1.64 thf(f4032,plain,(
% 7.99/1.64 spl112_43 | ~spl112_9 | ~spl112_13),
% 7.99/1.64 inference(avatar_split_clause,[],[f4028,f1777,f1757,f2074])).
% 7.99/1.64 thf(f4033,plain,(
% 7.99/1.64 (((insert @ nat @ bot_bot @ nat @ (domain @ nat @ sum_sum @ a @ b @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) != ((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))))) | (spl112_2 | ~spl112_13)),
% 7.99/1.64 inference(forward_demodulation,[],[f4029,f1779])).
% 7.99/1.64 thf(f4035,plain,(
% 7.99/1.64 (((insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat)) != ((insert @ nat @ bot_bot @ nat @ (domain @ nat @ sum_sum @ a @ b @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | (spl112_2 | ~spl112_13)),
% 7.99/1.64 inference(forward_demodulation,[],[f4033,f1291])).
% 7.99/1.64 thf(f4036,plain,(
% 7.99/1.64 (((insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat)) != ((insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) | (spl112_2 | ~spl112_13)),
% 7.99/1.64 inference(forward_demodulation,[],[f4035,f1552])).
% 7.99/1.64 thf(f4037,plain,(
% 7.99/1.64 $false | (spl112_2 | ~spl112_13)),
% 7.99/1.64 inference(trivial_inequality_removal,[],[f4036])).
% 7.99/1.64 thf(f4038,plain,(
% 7.99/1.64 spl112_2 | ~spl112_13),
% 7.99/1.64 inference(avatar_contradiction_clause,[],[f4037])).
% 7.99/1.64 thf(f4040,plain,(
% 7.99/1.64 (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) != ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))))) | (spl112_3 | ~spl112_13)),
% 7.99/1.64 inference(forward_demodulation,[],[f1732,f1779])).
% 7.99/1.64 thf(f4043,definition,(
% 7.99/1.64 spl112_82 <=> (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) = ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat)))))),
% 7.99/1.64 introduced(definition,[new_symbols(definition,[spl112_82])],[avatar_definition])).
% 7.99/1.64 thf(f4045,plain,(
% 7.99/1.64 (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) != ((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))))) | spl112_82),
% 7.99/1.64 inference(avatar_component_clause,[],[f4043])).
% 7.99/1.64 thf(f4046,plain,(
% 7.99/1.64 ~spl112_82 | spl112_3 | ~spl112_13),
% 7.99/1.64 inference(avatar_split_clause,[],[f4040,f1777,f1730,f4043])).
% 7.99/1.64 thf(f4101,plain,(
% 7.99/1.64 ( ! [X0 : set @ nat] : ((((restrict @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ X0)))) != ((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ X0)))) | (((ord_less_eq @ set @ nat @ X0 @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) != $true)) ) | spl112_82),
% 7.99/1.64 inference(superposition,[],[f4045,f1686])).
% 7.99/1.64 thf(f4199,plain,(
% 7.99/1.64 (((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat)))) != ((labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ bot_bot @ nat @ bot_bot @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ bot_bot @ nat @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))))) | (((ord_less_eq @ set @ nat @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) != $true) | spl112_82),
% 7.99/1.64 inference(superposition,[],[f4101,f1428])).
% 7.99/1.64 thf(f4200,plain,(
% 7.99/1.64 (((ord_less_eq @ set @ nat @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat) @ (insert @ nat @ bot_bot @ nat @ bot_bot @ set @ nat))) != $true) | spl112_82),
% 7.99/1.64 inference(trivial_inequality_removal,[],[f4199])).
% 7.99/1.64 thf(f4202,plain,(
% 7.99/1.64 $false | spl112_82),
% 7.99/1.64 inference(forward_subsumption_resolution,[],[f4200,f1631])).
% 7.99/1.64 thf(f4203,plain,(
% 7.99/1.64 spl112_82),
% 7.99/1.64 inference(avatar_contradiction_clause,[],[f4202])).
% 7.99/1.64 thf(f4204,definition,(
% 7.99/1.64 (f != ((insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) | (zero_zero @ nat != bot_bot @ nat) | (((univalent @ nat @ sum_sum @ a @ b @ f)) != $true) | (((univalent @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) = $true)),
% 7.99/1.64 introduced(theory,[theory_tautology_sat_conflict])).
% 7.99/1.64 thf(f4205,definition,(
% 7.99/1.64 (f != ((insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b))) | (zero_zero @ nat != bot_bot @ nat) | (((labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) != ((domain @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b)))) | (((insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) != ((domain @ nat @ sum_sum @ a @ b @ f))) | (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ f @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) != $true) | (((ord_less_eq @ set @ sum_sum @ a @ b @ (image @ nat @ sum_sum @ a @ b @ (insert @ product_prod @ nat @ sum_sum @ a @ b @ (product_Pair @ nat @ sum_sum @ a @ b @ zero_zero @ nat @ v) @ bot_bot @ set @ product_prod @ nat @ sum_sum @ a @ b) @ (labeled_vertices @ standard_Constant @ a @ nat @ (labeled_LG @ standard_Constant @ a @ nat @ (insert @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat @ (product_Pair @ standard_Constant @ a @ product_prod @ nat @ nat @ standard_S_Idt @ a @ (product_Pair @ nat @ nat @ zero_zero @ nat @ zero_zero @ nat)) @ bot_bot @ set @ product_prod @ standard_Constant @ a @ product_prod @ nat @ nat) @ (insert @ nat @ zero_zero @ nat @ bot_bot @ set @ nat)))) @ (labeled_vertices @ standard_Constant @ a @ sum_sum @ a @ b @ g))) = $true)),
% 7.99/1.64 introduced(theory,[theory_tautology_sat_conflict])).
% 7.99/1.64 cnf(s1, plain, ~spl112_1 | ~spl112_2 | ~spl112_3 | ~spl112_4 | ~spl112_5 | ~spl112_6, inference(sat_conversion,[],[f1745])).
% 7.99/1.64 cnf(s4, plain, spl112_9, inference(sat_conversion,[],[f1760])).
% 7.99/1.64 cnf(s8, plain, spl112_13, inference(sat_conversion,[],[f1780])).
% 7.99/1.64 cnf(s13, plain, spl112_18, inference(sat_conversion,[],[f1805])).
% 7.99/1.64 cnf(s14, plain, spl112_19, inference(sat_conversion,[],[f1810])).
% 7.99/1.64 cnf(s28, plain, spl112_33, inference(sat_conversion,[],[f1880])).
% 7.99/1.64 cnf(s33, plain, spl112_5, inference(sat_conversion,[],[f1896])).
% 7.99/1.64 cnf(s35, plain, spl112_38, inference(sat_conversion,[],[f1906])).
% 7.99/1.64 cnf(s36, plain, spl112_1 | ~spl112_13 | ~spl112_39, inference(sat_conversion,[],[f1916])).
% 7.99/1.64 cnf(s40, plain, spl112_39 | ~spl112_43, inference(sat_conversion,[],[f2077])).
% 7.99/1.64 cnf(s86, plain, ~spl112_9 | ~spl112_13 | spl112_43, inference(sat_conversion,[],[f4032])).
% 7.99/1.64 cnf(s88, plain, spl112_2 | ~spl112_13, inference(sat_conversion,[],[f4038])).
% 7.99/1.64 cnf(s89, plain, spl112_3 | ~spl112_13 | ~spl112_82, inference(sat_conversion,[],[f4046])).
% 7.99/1.64 cnf(s90, plain, spl112_82, inference(sat_conversion,[],[f4203])).
% 7.99/1.64 cnf(s91, plain, spl112_4 | ~spl112_13 | ~spl112_18 | ~spl112_38, inference(sat_conversion,[],[f4204])).
% 7.99/1.64 cnf(s92, plain, ~spl112_2 | spl112_6 | ~spl112_13 | ~spl112_19 | ~spl112_33 | ~spl112_38, inference(sat_conversion,[],[f4205])).
% 7.99/1.64 cnf(s93, plain, spl112_3 | ~spl112_13, inference(rat,[],[s89,s90])).
% 7.99/1.64 cnf(s108, plain, spl112_4, inference(rat,[],[s91,s35,s13,s8])).
% 7.99/1.64 cnf(s109, plain, spl112_3, inference(rat,[],[s93,s8])).
% 7.99/1.64 cnf(s110, plain, spl112_2, inference(rat,[],[s88,s8])).
% 7.99/1.64 cnf(s114, plain, spl112_6, inference(rat,[],[s92,s35,s28,s14,s8,s110])).
% 7.99/1.64 cnf(s119, plain, spl112_43, inference(rat,[],[s86,s8,s4])).
% 7.99/1.64 cnf(s120, plain, spl112_39, inference(rat,[],[s40,s119])).
% 7.99/1.64 cnf(s121, plain, spl112_1, inference(rat,[],[s36,s8,s120])).
% 7.99/1.64 cnf(s127, plain, $false, inference(rat,[],[s1,s114,s33,s108,s109,s110,s121])).
% 7.99/1.64 thf(f4206,plain,(
% 7.99/1.64 $false),
% 7.99/1.64 inference(avatar_sat_refutation,[],[s127])).
% 7.99/1.64 % SZS output end Proof for theBenchmark
% 7.99/1.64 % (577207)------------------------------
% 7.99/1.64 % (577207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.99/1.64 % (577207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.99/1.64 % (577207)CaDiCaL version: 2.1.3
% 7.99/1.64 % (577207)Termination reason: Refutation
% 7.99/1.64 % (577207)Time elapsed: 0.195 s
% 7.99/1.64 % (577207)Peak memory usage: 17 MB
% 7.99/1.64 % (577207)Instructions burned: 648 (million)
% 7.99/1.64 % (577036)Success in time 1.335 s
% 7.99/1.64 % Vampire exiting
%------------------------------------------------------------------------------