%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP039^1 : 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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:08:04 AM UTC 2026
% Result : Theorem 0.49s 0.45s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP039^1 : 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 : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 19:39:55 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.22/0.30 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.49/0.42 % (1212933)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.49/0.42 % (1212939)lrs+10_16_si=on:nwc=1.5:random_seed=909108031:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.49/0.42 % (1212944)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.49/0.42 % (1212944)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.49/0.42 % (1212938)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1409093085:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.49/0.42 % (1212940)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2989018198:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.49/0.42 % (1212944)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=3074943449:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.49/0.42 % (1212941)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=899226556: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.49/0.42 % (1212942)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=1907482871:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.49/0.42 % (1212943)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1142803516:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.49/0.42 % (1212939)Instruction limit reached!
% 0.49/0.42 % (1212939)------------------------------
% 0.49/0.42 % (1212939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.42 % (1212939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.42 % (1212939)CaDiCaL version: 2.1.3
% 0.49/0.42 % (1212939)Termination reason: Instruction limit
% 0.49/0.42 % (1212939)Termination phase: shuffling
% 0.49/0.42 % (1212939)Time elapsed: 0.005 s
% 0.49/0.42 % (1212939)Peak memory usage: 10 MB
% 0.49/0.42 % (1212939)Instructions burned: 20 (million)
% 0.49/0.42 % (1212940)Instruction limit reached!
% 0.49/0.42 % (1212940)------------------------------
% 0.49/0.42 % (1212940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.42 % (1212940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.42 % (1212940)CaDiCaL version: 2.1.3
% 0.49/0.42 % (1212940)Termination reason: Instruction limit
% 0.49/0.42 % (1212940)Termination phase: shuffling
% 0.49/0.42 % (1212940)Time elapsed: 0.003 s
% 0.49/0.42 % (1212940)Peak memory usage: 10 MB
% 0.49/0.42 % (1212940)Instructions burned: 5 (million)
% 0.49/0.42 % (1212942)Instruction limit reached!
% 0.49/0.42 % (1212942)------------------------------
% 0.49/0.42 % (1212942)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.42 % (1212942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.42 % (1212942)CaDiCaL version: 2.1.3
% 0.49/0.42 % (1212942)Termination reason: Instruction limit
% 0.49/0.42 % (1212942)Termination phase: shuffling
% 0.49/0.42 % (1212942)Time elapsed: 0.011 s
% 0.49/0.42 % (1212942)Peak memory usage: 10 MB
% 0.49/0.42 % (1212942)Instructions burned: 25 (million)
% 0.49/0.42 % (1212952)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1771339326:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.49/0.42 % (1212952)Instruction limit reached!
% 0.49/0.42 % (1212952)------------------------------
% 0.49/0.42 % (1212952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.42 % (1212952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.42 % (1212952)CaDiCaL version: 2.1.3
% 0.49/0.42 % (1212952)Termination reason: Instruction limit
% 0.49/0.42 % (1212952)Termination phase: shuffling
% 0.49/0.42 % (1212952)Time elapsed: 0.001 s
% 0.49/0.42 % (1212952)Peak memory usage: 10 MB
% 0.49/0.42 % (1212952)Instructions burned: 2 (million)
% 0.49/0.42 % (1212953)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=165594355:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.49/0.45 % (1212956)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=733358357:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.49/0.45 % (1212953)Instruction limit reached!
% 0.49/0.45 % (1212953)------------------------------
% 0.49/0.45 % (1212953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212953)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212953)Termination reason: Instruction limit
% 0.49/0.45 % (1212953)Termination phase: shuffling
% 0.49/0.45 % (1212953)Time elapsed: 0.003 s
% 0.49/0.45 % (1212953)Peak memory usage: 10 MB
% 0.49/0.45 % (1212953)Instructions burned: 6 (million)
% 0.49/0.45 % (1212956)Instruction limit reached!
% 0.49/0.45 % (1212956)------------------------------
% 0.49/0.45 % (1212956)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212956)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212956)Termination reason: Instruction limit
% 0.49/0.45 % (1212956)Termination phase: shuffling
% 0.49/0.45 % (1212956)Time elapsed: 0.003 s
% 0.49/0.45 % (1212956)Peak memory usage: 10 MB
% 0.49/0.45 % (1212956)Instructions burned: 12 (million)
% 0.49/0.45 % (1212955)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.49/0.45 % (1212955)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4279292271:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.49/0.45 % (1212943)Instruction limit reached!
% 0.49/0.45 % (1212943)------------------------------
% 0.49/0.45 % (1212943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212943)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212943)Termination reason: Instruction limit
% 0.49/0.45 % (1212943)Termination phase: Preprocessing 3
% 0.49/0.45 % (1212943)Time elapsed: 0.035 s
% 0.49/0.45 % (1212943)Peak memory usage: 12 MB
% 0.49/0.45 % (1212943)Instructions burned: 75 (million)
% 0.49/0.45 % (1212955)Instruction limit reached!
% 0.49/0.45 % (1212955)------------------------------
% 0.49/0.45 % (1212955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212955)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212955)Termination reason: Instruction limit
% 0.49/0.45 % (1212955)Termination phase: shuffling
% 0.49/0.45 % (1212955)Time elapsed: 0.004 s
% 0.49/0.45 % (1212955)Peak memory usage: 10 MB
% 0.49/0.45 % (1212955)Instructions burned: 8 (million)
% 0.49/0.45 % (1212960)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=3864564527:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.49/0.45 % (1212938)Instruction limit reached!
% 0.49/0.45 % (1212938)------------------------------
% 0.49/0.45 % (1212938)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212938)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212938)Termination reason: Instruction limit
% 0.49/0.45 % (1212938)Termination phase: Property scanning
% 0.49/0.45 % (1212938)Time elapsed: 0.041 s
% 0.49/0.45 % (1212938)Peak memory usage: 12 MB
% 0.49/0.45 % (1212938)Instructions burned: 89 (million)
% 0.49/0.45 % (1212959)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.49/0.45 % (1212959)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.49/0.45 % (1212959)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=590324065:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.49/0.45 % (1212963)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.49/0.45 % (1212962)lrs+10_1_si=on:cs=on:random_seed=2666525205:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.49/0.45 % (1212963)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=2402537510:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.49/0.45 % (1212963)Instruction limit reached!
% 0.49/0.45 % (1212963)------------------------------
% 0.49/0.45 % (1212963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212963)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212963)Termination reason: Instruction limit
% 0.49/0.45 % (1212963)Termination phase: shuffling
% 0.49/0.45 % (1212963)Time elapsed: 0.002 s
% 0.49/0.45 % (1212963)Peak memory usage: 10 MB
% 0.49/0.45 % (1212963)Instructions burned: 3 (million)
% 0.49/0.45 % (1212960)Instruction limit reached!
% 0.49/0.45 % (1212960)------------------------------
% 0.49/0.45 % (1212960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212960)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212960)Termination reason: Instruction limit
% 0.49/0.45 % (1212960)Termination phase: Property scanning
% 0.49/0.45 % (1212960)Time elapsed: 0.021 s
% 0.49/0.45 % (1212960)Peak memory usage: 11 MB
% 0.49/0.45 % (1212960)Instructions burned: 88 (million)
% 0.49/0.45 % (1212959)Instruction limit reached!
% 0.49/0.45 % (1212959)------------------------------
% 0.49/0.45 % (1212959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212959)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212959)Termination reason: Instruction limit
% 0.49/0.45 % (1212959)Termination phase: shuffling
% 0.49/0.45 % (1212959)Time elapsed: 0.013 s
% 0.49/0.45 % (1212959)Peak memory usage: 11 MB
% 0.49/0.45 % (1212959)Instructions burned: 28 (million)
% 0.49/0.45 % (1212962)Instruction limit reached!
% 0.49/0.45 % (1212962)------------------------------
% 0.49/0.45 % (1212962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212962)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212962)Termination reason: Instruction limit
% 0.49/0.45 % (1212962)Termination phase: shuffling
% 0.49/0.45 % (1212962)Time elapsed: 0.004 s
% 0.49/0.45 % (1212962)Peak memory usage: 10 MB
% 0.49/0.45 % (1212962)Instructions burned: 8 (million)
% 0.49/0.45 % (1212965)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=944263528:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.49/0.45 % (1212970)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=3955269834:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 0.49/0.45 % (1212944)Instruction limit reached!
% 0.49/0.45 % (1212944)------------------------------
% 0.49/0.45 % (1212944)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212944)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212944)Termination reason: Instruction limit
% 0.49/0.45 % (1212944)Termination phase: Saturation
% 0.49/0.45 % (1212944)Time elapsed: 0.069 s
% 0.49/0.45 % (1212944)Peak memory usage: 14 MB
% 0.49/0.45 % (1212944)Instructions burned: 159 (million)
% 0.49/0.45 % (1212970)Instruction limit reached!
% 0.49/0.45 % (1212970)------------------------------
% 0.49/0.45 % (1212970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212970)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212970)Termination reason: Instruction limit
% 0.49/0.45 % (1212970)Termination phase: shuffling
% 0.49/0.45 % (1212970)Time elapsed: 0.006 s
% 0.49/0.45 % (1212970)Peak memory usage: 10 MB
% 0.49/0.45 % (1212970)Instructions burned: 29 (million)
% 0.49/0.45 % (1212969)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=1589141278:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 0.49/0.45 % (1212965)Instruction limit reached!
% 0.49/0.45 % (1212965)------------------------------
% 0.49/0.45 % (1212965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212965)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212965)Termination reason: Instruction limit
% 0.49/0.45 % (1212965)Termination phase: Property scanning
% 0.49/0.45 % (1212965)Time elapsed: 0.016 s
% 0.49/0.45 % (1212965)Peak memory usage: 11 MB
% 0.49/0.45 % (1212965)Instructions burned: 38 (million)
% 0.49/0.45 % (1212971)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=680348630:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.49/0.45 % (1212972)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1277662462:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 0.49/0.45 % (1212971)Instruction limit reached!
% 0.49/0.45 % (1212971)------------------------------
% 0.49/0.45 % (1212971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212971)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212971)Termination reason: Instruction limit
% 0.49/0.45 % (1212971)Termination phase: shuffling
% 0.49/0.45 % (1212971)Time elapsed: 0.007 s
% 0.49/0.45 % (1212971)Peak memory usage: 10 MB
% 0.49/0.45 % (1212971)Instructions burned: 16 (million)
% 0.49/0.45 % (1212976)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=1808998054: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)
% 0.49/0.45 % (1212976)Instruction limit reached!
% 0.49/0.45 % (1212976)------------------------------
% 0.49/0.45 % (1212976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212976)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212976)Termination reason: Instruction limit
% 0.49/0.45 % (1212976)Termination phase: shuffling
% 0.49/0.45 % (1212976)Time elapsed: 0.001 s
% 0.49/0.45 % (1212976)Peak memory usage: 10 MB
% 0.49/0.45 % (1212976)Instructions burned: 4 (million)
% 0.49/0.45 % (1212975)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=2593040318:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 0.49/0.45 % (1212978)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=3185626803:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 0.49/0.45 % (1212975)Instruction limit reached!
% 0.49/0.45 % (1212975)------------------------------
% 0.49/0.45 % (1212975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212975)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212975)Termination reason: Instruction limit
% 0.49/0.45 % (1212975)Termination phase: shuffling
% 0.49/0.45 % (1212975)Time elapsed: 0.007 s
% 0.49/0.45 % (1212975)Peak memory usage: 10 MB
% 0.49/0.45 % (1212975)Instructions burned: 15 (million)
% 0.49/0.45 % (1212941) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1212933-1212941"...
% 0.49/0.45 % (1212983)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=1304880910:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 0.49/0.45 % (1212982)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=3657523296:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 0.49/0.45 % (1212941)...printing done.
% 0.49/0.45 % (1212941)Refutation found. Thanks to Tanya!
% 0.49/0.45 % SZS status Theorem for theBenchmark
% 0.49/0.45 % SZS output start Proof for theBenchmark
% 0.49/0.45 thf(type_def_5, type, set_Pr754230471real_c: $tType).
% 0.49/0.45 thf(type_def_6, type, produc640052711real_c: $tType).
% 0.49/0.45 thf(type_def_7, type, set_Pr2041213564t_unit: $tType).
% 0.49/0.45 thf(type_def_8, type, set_Pr1169339874_sc_sz: $tType).
% 0.49/0.45 thf(type_def_9, type, produc999471430t_unit: $tType).
% 0.49/0.45 thf(type_def_10, type, produc1821101996_sc_sz: $tType).
% 0.49/0.45 thf(type_def_11, type, set_Pr60491591eal_sz: $tType).
% 0.49/0.45 thf(type_def_12, type, set_Pr1389752855real_c: $tType).
% 0.49/0.45 thf(type_def_13, type, set_Pr1774599175_sc_sz: $tType).
% 0.49/0.45 thf(type_def_14, type, produc1149990247eal_sz: $tType).
% 0.49/0.45 thf(type_def_15, type, produc190496183real_c: $tType).
% 0.49/0.45 thf(type_def_16, type, produc866628903_sc_sz: $tType).
% 0.49/0.45 thf(type_def_17, type, set_De208295462t_unit: $tType).
% 0.49/0.45 thf(type_def_18, type, denota610675952t_unit: $tType).
% 0.49/0.45 thf(type_def_19, type, denota231621370t_unit: $tType).
% 0.49/0.45 thf(type_def_20, type, set_Su1783761653um_b_c: $tType).
% 0.49/0.45 thf(type_def_21, type, set_Fi1407883041real_c: $tType).
% 0.49/0.45 thf(type_def_22, type, finite1398487019real_c: $tType).
% 0.49/0.45 thf(type_def_23, type, list_f1238882004_sc_sz: $tType).
% 0.49/0.45 thf(type_def_24, type, set_Sum_sum_c_c: $tType).
% 0.49/0.45 thf(type_def_25, type, formula_sf_sc_sz: $tType).
% 0.49/0.45 thf(type_def_26, type, formula_a_b_c: $tType).
% 0.49/0.45 thf(type_def_27, type, set_o: $tType).
% 0.49/0.45 thf(type_def_28, type, sz: $tType).
% 0.49/0.45 thf(type_def_29, type, sf: $tType).
% 0.49/0.45 thf(type_def_30, type, sc: $tType).
% 0.49/0.45 thf(type_def_31, type, sTfun: ($tType * $tType) > $tType).
% 0.49/0.45 thf(func_def_0, type, coinci501627771_a_b_c: (formula_a_b_c > $o)).
% 0.49/0.45 thf(func_def_1, type, denota69106024_a_b_c: (denota231621370t_unit > denota231621370t_unit > set_Su1783761653um_b_c > $o)).
% 0.49/0.45 thf(func_def_2, type, denota1997846518gree_c: (produc190496183real_c > produc190496183real_c > set_Sum_sum_c_c > $o)).
% 0.49/0.45 thf(func_def_3, type, denota968303861_a_b_c: (denota231621370t_unit > formula_a_b_c > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_4, type, denota1711272799_sc_sz: (denota610675952t_unit > formula_sf_sc_sz > set_Pr60491591eal_sz)).
% 0.49/0.45 thf(func_def_5, type, denota1946510237_sc_sz: (formula_sf_sc_sz > $o)).
% 0.49/0.45 thf(func_def_6, type, denota1579475975_sc_sz: (denota610675952t_unit > $o)).
% 0.49/0.45 thf(func_def_7, type, ids_sz_sf_sc: (sz > sz > sz > sf > sf > sf > sc > sc > sc > sc > $o)).
% 0.49/0.45 thf(func_def_8, type, top_to1399053141c_sz_o: (denota610675952t_unit > produc866628903_sc_sz > $o)).
% 0.49/0.45 thf(func_def_9, type, top_to964419200al_c_o: (finite1398487019real_c > finite1398487019real_c > $o)).
% 0.49/0.45 thf(func_def_10, type, top_to1499569298_sc_sz: set_Pr1169339874_sc_sz).
% 0.49/0.45 thf(func_def_11, type, top_to226056039real_c: set_Pr1389752855real_c).
% 0.49/0.45 thf(func_def_12, type, top_to1660572043um_c_c: set_Sum_sum_c_c).
% 0.49/0.45 thf(func_def_13, type, produc789536734_sc_sz: (denota610675952t_unit > produc866628903_sc_sz > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_14, type, produc394644079real_c: (finite1398487019real_c > finite1398487019real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_15, type, produc1822718231_sc_sz: (list_f1238882004_sc_sz > list_f1238882004_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_16, type, produc1687028567real_c: (produc190496183real_c > produc190496183real_c > produc640052711real_c)).
% 0.49/0.45 thf(func_def_17, type, produc502616768t_unit: (produc866628903_sc_sz > denota610675952t_unit > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_18, type, produc159603053_sc_sz: (set_De208295462t_unit > (denota610675952t_unit > set_Pr1774599175_sc_sz) > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_19, type, produc563345056real_c: (set_Fi1407883041real_c > (finite1398487019real_c > set_Fi1407883041real_c) > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_20, type, produc1017530376real_c: (set_Pr1389752855real_c > (produc190496183real_c > set_Pr1389752855real_c) > set_Pr754230471real_c)).
% 0.49/0.45 thf(func_def_21, type, produc2020166735t_unit: (set_Pr1774599175_sc_sz > (produc866628903_sc_sz > set_De208295462t_unit) > set_Pr2041213564t_unit)).
% 0.49/0.45 thf(func_def_22, type, produc793407943_sc_sz: ((denota610675952t_unit > denota610675952t_unit) > produc999471430t_unit > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_23, type, produc981295297real_c: ((finite1398487019real_c > finite1398487019real_c) > produc190496183real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_24, type, produc233219286_sc_sz: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz) > produc866628903_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_25, type, produc2089853305real_c: ((produc190496183real_c > produc190496183real_c) > produc640052711real_c > produc640052711real_c)).
% 0.49/0.45 thf(func_def_26, type, produc1959054510t_unit: ((produc866628903_sc_sz > produc866628903_sc_sz) > produc1821101996_sc_sz > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_27, type, produc1086673900c_sz_o: ((produc1821101996_sc_sz > $o) > denota610675952t_unit > produc866628903_sc_sz > $o)).
% 0.49/0.45 thf(func_def_28, type, produc753314315real_c: ((produc1821101996_sc_sz > produc190496183real_c) > denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c)).
% 0.49/0.45 thf(func_def_29, type, produc1827049067real_c: ((produc1821101996_sc_sz > set_Pr1389752855real_c) > denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_30, type, produc1716060341al_c_o: ((produc190496183real_c > $o) > finite1398487019real_c > finite1398487019real_c > $o)).
% 0.49/0.45 thf(func_def_31, type, produc1119115220real_c: ((produc190496183real_c > produc190496183real_c) > finite1398487019real_c > finite1398487019real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_32, type, produc880541325c_sz_o: ((produc866628903_sc_sz > $o) > list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o)).
% 0.49/0.45 thf(func_def_33, type, produc440529997al_c_o: ((produc640052711real_c > $o) > produc190496183real_c > produc190496183real_c > $o)).
% 0.49/0.45 thf(func_def_34, type, produc38128778unit_o: ((produc999471430t_unit > $o) > produc866628903_sc_sz > denota610675952t_unit > $o)).
% 0.49/0.45 thf(func_def_35, type, produc295339066_sc_sz: ((produc999471430t_unit > produc1821101996_sc_sz) > produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_36, type, produc198687651c_sz_o: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > $o)).
% 0.49/0.45 thf(func_def_37, type, produc383750338real_c: ((denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > produc1821101996_sc_sz > produc190496183real_c)).
% 0.49/0.45 thf(func_def_38, type, produc1894848802real_c: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc1821101996_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_39, type, produc1442549981real_c: ((finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > produc190496183real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_40, type, produc2099580355_sc_sz: ((produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > produc999471430t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_41, type, produc403791768_sc_sz: ((denota610675952t_unit > denota610675952t_unit) > (produc866628903_sc_sz > produc866628903_sc_sz) > produc1821101996_sc_sz > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_42, type, produc1612557567real_c: ((denota610675952t_unit > finite1398487019real_c) > (produc866628903_sc_sz > finite1398487019real_c) > produc1821101996_sc_sz > produc190496183real_c)).
% 0.49/0.45 thf(func_def_43, type, produc1784590311_sc_sz: ((finite1398487019real_c > denota610675952t_unit) > (finite1398487019real_c > produc866628903_sc_sz) > produc190496183real_c > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_44, type, produc368345510real_c: ((finite1398487019real_c > finite1398487019real_c) > (finite1398487019real_c > finite1398487019real_c) > produc190496183real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_45, type, produc619560141c_sz_o: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > $o)).
% 0.49/0.45 thf(func_def_46, type, produc1920474870real_c: ((denota610675952t_unit > produc866628903_sc_sz > finite1398487019real_c) > produc1821101996_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_47, type, produc448466487_sc_sz: ((denota610675952t_unit > produc866628903_sc_sz > produc1821101996_sc_sz) > produc1821101996_sc_sz > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_48, type, produc1575513068real_c: ((denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > produc1821101996_sc_sz > produc190496183real_c)).
% 0.49/0.45 thf(func_def_49, type, produc2068697644real_c: ((denota610675952t_unit > produc866628903_sc_sz > set_Fi1407883041real_c) > produc1821101996_sc_sz > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_50, type, produc237521996real_c: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc1821101996_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_51, type, produc353381908al_c_o: ((finite1398487019real_c > finite1398487019real_c > $o) > produc190496183real_c > $o)).
% 0.49/0.45 thf(func_def_52, type, produc567249007real_c: ((finite1398487019real_c > finite1398487019real_c > finite1398487019real_c) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_53, type, produc107375667real_c: ((finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > produc190496183real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_54, type, produc1341776291_sc_sz: ((finite1398487019real_c > finite1398487019real_c > produc866628903_sc_sz) > produc190496183real_c > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_55, type, produc29022117real_c: ((finite1398487019real_c > finite1398487019real_c > set_Fi1407883041real_c) > produc190496183real_c > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_56, type, produc923381907real_c: ((finite1398487019real_c > finite1398487019real_c > set_Pr1389752855real_c) > produc190496183real_c > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_57, type, produc642283651_sc_sz: ((finite1398487019real_c > finite1398487019real_c > set_Pr1774599175_sc_sz) > produc190496183real_c > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_58, type, produc2039065452c_sz_o: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o) > produc866628903_sc_sz > $o)).
% 0.49/0.45 thf(func_def_59, type, produc236226839real_c: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > finite1398487019real_c) > produc866628903_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_60, type, produc126255499real_c: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > produc190496183real_c) > produc866628903_sc_sz > produc190496183real_c)).
% 0.49/0.45 thf(func_def_61, type, produc1449736269real_c: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_62, type, produc6841835real_c: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1389752855real_c) > produc866628903_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_63, type, produc1563580891_sc_sz: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1774599175_sc_sz) > produc866628903_sc_sz > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_64, type, produc1726730540al_c_o: ((produc190496183real_c > produc190496183real_c > $o) > produc640052711real_c > $o)).
% 0.49/0.45 thf(func_def_65, type, produc344593239real_c: ((produc190496183real_c > produc190496183real_c > finite1398487019real_c) > produc640052711real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_66, type, produc1066779277real_c: ((produc190496183real_c > produc190496183real_c > set_Fi1407883041real_c) > produc640052711real_c > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_67, type, produc1718498667unit_o: ((produc866628903_sc_sz > denota610675952t_unit > $o) > produc999471430t_unit > $o)).
% 0.49/0.45 thf(func_def_68, type, produc1753599960real_c: ((produc866628903_sc_sz > denota610675952t_unit > finite1398487019real_c) > produc999471430t_unit > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_69, type, produc435149849_sc_sz: ((produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > produc999471430t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_70, type, produc645763722real_c: ((produc866628903_sc_sz > denota610675952t_unit > produc190496183real_c) > produc999471430t_unit > produc190496183real_c)).
% 0.49/0.45 thf(func_def_71, type, produc1368849166real_c: ((produc866628903_sc_sz > denota610675952t_unit > set_Fi1407883041real_c) > produc999471430t_unit > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_72, type, produc593754858real_c: ((produc866628903_sc_sz > denota610675952t_unit > set_Pr1389752855real_c) > produc999471430t_unit > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_73, type, produc1503602930_sc_sz: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_74, type, produc532048446_sc_sz: (produc1821101996_sc_sz > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_75, type, produc704157711real_c: (produc190496183real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_76, type, produc1145837239_sc_sz: (produc866628903_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_77, type, produc350724343real_c: (produc640052711real_c > produc640052711real_c)).
% 0.49/0.45 thf(func_def_78, type, produc245128480t_unit: (produc999471430t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_79, type, produc3751594real_c: (set_Fi1407883041real_c > set_Fi1407883041real_c > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_80, type, inv_im1827249322real_c: (set_Pr1389752855real_c > (finite1398487019real_c > finite1398487019real_c) > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_81, type, collec230941376real_c: ((finite1398487019real_c > $o) > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_82, type, collec1199592193_sc_sz: ((produc1821101996_sc_sz > $o) > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_83, type, collec1643251106real_c: ((produc190496183real_c > $o) > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_84, type, collec2036662930_sc_sz: ((produc866628903_sc_sz > $o) > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_85, type, collec1126017874real_c: ((produc640052711real_c > $o) > set_Pr754230471real_c)).
% 0.49/0.45 thf(func_def_86, type, collec377961627t_unit: ((produc999471430t_unit > $o) > set_Pr2041213564t_unit)).
% 0.49/0.45 thf(func_def_87, type, image_1514048989real_c: ((finite1398487019real_c > finite1398487019real_c) > set_Fi1407883041real_c > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_88, type, image_1461287749real_c: ((finite1398487019real_c > produc190496183real_c) > set_Fi1407883041real_c > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_89, type, image_290183605_sc_sz: ((finite1398487019real_c > produc866628903_sc_sz) > set_Fi1407883041real_c > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_90, type, image_1746662005real_c: ((finite1398487019real_c > produc640052711real_c) > set_Fi1407883041real_c > set_Pr754230471real_c)).
% 0.49/0.45 thf(func_def_91, type, image_1641704997c_sz_o: ((produc1821101996_sc_sz > $o) > set_Pr1169339874_sc_sz > set_o)).
% 0.49/0.45 thf(func_def_92, type, image_1268968350real_c: ((produc1821101996_sc_sz > finite1398487019real_c) > set_Pr1169339874_sc_sz > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_93, type, image_1726193375_sc_sz: ((produc1821101996_sc_sz > produc1821101996_sc_sz) > set_Pr1169339874_sc_sz > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_94, type, image_386905412real_c: ((produc1821101996_sc_sz > produc190496183real_c) > set_Pr1169339874_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_95, type, image_904562809t_unit: ((produc1821101996_sc_sz > produc999471430t_unit) > set_Pr1169339874_sc_sz > set_Pr2041213564t_unit)).
% 0.49/0.45 thf(func_def_96, type, image_14429021real_c: ((produc190496183real_c > finite1398487019real_c) > set_Pr1389752855real_c > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_97, type, image_1259833374_sc_sz: ((produc190496183real_c > produc1821101996_sc_sz) > set_Pr1389752855real_c > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_98, type, image_738229701real_c: ((produc190496183real_c > produc190496183real_c) > set_Pr1389752855real_c > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_99, type, image_388766773_sc_sz: ((produc190496183real_c > produc866628903_sc_sz) > set_Pr1389752855real_c > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_100, type, image_1332486093real_c: ((produc866628903_sc_sz > finite1398487019real_c) > set_Pr1774599175_sc_sz > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_101, type, image_226055310_sc_sz: ((produc866628903_sc_sz > produc1821101996_sc_sz) > set_Pr1774599175_sc_sz > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_102, type, image_1121381717real_c: ((produc866628903_sc_sz > produc190496183real_c) > set_Pr1774599175_sc_sz > set_Pr1389752855real_c)).
% 0.49/0.45 thf(func_def_103, type, image_1313166277_sc_sz: ((produc866628903_sc_sz > produc866628903_sc_sz) > set_Pr1774599175_sc_sz > set_Pr1774599175_sc_sz)).
% 0.49/0.45 thf(func_def_104, type, image_768765061real_c: ((produc866628903_sc_sz > produc640052711real_c) > set_Pr1774599175_sc_sz > set_Pr754230471real_c)).
% 0.49/0.45 thf(func_def_105, type, image_1551908392t_unit: ((produc866628903_sc_sz > produc999471430t_unit) > set_Pr1774599175_sc_sz > set_Pr2041213564t_unit)).
% 0.49/0.45 thf(func_def_106, type, image_124598413real_c: ((produc640052711real_c > finite1398487019real_c) > set_Pr754230471real_c > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_107, type, image_2041365445real_c: ((produc640052711real_c > produc640052711real_c) > set_Pr754230471real_c > set_Pr754230471real_c)).
% 0.49/0.45 thf(func_def_108, type, image_1269062456real_c: ((produc999471430t_unit > finite1398487019real_c) > set_Pr2041213564t_unit > set_Fi1407883041real_c)).
% 0.49/0.45 thf(func_def_109, type, image_1426741113_sc_sz: ((produc999471430t_unit > produc1821101996_sc_sz) > set_Pr2041213564t_unit > set_Pr1169339874_sc_sz)).
% 0.49/0.45 thf(func_def_110, type, static_FVF_a_b_c: (formula_a_b_c > set_Sum_sum_c_c)).
% 0.49/0.45 thf(func_def_111, type, static_SIGF_a_b_c: (formula_a_b_c > set_Su1783761653um_b_c)).
% 0.49/0.45 thf(func_def_112, type, equiv_a_b_c: (formula_a_b_c > formula_a_b_c > formula_a_b_c)).
% 0.49/0.45 thf(func_def_113, type, implies_a_b_c: (formula_a_b_c > formula_a_b_c > formula_a_b_c)).
% 0.49/0.45 thf(func_def_114, type, predic913887884_sf_sz: (sc > formula_sf_sc_sz)).
% 0.49/0.45 thf(func_def_115, type, p_sc_sf_sz: (sc > formula_sf_sc_sz)).
% 0.49/0.45 thf(func_def_116, type, member_o: ($o > set_o > $o)).
% 0.49/0.45 thf(func_def_117, type, member754147591t_unit: (denota610675952t_unit > set_De208295462t_unit > $o)).
% 0.49/0.45 thf(func_def_118, type, member1261661570real_c: (finite1398487019real_c > set_Fi1407883041real_c > $o)).
% 0.49/0.45 thf(func_def_119, type, member1057565379_sc_sz: (produc1821101996_sc_sz > set_Pr1169339874_sc_sz > $o)).
% 0.49/0.45 thf(func_def_120, type, member1895684704real_c: (produc190496183real_c > set_Pr1389752855real_c > $o)).
% 0.49/0.45 thf(func_def_121, type, member630771088eal_sz: (produc1149990247eal_sz > set_Pr60491591eal_sz > $o)).
% 0.49/0.45 thf(func_def_122, type, member245028432_sc_sz: (produc866628903_sc_sz > set_Pr1774599175_sc_sz > $o)).
% 0.49/0.45 thf(func_def_123, type, member346808080real_c: (produc640052711real_c > set_Pr754230471real_c > $o)).
% 0.49/0.45 thf(func_def_124, type, member235934813t_unit: (produc999471430t_unit > set_Pr2041213564t_unit > $o)).
% 0.49/0.45 thf(func_def_125, type, phi: formula_a_b_c).
% 0.49/0.45 thf(func_def_129, type, vAND: ($o > $o > $o)).
% 0.49/0.45 thf(func_def_130, type, db0: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_131, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.49/0.45 thf(func_def_132, type, db1: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_133, type, db6: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_134, type, db5: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_135, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.49/0.45 thf(func_def_136, type, vNOT: ($o > $o)).
% 0.49/0.45 thf(func_def_137, type, db8: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_138, type, db7: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_139, type, db3: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_140, type, db2: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_141, type, db9: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_142, type, db4: !>[X0: $tType]:(X0)).
% 0.49/0.45 thf(func_def_143, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.49/0.45 thf(func_def_144, type, vIMP: ($o > $o > $o)).
% 0.49/0.45 thf(func_def_145, type, sK0: (produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_146, type, sK1: (produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_147, type, sK2: (produc1821101996_sc_sz > (produc999471430t_unit > produc1821101996_sc_sz) > set_Pr2041213564t_unit > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_148, type, sK3: (set_Pr1389752855real_c > (produc190496183real_c > produc190496183real_c) > (produc190496183real_c > produc190496183real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_149, type, sK4: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > ($o > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_150, type, sK5: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > ($o > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_151, type, sK6: (produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_152, type, sK7: (produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_153, type, sK8: ((produc640052711real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_154, type, sK9: ((produc640052711real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_155, type, sK10: ((produc640052711real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_156, type, sK11: ((produc190496183real_c > produc190496183real_c > set_Fi1407883041real_c) > produc640052711real_c > finite1398487019real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_157, type, sK12: ((produc190496183real_c > produc190496183real_c > set_Fi1407883041real_c) > produc640052711real_c > finite1398487019real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_158, type, sK13: (produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_159, type, sK14: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_160, type, sK15: ((produc640052711real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_161, type, sK16: ((produc640052711real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_162, type, sK17: ((produc1821101996_sc_sz > produc999471430t_unit) > (produc999471430t_unit > $o) > set_Pr1169339874_sc_sz > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_163, type, sK18: (set_Pr1389752855real_c > (finite1398487019real_c > finite1398487019real_c) > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_164, type, sK19: (set_Pr1389752855real_c > (finite1398487019real_c > finite1398487019real_c) > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_165, type, sK20: ((produc1821101996_sc_sz > set_Pr1389752855real_c) > (denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_166, type, sK21: ((produc1821101996_sc_sz > set_Pr1389752855real_c) > (denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_167, type, sK22: (finite1398487019real_c > produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_168, type, sK23: (finite1398487019real_c > produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > set_Fi1407883041real_c) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_169, type, sK24: ((produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > (produc1821101996_sc_sz > $o) > produc999471430t_unit > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_170, type, sK25: ((produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > (produc1821101996_sc_sz > $o) > produc999471430t_unit > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_171, type, sK26: (produc190496183real_c > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1389752855real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_172, type, sK27: (produc190496183real_c > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1389752855real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_173, type, sK28: (produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_174, type, sK29: (produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_175, type, sK30: (set_Pr1389752855real_c > produc190496183real_c > (produc190496183real_c > produc190496183real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_176, type, sK31: (produc640052711real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_177, type, sK32: (produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_178, type, sK33: (produc640052711real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_179, type, sK34: ((produc1821101996_sc_sz > produc999471430t_unit) > set_Pr1169339874_sc_sz > (produc999471430t_unit > $o) > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_180, type, sK35: (produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_181, type, sK36: (produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_182, type, sK37: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_183, type, sK38: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_184, type, sK39: ((produc866628903_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_185, type, sK40: ((produc866628903_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_186, type, sK41: ((finite1398487019real_c > finite1398487019real_c > $o) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_187, type, sK42: ((finite1398487019real_c > finite1398487019real_c > $o) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_188, type, sK43: (produc866628903_sc_sz > (finite1398487019real_c > finite1398487019real_c > set_Pr1774599175_sc_sz) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_189, type, sK44: (produc866628903_sc_sz > (finite1398487019real_c > finite1398487019real_c > set_Pr1774599175_sc_sz) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_190, type, sK45: ((produc1821101996_sc_sz > produc999471430t_unit) > set_Pr1169339874_sc_sz > (produc1821101996_sc_sz > produc999471430t_unit) > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_191, type, sK46: (produc190496183real_c > (finite1398487019real_c > set_Fi1407883041real_c) > set_Fi1407883041real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_192, type, sK47: (produc190496183real_c > (finite1398487019real_c > set_Fi1407883041real_c) > set_Fi1407883041real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_193, type, sK48: ((produc999471430t_unit > produc1821101996_sc_sz) > (produc999471430t_unit > produc1821101996_sc_sz) > set_Pr2041213564t_unit > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_194, type, sK49: (produc999471430t_unit > (produc866628903_sc_sz > denota610675952t_unit > set_Fi1407883041real_c) > finite1398487019real_c > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_195, type, sK50: (produc999471430t_unit > (produc866628903_sc_sz > denota610675952t_unit > set_Fi1407883041real_c) > finite1398487019real_c > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_196, type, sK51: ((produc999471430t_unit > produc1821101996_sc_sz) > (produc1821101996_sc_sz > $o) > set_Pr2041213564t_unit > produc999471430t_unit)).
% 0.49/0.45 thf(func_def_197, type, sK52: (produc999471430t_unit > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_198, type, sK53: (produc999471430t_unit > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_199, type, sK54: ((produc1821101996_sc_sz > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_200, type, sK55: ((produc1821101996_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_201, type, sK56: (produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_202, type, sK57: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_203, type, sK58: ((produc190496183real_c > produc1821101996_sc_sz) > (produc190496183real_c > produc1821101996_sc_sz) > set_Pr1389752855real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_204, type, sK59: (produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_205, type, sK60: (produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_206, type, sK61: ((finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > (produc190496183real_c > produc190496183real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_207, type, sK62: ((finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > (produc190496183real_c > produc190496183real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_208, type, sK63: ((produc866628903_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_209, type, sK64: ((produc866628903_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_210, type, sK65: (produc1821101996_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_211, type, sK66: (produc1821101996_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_212, type, sK67: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_213, type, sK68: (produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_214, type, sK69: (produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_215, type, sK70: ((produc999471430t_unit > produc1821101996_sc_sz) > (produc1821101996_sc_sz > $o) > set_Pr2041213564t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_216, type, sK71: produc190496183real_c).
% 0.49/0.45 thf(func_def_217, type, sK72: denota231621370t_unit).
% 0.49/0.45 thf(func_def_218, type, sK73: denota231621370t_unit).
% 0.49/0.45 thf(func_def_219, type, sK74: produc190496183real_c).
% 0.49/0.45 thf(func_def_220, type, sK75: denota231621370t_unit).
% 0.49/0.45 thf(func_def_221, type, sK76: produc190496183real_c).
% 0.49/0.45 thf(func_def_222, type, sK77: denota231621370t_unit).
% 0.49/0.45 thf(func_def_223, type, sK78: produc190496183real_c).
% 0.49/0.45 thf(func_def_224, type, sK79: ((denota610675952t_unit > produc866628903_sc_sz > $o) > (produc1821101996_sc_sz > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_225, type, sK80: ((denota610675952t_unit > produc866628903_sc_sz > $o) > (produc1821101996_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_226, type, sK81: ((produc190496183real_c > produc190496183real_c) > set_Pr1389752855real_c > (produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_227, type, sK82: (produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_228, type, sK83: (produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_229, type, sK84: (produc190496183real_c > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1389752855real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_230, type, sK85: (produc190496183real_c > produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1389752855real_c) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_231, type, sK86: ((denota610675952t_unit > finite1398487019real_c) > set_Pr1169339874_sc_sz > produc190496183real_c > (produc866628903_sc_sz > finite1398487019real_c) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_232, type, sK87: ((denota610675952t_unit > finite1398487019real_c) > set_Pr1169339874_sc_sz > produc190496183real_c > (produc866628903_sc_sz > finite1398487019real_c) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_233, type, sK88: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_234, type, sK89: (produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_235, type, sK90: (set_Pr1169339874_sc_sz > produc190496183real_c > (produc1821101996_sc_sz > produc190496183real_c) > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_236, type, sK91: (set_Pr1389752855real_c > (produc1821101996_sc_sz > $o) > (produc190496183real_c > produc1821101996_sc_sz) > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_237, type, sK92: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_238, type, sK93: ((denota610675952t_unit > produc866628903_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_239, type, sK94: (set_Pr1169339874_sc_sz > (produc866628903_sc_sz > produc866628903_sc_sz) > produc1821101996_sc_sz > (denota610675952t_unit > denota610675952t_unit) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_240, type, sK95: (set_Pr1169339874_sc_sz > (produc866628903_sc_sz > produc866628903_sc_sz) > produc1821101996_sc_sz > (denota610675952t_unit > denota610675952t_unit) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_241, type, sK96: ((produc999471430t_unit > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_242, type, sK97: ((produc999471430t_unit > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_243, type, sK98: ((produc866628903_sc_sz > denota610675952t_unit > $o) > produc999471430t_unit > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_244, type, sK99: ((produc866628903_sc_sz > denota610675952t_unit > $o) > produc999471430t_unit > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_245, type, sK100: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_246, type, sK101: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_247, type, sK102: (finite1398487019real_c > (denota610675952t_unit > produc866628903_sc_sz > set_Fi1407883041real_c) > produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_248, type, sK103: (finite1398487019real_c > (denota610675952t_unit > produc866628903_sc_sz > set_Fi1407883041real_c) > produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_249, type, sK104: ((produc190496183real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_250, type, sK105: ((produc190496183real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_251, type, sK106: ((produc640052711real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_252, type, sK107: ((produc640052711real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_253, type, sK108: (produc999471430t_unit > (produc866628903_sc_sz > denota610675952t_unit > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_254, type, sK109: (produc999471430t_unit > (produc866628903_sc_sz > denota610675952t_unit > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_255, type, sK110: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1774599175_sc_sz) > produc866628903_sc_sz > produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_256, type, sK111: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1774599175_sc_sz) > produc866628903_sc_sz > produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_257, type, sK112: ((produc1821101996_sc_sz > produc190496183real_c) > set_Pr1169339874_sc_sz > (produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_258, type, sK113: ((produc190496183real_c > produc1821101996_sc_sz) > produc1821101996_sc_sz > set_Pr1389752855real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_259, type, sK114: (set_De208295462t_unit > produc1821101996_sc_sz > (denota610675952t_unit > set_Pr1774599175_sc_sz) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_260, type, sK115: (set_De208295462t_unit > produc1821101996_sc_sz > (denota610675952t_unit > set_Pr1774599175_sc_sz) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_261, type, sK116: ((produc190496183real_c > $o) > (produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_262, type, sK117: (produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > (produc190496183real_c > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_263, type, sK118: (produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > (produc190496183real_c > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_264, type, sK119: ((produc190496183real_c > produc190496183real_c > $o) > produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_265, type, sK120: ((produc190496183real_c > produc190496183real_c > $o) > produc640052711real_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_266, type, sK121: ((produc190496183real_c > $o) > (finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_267, type, sK122: ((produc190496183real_c > $o) > (finite1398487019real_c > finite1398487019real_c > produc190496183real_c) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_268, type, sK123: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Fi1407883041real_c) > finite1398487019real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_269, type, sK124: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Fi1407883041real_c) > finite1398487019real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_270, type, sK125: (set_Pr1389752855real_c > (finite1398487019real_c > produc866628903_sc_sz) > (finite1398487019real_c > denota610675952t_unit) > produc1821101996_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_271, type, sK126: (set_Pr1389752855real_c > (finite1398487019real_c > produc866628903_sc_sz) > (finite1398487019real_c > denota610675952t_unit) > produc1821101996_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_272, type, sK127: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > (set_Pr1389752855real_c > $o) > produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_273, type, sK128: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > (set_Pr1389752855real_c > $o) > produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_274, type, sK129: (set_Pr1389752855real_c > (produc190496183real_c > produc1821101996_sc_sz) > (produc1821101996_sc_sz > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_275, type, sK130: (finite1398487019real_c > produc640052711real_c > (produc190496183real_c > produc190496183real_c > set_Fi1407883041real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_276, type, sK131: (finite1398487019real_c > produc640052711real_c > (produc190496183real_c > produc190496183real_c > set_Fi1407883041real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_277, type, sK132: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz > finite1398487019real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_278, type, sK133: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz > finite1398487019real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_279, type, sK134: ((produc1821101996_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_280, type, sK135: ((produc1821101996_sc_sz > $o) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_281, type, sK136: ((produc1821101996_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_282, type, sK137: ((produc999471430t_unit > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_283, type, sK138: ((produc999471430t_unit > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_284, type, sK139: (produc866628903_sc_sz > produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1774599175_sc_sz) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_285, type, sK140: (produc866628903_sc_sz > produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1774599175_sc_sz) > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_286, type, sK141: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o) > produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_287, type, sK142: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > $o) > produc866628903_sc_sz > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_288, type, sK143: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz > finite1398487019real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_289, type, sK144: ((list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Fi1407883041real_c) > produc866628903_sc_sz > finite1398487019real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_290, type, sK145: (set_Pr1389752855real_c > (produc190496183real_c > produc190496183real_c) > (produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_291, type, sK146: (produc999471430t_unit > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_292, type, sK147: (produc999471430t_unit > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_293, type, sK148: (produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_294, type, sK149: (produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_295, type, sK150: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_296, type, sK151: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_297, type, sK152: (produc640052711real_c > (produc190496183real_c > produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_298, type, sK153: (produc640052711real_c > (produc190496183real_c > produc190496183real_c > $o) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_299, type, sK154: ((produc190496183real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_300, type, sK155: ((produc190496183real_c > $o) > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_301, type, sK156: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1774599175_sc_sz) > produc866628903_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_302, type, sK157: (produc190496183real_c > (finite1398487019real_c > finite1398487019real_c > set_Pr1774599175_sc_sz) > produc866628903_sc_sz > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_303, type, sK158: ((produc999471430t_unit > produc1821101996_sc_sz) > (produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_304, type, sK159: ((produc999471430t_unit > produc1821101996_sc_sz) > (produc866628903_sc_sz > denota610675952t_unit > produc1821101996_sc_sz) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_305, type, sK160: ((produc866628903_sc_sz > denota610675952t_unit > set_Fi1407883041real_c) > produc999471430t_unit > finite1398487019real_c > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_306, type, sK161: ((produc866628903_sc_sz > denota610675952t_unit > set_Fi1407883041real_c) > produc999471430t_unit > finite1398487019real_c > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_307, type, sK162: (produc190496183real_c > produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_308, type, sK163: (produc190496183real_c > produc1821101996_sc_sz > (denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_309, type, sK164: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_310, type, sK165: ((denota610675952t_unit > produc866628903_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_311, type, sK166: ((produc1821101996_sc_sz > produc999471430t_unit) > set_Pr1169339874_sc_sz > produc999471430t_unit > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_312, type, sK167: (set_Pr1169339874_sc_sz > (produc1821101996_sc_sz > produc190496183real_c) > (produc1821101996_sc_sz > produc190496183real_c) > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_313, type, sK168: ((produc1821101996_sc_sz > $o) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_314, type, sK169: ((produc1821101996_sc_sz > $o) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_315, type, sK170: (set_Pr1169339874_sc_sz > (produc1821101996_sc_sz > produc190496183real_c) > (produc190496183real_c > $o) > produc1821101996_sc_sz)).
% 0.49/0.45 thf(func_def_316, type, sK171: (finite1398487019real_c > (finite1398487019real_c > finite1398487019real_c > set_Fi1407883041real_c) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_317, type, sK172: (finite1398487019real_c > (finite1398487019real_c > finite1398487019real_c > set_Fi1407883041real_c) > produc190496183real_c > finite1398487019real_c)).
% 0.49/0.45 thf(func_def_318, type, sK173: (produc190496183real_c > set_Pr1389752855real_c > (produc190496183real_c > produc190496183real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_319, type, sK174: (formula_sf_sc_sz > produc1149990247eal_sz)).
% 0.49/0.45 thf(func_def_320, type, sK175: (formula_sf_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_321, type, sK176: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_322, type, sK177: ((denota610675952t_unit > produc866628903_sc_sz > $o) > produc1821101996_sc_sz > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_323, type, sK178: ((denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > (produc1821101996_sc_sz > produc190496183real_c) > denota610675952t_unit)).
% 0.49/0.45 thf(func_def_324, type, sK179: ((denota610675952t_unit > produc866628903_sc_sz > produc190496183real_c) > (produc1821101996_sc_sz > produc190496183real_c) > produc866628903_sc_sz)).
% 0.49/0.45 thf(func_def_325, type, sK180: (produc640052711real_c > set_Pr1389752855real_c > (produc190496183real_c > set_Pr1389752855real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_326, type, sK181: (produc640052711real_c > set_Pr1389752855real_c > (produc190496183real_c > set_Pr1389752855real_c) > produc190496183real_c)).
% 0.49/0.45 thf(func_def_327, type, sK182: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_328, type, sK183: (produc866628903_sc_sz > (list_f1238882004_sc_sz > list_f1238882004_sc_sz > set_Pr1389752855real_c) > produc190496183real_c > list_f1238882004_sc_sz)).
% 0.49/0.45 thf(func_def_329, type, sK184: (formula_a_b_c > denota231621370t_unit)).
% 0.49/0.45 thf(func_def_330, type, sK185: (formula_a_b_c > denota231621370t_unit)).
% 0.49/0.45 thf(func_def_331, type, sK186: (formula_a_b_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_332, type, sK187: (formula_a_b_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_334, type, sK189: (formula_a_b_c > produc190496183real_c)).
% 0.49/0.45 thf(func_def_335, type, sK190: (formula_a_b_c > denota231621370t_unit)).
% 0.49/0.45 thf(func_def_336, type, sK191: (formula_a_b_c > denota231621370t_unit)).
% 0.49/0.45 thf(func_def_337, type, sK192: (formula_a_b_c > produc190496183real_c)).
% 0.49/0.45 thf(f355,conjecture,(
% 0.49/0.45 (! [X0 : produc190496183real_c,X2 : denota231621370t_unit,X1 : produc190496183real_c,X3 : denota231621370t_unit] : ((denota69106024_a_b_c @ X2 @ X3 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X0 @ X1 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X2 @ phi))) = ((member1895684704real_c @ X1 @ (denota968303861_a_b_c @ X3 @ phi)))))) = ! [X3 : denota231621370t_unit,X1 : produc190496183real_c,X2 : denota231621370t_unit,X0 : produc190496183real_c] : ((denota69106024_a_b_c @ X2 @ X3 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X0 @ X1 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X2 @ phi))) = ((member1895684704real_c @ X1 @ (denota968303861_a_b_c @ X3 @ phi)))))))),
% 0.49/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 0.49/0.45 thf(f356,negated_conjecture,(
% 0.49/0.45 ~ (! [X0 : produc190496183real_c,X2 : denota231621370t_unit,X1 : produc190496183real_c,X3 : denota231621370t_unit] : ((denota69106024_a_b_c @ X2 @ X3 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X0 @ X1 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X2 @ phi))) = ((member1895684704real_c @ X1 @ (denota968303861_a_b_c @ X3 @ phi)))))) = ! [X3 : denota231621370t_unit,X1 : produc190496183real_c,X2 : denota231621370t_unit,X0 : produc190496183real_c] : ((denota69106024_a_b_c @ X2 @ X3 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X0 @ X1 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X2 @ phi))) = ((member1895684704real_c @ X1 @ (denota968303861_a_b_c @ X3 @ phi)))))))),
% 0.49/0.45 inference(negated_conjecture,[status(cth)],[f355])).
% 0.49/0.45 thf(f385,plain,(
% 0.49/0.45 ~ (! [X0 : produc190496183real_c,X1 : denota231621370t_unit,X2 : produc190496183real_c,X3 : denota231621370t_unit] : ((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) = ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))))) = ! [X4 : denota231621370t_unit,X5 : produc190496183real_c,X6 : denota231621370t_unit,X7 : produc190496183real_c] : ((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi)) => ((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi)) => (((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) = ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))))))),
% 0.49/0.45 inference(rectify,[],[f356])).
% 0.49/0.45 thf(f386,plain,(
% 0.49/0.45 ~(! [X3 : denota231621370t_unit,X1 : denota231621370t_unit,X0 : produc190496183real_c,X2 : produc190496183real_c] : ((((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi))) = $true) => ((((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi))) = $true) => (((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) = ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))))) <=> ! [X6 : denota231621370t_unit,X5 : produc190496183real_c,X7 : produc190496183real_c,X4 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi))) = $true) => ((((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) = $true) => (((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) = ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))))))),
% 0.49/0.45 inference(fool_elimination,[],[f385])).
% 0.49/0.45 thf(f1030,plain,(
% 0.49/0.45 ! [X3 : denota231621370t_unit,X1 : denota231621370t_unit,X0 : produc190496183real_c,X2 : produc190496183real_c] : (((((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) = ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))) | (((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi))) != $true)) | (((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi))) != $true)) <~> ! [X6 : denota231621370t_unit,X5 : produc190496183real_c,X7 : produc190496183real_c,X4 : denota231621370t_unit] : (((((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) = ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))) | (((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) != $true)) | (((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi))) != $true))),
% 0.49/0.45 inference(ennf_transformation,[],[f386])).
% 0.49/0.45 thf(f1031,plain,(
% 0.49/0.45 ! [X6 : denota231621370t_unit,X5 : produc190496183real_c,X4 : denota231621370t_unit,X7 : produc190496183real_c] : ((((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) = ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))) | (((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi))) != $true)) <~> ! [X2 : produc190496183real_c,X3 : denota231621370t_unit,X1 : denota231621370t_unit,X0 : produc190496183real_c] : ((((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) = ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))) | (((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi))) != $true))),
% 0.49/0.45 inference(flattening,[],[f1030])).
% 0.49/0.45 thf(f1377,plain,(
% 0.49/0.45 (? [X2 : produc190496183real_c,X3 : denota231621370t_unit,X1 : denota231621370t_unit,X0 : produc190496183real_c] : ((((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) != ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))) & (((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi))) = $true) & (((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi))) = $true)) | ? [X6 : denota231621370t_unit,X5 : produc190496183real_c,X4 : denota231621370t_unit,X7 : produc190496183real_c] : ((((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) = $true) & (((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) != ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))) & (((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi))) = $true))) & (! [X2 : produc190496183real_c,X3 : denota231621370t_unit,X1 : denota231621370t_unit,X0 : produc190496183real_c] : ((((member1895684704real_c @ X2 @ (denota968303861_a_b_c @ X3 @ phi))) = ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))) | (((denota69106024_a_b_c @ X1 @ X3 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X0 @ X2 @ (static_FVF_a_b_c @ phi))) != $true)) | ! [X6 : denota231621370t_unit,X5 : produc190496183real_c,X4 : denota231621370t_unit,X7 : produc190496183real_c] : ((((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X6 @ phi))) = ((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X4 @ phi)))) | (((denota69106024_a_b_c @ X6 @ X4 @ (static_SIGF_a_b_c @ phi))) != $true)))),
% 0.49/0.45 inference(nnf_transformation,[],[f1031])).
% 0.49/0.45 thf(f1378,plain,(
% 0.49/0.45 (? [X0 : produc190496183real_c,X1 : denota231621370t_unit,X2 : denota231621370t_unit,X3 : produc190496183real_c] : ((((member1895684704real_c @ X3 @ (denota968303861_a_b_c @ X2 @ phi))) != ((member1895684704real_c @ X0 @ (denota968303861_a_b_c @ X1 @ phi)))) & (((denota69106024_a_b_c @ X2 @ X1 @ (static_SIGF_a_b_c @ phi))) = $true) & ($true = ((denota1997846518gree_c @ X3 @ X0 @ (static_FVF_a_b_c @ phi))))) | ? [X4 : denota231621370t_unit,X5 : produc190496183real_c,X6 : denota231621370t_unit,X7 : produc190496183real_c] : ((((denota1997846518gree_c @ X7 @ X5 @ (static_FVF_a_b_c @ phi))) = $true) & (((member1895684704real_c @ X5 @ (denota968303861_a_b_c @ X6 @ phi))) != ((member1895684704real_c @ X7 @ (denota968303861_a_b_c @ X4 @ phi)))) & ($true = ((denota69106024_a_b_c @ X4 @ X6 @ (static_SIGF_a_b_c @ phi)))))) & (! [X8 : produc190496183real_c,X9 : denota231621370t_unit,X10 : denota231621370t_unit,X11 : produc190496183real_c] : ((((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi)))) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true)) | ! [X12 : denota231621370t_unit,X13 : produc190496183real_c,X14 : denota231621370t_unit,X15 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = ((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi)))) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true)))),
% 0.49/0.45 inference(rectify,[],[f1377])).
% 0.49/0.45 thf(f1379,plain,(
% 0.49/0.45 (((((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) & ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) & (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true)) | ((((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true) & (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) != ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) & (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true))) & (! [X8 : produc190496183real_c,X9 : denota231621370t_unit,X10 : denota231621370t_unit,X11 : produc190496183real_c] : ((((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi)))) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true)) | ! [X12 : denota231621370t_unit,X13 : produc190496183real_c,X14 : denota231621370t_unit,X15 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = ((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi)))) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true)))),
% 0.49/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78]),skolemize(X0,sK71),skolemize(X1,sK72),skolemize(X2,sK73),skolemize(X3,sK74),skolemize(X4,sK75),skolemize(X5,sK76),skolemize(X6,sK77),skolemize(X7,sK78)],[f1378])).
% 0.49/0.45 thf(f1803,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit,X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = ((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi)))) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi))))) )),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1804,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true) | (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1805,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) != ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))))),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1806,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true) | (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1807,plain,(
% 0.49/0.45 (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true) | ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi))))),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1808,plain,(
% 0.49/0.45 ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) != ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))))),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1809,plain,(
% 0.49/0.45 ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) | (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1810,plain,(
% 0.49/0.45 (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1811,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) != ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f1812,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(cnf_transformation,[],[f1379])).
% 0.49/0.45 thf(f2238,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true) | ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1812])).
% 0.49/0.45 thf(f2239,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1812])).
% 0.49/0.45 thf(f2254,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit,X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $false) | (((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi)))) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $true)) )),
% 0.49/0.45 inference(iff_proxy_clausification,[],[f1803])).
% 0.49/0.45 thf(f2255,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit,X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi)))) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $false) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $true)) )),
% 0.49/0.45 inference(iff_proxy_clausification,[],[f1803])).
% 0.49/0.45 thf(f2256,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit,X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | ($false = ((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi)))) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $false) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true)) )),
% 0.49/0.45 inference(iff_proxy_clausification,[],[f2255])).
% 0.49/0.45 thf(f2259,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit,X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi))) = $true) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = $false) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $false)) )),
% 0.49/0.45 inference(iff_proxy_clausification,[],[f2254])).
% 0.49/0.45 thf(f2267,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1811])).
% 0.49/0.45 thf(f2268,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))) != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1811])).
% 0.49/0.45 thf(f2269,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f2268])).
% 0.49/0.45 thf(f2270,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f2268])).
% 0.49/0.45 thf(f2271,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f2267])).
% 0.49/0.45 thf(f2272,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f2267])).
% 0.49/0.45 thf(f2275,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true) | ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1810])).
% 0.49/0.45 thf(f2276,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1810])).
% 0.49/0.45 thf(f2284,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1805])).
% 0.49/0.45 thf(f2285,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1805])).
% 0.49/0.45 thf(f2298,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1808])).
% 0.49/0.45 thf(f2299,plain,(
% 0.49/0.45 ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) | ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false)),
% 0.49/0.45 inference(xor_proxy_clausification,[],[f1808])).
% 0.49/0.45 thf(f2337,definition,(
% 0.49/0.45 spl188_4 <=> ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_4])],[avatar_definition])).
% 0.49/0.45 thf(f2341,definition,(
% 0.49/0.45 spl188_5 <=> (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_5])],[avatar_definition])).
% 0.49/0.45 thf(f2343,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK78 @ sK76 @ (static_FVF_a_b_c @ phi))) = $true) | ~spl188_5),
% 0.49/0.45 inference(avatar_component_clause,[],[f2341])).
% 0.49/0.45 thf(f2345,definition,(
% 0.49/0.45 spl188_6 <=> ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_6])],[avatar_definition])).
% 0.49/0.45 thf(f2347,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ~spl188_6),
% 0.49/0.45 inference(avatar_component_clause,[],[f2345])).
% 0.49/0.45 thf(f2348,plain,(
% 0.49/0.45 spl188_4 | spl188_5 | spl188_6),
% 0.49/0.45 inference(avatar_split_clause,[],[f2239,f2345,f2341,f2337])).
% 0.49/0.45 thf(f2350,definition,(
% 0.49/0.45 spl188_7 <=> ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_7])],[avatar_definition])).
% 0.49/0.45 thf(f2352,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ~spl188_7),
% 0.49/0.45 inference(avatar_component_clause,[],[f2350])).
% 0.49/0.45 thf(f2354,definition,(
% 0.49/0.45 spl188_8 <=> ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_8])],[avatar_definition])).
% 0.49/0.45 thf(f2356,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ~spl188_8),
% 0.49/0.45 inference(avatar_component_clause,[],[f2354])).
% 0.49/0.45 thf(f2357,plain,(
% 0.49/0.45 spl188_7 | spl188_8 | spl188_5),
% 0.49/0.45 inference(avatar_split_clause,[],[f2238,f2341,f2354,f2350])).
% 0.49/0.45 thf(f2367,definition,(
% 0.49/0.45 spl188_11 <=> ! [X13 : produc190496183real_c,X14 : denota231621370t_unit,X12 : denota231621370t_unit,X15 : produc190496183real_c] : ((((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $false) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $true) | (((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_11])],[avatar_definition])).
% 0.49/0.45 thf(f2368,plain,(
% 0.49/0.45 ( ! [X14 : denota231621370t_unit,X15 : produc190496183real_c,X12 : denota231621370t_unit,X13 : produc190496183real_c] : ((((denota1997846518gree_c @ X15 @ X13 @ (static_FVF_a_b_c @ phi))) != $true) | (((denota69106024_a_b_c @ X12 @ X14 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X15 @ (denota968303861_a_b_c @ X12 @ phi))) = $false) | (((member1895684704real_c @ X13 @ (denota968303861_a_b_c @ X14 @ phi))) = $true)) ) | ~spl188_11),
% 0.49/0.45 inference(avatar_component_clause,[],[f2367])).
% 0.49/0.45 thf(f2370,definition,(
% 0.49/0.45 spl188_12 <=> ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X9 : denota231621370t_unit,X8 : produc190496183real_c] : ((((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi))) = $true) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = $false))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_12])],[avatar_definition])).
% 0.49/0.45 thf(f2371,plain,(
% 0.49/0.45 ( ! [X10 : denota231621370t_unit,X11 : produc190496183real_c,X8 : produc190496183real_c,X9 : denota231621370t_unit] : ((((denota1997846518gree_c @ X11 @ X8 @ (static_FVF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X8 @ (denota968303861_a_b_c @ X9 @ phi))) = $false) | (((denota69106024_a_b_c @ X10 @ X9 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ X11 @ (denota968303861_a_b_c @ X10 @ phi))) = $true)) ) | ~spl188_12),
% 0.49/0.45 inference(avatar_component_clause,[],[f2370])).
% 0.49/0.45 thf(f2373,plain,(
% 0.49/0.45 spl188_11 | spl188_11),
% 0.49/0.45 inference(avatar_split_clause,[],[f2256,f2367,f2367])).
% 0.49/0.45 thf(f2374,plain,(
% 0.49/0.45 spl188_12 | spl188_12),
% 0.49/0.45 inference(avatar_split_clause,[],[f2259,f2370,f2370])).
% 0.49/0.45 thf(f2382,definition,(
% 0.49/0.45 spl188_14 <=> (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_14])],[avatar_definition])).
% 0.49/0.45 thf(f2384,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | ~spl188_14),
% 0.49/0.45 inference(avatar_component_clause,[],[f2382])).
% 0.49/0.45 thf(f2386,definition,(
% 0.49/0.45 spl188_15 <=> ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_15])],[avatar_definition])).
% 0.49/0.45 thf(f2388,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | ~spl188_15),
% 0.49/0.45 inference(avatar_component_clause,[],[f2386])).
% 0.49/0.45 thf(f2389,plain,(
% 0.49/0.45 spl188_6 | spl188_4 | spl188_14 | spl188_15),
% 0.49/0.45 inference(avatar_split_clause,[],[f2270,f2386,f2382,f2337,f2345])).
% 0.49/0.45 thf(f2390,plain,(
% 0.49/0.45 spl188_15 | spl188_7 | spl188_14 | spl188_8),
% 0.49/0.45 inference(avatar_split_clause,[],[f2269,f2354,f2382,f2350,f2386])).
% 0.49/0.45 thf(f2392,definition,(
% 0.49/0.45 spl188_16 <=> (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_16])],[avatar_definition])).
% 0.49/0.45 thf(f2394,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | ~spl188_16),
% 0.49/0.45 inference(avatar_component_clause,[],[f2392])).
% 0.49/0.45 thf(f2396,definition,(
% 0.49/0.45 spl188_17 <=> (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_17])],[avatar_definition])).
% 0.49/0.45 thf(f2398,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | ~spl188_17),
% 0.49/0.45 inference(avatar_component_clause,[],[f2396])).
% 0.49/0.45 thf(f2399,plain,(
% 0.49/0.45 spl188_16 | spl188_4 | spl188_17 | spl188_6),
% 0.49/0.45 inference(avatar_split_clause,[],[f2272,f2345,f2396,f2337,f2392])).
% 0.49/0.45 thf(f2400,plain,(
% 0.49/0.45 spl188_8 | spl188_7 | spl188_16 | spl188_17),
% 0.49/0.45 inference(avatar_split_clause,[],[f2271,f2396,f2392,f2350,f2354])).
% 0.49/0.45 thf(f2402,definition,(
% 0.49/0.45 spl188_18 <=> (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_18])],[avatar_definition])).
% 0.49/0.45 thf(f2404,plain,(
% 0.49/0.45 (((denota69106024_a_b_c @ sK75 @ sK77 @ (static_SIGF_a_b_c @ phi))) = $true) | ~spl188_18),
% 0.49/0.45 inference(avatar_component_clause,[],[f2402])).
% 0.49/0.45 thf(f2405,plain,(
% 0.49/0.45 spl188_6 | spl188_18 | spl188_4),
% 0.49/0.45 inference(avatar_split_clause,[],[f2276,f2337,f2402,f2345])).
% 0.49/0.45 thf(f2406,plain,(
% 0.49/0.45 spl188_7 | spl188_8 | spl188_18),
% 0.49/0.45 inference(avatar_split_clause,[],[f2275,f2402,f2354,f2350])).
% 0.49/0.45 thf(f2412,definition,(
% 0.49/0.45 spl188_20 <=> ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi))))),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_20])],[avatar_definition])).
% 0.49/0.45 thf(f2414,plain,(
% 0.49/0.45 ($true = ((denota69106024_a_b_c @ sK73 @ sK72 @ (static_SIGF_a_b_c @ phi)))) | ~spl188_20),
% 0.49/0.45 inference(avatar_component_clause,[],[f2412])).
% 0.49/0.45 thf(f2415,plain,(
% 0.49/0.45 spl188_18 | spl188_20),
% 0.49/0.45 inference(avatar_split_clause,[],[f1807,f2412,f2402])).
% 0.49/0.45 thf(f2426,definition,(
% 0.49/0.45 spl188_23 <=> (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true)),
% 0.49/0.45 introduced(definition,[new_symbols(definition,[spl188_23])],[avatar_definition])).
% 0.49/0.45 thf(f2428,plain,(
% 0.49/0.45 (((denota1997846518gree_c @ sK74 @ sK71 @ (static_FVF_a_b_c @ phi))) = $true) | ~spl188_23),
% 0.49/0.45 inference(avatar_component_clause,[],[f2426])).
% 0.49/0.45 thf(f2429,plain,(
% 0.49/0.45 spl188_15 | spl188_23 | spl188_14),
% 0.49/0.45 inference(avatar_split_clause,[],[f2285,f2382,f2426,f2386])).
% 0.49/0.45 thf(f2430,plain,(
% 0.49/0.45 spl188_23 | spl188_16 | spl188_17),
% 0.49/0.45 inference(avatar_split_clause,[],[f2284,f2396,f2392,f2426])).
% 0.49/0.45 thf(f2444,plain,(
% 0.49/0.45 spl188_15 | spl188_14 | spl188_20),
% 0.49/0.45 inference(avatar_split_clause,[],[f2299,f2412,f2382,f2386])).
% 0.49/0.45 thf(f2445,plain,(
% 0.49/0.45 spl188_16 | spl188_17 | spl188_20),
% 0.49/0.45 inference(avatar_split_clause,[],[f2298,f2412,f2396,f2392])).
% 0.49/0.45 thf(f2496,plain,(
% 0.49/0.45 spl188_23 | spl188_18),
% 0.49/0.45 inference(avatar_split_clause,[],[f1804,f2402,f2426])).
% 0.49/0.45 thf(f2497,plain,(
% 0.49/0.45 spl188_20 | spl188_5),
% 0.49/0.45 inference(avatar_split_clause,[],[f1809,f2341,f2412])).
% 0.49/0.45 thf(f2498,plain,(
% 0.49/0.45 spl188_5 | spl188_23),
% 0.49/0.45 inference(avatar_split_clause,[],[f1806,f2426,f2341])).
% 0.49/0.45 thf(f2510,plain,(
% 0.49/0.45 ($false = $true) | (~spl188_14 | ~spl188_16)),
% 0.49/0.45 inference(forward_demodulation,[],[f2394,f2384])).
% 0.49/0.45 thf(f2511,plain,(
% 0.49/0.45 $false | (~spl188_14 | ~spl188_16)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2510])).
% 0.49/0.45 thf(f2512,plain,(
% 0.49/0.45 ~spl188_14 | ~spl188_16),
% 0.49/0.45 inference(avatar_contradiction_clause,[],[f2511])).
% 0.49/0.45 thf(f2516,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X0 @ X1 @ (static_SIGF_a_b_c @ phi))) != $true) | ($true != $true) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ X0 @ phi))) = $false) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ X1 @ phi))) = $true)) ) | (~spl188_5 | ~spl188_11)),
% 0.49/0.45 inference(superposition,[],[f2368,f2343])).
% 0.49/0.45 thf(f2520,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X0 @ X1 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ X0 @ phi))) = $false) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ X1 @ phi))) = $true)) ) | (~spl188_5 | ~spl188_11)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2516])).
% 0.49/0.45 thf(f2522,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X1 @ X0 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ X1 @ phi))) = $true) | ($true != $true) | ($false = ((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ X0 @ phi))))) ) | (~spl188_5 | ~spl188_12)),
% 0.49/0.45 inference(superposition,[],[f2371,f2343])).
% 0.49/0.45 thf(f2526,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X1 @ X0 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ X1 @ phi))) = $true) | ($false = ((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ X0 @ phi))))) ) | (~spl188_5 | ~spl188_12)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2522])).
% 0.49/0.45 thf(f2591,plain,(
% 0.49/0.45 ($false = $true) | (~spl188_15 | ~spl188_17)),
% 0.49/0.45 inference(forward_demodulation,[],[f2398,f2388])).
% 0.49/0.45 thf(f2592,plain,(
% 0.49/0.45 $false | (~spl188_15 | ~spl188_17)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2591])).
% 0.49/0.45 thf(f2593,plain,(
% 0.49/0.45 ~spl188_15 | ~spl188_17),
% 0.49/0.45 inference(avatar_contradiction_clause,[],[f2592])).
% 0.49/0.45 thf(f2599,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | ($true != $true) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | (~spl188_5 | ~spl188_11 | ~spl188_18)),
% 0.49/0.45 inference(superposition,[],[f2520,f2404])).
% 0.49/0.45 thf(f2603,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi)))) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $true) | (~spl188_5 | ~spl188_11 | ~spl188_18)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2599])).
% 0.49/0.45 thf(f2643,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | ($true != $true) | (~spl188_5 | ~spl188_12 | ~spl188_18)),
% 0.49/0.45 inference(superposition,[],[f2526,f2404])).
% 0.49/0.45 thf(f2646,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | (((member1895684704real_c @ sK78 @ (denota968303861_a_b_c @ sK75 @ phi))) = $true) | (~spl188_5 | ~spl188_12 | ~spl188_18)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2643])).
% 0.49/0.45 thf(f2649,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | ($false = $true) | (~spl188_5 | ~spl188_12 | ~spl188_15 | ~spl188_18)),
% 0.49/0.45 inference(forward_demodulation,[],[f2646,f2388])).
% 0.49/0.45 thf(f2650,plain,(
% 0.49/0.45 (((member1895684704real_c @ sK76 @ (denota968303861_a_b_c @ sK77 @ phi))) = $false) | (~spl188_5 | ~spl188_12 | ~spl188_15 | ~spl188_18)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2649])).
% 0.49/0.45 thf(f2651,plain,(
% 0.49/0.45 spl188_14 | ~spl188_5 | ~spl188_12 | ~spl188_15 | ~spl188_18),
% 0.49/0.45 inference(avatar_split_clause,[],[f2650,f2402,f2386,f2370,f2341,f2382])).
% 0.49/0.45 thf(f2654,plain,(
% 0.49/0.45 spl188_15 | spl188_16 | ~spl188_5 | ~spl188_11 | ~spl188_18),
% 0.49/0.45 inference(avatar_split_clause,[],[f2603,f2402,f2367,f2341,f2392,f2386])).
% 0.49/0.45 thf(f2698,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X1 @ X0 @ (static_SIGF_a_b_c @ phi))) != $true) | ($true != $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ X0 @ phi))) = $false) | (((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ X1 @ phi))) = $true)) ) | (~spl188_12 | ~spl188_23)),
% 0.49/0.45 inference(superposition,[],[f2371,f2428])).
% 0.49/0.45 thf(f2699,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X0 @ X1 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ X1 @ phi))) = $true) | ($true != $true) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ X0 @ phi))))) ) | (~spl188_11 | ~spl188_23)),
% 0.49/0.45 inference(superposition,[],[f2368,f2428])).
% 0.49/0.45 thf(f2700,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X1 @ X0 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ X1 @ phi))) = $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ X0 @ phi))) = $false)) ) | (~spl188_12 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2698])).
% 0.49/0.45 thf(f2701,plain,(
% 0.49/0.45 ( ! [X0 : denota231621370t_unit,X1 : denota231621370t_unit] : ((((denota69106024_a_b_c @ X0 @ X1 @ (static_SIGF_a_b_c @ phi))) != $true) | (((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ X1 @ phi))) = $true) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ X0 @ phi))))) ) | (~spl188_11 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2699])).
% 0.49/0.45 thf(f2721,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($true != $true) | (~spl188_12 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(superposition,[],[f2700,f2414])).
% 0.49/0.45 thf(f2726,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (~spl188_12 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2721])).
% 0.49/0.45 thf(f2738,plain,(
% 0.49/0.45 ($true != $true) | ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(superposition,[],[f2701,f2414])).
% 0.49/0.45 thf(f2743,plain,(
% 0.49/0.45 ($false = ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2738])).
% 0.49/0.45 thf(f2754,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($false = $true) | (~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(forward_demodulation,[],[f2743,f2352])).
% 0.49/0.45 thf(f2755,plain,(
% 0.49/0.45 ($true = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | (~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2754])).
% 0.49/0.45 thf(f2756,plain,(
% 0.49/0.45 ($false = $true) | (~spl188_6 | ~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(forward_demodulation,[],[f2755,f2347])).
% 0.49/0.45 thf(f2757,plain,(
% 0.49/0.45 $false | (~spl188_6 | ~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2756])).
% 0.49/0.45 thf(f2758,plain,(
% 0.49/0.45 ~spl188_6 | ~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23),
% 0.49/0.45 inference(avatar_contradiction_clause,[],[f2757])).
% 0.49/0.45 thf(f2766,plain,(
% 0.49/0.45 spl188_8 | ~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23),
% 0.49/0.45 inference(avatar_split_clause,[],[f2755,f2426,f2412,f2367,f2350,f2354])).
% 0.49/0.45 thf(f2767,definition,(
% 0.49/0.45 ($true != ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi)))) | ($true != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false != ((member1895684704real_c @ sK74 @ (denota968303861_a_b_c @ sK73 @ phi)))) | ($false = ((member1895684704real_c @ sK71 @ (denota968303861_a_b_c @ sK72 @ phi))))),
% 0.49/0.45 introduced(theory,[theory_tautology_sat_conflict])).
% 0.49/0.45 thf(f2776,plain,(
% 0.49/0.45 spl188_6 | spl188_7 | ~spl188_12 | ~spl188_20 | ~spl188_23),
% 0.49/0.45 inference(avatar_split_clause,[],[f2726,f2426,f2412,f2370,f2350,f2345])).
% 0.49/0.45 thf(f2777,plain,(
% 0.49/0.45 spl188_4 | spl188_8 | ~spl188_11 | ~spl188_20 | ~spl188_23),
% 0.49/0.45 inference(avatar_split_clause,[],[f2743,f2426,f2412,f2367,f2354,f2337])).
% 0.49/0.45 thf(f2780,plain,(
% 0.49/0.45 ($false = $true) | (~spl188_6 | ~spl188_8)),
% 0.49/0.45 inference(forward_demodulation,[],[f2356,f2347])).
% 0.49/0.45 thf(f2781,plain,(
% 0.49/0.45 $false | (~spl188_6 | ~spl188_8)),
% 0.49/0.45 inference(trivial_inequality_removal,[],[f2780])).
% 0.49/0.45 thf(f2782,plain,(
% 0.49/0.45 ~spl188_6 | ~spl188_8),
% 0.49/0.45 inference(avatar_contradiction_clause,[],[f2781])).
% 0.49/0.45 cnf(s3, plain, spl188_4 | spl188_5 | spl188_6, inference(sat_conversion,[],[f2348])).
% 0.49/0.45 cnf(s4, plain, spl188_5 | spl188_7 | spl188_8, inference(sat_conversion,[],[f2357])).
% 0.49/0.45 cnf(s8, plain, spl188_11 | spl188_11, inference(sat_conversion,[],[f2373])).
% 0.49/0.45 cnf(s9, plain, spl188_11, inference(rat,[],[s8])).
% 0.49/0.45 cnf(s10, plain, spl188_12 | spl188_12, inference(sat_conversion,[],[f2374])).
% 0.49/0.45 cnf(s11, plain, spl188_12, inference(rat,[],[s10])).
% 0.49/0.45 cnf(s14, plain, spl188_4 | spl188_6 | spl188_14 | spl188_15, inference(sat_conversion,[],[f2389])).
% 0.49/0.45 cnf(s15, plain, spl188_7 | spl188_8 | spl188_14 | spl188_15, inference(sat_conversion,[],[f2390])).
% 0.49/0.45 cnf(s16, plain, spl188_4 | spl188_6 | spl188_16 | spl188_17, inference(sat_conversion,[],[f2399])).
% 0.49/0.45 cnf(s17, plain, spl188_7 | spl188_8 | spl188_16 | spl188_17, inference(sat_conversion,[],[f2400])).
% 0.49/0.45 cnf(s18, plain, spl188_4 | spl188_6 | spl188_18, inference(sat_conversion,[],[f2405])).
% 0.49/0.45 cnf(s19, plain, spl188_7 | spl188_8 | spl188_18, inference(sat_conversion,[],[f2406])).
% 0.49/0.45 cnf(s21, plain, spl188_18 | spl188_20, inference(sat_conversion,[],[f2415])).
% 0.49/0.45 cnf(s24, plain, spl188_14 | spl188_15 | spl188_23, inference(sat_conversion,[],[f2429])).
% 0.49/0.45 cnf(s25, plain, spl188_16 | spl188_17 | spl188_23, inference(sat_conversion,[],[f2430])).
% 0.49/0.45 cnf(s29, plain, spl188_14 | spl188_15 | spl188_20, inference(sat_conversion,[],[f2444])).
% 0.49/0.45 cnf(s30, plain, spl188_16 | spl188_17 | spl188_20, inference(sat_conversion,[],[f2445])).
% 0.49/0.45 cnf(s43, plain, spl188_18 | spl188_23, inference(sat_conversion,[],[f2496])).
% 0.49/0.45 cnf(s44, plain, spl188_5 | spl188_20, inference(sat_conversion,[],[f2497])).
% 0.49/0.45 cnf(s45, plain, spl188_5 | spl188_23, inference(sat_conversion,[],[f2498])).
% 0.49/0.45 cnf(s47, plain, ~spl188_14 | ~spl188_16, inference(sat_conversion,[],[f2512])).
% 0.49/0.45 cnf(s55, plain, ~spl188_15 | ~spl188_17, inference(sat_conversion,[],[f2593])).
% 0.49/0.45 cnf(s58, plain, ~spl188_5 | ~spl188_12 | spl188_14 | ~spl188_15 | ~spl188_18, inference(sat_conversion,[],[f2651])).
% 0.49/0.45 cnf(s61, plain, ~spl188_5 | ~spl188_11 | spl188_15 | spl188_16 | ~spl188_18, inference(sat_conversion,[],[f2654])).
% 0.49/0.45 cnf(s79, plain, ~spl188_6 | ~spl188_7 | ~spl188_11 | ~spl188_20 | ~spl188_23, inference(sat_conversion,[],[f2758])).
% 0.49/0.45 cnf(s87, plain, ~spl188_7 | spl188_8 | ~spl188_11 | ~spl188_20 | ~spl188_23, inference(sat_conversion,[],[f2766])).
% 0.49/0.45 cnf(s88, plain, ~spl188_4 | spl188_6 | ~spl188_7 | ~spl188_8, inference(sat_conversion,[],[f2767])).
% 0.49/0.45 cnf(s97, plain, spl188_6 | spl188_7 | ~spl188_12 | ~spl188_20 | ~spl188_23, inference(sat_conversion,[],[f2776])).
% 0.49/0.45 cnf(s98, plain, spl188_4 | spl188_8 | ~spl188_11 | ~spl188_20 | ~spl188_23, inference(sat_conversion,[],[f2777])).
% 0.49/0.45 cnf(s101, plain, ~spl188_6 | ~spl188_8, inference(sat_conversion,[],[f2782])).
% 0.49/0.45 cnf(s103, plain, spl188_5 | spl188_4, inference(rat,[],[s101,s98,s3,s44,s45,s9])).
% 0.49/0.45 cnf(s104, plain, spl188_14 | spl188_23 | ~spl188_5, inference(rat,[],[s58,s24,s43,s11])).
% 0.49/0.45 cnf(s105, plain, spl188_23 | ~spl188_5, inference(rat,[],[s55,s61,s25,s47,s104,s43,s9])).
% 0.49/0.45 cnf(s106, plain, spl188_14 | spl188_20 | ~spl188_5, inference(rat,[],[s58,s29,s21,s11])).
% 0.49/0.45 cnf(s107, plain, spl188_20 | ~spl188_5, inference(rat,[],[s55,s61,s30,s47,s106,s21,s9])).
% 0.49/0.45 cnf(s108, plain, spl188_14 | spl188_4, inference(rat,[],[s14,s58,s18,s101,s98,s107,s105,s103,s11,s9])).
% 0.49/0.45 cnf(s109, plain, spl188_4, inference(rat,[],[s55,s16,s61,s47,s108,s18,s101,s98,s107,s105,s103,s9])).
% 0.49/0.45 cnf(s110, plain, spl188_14 | ~spl188_6 | ~spl188_5, inference(rat,[],[s15,s58,s19,s79,s107,s105,s101,s11,s9])).
% 0.49/0.45 cnf(s111, plain, ~spl188_6 | ~spl188_5, inference(rat,[],[s55,s17,s61,s47,s110,s19,s79,s101,s105,s107,s9])).
% 0.49/0.45 cnf(s112, plain, spl188_6 | ~spl188_23 | ~spl188_20, inference(rat,[],[s87,s88,s97,s11,s109,s9])).
% 0.49/0.45 cnf(s113, plain, ~spl188_5, inference(rat,[],[s112,s111,s107,s105])).
% 0.49/0.45 cnf(s114, plain, spl188_23, inference(rat,[],[s45,s113])).
% 0.49/0.45 cnf(s115, plain, spl188_20, inference(rat,[],[s44,s113])).
% 0.49/0.45 cnf(s116, plain, spl188_6, inference(rat,[],[s112,s115,s114])).
% 0.49/0.45 cnf(s117, plain, ~spl188_8, inference(rat,[],[s101,s116])).
% 0.49/0.45 cnf(s118, plain, ~spl188_7, inference(rat,[],[s79,s114,s115,s9,s116])).
% 0.49/0.45 cnf(s119, plain, $false, inference(rat,[],[s4,s113,s117,s118])).
% 0.49/0.45 thf(f2783,plain,(
% 0.49/0.45 $false),
% 0.49/0.45 inference(avatar_sat_refutation,[],[s119])).
% 0.49/0.45 % SZS output end Proof for theBenchmark
% 0.49/0.45 % (1212941)------------------------------
% 0.49/0.45 % (1212941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.49/0.45 % (1212941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.49/0.45 % (1212941)CaDiCaL version: 2.1.3
% 0.49/0.45 % (1212941)Termination reason: Refutation
% 0.49/0.45 % (1212941)Time elapsed: 0.104 s
% 0.49/0.45 % (1212941)Peak memory usage: 15 MB
% 0.49/0.45 % (1212941)Instructions burned: 213 (million)
% 0.49/0.45 % (1212933)Success in time 0.147 s
% 0.49/0.45 % Vampire exiting
%------------------------------------------------------------------------------