%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : ITP011^3 : TPTP v9.3.1. Bugfixed 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:07:43 AM UTC 2026
% Result : Theorem 2.14s 0.74s
% Output : Refutation 2.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP011^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 % Computer : n006.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 19:25:40 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 Running higher-order theorem proving
% 0.21/0.28 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.63/0.48 % (1187912)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.63/0.48 % (1187921)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3748153469:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.63/0.48 % (1187918)lrs+10_16_si=on:nwc=1.5:random_seed=507551760:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.63/0.48 % (1187920)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=1384111968: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.63/0.48 % (1187921)Instruction limit reached!
% 0.63/0.48 % (1187921)------------------------------
% 0.63/0.48 % (1187921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (1187921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (1187921)CaDiCaL version: 2.1.3
% 0.63/0.48 % (1187921)Termination reason: Instruction limit
% 0.63/0.48 % (1187921)Termination phase: Saturation
% 0.63/0.48 % (1187921)Time elapsed: 0.012 s
% 0.63/0.48 % (1187921)Peak memory usage: 12 MB
% 0.63/0.48 % (1187921)Instructions burned: 25 (million)
% 0.63/0.48 % (1187918)Instruction limit reached!
% 0.63/0.48 % (1187918)------------------------------
% 0.63/0.48 % (1187918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (1187918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (1187918)CaDiCaL version: 2.1.3
% 0.63/0.48 % (1187918)Termination reason: Instruction limit
% 0.63/0.48 % (1187918)Termination phase: Saturation
% 0.63/0.48 % (1187918)Time elapsed: 0.011 s
% 0.63/0.48 % (1187918)Peak memory usage: 12 MB
% 0.63/0.48 % (1187918)Instructions burned: 20 (million)
% 0.63/0.48 % (1187919)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1931529996:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.63/0.48 % (1187919)Instruction limit reached!
% 0.63/0.48 % (1187919)------------------------------
% 0.63/0.48 % (1187919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (1187919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (1187919)CaDiCaL version: 2.1.3
% 0.63/0.48 % (1187919)Termination reason: Instruction limit
% 0.63/0.48 % (1187919)Termination phase: Preprocessing 3
% 0.63/0.48 % (1187919)Time elapsed: 0.004 s
% 0.63/0.48 % (1187919)Peak memory usage: 10 MB
% 0.63/0.48 % (1187919)Instructions burned: 3 (million)
% 0.63/0.48 % (1187923)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.63/0.48 % (1187923)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.63/0.48 % (1187928)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=80424636:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.63/0.48 % (1187928)Instruction limit reached!
% 0.63/0.48 % (1187928)------------------------------
% 0.63/0.48 % (1187928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.48 % (1187928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.48 % (1187928)CaDiCaL version: 2.1.3
% 0.63/0.48 % (1187928)Termination reason: Instruction limit
% 0.63/0.48 % (1187928)Termination phase: Clausification
% 0.63/0.48 % (1187928)Time elapsed: 0.003 s
% 0.63/0.48 % (1187928)Peak memory usage: 10 MB
% 0.63/0.48 % (1187928)Instructions burned: 5 (million)
% 0.63/0.48 % (1187917)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2183232801:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.63/0.48 % (1187922)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=1680589829:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.63/0.48 % (1187923)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=1624762773:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.63/0.48 % (1187930)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.27/0.53 % (1187927)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=784819282:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 1.27/0.53 % (1187927)Instruction limit reached!
% 1.27/0.53 % (1187927)------------------------------
% 1.27/0.53 % (1187927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.53 % (1187927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.53 % (1187927)CaDiCaL version: 2.1.3
% 1.27/0.53 % (1187927)Termination reason: Instruction limit
% 1.27/0.53 % (1187927)Termination phase: Property scanning
% 1.27/0.53 % (1187927)Time elapsed: 0.004 s
% 1.27/0.53 % (1187927)Peak memory usage: 10 MB
% 1.27/0.53 % (1187927)Instructions burned: 6 (million)
% 1.27/0.53 % (1187932)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=4018680157:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 1.27/0.53 % (1187930)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2809633189:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 1.27/0.53 % (1187930)Instruction limit reached!
% 1.27/0.53 % (1187930)------------------------------
% 1.27/0.53 % (1187930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.53 % (1187930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.53 % (1187930)CaDiCaL version: 2.1.3
% 1.27/0.53 % (1187930)Termination reason: Instruction limit
% 1.27/0.53 % (1187930)Termination phase: Preprocessing 3
% 1.27/0.53 % (1187930)Time elapsed: 0.005 s
% 1.27/0.53 % (1187930)Peak memory usage: 10 MB
% 1.27/0.53 % (1187930)Instructions burned: 8 (million)
% 1.27/0.53 % (1187932)Instruction limit reached!
% 1.27/0.53 % (1187932)------------------------------
% 1.27/0.53 % (1187932)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.53 % (1187932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.53 % (1187932)CaDiCaL version: 2.1.3
% 1.27/0.53 % (1187932)Termination reason: Instruction limit
% 1.27/0.53 % (1187932)Termination phase: Saturation
% 1.27/0.53 % (1187932)Time elapsed: 0.007 s
% 1.27/0.53 % (1187932)Peak memory usage: 12 MB
% 1.27/0.53 % (1187932)Instructions burned: 12 (million)
% 1.27/0.53 % (1187939)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 1.27/0.53 % (1187939)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 1.27/0.53 % (1187939)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=1780993997:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 1.27/0.53 % (1187940)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=1095400984:i=86:piset=equals:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/86Mi)
% 1.27/0.53 % (1187941)lrs+10_1_si=on:cs=on:random_seed=1117389426:i=8:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/8Mi)
% 1.27/0.53 % (1187941)Instruction limit reached!
% 1.27/0.53 % (1187941)------------------------------
% 1.27/0.53 % (1187941)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.53 % (1187941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.53 % (1187941)CaDiCaL version: 2.1.3
% 1.27/0.53 % (1187941)Termination reason: Instruction limit
% 1.27/0.53 % (1187941)Termination phase: Saturation
% 1.27/0.53 % (1187941)Time elapsed: 0.005 s
% 1.27/0.53 % (1187941)Peak memory usage: 11 MB
% 1.27/0.53 % (1187941)Instructions burned: 10 (million)
% 1.27/0.53 % (1187939)Instruction limit reached!
% 1.27/0.53 % (1187939)------------------------------
% 1.27/0.53 % (1187939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.53 % (1187939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.53 % (1187939)CaDiCaL version: 2.1.3
% 1.27/0.53 % (1187939)Termination reason: Instruction limit
% 1.27/0.53 % (1187939)Termination phase: Saturation
% 1.27/0.53 % (1187939)Time elapsed: 0.014 s
% 1.27/0.53 % (1187939)Peak memory usage: 12 MB
% 1.27/0.53 % (1187939)Instructions burned: 28 (million)
% 1.27/0.53 % (1187945)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 1.27/0.61 % (1187945)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=404510031:i=2:add=on:rtra=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.27/0.61 % (1187946)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=4084200146:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/38Mi)
% 1.27/0.61 % (1187945)Instruction limit reached!
% 1.27/0.61 % (1187945)------------------------------
% 1.27/0.61 % (1187945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187945)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187945)Termination reason: Instruction limit
% 1.27/0.61 % (1187945)Termination phase: Property scanning
% 1.27/0.61 % (1187945)Time elapsed: 0.002 s
% 1.27/0.61 % (1187945)Peak memory usage: 9 MB
% 1.27/0.61 % (1187945)Instructions burned: 4 (million)
% 1.27/0.61 % (1187917)Instruction limit reached!
% 1.27/0.61 % (1187917)------------------------------
% 1.27/0.61 % (1187917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187917)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187917)Termination reason: Instruction limit
% 1.27/0.61 % (1187917)Termination phase: Saturation
% 1.27/0.61 % (1187917)Time elapsed: 0.084 s
% 1.27/0.61 % (1187917)Peak memory usage: 13 MB
% 1.27/0.61 % (1187917)Instructions burned: 87 (million)
% 1.27/0.61 % (1187940)Instruction limit reached!
% 1.27/0.61 % (1187940)------------------------------
% 1.27/0.61 % (1187940)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187940)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187940)Termination reason: Instruction limit
% 1.27/0.61 % (1187940)Termination phase: Saturation
% 1.27/0.61 % (1187940)Time elapsed: 0.037 s
% 1.27/0.61 % (1187940)Peak memory usage: 13 MB
% 1.27/0.61 % (1187940)Instructions burned: 86 (million)
% 1.27/0.61 % (1187922)Instruction limit reached!
% 1.27/0.61 % (1187922)------------------------------
% 1.27/0.61 % (1187922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187922)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187922)Termination reason: Instruction limit
% 1.27/0.61 % (1187922)Termination phase: Saturation
% 1.27/0.61 % (1187922)Time elapsed: 0.081 s
% 1.27/0.61 % (1187922)Peak memory usage: 13 MB
% 1.27/0.61 % (1187922)Instructions burned: 75 (million)
% 1.27/0.61 % (1187946)Instruction limit reached!
% 1.27/0.61 % (1187946)------------------------------
% 1.27/0.61 % (1187946)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187946)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187946)Termination reason: Instruction limit
% 1.27/0.61 % (1187946)Termination phase: Saturation
% 1.27/0.61 % (1187946)Time elapsed: 0.022 s
% 1.27/0.61 % (1187946)Peak memory usage: 13 MB
% 1.27/0.61 % (1187946)Instructions burned: 39 (million)
% 1.27/0.61 % (1187949)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=2353408965:st=2:i=249:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/249Mi)
% 1.27/0.61 % (1187953)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=266330558:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.27/0.61 % (1187950)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=1111511550:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2998 on theBenchmark for (2998ds/25Mi)
% 1.27/0.61 % (1187949)Refutation not found, incomplete strategy
% 1.27/0.61 % (1187949)------------------------------
% 1.27/0.61 % (1187949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.27/0.61 % (1187949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.27/0.61 % (1187949)CaDiCaL version: 2.1.3
% 1.27/0.61 % (1187949)Termination reason: Refutation not found, incomplete strategy
% 1.27/0.61 % (1187949)Time elapsed: 0.013 s
% 2.02/0.68 % (1187949)Peak memory usage: 12 MB
% 2.02/0.68 % (1187949)Instructions burned: 9 (million)
% 2.02/0.68 % (1187949)------------------------------
% 2.02/0.68 % (1187949)------------------------------
% 2.02/0.68 % (1187953)Instruction limit reached!
% 2.02/0.68 % (1187953)------------------------------
% 2.02/0.68 % (1187953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.68 % (1187953)CaDiCaL version: 2.1.3
% 2.02/0.68 % (1187953)Termination reason: Instruction limit
% 2.02/0.68 % (1187953)Termination phase: Saturation
% 2.02/0.68 % (1187953)Time elapsed: 0.009 s
% 2.02/0.68 % (1187953)Peak memory usage: 12 MB
% 2.02/0.68 % (1187953)Instructions burned: 15 (million)
% 2.02/0.68 % (1187952)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1436627563:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/327Mi)
% 2.02/0.68 % (1187951)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3257101263:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.02/0.68 % (1187950)Instruction limit reached!
% 2.02/0.68 % (1187950)------------------------------
% 2.02/0.68 % (1187950)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.68 % (1187950)CaDiCaL version: 2.1.3
% 2.02/0.68 % (1187950)Termination reason: Instruction limit
% 2.02/0.68 % (1187950)Termination phase: Saturation
% 2.02/0.68 % (1187950)Time elapsed: 0.013 s
% 2.02/0.68 % (1187950)Peak memory usage: 12 MB
% 2.02/0.68 % (1187950)Instructions burned: 26 (million)
% 2.02/0.68 % (1187951)Instruction limit reached!
% 2.02/0.68 % (1187951)------------------------------
% 2.02/0.68 % (1187951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.68 % (1187951)CaDiCaL version: 2.1.3
% 2.02/0.68 % (1187951)Termination reason: Instruction limit
% 2.02/0.68 % (1187951)Termination phase: Saturation
% 2.02/0.68 % (1187951)Time elapsed: 0.013 s
% 2.02/0.68 % (1187951)Peak memory usage: 11 MB
% 2.02/0.68 % (1187951)Instructions burned: 14 (million)
% 2.02/0.68 % (1187957)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3959014455:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2997 on theBenchmark for (2997ds/2Mi)
% 2.02/0.68 % (1187961)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2210403090:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.02/0.68 % (1187957)Instruction limit reached!
% 2.02/0.68 % (1187957)------------------------------
% 2.02/0.68 % (1187957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.68 % (1187957)CaDiCaL version: 2.1.3
% 2.02/0.68 % (1187957)Termination reason: Instruction limit
% 2.02/0.68 % (1187957)Termination phase: Property scanning
% 2.02/0.68 % (1187957)Time elapsed: 0.003 s
% 2.02/0.68 % (1187957)Peak memory usage: 10 MB
% 2.02/0.68 % (1187957)Instructions burned: 5 (million)
% 2.02/0.68 % (1187923)Instruction limit reached!
% 2.02/0.68 % (1187923)------------------------------
% 2.02/0.68 % (1187923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.02/0.68 % (1187923)CaDiCaL version: 2.1.3
% 2.02/0.68 % (1187923)Termination reason: Instruction limit
% 2.02/0.68 % (1187923)Termination phase: Saturation
% 2.02/0.68 % (1187923)Time elapsed: 0.159 s
% 2.02/0.68 % (1187923)Peak memory usage: 13 MB
% 2.02/0.68 % (1187923)Instructions burned: 157 (million)
% 2.02/0.68 % (1187958)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=4145240579:i=26:ep=R:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/26Mi)
% 2.02/0.68 % (1187962)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3757012688:cond=on:i=60:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/60Mi)
% 2.02/0.68 % (1187961)Instruction limit reached!
% 2.02/0.68 % (1187961)------------------------------
% 2.02/0.68 % (1187961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.02/0.68 % (1187961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187961)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187961)Termination reason: Instruction limit
% 2.14/0.74 % (1187961)Termination phase: Saturation
% 2.14/0.74 % (1187961)Time elapsed: 0.012 s
% 2.14/0.74 % (1187961)Peak memory usage: 11 MB
% 2.14/0.74 % (1187961)Instructions burned: 23 (million)
% 2.14/0.74 % (1187958)Instruction limit reached!
% 2.14/0.74 % (1187958)------------------------------
% 2.14/0.74 % (1187958)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187958)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187958)Termination reason: Instruction limit
% 2.14/0.74 % (1187958)Termination phase: Saturation
% 2.14/0.74 % (1187958)Time elapsed: 0.023 s
% 2.14/0.74 % (1187958)Peak memory usage: 12 MB
% 2.14/0.74 % (1187958)Instructions burned: 26 (million)
% 2.14/0.74 % (1187965)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.14/0.74 % (1187965)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.14/0.74 % (1187968)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.14/0.74 % (1187965)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=949230764:i=14:add=off:nm=40:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 2.14/0.74 % (1187968)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=4212911610:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2997 on theBenchmark for (2997ds/8Mi)
% 2.14/0.74 % (1187965)Instruction limit reached!
% 2.14/0.74 % (1187965)------------------------------
% 2.14/0.74 % (1187965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187965)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187965)Termination reason: Instruction limit
% 2.14/0.74 % (1187965)Termination phase: Property scanning
% 2.14/0.74 % (1187965)Time elapsed: 0.012 s
% 2.14/0.74 % (1187965)Peak memory usage: 10 MB
% 2.14/0.74 % (1187965)Instructions burned: 14 (million)
% 2.14/0.74 % (1187969)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=1372769487:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/31Mi)
% 2.14/0.74 % (1187970)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2277356329:i=7:hud=5:bd=preordered:rtra=on:bet=on_2997 on theBenchmark for (2997ds/7Mi)
% 2.14/0.74 % (1187968)Instruction limit reached!
% 2.14/0.74 % (1187968)------------------------------
% 2.14/0.74 % (1187968)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187968)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187968)Termination reason: Instruction limit
% 2.14/0.74 % (1187968)Termination phase: Saturation
% 2.14/0.74 % (1187968)Time elapsed: 0.008 s
% 2.14/0.74 % (1187968)Peak memory usage: 11 MB
% 2.14/0.74 % (1187968)Instructions burned: 8 (million)
% 2.14/0.74 % (1187970)Instruction limit reached!
% 2.14/0.74 % (1187970)------------------------------
% 2.14/0.74 % (1187970)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187970)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187970)Termination reason: Instruction limit
% 2.14/0.74 % (1187970)Termination phase: Saturation
% 2.14/0.74 % (1187970)Time elapsed: 0.004 s
% 2.14/0.74 % (1187970)Peak memory usage: 11 MB
% 2.14/0.74 % (1187970)Instructions burned: 9 (million)
% 2.14/0.74 % (1187962)Instruction limit reached!
% 2.14/0.74 % (1187962)------------------------------
% 2.14/0.74 % (1187962)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187962)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187962)Termination reason: Instruction limit
% 2.14/0.74 % (1187962)Termination phase: Saturation
% 2.14/0.74 % (1187962)Time elapsed: 0.077 s
% 2.14/0.74 % (1187962)Peak memory usage: 12 MB
% 2.14/0.74 % (1187962)Instructions burned: 60 (million)
% 2.14/0.74 % (1187969)Instruction limit reached!
% 2.14/0.74 % (1187969)------------------------------
% 2.14/0.74 % (1187969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187969)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187969)Termination reason: Instruction limit
% 2.14/0.74 % (1187969)Termination phase: Saturation
% 2.14/0.74 % (1187969)Time elapsed: 0.043 s
% 2.14/0.74 % (1187969)Peak memory usage: 12 MB
% 2.14/0.74 % (1187969)Instructions burned: 32 (million)
% 2.14/0.74 % (1187974)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1090377261:i=23:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/23Mi)
% 2.14/0.74 % (1187976)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=3160826974:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2997 on theBenchmark for (2997ds/20Mi)
% 2.14/0.74 % (1187974)Instruction limit reached!
% 2.14/0.74 % (1187974)------------------------------
% 2.14/0.74 % (1187974)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187974)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187974)Termination reason: Instruction limit
% 2.14/0.74 % (1187974)Termination phase: Saturation
% 2.14/0.74 % (1187974)Time elapsed: 0.011 s
% 2.14/0.74 % (1187974)Peak memory usage: 11 MB
% 2.14/0.74 % (1187974)Instructions burned: 24 (million)
% 2.14/0.74 % (1187977)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=3261745093:i=1240:rtra=on:ixr=off_2997 on theBenchmark for (2997ds/1240Mi)
% 2.14/0.74 % (1187978)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1449119195:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2996 on theBenchmark for (2996ds/143Mi)
% 2.14/0.74 % (1187976)Instruction limit reached!
% 2.14/0.74 % (1187976)------------------------------
% 2.14/0.74 % (1187976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187976)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187976)Termination reason: Instruction limit
% 2.14/0.74 % (1187976)Termination phase: Saturation
% 2.14/0.74 % (1187976)Time elapsed: 0.022 s
% 2.14/0.74 % (1187976)Peak memory usage: 12 MB
% 2.14/0.74 % (1187976)Instructions burned: 21 (million)
% 2.14/0.74 % (1187982)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=1330605404:i=42:hud=10:rtra=on_2996 on theBenchmark for (2996ds/42Mi)
% 2.14/0.74 % (1187979)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=2339879246:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/193Mi)
% 2.14/0.74 % (1187986)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.14/0.74 % (1187986)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3065179156:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2996 on theBenchmark for (2996ds/7Mi)
% 2.14/0.74 % (1187986)Instruction limit reached!
% 2.14/0.74 % (1187986)------------------------------
% 2.14/0.74 % (1187986)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187986)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187986)Termination reason: Instruction limit
% 2.14/0.74 % (1187986)Termination phase: Preprocessing 3
% 2.14/0.74 % (1187986)Time elapsed: 0.004 s
% 2.14/0.74 % (1187986)Peak memory usage: 10 MB
% 2.14/0.74 % (1187986)Instructions burned: 8 (million)
% 2.14/0.74 % (1187982)Instruction limit reached!
% 2.14/0.74 % (1187982)------------------------------
% 2.14/0.74 % (1187982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187982)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187982)Termination reason: Instruction limit
% 2.14/0.74 % (1187982)Termination phase: Saturation
% 2.14/0.74 % (1187982)Time elapsed: 0.024 s
% 2.14/0.74 % (1187982)Peak memory usage: 12 MB
% 2.14/0.74 % (1187982)Instructions burned: 42 (million)
% 2.14/0.74 % (1187952)Instruction limit reached!
% 2.14/0.74 % (1187952)------------------------------
% 2.14/0.74 % (1187952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187952)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187952)Termination reason: Instruction limit
% 2.14/0.74 % (1187952)Termination phase: Saturation
% 2.14/0.74 % (1187952)Time elapsed: 0.197 s
% 2.14/0.74 % (1187952)Peak memory usage: 13 MB
% 2.14/0.74 % (1187952)Instructions burned: 328 (million)
% 2.14/0.74 % (1187989)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=465838698:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2996 on theBenchmark for (2996ds/181Mi)
% 2.14/0.74 % (1187990)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=4113854895:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2996 on theBenchmark for (2996ds/169Mi)
% 2.14/0.74 % (1187991)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.14/0.74 % (1187991)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=2357814475:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2995 on theBenchmark for (2995ds/6Mi)
% 2.14/0.74 % (1187991)Instruction limit reached!
% 2.14/0.74 % (1187991)------------------------------
% 2.14/0.74 % (1187991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.74 % (1187991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.74 % (1187991)CaDiCaL version: 2.1.3
% 2.14/0.74 % (1187991)Termination reason: Instruction limit
% 2.14/0.74 % (1187991)Termination phase: SInE selection
% 2.14/0.74 % (1187991)Time elapsed: 0.003 s
% 2.14/0.74 % (1187991)Peak memory usage: 10 MB
% 2.14/0.74 % (1187991)Instructions burned: 7 (million)
% 2.14/0.74 % (1187995)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=1974844970:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2995 on theBenchmark for (2995ds/22Mi)
% 2.14/0.74 % (1187990) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1187912-1187990"...
% 2.14/0.74 % (1187990)...printing done.
% 2.14/0.74 % (1187990)Refutation found. Thanks to Tanya!
% 2.14/0.74 % SZS status Theorem for theBenchmark
% 2.14/0.74 % SZS output start Proof for theBenchmark
% 2.14/0.74 thf(type_def_5, type, tyop_2Emin_2Ebool: $tType).
% 2.14/0.74 thf(type_def_6, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 2.14/0.74 thf(type_def_7, type, tyop_2Eoption_2Eoption: $tType > $tType).
% 2.14/0.74 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 2.14/0.74 thf(type_def_9, type, sK2: $tType).
% 2.14/0.74 thf(func_def_0, type, c_2Ebool_2E_21: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.14/0.74 thf(func_def_1, type, c_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 2.14/0.74 thf(func_def_2, type, c_2Emin_2E_3D: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.14/0.74 thf(func_def_3, type, c_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 2.14/0.74 thf(func_def_4, type, c_2Ebool_2E_3F: !>[X0: $tType]:(((X0 > $o) > $o))).
% 2.14/0.74 thf(func_def_5, type, c_2Ebool_2EF: $o).
% 2.14/0.74 thf(func_def_6, type, c_2Eoption_2EIS__NONE: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ X0 > $o))).
% 2.14/0.74 thf(func_def_7, type, c_2Eoption_2EIS__SOME: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ X0 > $o))).
% 2.14/0.74 thf(func_def_8, type, c_2Eoption_2ENONE: !>[X0: $tType]:(tyop_2Eoption_2Eoption @ X0)).
% 2.14/0.74 thf(func_def_9, type, c_2Eoption_2EOPTION__JOIN: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ tyop_2Eoption_2Eoption @ X0 > tyop_2Eoption_2Eoption @ X0))).
% 2.14/0.74 thf(func_def_10, type, c_2Eoption_2EOPTION__MAP: !>[X0: $tType, X1: $tType]:(((X0 > X1) > tyop_2Eoption_2Eoption @ X0 > tyop_2Eoption_2Eoption @ X1))).
% 2.14/0.74 thf(func_def_11, type, c_2Eoption_2EOPTREL: !>[X0: $tType, X1: $tType]:(((X0 > X1 > $o) > tyop_2Eoption_2Eoption @ X0 > tyop_2Eoption_2Eoption @ X1 > $o))).
% 2.14/0.74 thf(func_def_12, type, c_2Eoption_2ESOME: !>[X0: $tType]:((X0 > tyop_2Eoption_2Eoption @ X0))).
% 2.14/0.74 thf(func_def_13, type, c_2Ebool_2ET: $o).
% 2.14/0.74 thf(func_def_14, type, c_2Eoption_2ETHE: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ X0 > X0))).
% 2.14/0.74 thf(func_def_15, type, c_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 2.14/0.74 thf(func_def_16, type, c_2Eoption_2Eoption__CASE: !>[X0: $tType, X1: $tType]:((tyop_2Eoption_2Eoption @ X0 > X1 > (X0 > X1) > X1))).
% 2.14/0.74 thf(func_def_17, type, c_2Ebool_2E_7E: ($o > $o)).
% 2.14/0.74 thf(func_def_19, type, vNOT: ($o > $o)).
% 2.14/0.74 thf(func_def_22, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.14/0.74 thf(func_def_23, type, sK0: !>[X0: $tType, X1: $tType]:((tyop_2Eoption_2Eoption @ X0 > tyop_2Eoption_2Eoption @ X1 > (X0 > X1 > $o) > X1))).
% 2.14/0.74 thf(func_def_24, type, sK1: !>[X0: $tType, X1: $tType]:((tyop_2Eoption_2Eoption @ X0 > tyop_2Eoption_2Eoption @ X1 > (X0 > X1 > $o) > X0))).
% 2.14/0.74 thf(func_def_25, type, sK3: sK2).
% 2.14/0.74 thf(func_def_26, type, sK4: (sK2 > sK2 > $o)).
% 2.14/0.74 thf(func_def_27, type, sK5: sK2).
% 2.14/0.74 thf(f8,axiom,(
% 2.14/0.74 c_2Ebool_2ET),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH)).
% 2.14/0.74 thf(f12,axiom,(
% 2.14/0.74 ! [X0 : $o] : (((c_2Ebool_2ET & X0) <=> X0) & (X0 <=> (X0 & c_2Ebool_2ET)) & (c_2Ebool_2EF <=> (X0 & c_2Ebool_2EF)) & (c_2Ebool_2EF <=> (c_2Ebool_2EF & X0)) & (X0 <=> (X0 & X0)))),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EAND__CLAUSES)).
% 2.14/0.74 thf(f14,axiom,(
% 2.14/0.74 (c_2Ebool_2EF <=> (~ c_2Ebool_2ET)) & (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & ! [X0 : $o] : ((~ (~ X0)) <=> X0)),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ENOT__CLAUSES)).
% 2.14/0.74 thf(f17,axiom,(
% 2.14/0.74 ! [X1 : $tType,X0 : $tType,X4 : X1,X2 : (X0 > X1),X3 : tyop_2Eoption_2Eoption @ X0] : (! [X7 : X0] : (((c_2Eoption_2ETHE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X7))) = X7) & ! [X8 : X0] : (~ (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2ESOME @ X0 @ X8)))) & ! [X14 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X14 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ESOME @ X0)) = X14) & ! [X27 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2EOPTION__JOIN @ X0 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X0 @ X27))) = X27) & ! [X17 : tyop_2Eoption_2Eoption @ X0] : ((c_2Eoption_2EIS__SOME @ X0 @ X17) => (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ X17 @ X4 @ X2)) = ((X2 @ (c_2Eoption_2ETHE @ X0 @ X17))))) & ! [X9 : X0] : (~ (((c_2Eoption_2ESOME @ X0 @ X9)) = c_2Eoption_2ENONE @ X0)) & ! [X13 : tyop_2Eoption_2Eoption @ X0] : ((c_2Eoption_2EIS__SOME @ X0 @ X13) => (((c_2Eoption_2ESOME @ X0 @ (c_2Eoption_2ETHE @ X0 @ X13))) = X13)) & ! [X20 : (X0 > X1),X19 : X1] : (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ c_2Eoption_2ENONE @ X0 @ X19 @ X20)) = X19) & ! [X10 : X0] : (((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X10))) = c_2Ebool_2ET) & ! [X15 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X15 @ X15 @ c_2Eoption_2ESOME @ X0)) = X15) & (((c_2Eoption_2EOPTION__JOIN @ X0 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X0)) = c_2Eoption_2ENONE @ X0) & ! [X23 : (X0 > X1),X21 : X0,X22 : X1] : (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ (c_2Eoption_2ESOME @ X0 @ X21) @ X22 @ X23)) = ((X23 @ X21))) & ! [X25 : X0,X24 : (X0 > X1)] : (((c_2Eoption_2EOPTION__MAP @ X0 @ X1 @ X24 @ (c_2Eoption_2ESOME @ X0 @ X25))) = ((c_2Eoption_2ESOME @ X1 @ (X24 @ X25)))) & ! [X18 : tyop_2Eoption_2Eoption @ X0] : ((c_2Eoption_2EIS__SOME @ X0 @ X18) => (((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X18 @ X3 @ c_2Eoption_2ESOME @ X0)) = X18)) & ! [X11 : tyop_2Eoption_2Eoption @ X0] : ((X11 = c_2Eoption_2ENONE @ X0) <=> (c_2Eoption_2EIS__NONE @ X0 @ X11)) & ! [X26 : (X0 > X1)] : (((c_2Eoption_2EOPTION__MAP @ X0 @ X1 @ X26 @ c_2Eoption_2ENONE @ X0)) = c_2Eoption_2ENONE @ X1) & ! [X6 : X0,X5 : X0] : ((((c_2Eoption_2ESOME @ X0 @ X5)) = ((c_2Eoption_2ESOME @ X0 @ X6))) <=> (X5 = X6)) & ! [X16 : tyop_2Eoption_2Eoption @ X0] : ((c_2Eoption_2EIS__NONE @ X0 @ X16) => (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ X16 @ X4 @ X2)) = X4)) & (((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2EF) & ! [X12 : tyop_2Eoption_2Eoption @ X0] : ((X12 = c_2Eoption_2ENONE @ X0) <=> (~ (c_2Eoption_2EIS__SOME @ X0 @ X12))))),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2Eoption__CLAUSES)).
% 2.14/0.74 thf(f18,axiom,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X3 : tyop_2Eoption_2Eoption @ X0,X4 : tyop_2Eoption_2Eoption @ X1,X2 : (X0 > X1 > $o)] : ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X3 @ X4) <=> (((X4 = c_2Eoption_2ENONE @ X1) & (X3 = c_2Eoption_2ENONE @ X0)) | ? [X5 : X0,X6 : X1] : ((X4 = ((c_2Eoption_2ESOME @ X1 @ X6))) & (X3 = ((c_2Eoption_2ESOME @ X0 @ X5))) & (X2 @ X5 @ X6))))),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2EOPTREL__def)).
% 2.14/0.74 thf(f19,conjecture,(
% 2.14/0.74 ! [X0 : $tType,X1 : X0,X3 : (X0 > X0 > $o),X2 : X0] : ((((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ c_2Eoption_2ENONE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = c_2Ebool_2EF) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2ET) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ (c_2Eoption_2ESOME @ X0 @ X2) @ (c_2Eoption_2ESOME @ X0 @ X1))) = ((X3 @ X2 @ X1))) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ (c_2Eoption_2ESOME @ X0 @ X2) @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2EF))),
% 2.14/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Equotient__option_2EOPTION__REL__def)).
% 2.14/0.74 thf(f20,negated_conjecture,(
% 2.14/0.74 ~ ! [X0 : $tType,X1 : X0,X3 : (X0 > X0 > $o),X2 : X0] : ((((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ c_2Eoption_2ENONE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = c_2Ebool_2EF) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2ET) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ (c_2Eoption_2ESOME @ X0 @ X2) @ (c_2Eoption_2ESOME @ X0 @ X1))) = ((X3 @ X2 @ X1))) & (((c_2Eoption_2EOPTREL @ X0 @ X0 @ X3 @ (c_2Eoption_2ESOME @ X0 @ X2) @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2EF))),
% 2.14/0.74 inference(negated_conjecture,[status(cth)],[f19])).
% 2.14/0.74 thf(f27,plain,(
% 2.14/0.74 c_2Ebool_2ET),
% 2.14/0.74 inference(rectify,[],[f8])).
% 2.14/0.74 thf(f28,plain,(
% 2.14/0.74 (c_2Ebool_2ET = $true)),
% 2.14/0.74 inference(fool_elimination,[],[f27])).
% 2.14/0.74 thf(f31,plain,(
% 2.14/0.74 ! [X0 : $o] : (((c_2Ebool_2ET & X0) <=> X0) & (X0 <=> (X0 & c_2Ebool_2ET)) & (c_2Ebool_2EF <=> (X0 & c_2Ebool_2EF)) & (c_2Ebool_2EF <=> (c_2Ebool_2EF & X0)) & (X0 <=> (X0 & X0)))),
% 2.14/0.74 inference(rectify,[],[f12])).
% 2.14/0.74 thf(f32,plain,(
% 2.14/0.74 ! [X0 : $o] : ((($true = X0) <=> (($true = X0) & (c_2Ebool_2ET = $true))) & (((c_2Ebool_2EF = $true) & ($true = X0)) <=> (c_2Ebool_2EF = $true)) & ((($true = X0) & ($true = X0)) <=> ($true = X0)) & (($true = X0) <=> (($true = X0) & (c_2Ebool_2ET = $true))) & ((c_2Ebool_2EF = $true) <=> ((c_2Ebool_2EF = $true) & ($true = X0))))),
% 2.14/0.74 inference(fool_elimination,[],[f31])).
% 2.14/0.74 thf(f33,plain,(
% 2.14/0.74 (c_2Ebool_2EF <=> (~ c_2Ebool_2ET)) & (c_2Ebool_2ET <=> (~ c_2Ebool_2EF)) & ! [X0 : $o] : ((~ (~ X0)) <=> X0)),
% 2.14/0.74 inference(rectify,[],[f14])).
% 2.14/0.74 thf(f34,plain,(
% 2.14/0.74 ! [X0 : $o] : (((~ (~ X0))) = X0) & (c_2Ebool_2EF = ((~ c_2Ebool_2ET))) & (c_2Ebool_2ET = ((~ c_2Ebool_2EF)))),
% 2.14/0.74 inference(fool_elimination,[],[f33])).
% 2.14/0.74 thf(f39,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : tyop_2Eoption_2Eoption @ X0,X3 : tyop_2Eoption_2Eoption @ X1,X4 : (X0 > X1 > $o)] : ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3) <=> (((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X2)) | ? [X5 : X0,X6 : X1] : ((((c_2Eoption_2ESOME @ X1 @ X6)) = X3) & (((c_2Eoption_2ESOME @ X0 @ X5)) = X2) & (X4 @ X5 @ X6))))),
% 2.14/0.74 inference(rectify,[],[f18])).
% 2.14/0.74 thf(f40,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X4 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X2 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3)) = $true) <=> (? [X6 : X1,X5 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X6)) = X3) & (((c_2Eoption_2ESOME @ X0 @ X5)) = X2) & (((X4 @ X5 @ X6)) = $true)) | ((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X2))))),
% 2.14/0.74 inference(fool_elimination,[],[f39])).
% 2.14/0.74 thf(f43,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X3 : (X1 > X0),X4 : tyop_2Eoption_2Eoption @ X1] : (! [X5 : X1] : (((c_2Eoption_2ETHE @ X1 @ (c_2Eoption_2ESOME @ X1 @ X5))) = X5) & ! [X6 : X1] : (~ (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2ESOME @ X1 @ X6)))) & ! [X7 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X7 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ESOME @ X1)) = X7) & ! [X8 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2EOPTION__JOIN @ X1 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X1 @ X8))) = X8) & ! [X9 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2EIS__SOME @ X1 @ X9) => (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X9 @ X2 @ X3)) = ((X3 @ (c_2Eoption_2ETHE @ X1 @ X9))))) & ! [X10 : X1] : (~ (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2ESOME @ X1 @ X10)))) & ! [X11 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2EIS__SOME @ X1 @ X11) => (((c_2Eoption_2ESOME @ X1 @ (c_2Eoption_2ETHE @ X1 @ X11))) = X11)) & ! [X12 : (X1 > X0),X13 : X0] : (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ c_2Eoption_2ENONE @ X1 @ X13 @ X12)) = X13) & ! [X14 : X1] : (c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X1 @ (c_2Eoption_2ESOME @ X1 @ X14)))) & ! [X15 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X15 @ X15 @ c_2Eoption_2ESOME @ X1)) = X15) & (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2EOPTION__JOIN @ X1 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X1))) & ! [X16 : (X1 > X0),X17 : X1,X18 : X0] : (((X16 @ X17)) = ((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ (c_2Eoption_2ESOME @ X1 @ X17) @ X18 @ X16))) & ! [X19 : X1,X20 : (X1 > X0)] : (((c_2Eoption_2ESOME @ X0 @ (X20 @ X19))) = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X20 @ (c_2Eoption_2ESOME @ X1 @ X19)))) & ! [X21 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2EIS__SOME @ X1 @ X21) => (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X21 @ X4 @ c_2Eoption_2ESOME @ X1)) = X21)) & ! [X22 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2ENONE @ X1 = X22) <=> (c_2Eoption_2EIS__NONE @ X1 @ X22)) & ! [X23 : (X1 > X0)] : (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X23 @ c_2Eoption_2ENONE @ X1))) & ! [X24 : X1,X25 : X1] : ((((c_2Eoption_2ESOME @ X1 @ X25)) = ((c_2Eoption_2ESOME @ X1 @ X24))) <=> (X24 = X25)) & ! [X26 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2EIS__NONE @ X1 @ X26) => (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X26 @ X2 @ X3)) = X2)) & (c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X1 @ c_2Eoption_2ENONE @ X1))) & ! [X27 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2ENONE @ X1 = X27) <=> (~ (c_2Eoption_2EIS__SOME @ X1 @ X27))))),
% 2.14/0.74 inference(rectify,[],[f17])).
% 2.14/0.74 thf(f44,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : X0,X4 : tyop_2Eoption_2Eoption @ X1,X3 : (X1 > X0)] : (! [X11 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__SOME @ X1 @ X11)) = $true) => (((c_2Eoption_2ESOME @ X1 @ (c_2Eoption_2ETHE @ X1 @ X11))) = X11)) & ! [X23 : (X1 > X0)] : (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X23 @ c_2Eoption_2ENONE @ X1))) & ! [X22 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__NONE @ X1 @ X22)) = $true) <=> (c_2Eoption_2ENONE @ X1 = X22)) & ! [X19 : X1,X20 : (X1 > X0)] : (((c_2Eoption_2ESOME @ X0 @ (X20 @ X19))) = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X20 @ (c_2Eoption_2ESOME @ X1 @ X19)))) & (c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X1 @ c_2Eoption_2ENONE @ X1))) & ! [X12 : (X1 > X0),X13 : X0] : (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ c_2Eoption_2ENONE @ X1 @ X13 @ X12)) = X13) & ! [X26 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__NONE @ X1 @ X26)) = $true) => (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X26 @ X2 @ X3)) = X2)) & ! [X8 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2EOPTION__JOIN @ X1 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X1 @ X8))) = X8) & (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2EOPTION__JOIN @ X1 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X1))) & ! [X17 : X1,X16 : (X1 > X0),X18 : X0] : (((X16 @ X17)) = ((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ (c_2Eoption_2ESOME @ X1 @ X17) @ X18 @ X16))) & ! [X24 : X1,X25 : X1] : ((((c_2Eoption_2ESOME @ X1 @ X25)) = ((c_2Eoption_2ESOME @ X1 @ X24))) <=> (X24 = X25)) & ! [X27 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2ENONE @ X1 = X27) <=> ($true = ((~ (c_2Eoption_2EIS__SOME @ X1 @ X27))))) & ! [X7 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X7 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ESOME @ X1)) = X7) & ! [X9 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__SOME @ X1 @ X9)) = $true) => (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X9 @ X2 @ X3)) = ((X3 @ (c_2Eoption_2ETHE @ X1 @ X9))))) & ! [X5 : X1] : (((c_2Eoption_2ETHE @ X1 @ (c_2Eoption_2ESOME @ X1 @ X5))) = X5) & ! [X15 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X15 @ X15 @ c_2Eoption_2ESOME @ X1)) = X15) & ! [X6 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X6)))) = $true) & ! [X21 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__SOME @ X1 @ X21)) = $true) => (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X21 @ X4 @ c_2Eoption_2ESOME @ X1)) = X21)) & ! [X10 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X10)))) = $true) & ! [X14 : X1] : (c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X1 @ (c_2Eoption_2ESOME @ X1 @ X14)))))),
% 2.14/0.74 inference(fool_elimination,[],[f43])).
% 2.14/0.74 thf(f57,plain,(
% 2.14/0.74 ~ ! [X0 : $tType,X2 : (X0 > X0 > $o),X1 : X0,X3 : X0] : ((c_2Ebool_2ET = ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X0))) & (c_2Ebool_2EF = ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1)))) & (c_2Ebool_2EF = ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X3) @ c_2Eoption_2ENONE @ X0))) & (((X2 @ X3 @ X1)) = ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X3) @ (c_2Eoption_2ESOME @ X0 @ X1)))))),
% 2.14/0.74 inference(rectify,[],[f20])).
% 2.14/0.74 thf(f60,plain,(
% 2.14/0.74 ? [X0 : $tType,X3 : X0,X2 : (X0 > X0 > $o),X1 : X0] : ((c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1)))) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X3) @ c_2Eoption_2ENONE @ X0))) | (c_2Ebool_2ET != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X0))) | (((X2 @ X3 @ X1)) != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X3) @ (c_2Eoption_2ESOME @ X0 @ X1)))))),
% 2.14/0.74 inference(ennf_transformation,[],[f57])).
% 2.14/0.74 thf(f61,plain,(
% 2.14/0.74 ! [X1 : $tType,X0 : $tType,X4 : tyop_2Eoption_2Eoption @ X1,X3 : (X1 > X0),X2 : X0] : (! [X14 : X1] : (c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X1 @ (c_2Eoption_2ESOME @ X1 @ X14)))) & ! [X9 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__SOME @ X1 @ X9)) != $true) | (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X9 @ X2 @ X3)) = ((X3 @ (c_2Eoption_2ETHE @ X1 @ X9))))) & ! [X19 : X1,X20 : (X1 > X0)] : (((c_2Eoption_2ESOME @ X0 @ (X20 @ X19))) = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X20 @ (c_2Eoption_2ESOME @ X1 @ X19)))) & ! [X5 : X1] : (((c_2Eoption_2ETHE @ X1 @ (c_2Eoption_2ESOME @ X1 @ X5))) = X5) & ! [X11 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2ESOME @ X1 @ (c_2Eoption_2ETHE @ X1 @ X11))) = X11) | (((c_2Eoption_2EIS__SOME @ X1 @ X11)) != $true)) & ! [X6 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X6)))) = $true) & ! [X23 : (X1 > X0)] : (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X23 @ c_2Eoption_2ENONE @ X1))) & (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2EOPTION__JOIN @ X1 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X1))) & ! [X15 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X15 @ X15 @ c_2Eoption_2ESOME @ X1)) = X15) & ! [X24 : X1,X25 : X1] : ((((c_2Eoption_2ESOME @ X1 @ X25)) = ((c_2Eoption_2ESOME @ X1 @ X24))) <=> (X24 = X25)) & ! [X7 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X7 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ESOME @ X1)) = X7) & ! [X22 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__NONE @ X1 @ X22)) = $true) <=> (c_2Eoption_2ENONE @ X1 = X22)) & ! [X21 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X21 @ X4 @ c_2Eoption_2ESOME @ X1)) = X21) | (((c_2Eoption_2EIS__SOME @ X1 @ X21)) != $true)) & (c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X1 @ c_2Eoption_2ENONE @ X1))) & ! [X26 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__NONE @ X1 @ X26)) != $true) | (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X26 @ X2 @ X3)) = X2)) & ! [X17 : X1,X16 : (X1 > X0),X18 : X0] : (((X16 @ X17)) = ((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ (c_2Eoption_2ESOME @ X1 @ X17) @ X18 @ X16))) & ! [X8 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2EOPTION__JOIN @ X1 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X1 @ X8))) = X8) & ! [X10 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X10)))) = $true) & ! [X12 : (X1 > X0),X13 : X0] : (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ c_2Eoption_2ENONE @ X1 @ X13 @ X12)) = X13) & ! [X27 : tyop_2Eoption_2Eoption @ X1] : ((c_2Eoption_2ENONE @ X1 = X27) <=> ($true = ((~ (c_2Eoption_2EIS__SOME @ X1 @ X27))))))),
% 2.14/0.74 inference(ennf_transformation,[],[f44])).
% 2.14/0.74 thf(f64,plain,(
% 2.14/0.74 ! [X0 : $o] : (((($true = X0) | (($true != X0) | (c_2Ebool_2ET != $true))) & ((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0))) & ((((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | ((c_2Ebool_2EF != $true) | ($true != X0)))) & (((($true = X0) & ($true = X0)) | ($true != X0)) & (($true = X0) | (($true != X0) | ($true != X0)))) & ((($true = X0) | (($true != X0) | (c_2Ebool_2ET != $true))) & ((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0))) & (((c_2Ebool_2EF = $true) | ((c_2Ebool_2EF != $true) | ($true != X0))) & (((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true))))),
% 2.14/0.74 inference(nnf_transformation,[],[f32])).
% 2.14/0.74 thf(f65,plain,(
% 2.14/0.74 ! [X0 : $o] : ((($true = X0) | ($true != X0) | (c_2Ebool_2ET != $true)) & ((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0)) & (((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | (c_2Ebool_2EF != $true) | ($true != X0)) & ((($true = X0) & ($true = X0)) | ($true != X0)) & (($true = X0) | ($true != X0) | ($true != X0)) & (($true = X0) | ($true != X0) | (c_2Ebool_2ET != $true)) & ((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0)) & ((c_2Ebool_2EF = $true) | (c_2Ebool_2EF != $true) | ($true != X0)) & (((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true)))),
% 2.14/0.74 inference(flattening,[],[f64])).
% 2.14/0.74 thf(f66,plain,(
% 2.14/0.74 ! [X1 : $tType,X0 : $tType,X4 : tyop_2Eoption_2Eoption @ X1,X3 : (X1 > X0),X2 : X0] : (! [X14 : X1] : (c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X1 @ (c_2Eoption_2ESOME @ X1 @ X14)))) & ! [X9 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__SOME @ X1 @ X9)) != $true) | (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X9 @ X2 @ X3)) = ((X3 @ (c_2Eoption_2ETHE @ X1 @ X9))))) & ! [X19 : X1,X20 : (X1 > X0)] : (((c_2Eoption_2ESOME @ X0 @ (X20 @ X19))) = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X20 @ (c_2Eoption_2ESOME @ X1 @ X19)))) & ! [X5 : X1] : (((c_2Eoption_2ETHE @ X1 @ (c_2Eoption_2ESOME @ X1 @ X5))) = X5) & ! [X11 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2ESOME @ X1 @ (c_2Eoption_2ETHE @ X1 @ X11))) = X11) | (((c_2Eoption_2EIS__SOME @ X1 @ X11)) != $true)) & ! [X6 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X6)))) = $true) & ! [X23 : (X1 > X0)] : (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2EOPTION__MAP @ X1 @ X0 @ X23 @ c_2Eoption_2ENONE @ X1))) & (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2EOPTION__JOIN @ X1 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X1))) & ! [X15 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X15 @ X15 @ c_2Eoption_2ESOME @ X1)) = X15) & ! [X24 : X1,X25 : X1] : (((((c_2Eoption_2ESOME @ X1 @ X25)) = ((c_2Eoption_2ESOME @ X1 @ X24))) | (X24 != X25)) & ((X24 = X25) | (((c_2Eoption_2ESOME @ X1 @ X25)) != ((c_2Eoption_2ESOME @ X1 @ X24))))) & ! [X7 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X7 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ESOME @ X1)) = X7) & ! [X22 : tyop_2Eoption_2Eoption @ X1] : (((((c_2Eoption_2EIS__NONE @ X1 @ X22)) = $true) | (c_2Eoption_2ENONE @ X1 != X22)) & ((c_2Eoption_2ENONE @ X1 = X22) | (((c_2Eoption_2EIS__NONE @ X1 @ X22)) != $true))) & ! [X21 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2Eoption__CASE @ X1 @ tyop_2Eoption_2Eoption @ X1 @ X21 @ X4 @ c_2Eoption_2ESOME @ X1)) = X21) | (((c_2Eoption_2EIS__SOME @ X1 @ X21)) != $true)) & (c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X1 @ c_2Eoption_2ENONE @ X1))) & ! [X26 : tyop_2Eoption_2Eoption @ X1] : ((((c_2Eoption_2EIS__NONE @ X1 @ X26)) != $true) | (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ X26 @ X2 @ X3)) = X2)) & ! [X17 : X1,X16 : (X1 > X0),X18 : X0] : (((X16 @ X17)) = ((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ (c_2Eoption_2ESOME @ X1 @ X17) @ X18 @ X16))) & ! [X8 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2EOPTION__JOIN @ X1 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X1 @ X8))) = X8) & ! [X10 : X1] : (((~ (c_2Eoption_2ENONE @ X1 = (c_2Eoption_2ESOME @ X1 @ X10)))) = $true) & ! [X12 : (X1 > X0),X13 : X0] : (((c_2Eoption_2Eoption__CASE @ X1 @ X0 @ c_2Eoption_2ENONE @ X1 @ X13 @ X12)) = X13) & ! [X27 : tyop_2Eoption_2Eoption @ X1] : (((c_2Eoption_2ENONE @ X1 = X27) | ($true != ((~ (c_2Eoption_2EIS__SOME @ X1 @ X27))))) & (($true = ((~ (c_2Eoption_2EIS__SOME @ X1 @ X27)))) | (c_2Eoption_2ENONE @ X1 != X27))))),
% 2.14/0.74 inference(nnf_transformation,[],[f61])).
% 2.14/0.74 thf(f67,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : tyop_2Eoption_2Eoption @ X0,X3 : (X0 > X1),X4 : X1] : (! [X5 : X0] : (c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X5)))) & ! [X6 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2EIS__SOME @ X0 @ X6)) != $true) | (((X3 @ (c_2Eoption_2ETHE @ X0 @ X6))) = ((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ X6 @ X4 @ X3)))) & ! [X7 : X0,X8 : (X0 > X1)] : (((c_2Eoption_2ESOME @ X1 @ (X8 @ X7))) = ((c_2Eoption_2EOPTION__MAP @ X0 @ X1 @ X8 @ (c_2Eoption_2ESOME @ X0 @ X7)))) & ! [X9 : X0] : (((c_2Eoption_2ETHE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X9))) = X9) & ! [X10 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2ESOME @ X0 @ (c_2Eoption_2ETHE @ X0 @ X10))) = X10) | ($true != ((c_2Eoption_2EIS__SOME @ X0 @ X10)))) & ! [X11 : X0] : (((~ (c_2Eoption_2ENONE @ X0 = (c_2Eoption_2ESOME @ X0 @ X11)))) = $true) & ! [X12 : (X0 > X1)] : (c_2Eoption_2ENONE @ X1 = ((c_2Eoption_2EOPTION__MAP @ X0 @ X1 @ X12 @ c_2Eoption_2ENONE @ X0))) & (c_2Eoption_2ENONE @ X0 = ((c_2Eoption_2EOPTION__JOIN @ X0 @ c_2Eoption_2ENONE @ tyop_2Eoption_2Eoption @ X0))) & ! [X13 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X13 @ X13 @ c_2Eoption_2ESOME @ X0)) = X13) & ! [X14 : X0,X15 : X0] : (((((c_2Eoption_2ESOME @ X0 @ X15)) = ((c_2Eoption_2ESOME @ X0 @ X14))) | (X14 != X15)) & ((X14 = X15) | (((c_2Eoption_2ESOME @ X0 @ X15)) != ((c_2Eoption_2ESOME @ X0 @ X14))))) & ! [X16 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X16 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ESOME @ X0)) = X16) & ! [X17 : tyop_2Eoption_2Eoption @ X0] : (((((c_2Eoption_2EIS__NONE @ X0 @ X17)) = $true) | (c_2Eoption_2ENONE @ X0 != X17)) & ((c_2Eoption_2ENONE @ X0 = X17) | (((c_2Eoption_2EIS__NONE @ X0 @ X17)) != $true))) & ! [X18 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2Eoption__CASE @ X0 @ tyop_2Eoption_2Eoption @ X0 @ X18 @ X2 @ c_2Eoption_2ESOME @ X0)) = X18) | (((c_2Eoption_2EIS__SOME @ X0 @ X18)) != $true)) & (c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0))) & ! [X19 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2EIS__NONE @ X0 @ X19)) != $true) | (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ X19 @ X4 @ X3)) = X4)) & ! [X20 : X0,X21 : (X0 > X1),X22 : X1] : (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ (c_2Eoption_2ESOME @ X0 @ X20) @ X22 @ X21)) = ((X21 @ X20))) & ! [X23 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2EOPTION__JOIN @ X0 @ (c_2Eoption_2ESOME @ tyop_2Eoption_2Eoption @ X0 @ X23))) = X23) & ! [X24 : X0] : (((~ (c_2Eoption_2ENONE @ X0 = (c_2Eoption_2ESOME @ X0 @ X24)))) = $true) & ! [X25 : (X0 > X1),X26 : X1] : (((c_2Eoption_2Eoption__CASE @ X0 @ X1 @ c_2Eoption_2ENONE @ X0 @ X26 @ X25)) = X26) & ! [X27 : tyop_2Eoption_2Eoption @ X0] : (((c_2Eoption_2ENONE @ X0 = X27) | ($true != ((~ (c_2Eoption_2EIS__SOME @ X0 @ X27))))) & (($true = ((~ (c_2Eoption_2EIS__SOME @ X0 @ X27)))) | (c_2Eoption_2ENONE @ X0 != X27))))),
% 2.14/0.74 inference(rectify,[],[f66])).
% 2.14/0.74 thf(f69,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X4 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X2 : tyop_2Eoption_2Eoption @ X0] : (((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3)) = $true) | (! [X6 : X1,X5 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X6)) != X3) | (((c_2Eoption_2ESOME @ X0 @ X5)) != X2) | (((X4 @ X5 @ X6)) != $true)) & ((c_2Eoption_2ENONE @ X1 != X3) | (c_2Eoption_2ENONE @ X0 != X2)))) & ((? [X6 : X1,X5 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X6)) = X3) & (((c_2Eoption_2ESOME @ X0 @ X5)) = X2) & (((X4 @ X5 @ X6)) = $true)) | ((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X2))) | (((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3)) != $true)))),
% 2.14/0.74 inference(nnf_transformation,[],[f40])).
% 2.14/0.74 thf(f70,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X4 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X2 : tyop_2Eoption_2Eoption @ X0] : (((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3)) = $true) | (! [X6 : X1,X5 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X6)) != X3) | (((c_2Eoption_2ESOME @ X0 @ X5)) != X2) | (((X4 @ X5 @ X6)) != $true)) & ((c_2Eoption_2ENONE @ X1 != X3) | (c_2Eoption_2ENONE @ X0 != X2)))) & (? [X6 : X1,X5 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X6)) = X3) & (((c_2Eoption_2ESOME @ X0 @ X5)) = X2) & (((X4 @ X5 @ X6)) = $true)) | ((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X2)) | (((c_2Eoption_2EOPTREL @ X0 @ X1 @ X4 @ X2 @ X3)) != $true)))),
% 2.14/0.74 inference(flattening,[],[f69])).
% 2.14/0.74 thf(f71,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : ((($true = ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (! [X5 : X1,X6 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X5)) != X3) | (((c_2Eoption_2ESOME @ X0 @ X6)) != X4) | (((X2 @ X6 @ X5)) != $true)) & ((c_2Eoption_2ENONE @ X1 != X3) | (c_2Eoption_2ENONE @ X0 != X4)))) & (? [X7 : X1,X8 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X7)) = X3) & (((c_2Eoption_2ESOME @ X0 @ X8)) = X4) & (((X2 @ X8 @ X7)) = $true)) | ((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X4)) | ($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3)))))),
% 2.14/0.74 inference(rectify,[],[f70])).
% 2.14/0.74 thf(f72,plain,(
% 2.14/0.74 ! [X0 : $tType,X1 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : ((($true = ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (! [X5 : X1,X6 : X0] : ((((c_2Eoption_2ESOME @ X1 @ X5)) != X3) | (((c_2Eoption_2ESOME @ X0 @ X6)) != X4) | (((X2 @ X6 @ X5)) != $true)) & ((c_2Eoption_2ENONE @ X1 != X3) | (c_2Eoption_2ENONE @ X0 != X4)))) & (((((c_2Eoption_2ESOME @ X1 @ (sK0 @ X0 @ X1 @ X4 @ X3 @ X2))) = X3) & (((c_2Eoption_2ESOME @ X0 @ (sK1 @ X0 @ X1 @ X4 @ X3 @ X2))) = X4) & (((X2 @ (sK1 @ X0 @ X1 @ X4 @ X3 @ X2) @ (sK0 @ X0 @ X1 @ X4 @ X3 @ X2))) = $true)) | ((c_2Eoption_2ENONE @ X1 = X3) & (c_2Eoption_2ENONE @ X0 = X4)) | ($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3)))))),
% 2.14/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X8,sK1 @ X0 @ X1 @ X4 @ X3 @ X2),skolemize(X8,sK1 @ X0 @ X1 @ X4 @ X3 @ X2)],[f71])).
% 2.14/0.74 thf(f77,plain,(
% 2.14/0.74 ? [X0 : $tType,X1 : X0,X2 : (X0 > X0 > $o),X3 : X0] : ((c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X3)))) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X1) @ c_2Eoption_2ENONE @ X0))) | (c_2Ebool_2ET != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X0))) | (((X2 @ X1 @ X3)) != ((c_2Eoption_2EOPTREL @ X0 @ X0 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X1) @ (c_2Eoption_2ESOME @ X0 @ X3)))))),
% 2.14/0.74 inference(rectify,[],[f60])).
% 2.14/0.74 thf(f78,plain,(
% 2.14/0.74 (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | (c_2Ebool_2ET != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) != ((sK4 @ sK3 @ sK5)))),
% 2.14/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5)],[f77])).
% 2.14/0.74 thf(f80,plain,(
% 2.14/0.74 (c_2Ebool_2EF = ((~ c_2Ebool_2ET)))),
% 2.14/0.74 inference(cnf_transformation,[],[f34])).
% 2.14/0.74 thf(f92,plain,(
% 2.14/0.74 ( ! [X0 : $o] : ((c_2Ebool_2EF != $true) | ($true = X0)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f65])).
% 2.14/0.74 thf(f104,plain,(
% 2.14/0.74 ( ! [X0 : $tType] : ((c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)))) )),
% 2.14/0.74 inference(cnf_transformation,[],[f67])).
% 2.14/0.74 thf(f116,plain,(
% 2.14/0.74 ( ! [X0 : $tType,X9 : X0] : ((((c_2Eoption_2ETHE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X9))) = X9)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f67])).
% 2.14/0.74 thf(f119,plain,(
% 2.14/0.74 ( ! [X0 : $tType,X5 : X0] : ((c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X5))))) )),
% 2.14/0.74 inference(cnf_transformation,[],[f67])).
% 2.14/0.74 thf(f122,plain,(
% 2.14/0.74 (c_2Ebool_2ET = $true)),
% 2.14/0.74 inference(cnf_transformation,[],[f28])).
% 2.14/0.74 thf(f125,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : (($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (((X2 @ (sK1 @ X0 @ X1 @ X4 @ X3 @ X2) @ (sK0 @ X0 @ X1 @ X4 @ X3 @ X2))) = $true) | (c_2Eoption_2ENONE @ X1 = X3)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f127,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : (($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (((c_2Eoption_2ESOME @ X0 @ (sK1 @ X0 @ X1 @ X4 @ X3 @ X2))) = X4) | (c_2Eoption_2ENONE @ X1 = X3)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f128,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : (($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (((c_2Eoption_2ESOME @ X1 @ (sK0 @ X0 @ X1 @ X4 @ X3 @ X2))) = X3) | (c_2Eoption_2ENONE @ X0 = X4)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f129,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : (($true != ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (((c_2Eoption_2ESOME @ X1 @ (sK0 @ X0 @ X1 @ X4 @ X3 @ X2))) = X3) | (c_2Eoption_2ENONE @ X1 = X3)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f130,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X4 : tyop_2Eoption_2Eoption @ X0] : (($true = ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (c_2Eoption_2ENONE @ X1 != X3) | (c_2Eoption_2ENONE @ X0 != X4)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f131,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X3 : tyop_2Eoption_2Eoption @ X1,X6 : X0,X4 : tyop_2Eoption_2Eoption @ X0,X5 : X1] : (($true = ((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ X3))) | (((c_2Eoption_2ESOME @ X1 @ X5)) != X3) | (((c_2Eoption_2ESOME @ X0 @ X6)) != X4) | (((X2 @ X6 @ X5)) != $true)) )),
% 2.14/0.74 inference(cnf_transformation,[],[f72])).
% 2.14/0.74 thf(f160,plain,(
% 2.14/0.74 (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | (c_2Ebool_2ET != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) != ((sK4 @ sK3 @ sK5)))),
% 2.14/0.74 inference(cnf_transformation,[],[f78])).
% 2.14/0.74 thf(f162,plain,(
% 2.14/0.74 (c_2Ebool_2EF = ((~ $true)))),
% 2.14/0.74 inference(definition_unfolding,[],[f80,f122])).
% 2.14/0.74 thf(f168,plain,(
% 2.14/0.74 ( ! [X0 : $tType,X5 : X0] : ((((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X5))) = $true)) )),
% 2.14/0.74 inference(definition_unfolding,[],[f119,f122])).
% 2.14/0.74 thf(f181,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) != ((sK4 @ sK3 @ sK5)))),
% 2.14/0.74 inference(definition_unfolding,[],[f160,f122])).
% 2.14/0.74 thf(f196,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X6 : X0,X4 : tyop_2Eoption_2Eoption @ X0,X5 : X1] : ((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ (c_2Eoption_2ESOME @ X1 @ X5))) = $true) | (((c_2Eoption_2ESOME @ X0 @ X6)) != X4) | (((X2 @ X6 @ X5)) != $true)) )),
% 2.14/0.74 inference(equality_resolution,[],[f131])).
% 2.14/0.74 thf(f197,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X6 : X0,X5 : X1] : ((((X2 @ X6 @ X5)) != $true) | (((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ (c_2Eoption_2ESOME @ X0 @ X6) @ (c_2Eoption_2ESOME @ X1 @ X5))) = $true)) )),
% 2.14/0.74 inference(equality_resolution,[],[f196])).
% 2.14/0.74 thf(f198,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o),X4 : tyop_2Eoption_2Eoption @ X0] : ((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ X4 @ c_2Eoption_2ENONE @ X1)) = $true) | (c_2Eoption_2ENONE @ X0 != X4)) )),
% 2.14/0.74 inference(equality_resolution,[],[f130])).
% 2.14/0.74 thf(f199,plain,(
% 2.14/0.74 ( ! [X1 : $tType,X0 : $tType,X2 : (X0 > X1 > $o)] : ((((c_2Eoption_2EOPTREL @ X0 @ X1 @ X2 @ c_2Eoption_2ENONE @ X0 @ c_2Eoption_2ENONE @ X1)) = $true)) )),
% 2.14/0.74 inference(equality_resolution,[],[f198])).
% 2.14/0.74 thf(f219,plain,(
% 2.14/0.74 (c_2Ebool_2EF = $false)),
% 2.14/0.74 inference(boolean_simplification,[],[f162])).
% 2.14/0.74 thf(f222,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) != ((sK4 @ sK3 @ sK5))) | (c_2Ebool_2EF = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true)),
% 2.14/0.74 inference(xor_proxy_clausification,[],[f181])).
% 2.14/0.74 thf(f232,plain,(
% 2.14/0.74 (((sK4 @ sK3 @ sK5)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (c_2Ebool_2EF = $true) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true)),
% 2.14/0.74 inference(xor_proxy_clausification,[],[f222])).
% 2.14/0.74 thf(f233,plain,(
% 2.14/0.74 (c_2Ebool_2EF = $true) | (c_2Ebool_2EF != ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2))) | ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | ($false = ((sK4 @ sK3 @ sK5))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true)),
% 2.14/0.74 inference(xor_proxy_clausification,[],[f222])).
% 2.14/0.74 thf(f234,plain,(
% 2.14/0.74 (c_2Ebool_2EF = $true) | (c_2Ebool_2EF = $true) | ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ($false = ((sK4 @ sK3 @ sK5))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true)),
% 2.14/0.74 inference(xor_proxy_clausification,[],[f233])).
% 2.14/0.74 thf(f236,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ($false = ((sK4 @ sK3 @ sK5))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (c_2Ebool_2EF = $true) | ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))))),
% 2.14/0.74 inference(duplicate_literal_removal,[],[f234])).
% 2.14/0.74 thf(f237,plain,(
% 2.14/0.74 (c_2Ebool_2EF = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((sK4 @ sK3 @ sK5)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (c_2Ebool_2EF = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true)),
% 2.14/0.74 inference(xor_proxy_clausification,[],[f232])).
% 2.14/0.74 thf(f239,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (((sK4 @ sK3 @ sK5)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (c_2Ebool_2EF = $true)),
% 2.14/0.74 inference(duplicate_literal_removal,[],[f237])).
% 2.14/0.74 thf(f240,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ($false = ((sK4 @ sK3 @ sK5))) | (c_2Ebool_2EF = $true) | ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))))),
% 2.14/0.74 inference(forward_subsumption_resolution,[],[f236,f199])).
% 2.14/0.74 thf(f241,plain,(
% 2.14/0.74 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ c_2Eoption_2ENONE @ sK2)) != $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (c_2Ebool_2EF = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f239,f197])).
% 2.14/0.75 thf(f242,plain,(
% 2.14/0.75 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | ($false = ((sK4 @ sK3 @ sK5))) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f240,f92])).
% 2.14/0.75 thf(f243,plain,(
% 2.14/0.75 (c_2Ebool_2EF = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f241,f199])).
% 2.14/0.75 thf(f245,definition,(
% 2.14/0.75 spl6_1 <=> ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))))),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 2.14/0.75 thf(f247,plain,(
% 2.14/0.75 ($false = ((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | ~spl6_1),
% 2.14/0.75 inference(avatar_component_clause,[],[f245])).
% 2.14/0.75 thf(f249,definition,(
% 2.14/0.75 spl6_2 <=> ($false = ((sK4 @ sK3 @ sK5)))),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 2.14/0.75 thf(f251,plain,(
% 2.14/0.75 ($false = ((sK4 @ sK3 @ sK5))) | ~spl6_2),
% 2.14/0.75 inference(avatar_component_clause,[],[f249])).
% 2.14/0.75 thf(f253,definition,(
% 2.14/0.75 spl6_3 <=> (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true)),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 2.14/0.75 thf(f255,plain,(
% 2.14/0.75 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true) | ~spl6_3),
% 2.14/0.75 inference(avatar_component_clause,[],[f253])).
% 2.14/0.75 thf(f257,definition,(
% 2.14/0.75 spl6_4 <=> (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true)),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition])).
% 2.14/0.75 thf(f259,plain,(
% 2.14/0.75 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ~spl6_4),
% 2.14/0.75 inference(avatar_component_clause,[],[f257])).
% 2.14/0.75 thf(f260,plain,(
% 2.14/0.75 spl6_1 | spl6_2 | spl6_3 | spl6_4),
% 2.14/0.75 inference(avatar_split_clause,[],[f242,f257,f253,f249,f245])).
% 2.14/0.75 thf(f261,plain,(
% 2.14/0.75 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2)) = $true)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f243,f92])).
% 2.14/0.75 thf(f263,definition,(
% 2.14/0.75 spl6_5 <=> (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true)),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition])).
% 2.14/0.75 thf(f265,plain,(
% 2.14/0.75 (((c_2Eoption_2EOPTREL @ sK2 @ sK2 @ sK4 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5))) = $true) | ~spl6_5),
% 2.14/0.75 inference(avatar_component_clause,[],[f263])).
% 2.14/0.75 thf(f266,plain,(
% 2.14/0.75 spl6_5 | spl6_3 | spl6_4),
% 2.14/0.75 inference(avatar_split_clause,[],[f261,f257,f253,f263])).
% 2.14/0.75 thf(f284,definition,(
% 2.14/0.75 spl6_7 <=> (((c_2Eoption_2ESOME @ sK2 @ sK3)) = c_2Eoption_2ENONE @ sK2)),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_7])],[avatar_definition])).
% 2.14/0.75 thf(f285,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK3)) != c_2Eoption_2ENONE @ sK2) | spl6_7),
% 2.14/0.75 inference(avatar_component_clause,[],[f284])).
% 2.14/0.75 thf(f286,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK3)) = c_2Eoption_2ENONE @ sK2) | ~spl6_7),
% 2.14/0.75 inference(avatar_component_clause,[],[f284])).
% 2.14/0.75 thf(f289,definition,(
% 2.14/0.75 spl6_8 <=> (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2 @ sK4))))),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_8])],[avatar_definition])).
% 2.14/0.75 thf(f291,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2 @ sK4)))) | ~spl6_8),
% 2.14/0.75 inference(avatar_component_clause,[],[f289])).
% 2.14/0.75 thf(f326,plain,(
% 2.14/0.75 (((c_2Eoption_2EIS__SOME @ sK2 @ c_2Eoption_2ENONE @ sK2)) = $true) | ~spl6_7),
% 2.14/0.75 inference(constrained_superposition,[],[f168,f286])).
% 2.14/0.75 thf(f335,plain,(
% 2.14/0.75 (c_2Ebool_2EF = $true) | ~spl6_7),
% 2.14/0.75 inference(forward_demodulation,[],[f326,f104])).
% 2.14/0.75 thf(f338,plain,(
% 2.14/0.75 ($false = $true) | ~spl6_7),
% 2.14/0.75 inference(forward_demodulation,[],[f335,f219])).
% 2.14/0.75 thf(f339,plain,(
% 2.14/0.75 $false | ~spl6_7),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f338])).
% 2.14/0.75 thf(f340,plain,(
% 2.14/0.75 ~spl6_7),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f339])).
% 2.14/0.75 thf(f345,plain,(
% 2.14/0.75 ($true != $true) | (((c_2Eoption_2ESOME @ sK2 @ sK3)) = c_2Eoption_2ENONE @ sK2) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2 @ sK4)))) | ~spl6_3),
% 2.14/0.75 inference(constrained_superposition,[],[f128,f255])).
% 2.14/0.75 thf(f352,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2 @ sK4)))) | (((c_2Eoption_2ESOME @ sK2 @ sK3)) = c_2Eoption_2ENONE @ sK2) | ~spl6_3),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f345])).
% 2.14/0.75 thf(f355,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ c_2Eoption_2ENONE @ sK2 @ sK4)))) | (~spl6_3 | spl6_7)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f352,f285])).
% 2.14/0.75 thf(f358,plain,(
% 2.14/0.75 spl6_8 | ~spl6_3 | spl6_7),
% 2.14/0.75 inference(avatar_split_clause,[],[f355,f284,f253,f289])).
% 2.14/0.75 thf(f376,definition,(
% 2.14/0.75 spl6_13 <=> (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5)))),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_13])],[avatar_definition])).
% 2.14/0.75 thf(f377,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2ESOME @ sK2 @ sK5))) | spl6_13),
% 2.14/0.75 inference(avatar_component_clause,[],[f376])).
% 2.14/0.75 thf(f378,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_13),
% 2.14/0.75 inference(avatar_component_clause,[],[f376])).
% 2.14/0.75 thf(f381,definition,(
% 2.14/0.75 spl6_14 <=> (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))))),
% 2.14/0.75 introduced(definition,[new_symbols(definition,[spl6_14])],[avatar_definition])).
% 2.14/0.75 thf(f383,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | ~spl6_14),
% 2.14/0.75 inference(avatar_component_clause,[],[f381])).
% 2.14/0.75 thf(f398,plain,(
% 2.14/0.75 (((c_2Eoption_2EIS__SOME @ sK2 @ c_2Eoption_2ENONE @ sK2)) = $true) | ~spl6_13),
% 2.14/0.75 inference(constrained_superposition,[],[f168,f378])).
% 2.14/0.75 thf(f408,plain,(
% 2.14/0.75 (c_2Ebool_2EF = $true) | ~spl6_13),
% 2.14/0.75 inference(forward_demodulation,[],[f398,f104])).
% 2.14/0.75 thf(f410,plain,(
% 2.14/0.75 ($false = $true) | ~spl6_13),
% 2.14/0.75 inference(forward_demodulation,[],[f408,f219])).
% 2.14/0.75 thf(f411,plain,(
% 2.14/0.75 $false | ~spl6_13),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f410])).
% 2.14/0.75 thf(f412,plain,(
% 2.14/0.75 ~spl6_13),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f411])).
% 2.14/0.75 thf(f580,plain,(
% 2.14/0.75 ($true != $true) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_4),
% 2.14/0.75 inference(constrained_superposition,[],[f127,f259])).
% 2.14/0.75 thf(f588,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | ~spl6_4),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f580])).
% 2.14/0.75 thf(f591,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ c_2Eoption_2ENONE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (~spl6_4 | spl6_13)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f588,f377])).
% 2.14/0.75 thf(f594,plain,(
% 2.14/0.75 spl6_14 | ~spl6_4 | spl6_13),
% 2.14/0.75 inference(avatar_split_clause,[],[f591,f376,f257,f381])).
% 2.14/0.75 thf(f603,plain,(
% 2.14/0.75 (((c_2Eoption_2EIS__SOME @ sK2 @ c_2Eoption_2ENONE @ sK2)) = $true) | ~spl6_8),
% 2.14/0.75 inference(constrained_superposition,[],[f168,f291])).
% 2.14/0.75 thf(f614,plain,(
% 2.14/0.75 (c_2Ebool_2EF = $true) | ~spl6_8),
% 2.14/0.75 inference(forward_demodulation,[],[f603,f104])).
% 2.14/0.75 thf(f615,plain,(
% 2.14/0.75 ($false = $true) | ~spl6_8),
% 2.14/0.75 inference(forward_demodulation,[],[f614,f219])).
% 2.14/0.75 thf(f616,plain,(
% 2.14/0.75 $false | ~spl6_8),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f615])).
% 2.14/0.75 thf(f617,plain,(
% 2.14/0.75 ~spl6_8),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f616])).
% 2.14/0.75 thf(f656,plain,(
% 2.14/0.75 (((c_2Eoption_2EIS__SOME @ sK2 @ c_2Eoption_2ENONE @ sK2)) = $true) | ~spl6_14),
% 2.14/0.75 inference(constrained_superposition,[],[f168,f383])).
% 2.14/0.75 thf(f667,plain,(
% 2.14/0.75 (c_2Ebool_2EF = $true) | ~spl6_14),
% 2.14/0.75 inference(forward_demodulation,[],[f656,f104])).
% 2.14/0.75 thf(f668,plain,(
% 2.14/0.75 ($false = $true) | ~spl6_14),
% 2.14/0.75 inference(forward_demodulation,[],[f667,f219])).
% 2.14/0.75 thf(f669,plain,(
% 2.14/0.75 $false | ~spl6_14),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f668])).
% 2.14/0.75 thf(f670,plain,(
% 2.14/0.75 ~spl6_14),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f669])).
% 2.14/0.75 thf(f721,plain,(
% 2.14/0.75 ($false = $true) | (~spl6_1 | ~spl6_5)),
% 2.14/0.75 inference(forward_demodulation,[],[f265,f247])).
% 2.14/0.75 thf(f722,plain,(
% 2.14/0.75 $false | (~spl6_1 | ~spl6_5)),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f721])).
% 2.14/0.75 thf(f723,plain,(
% 2.14/0.75 ~spl6_1 | ~spl6_5),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f722])).
% 2.14/0.75 thf(f756,plain,(
% 2.14/0.75 ($true != $true) | (((c_2Eoption_2ESOME @ sK2 @ sK3)) = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_5),
% 2.14/0.75 inference(constrained_superposition,[],[f127,f265])).
% 2.14/0.75 thf(f759,plain,(
% 2.14/0.75 ($true != $true) | (((sK4 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4) @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) = $true) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_5),
% 2.14/0.75 inference(constrained_superposition,[],[f125,f265])).
% 2.14/0.75 thf(f760,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK5)) = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | ($true != $true) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_5),
% 2.14/0.75 inference(constrained_superposition,[],[f129,f265])).
% 2.14/0.75 thf(f763,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK3)) = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_5),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f756])).
% 2.14/0.75 thf(f764,plain,(
% 2.14/0.75 (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | (((sK4 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4) @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) = $true) | ~spl6_5),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f759])).
% 2.14/0.75 thf(f765,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK5)) = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (c_2Eoption_2ENONE @ sK2 = ((c_2Eoption_2ESOME @ sK2 @ sK5))) | ~spl6_5),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f760])).
% 2.14/0.75 thf(f771,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK3)) = ((c_2Eoption_2ESOME @ sK2 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f763,f377])).
% 2.14/0.75 thf(f772,plain,(
% 2.14/0.75 (((sK4 @ (sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4) @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) = $true) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f764,f377])).
% 2.14/0.75 thf(f773,plain,(
% 2.14/0.75 (((c_2Eoption_2ESOME @ sK2 @ sK5)) = ((c_2Eoption_2ESOME @ sK2 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)))) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_subsumption_resolution,[],[f765,f377])).
% 2.14/0.75 thf(f812,plain,(
% 2.14/0.75 (((c_2Eoption_2ETHE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3))) = ((sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(constrained_superposition,[],[f116,f771])).
% 2.14/0.75 thf(f819,plain,(
% 2.14/0.75 (sK3 = ((sK1 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_demodulation,[],[f812,f116])).
% 2.14/0.75 thf(f831,plain,(
% 2.14/0.75 (((sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)) = ((c_2Eoption_2ETHE @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK5)))) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(constrained_superposition,[],[f116,f773])).
% 2.14/0.75 thf(f838,plain,(
% 2.14/0.75 (((sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4)) = sK5) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_demodulation,[],[f831,f116])).
% 2.14/0.75 thf(f1049,plain,(
% 2.14/0.75 (((sK4 @ sK3 @ (sK0 @ sK2 @ sK2 @ (c_2Eoption_2ESOME @ sK2 @ sK3) @ (c_2Eoption_2ESOME @ sK2 @ sK5) @ sK4))) = $true) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_demodulation,[],[f772,f819])).
% 2.14/0.75 thf(f1050,plain,(
% 2.14/0.75 (((sK4 @ sK3 @ sK5)) = $true) | (~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_demodulation,[],[f1049,f838])).
% 2.14/0.75 thf(f1051,plain,(
% 2.14/0.75 ($false = $true) | (~spl6_2 | ~spl6_5 | spl6_13)),
% 2.14/0.75 inference(forward_demodulation,[],[f1050,f251])).
% 2.14/0.75 thf(f1052,plain,(
% 2.14/0.75 $false | (~spl6_2 | ~spl6_5 | spl6_13)),
% 2.14/0.75 inference(trivial_inequality_removal,[],[f1051])).
% 2.14/0.75 thf(f1053,plain,(
% 2.14/0.75 ~spl6_2 | ~spl6_5 | spl6_13),
% 2.14/0.75 inference(avatar_contradiction_clause,[],[f1052])).
% 2.14/0.75 cnf(s1, plain, spl6_1 | spl6_2 | spl6_3 | spl6_4, inference(sat_conversion,[],[f260])).
% 2.14/0.75 cnf(s2, plain, spl6_3 | spl6_4 | spl6_5, inference(sat_conversion,[],[f266])).
% 2.14/0.75 cnf(s10, plain, ~spl6_7, inference(sat_conversion,[],[f340])).
% 2.14/0.75 cnf(s13, plain, ~spl6_3 | spl6_7 | spl6_8, inference(sat_conversion,[],[f358])).
% 2.14/0.75 cnf(s19, plain, ~spl6_13, inference(sat_conversion,[],[f412])).
% 2.14/0.75 cnf(s31, plain, ~spl6_4 | spl6_13 | spl6_14, inference(sat_conversion,[],[f594])).
% 2.14/0.75 cnf(s35, plain, ~spl6_8, inference(sat_conversion,[],[f617])).
% 2.14/0.75 cnf(s40, plain, ~spl6_14, inference(sat_conversion,[],[f670])).
% 2.14/0.75 cnf(s43, plain, ~spl6_1 | ~spl6_5, inference(sat_conversion,[],[f723])).
% 2.14/0.75 cnf(s66, plain, ~spl6_2 | ~spl6_5 | spl6_13, inference(sat_conversion,[],[f1053])).
% 2.14/0.75 cnf(s73, plain, ~spl6_4 | spl6_13, inference(rat,[],[s31,s40])).
% 2.14/0.75 cnf(s76, plain, ~spl6_4, inference(rat,[],[s73,s19])).
% 2.14/0.75 cnf(s78, plain, ~spl6_3 | spl6_7, inference(rat,[],[s13,s35])).
% 2.14/0.75 cnf(s79, plain, ~spl6_3, inference(rat,[],[s78,s10])).
% 2.14/0.75 cnf(s81, plain, spl6_5, inference(rat,[],[s2,s76,s79])).
% 2.14/0.75 cnf(s82, plain, ~spl6_2, inference(rat,[],[s66,s19,s81])).
% 2.14/0.75 cnf(s86, plain, ~spl6_1, inference(rat,[],[s43,s81])).
% 2.14/0.75 cnf(s87, plain, $false, inference(rat,[],[s1,s76,s79,s82,s86])).
% 2.14/0.75 thf(f1054,plain,(
% 2.14/0.75 $false),
% 2.14/0.75 inference(avatar_sat_refutation,[],[s87])).
% 2.14/0.75 % SZS output end Proof for theBenchmark
% 2.14/0.75 % (1187990)------------------------------
% 2.14/0.75 % (1187990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.14/0.75 % (1187990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.75 % (1187990)CaDiCaL version: 2.1.3
% 2.14/0.75 % (1187990)Termination reason: Refutation
% 2.14/0.75 % (1187990)Time elapsed: 0.041 s
% 2.14/0.75 % (1187990)Peak memory usage: 13 MB
% 2.14/0.75 % (1187990)Instructions burned: 71 (million)
% 2.14/0.75 % (1187912)Success in time 0.459 s
% 2.14/0.75 % Vampire exiting
%------------------------------------------------------------------------------