%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP002^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:09:59 AM UTC 2026
% Result : Theorem 1.11s 0.43s
% Output : Refutation 1.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP002^3 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n018.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:21:30 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.11/0.43 % (511542)Will run a generic schedule for satisfiability detection.
% 1.11/0.43 % (511550)dis+10_1_sil=32000:sp=arity:random_seed=4261990187:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.11/0.43 % (511548)% WARNING: option uhcvi not known.
% 1.11/0.43 % (511551)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=908213636:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.11/0.43 % (511547)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=548607290_2999 on theBenchmark for (2999ds/0Mi)
% 1.11/0.43 % (511548)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3193569982:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.11/0.43 % (511549)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=28604752:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.11/0.43 % (511551)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.11/0.43 % (511548)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.11/0.43 % Exception at run slice level
% 1.11/0.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.11/0.43 % (511548)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.11/0.43 % (511553)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2315787002:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.11/0.43 % (511552)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=299180017:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.11/0.43 % (511559)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3152477747:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.11/0.43 % (511550)Instruction limit reached!
% 1.11/0.43 % (511550)------------------------------
% 1.11/0.43 % (511550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511550)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511550)Termination reason: Instruction limit
% 1.11/0.43 % (511550)Termination phase: Saturation
% 1.11/0.43 % (511550)Time elapsed: 0.031 s
% 1.11/0.43 % (511550)Peak memory usage: 13 MB
% 1.11/0.43 % (511550)Instructions burned: 106 (million)
% 1.11/0.43 % Exception at run slice level
% 1.11/0.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.11/0.43 % (511563)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1541783092:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.11/0.43 % (511564)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2934252369:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.11/0.43 % (511564)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.11/0.43 % (511564)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.11/0.43 % (511551)Instruction limit reached!
% 1.11/0.43 % (511551)------------------------------
% 1.11/0.43 % (511551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511551)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511551)Termination reason: Instruction limit
% 1.11/0.43 % (511551)Termination phase: Saturation
% 1.11/0.43 % (511551)Time elapsed: 0.062 s
% 1.11/0.43 % (511551)Peak memory usage: 13 MB
% 1.11/0.43 % (511551)Instructions burned: 116 (million)
% 1.11/0.43 % (511563)Instruction limit reached!
% 1.11/0.43 % (511563)------------------------------
% 1.11/0.43 % (511563)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511563)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511563)Termination reason: Instruction limit
% 1.11/0.43 % (511563)Termination phase: Saturation
% 1.11/0.43 % (511563)Time elapsed: 0.037 s
% 1.11/0.43 % (511563)Peak memory usage: 13 MB
% 1.11/0.43 % (511563)Instructions burned: 132 (million)
% 1.11/0.43 % (511567)ott-21_1_sil=16000:fs=off:random_seed=1717996805:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.11/0.43 % (511568)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2183324136:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 1.11/0.43 % (511552)Instruction limit reached!
% 1.11/0.43 % (511552)------------------------------
% 1.11/0.43 % (511552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511552)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511552)Termination reason: Instruction limit
% 1.11/0.43 % (511552)Termination phase: Saturation
% 1.11/0.43 % (511552)Time elapsed: 0.082 s
% 1.11/0.43 % (511552)Peak memory usage: 13 MB
% 1.11/0.43 % (511552)Instructions burned: 131 (million)
% 1.11/0.43 % (511553)Instruction limit reached!
% 1.11/0.43 % (511553)------------------------------
% 1.11/0.43 % (511553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511553)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511553)Termination reason: Instruction limit
% 1.11/0.43 % (511553)Termination phase: Saturation
% 1.11/0.43 % (511553)Time elapsed: 0.084 s
% 1.11/0.43 % (511553)Peak memory usage: 13 MB
% 1.11/0.43 % (511553)Instructions burned: 160 (million)
% 1.11/0.43 % (511572)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3437668304:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.11/0.43 % (511571)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=816342467:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.11/0.43 % Exception at run slice level
% 1.11/0.43 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.11/0.43 % (511572) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-511542-511572"...
% 1.11/0.43 % (511572)...printing done.
% 1.11/0.43 % (511567)Instruction limit reached!
% 1.11/0.43 % (511567)------------------------------
% 1.11/0.43 % (511567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511572)Refutation found. Thanks to Tanya!
% 1.11/0.43 % SZS status Theorem for theBenchmark
% 1.11/0.43 % SZS output start Proof for theBenchmark
% 1.11/0.43 thf(type_def_5, type, tyop_2Emin_2Ebool: $tType).
% 1.11/0.43 thf(type_def_6, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 1.11/0.43 thf(type_def_7, type, tyop_2Eoption_2Eoption: $tType > $tType).
% 1.11/0.43 thf(type_def_8, type, sTfun: ($tType * $tType) > $tType).
% 1.11/0.43 thf(type_def_9, type, sK2: $tType).
% 1.11/0.43 thf(type_def_10, type, sK3: $tType).
% 1.11/0.43 thf(type_def_11, type, sK4: $tType).
% 1.11/0.43 thf(func_def_0, type, c_2Ebool_2E_21: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.11/0.43 thf(func_def_1, type, c_2Ebool_2E_2F_5C: ($o > $o > $o)).
% 1.11/0.43 thf(func_def_2, type, c_2Emin_2E_3D: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.11/0.43 thf(func_def_3, type, c_2Emin_2E_3D_3D_3E: ($o > $o > $o)).
% 1.11/0.43 thf(func_def_4, type, c_2Ebool_2E_3F: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.11/0.43 thf(func_def_5, type, c_2Ebool_2ECOND: !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 1.11/0.43 thf(func_def_6, type, c_2Ebool_2EF: $o).
% 1.11/0.43 thf(func_def_7, type, c_2Eoption_2EIS__SOME: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ X0 > $o))).
% 1.11/0.43 thf(func_def_8, type, c_2Eoption_2ENONE: !>[X0: $tType]:(tyop_2Eoption_2Eoption @ X0)).
% 1.11/0.43 thf(func_def_9, type, c_2Eoption_2EOPTION__MAP2: !>[X0: $tType, X1: $tType, X2: $tType]:(((X1 > X2 > X0) > tyop_2Eoption_2Eoption @ X1 > tyop_2Eoption_2Eoption @ X2 > tyop_2Eoption_2Eoption @ X0))).
% 1.11/0.43 thf(func_def_10, type, c_2Eoption_2ESOME: !>[X0: $tType]:((X0 > tyop_2Eoption_2Eoption @ X0))).
% 1.11/0.43 thf(func_def_11, type, c_2Ebool_2ET: $o).
% 1.11/0.43 thf(func_def_12, type, c_2Eoption_2ETHE: !>[X0: $tType]:((tyop_2Eoption_2Eoption @ X0 > X0))).
% 1.11/0.43 thf(func_def_13, type, c_2Ebool_2E_5C_2F: ($o > $o > $o)).
% 1.11/0.43 thf(func_def_14, type, c_2Ebool_2E_7E: ($o > $o)).
% 1.11/0.43 thf(func_def_16, type, vNOT: ($o > $o)).
% 1.11/0.43 thf(func_def_19, type, sK0: !>[X0: $tType]:(((X0 > $o) > X0))).
% 1.11/0.43 thf(func_def_20, type, sK1: !>[X0: $tType]:(((X0 > $o) > X0))).
% 1.11/0.43 thf(func_def_21, type, sK5: sK4).
% 1.11/0.43 thf(func_def_22, type, sK6: sK3).
% 1.11/0.43 thf(func_def_23, type, sK7: (sK3 > sK4 > sK2)).
% 1.11/0.43 thf(func_def_24, type, sF8: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_25, type, sF9: tyop_2Eoption_2Eoption @ sK3).
% 1.11/0.43 thf(func_def_26, type, sF10: tyop_2Eoption_2Eoption @ sK4).
% 1.11/0.43 thf(func_def_27, type, sF11: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_28, type, sF12: tyop_2Eoption_2Eoption @ sK4).
% 1.11/0.43 thf(func_def_29, type, sF13: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_30, type, sF14: tyop_2Eoption_2Eoption @ sK3).
% 1.11/0.43 thf(func_def_31, type, sF15: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_32, type, sF16: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_33, type, sF17: sK2).
% 1.11/0.43 thf(func_def_34, type, sF18: tyop_2Eoption_2Eoption @ sK2).
% 1.11/0.43 thf(func_def_36, type, db0: !>[X0: $tType]:(X0)).
% 1.11/0.43 thf(func_def_37, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.11/0.43 thf(func_def_38, type, db1: !>[X0: $tType]:(X0)).
% 1.11/0.43 thf(f1,axiom,(
% 1.11/0.43 ! [X3 : $o,X4 : $o] : ((c_2Ebool_2E_2F_5C @ X3 @ X4) <=> (X4 & X3))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',logicdef_2E_2F_5C)).
% 1.11/0.43 thf(f5,axiom,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0,X2 : X0] : ((c_2Emin_2E_3D @ X0 @ X1 @ X2) <=> (X1 = X2))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',logicdef_2E_3D)).
% 1.11/0.43 thf(f8,axiom,(
% 1.11/0.43 c_2Ebool_2ET),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH)).
% 1.11/0.43 thf(f9,axiom,(
% 1.11/0.43 ! [X0 : $o] : (((X0 & X0) <=> X0) & ((c_2Ebool_2EF & X0) <=> c_2Ebool_2EF) & ((X0 & c_2Ebool_2EF) <=> c_2Ebool_2EF) & ((c_2Ebool_2ET & X0) <=> X0) & ((X0 & c_2Ebool_2ET) <=> X0))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EAND__CLAUSES)).
% 1.11/0.43 thf(f11,axiom,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0,X2 : X0] : ((((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2)) = X2) & (((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2)) = X1))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CLAUSES)).
% 1.11/0.43 thf(f13,axiom,(
% 1.11/0.43 ! [X0 : $tType] : ((((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)) = c_2Ebool_2EF) & ! [X1 : X0] : (((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = c_2Ebool_2ET))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2EIS__SOME__DEF)).
% 1.11/0.43 thf(f14,axiom,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0] : (((c_2Eoption_2ETHE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = X1)),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2ETHE__DEF)).
% 1.11/0.43 thf(f15,axiom,(
% 1.11/0.43 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : (X1 > X2 > X0),X4 : tyop_2Eoption_2Eoption @ X1,X5 : tyop_2Eoption_2Eoption @ X2] : (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X3 @ X4 @ X5)) = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ X0 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ X1 @ X4) @ (c_2Eoption_2EIS__SOME @ X2 @ X5)) @ (c_2Eoption_2ESOME @ X0 @ (X3 @ (c_2Eoption_2ETHE @ X1 @ X4) @ (c_2Eoption_2ETHE @ X2 @ X5))) @ c_2Eoption_2ENONE @ X0)))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2EOPTION__MAP2__DEF)).
% 1.11/0.43 thf(f16,conjecture,(
% 1.11/0.43 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : X2,X4 : X1,X5 : (X1 > X2 > X0)] : ((((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ENONE @ X2)) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ (c_2Eoption_2ESOME @ X2 @ X3))) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ c_2Eoption_2ENONE @ X2)) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ (c_2Eoption_2ESOME @ X2 @ X3))) = ((c_2Eoption_2ESOME @ X0 @ (X5 @ X4 @ X3)))))),
% 1.11/0.43 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eoption_2EOPTION__MAP2__THM)).
% 1.11/0.43 thf(f17,negated_conjecture,(
% 1.11/0.43 ~ ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : X2,X4 : X1,X5 : (X1 > X2 > X0)] : ((((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ENONE @ X2)) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ (c_2Eoption_2ESOME @ X2 @ X3))) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ c_2Eoption_2ENONE @ X2)) = c_2Eoption_2ENONE @ X0) & (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ (c_2Eoption_2ESOME @ X2 @ X3))) = ((c_2Eoption_2ESOME @ X0 @ (X5 @ X4 @ X3)))))),
% 1.11/0.43 inference(negated_conjecture,[status(cth)],[f16])).
% 1.11/0.43 thf(f18,plain,(
% 1.11/0.43 ! [X0 : $o,X1 : $o] : ((c_2Ebool_2E_2F_5C @ X0 @ X1) <=> (X1 & X0))),
% 1.11/0.43 inference(rectify,[],[f1])).
% 1.11/0.43 thf(f19,plain,(
% 1.11/0.43 ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $true) <=> (($true = X1) & ($true = X0)))),
% 1.11/0.43 inference(fool_elimination,[],[f18])).
% 1.11/0.43 thf(f26,plain,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0,X2 : X0] : ((c_2Emin_2E_3D @ X0 @ X1 @ X2) <=> (X1 = X2))),
% 1.11/0.43 inference(rectify,[],[f5])).
% 1.11/0.43 thf(f27,plain,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0,X2 : X0] : ((((c_2Emin_2E_3D @ X0 @ X1 @ X2)) = $true) <=> (X1 = X2))),
% 1.11/0.43 inference(fool_elimination,[],[f26])).
% 1.11/0.43 thf(f32,plain,(
% 1.11/0.43 c_2Ebool_2ET),
% 1.11/0.43 inference(rectify,[],[f8])).
% 1.11/0.43 thf(f33,plain,(
% 1.11/0.43 (c_2Ebool_2ET = $true)),
% 1.11/0.43 inference(fool_elimination,[],[f32])).
% 1.11/0.43 thf(f34,plain,(
% 1.11/0.43 ! [X0 : $o] : (((X0 & X0) <=> X0) & ((c_2Ebool_2EF & X0) <=> c_2Ebool_2EF) & ((X0 & c_2Ebool_2EF) <=> c_2Ebool_2EF) & ((c_2Ebool_2ET & X0) <=> X0) & ((X0 & c_2Ebool_2ET) <=> X0))),
% 1.11/0.43 inference(rectify,[],[f9])).
% 1.11/0.43 thf(f35,plain,(
% 1.11/0.43 ! [X0 : $o] : (((($true = X0) & ($true = X0)) <=> ($true = X0)) & (((c_2Ebool_2EF = $true) & ($true = X0)) <=> (c_2Ebool_2EF = $true)) & ((($true = X0) & (c_2Ebool_2EF = $true)) <=> (c_2Ebool_2EF = $true)) & (((c_2Ebool_2ET = $true) & ($true = X0)) <=> ($true = X0)) & ((($true = X0) & (c_2Ebool_2ET = $true)) <=> ($true = X0)))),
% 1.11/0.43 inference(fool_elimination,[],[f34])).
% 1.11/0.43 thf(f39,plain,(
% 1.11/0.43 ? [X0 : $tType,X1 : $tType,X2 : $tType,X3 : X2,X4 : X1,X5 : (X1 > X2 > X0)] : ((c_2Eoption_2ENONE @ X0 != ((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ c_2Eoption_2ENONE @ X2))) | (c_2Eoption_2ENONE @ X0 != ((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ c_2Eoption_2ENONE @ X1 @ (c_2Eoption_2ESOME @ X2 @ X3)))) | (c_2Eoption_2ENONE @ X0 != ((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ c_2Eoption_2ENONE @ X2))) | (((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X5 @ (c_2Eoption_2ESOME @ X1 @ X4) @ (c_2Eoption_2ESOME @ X2 @ X3))) != ((c_2Eoption_2ESOME @ X0 @ (X5 @ X4 @ X3)))))),
% 1.11/0.43 inference(ennf_transformation,[],[f17])).
% 1.11/0.43 thf(f40,plain,(
% 1.11/0.43 ! [X0 : $o,X1 : $o] : (((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $true) | (($true != X1) | ($true != X0))) & ((($true = X1) & ($true = X0)) | (((c_2Ebool_2E_2F_5C @ X0 @ X1)) != $true)))),
% 1.11/0.43 inference(nnf_transformation,[],[f19])).
% 1.11/0.43 thf(f41,plain,(
% 1.11/0.43 ! [X0 : $o,X1 : $o] : (((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $true) | ($true != X1) | ($true != X0)) & ((($true = X1) & ($true = X0)) | (((c_2Ebool_2E_2F_5C @ X0 @ X1)) != $true)))),
% 1.11/0.43 inference(flattening,[],[f40])).
% 1.11/0.43 thf(f46,plain,(
% 1.11/0.43 ! [X0 : $tType,X1 : X0,X2 : X0] : (((((c_2Emin_2E_3D @ X0 @ X1 @ X2)) = $true) | (X1 != X2)) & ((X1 = X2) | (((c_2Emin_2E_3D @ X0 @ X1 @ X2)) != $true)))),
% 1.11/0.43 inference(nnf_transformation,[],[f27])).
% 1.11/0.43 thf(f53,plain,(
% 1.11/0.43 ! [X0 : $o] : ((((($true = X0) & ($true = X0)) | ($true != X0)) & (($true = X0) | (($true != X0) | ($true != X0)))) & ((((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | ((c_2Ebool_2EF != $true) | ($true != X0)))) & (((($true = X0) & (c_2Ebool_2EF = $true)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | (($true != X0) | (c_2Ebool_2EF != $true)))) & ((((c_2Ebool_2ET = $true) & ($true = X0)) | ($true != X0)) & (($true = X0) | ((c_2Ebool_2ET != $true) | ($true != X0)))) & (((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0)) & (($true = X0) | (($true != X0) | (c_2Ebool_2ET != $true)))))),
% 1.11/0.43 inference(nnf_transformation,[],[f35])).
% 1.11/0.43 thf(f54,plain,(
% 1.11/0.43 ! [X0 : $o] : (((($true = X0) & ($true = X0)) | ($true != X0)) & (($true = X0) | ($true != X0) | ($true != X0)) & (((c_2Ebool_2EF = $true) & ($true = X0)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | (c_2Ebool_2EF != $true) | ($true != X0)) & ((($true = X0) & (c_2Ebool_2EF = $true)) | (c_2Ebool_2EF != $true)) & ((c_2Ebool_2EF = $true) | ($true != X0) | (c_2Ebool_2EF != $true)) & (((c_2Ebool_2ET = $true) & ($true = X0)) | ($true != X0)) & (($true = X0) | (c_2Ebool_2ET != $true) | ($true != X0)) & ((($true = X0) & (c_2Ebool_2ET = $true)) | ($true != X0)) & (($true = X0) | ($true != X0) | (c_2Ebool_2ET != $true)))),
% 1.11/0.43 inference(flattening,[],[f53])).
% 1.11/0.43 thf(f57,plain,(
% 1.11/0.43 (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ c_2Eoption_2ENONE @ sK3 @ c_2Eoption_2ENONE @ sK4))) | (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ c_2Eoption_2ENONE @ sK3 @ (c_2Eoption_2ESOME @ sK4 @ sK5)))) | (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ (c_2Eoption_2ESOME @ sK3 @ sK6) @ c_2Eoption_2ENONE @ sK4))) | (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ (c_2Eoption_2ESOME @ sK3 @ sK6) @ (c_2Eoption_2ESOME @ sK4 @ sK5))) != ((c_2Eoption_2ESOME @ sK2 @ (sK7 @ sK6 @ sK5))))),
% 1.11/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK5,sK6,sK7]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK6),skolemize(X5,sK7)],[f39])).
% 1.11/0.43 thf(f58,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) != $true) | ($true = X0)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f41])).
% 1.11/0.43 thf(f59,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) != $true) | ($true = X1)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f41])).
% 1.11/0.43 thf(f60,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $true) | ($true != X1) | ($true != X0)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f41])).
% 1.11/0.43 thf(f68,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Emin_2E_3D @ X0 @ X1 @ X2)) != $true) | (X1 = X2)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f46])).
% 1.11/0.43 thf(f74,plain,(
% 1.11/0.43 (c_2Ebool_2ET = $true)),
% 1.11/0.43 inference(cnf_transformation,[],[f33])).
% 1.11/0.43 thf(f85,plain,(
% 1.11/0.43 ( ! [X0 : $o] : (($true = X0) | (c_2Ebool_2EF != $true)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f54])).
% 1.11/0.43 thf(f92,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2ET @ X1 @ X2)) = X1)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f11])).
% 1.11/0.43 thf(f93,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ c_2Ebool_2EF @ X1 @ X2)) = X2)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f11])).
% 1.11/0.43 thf(f96,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X1 : X0] : ((c_2Ebool_2ET = ((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))))) )),
% 1.11/0.43 inference(cnf_transformation,[],[f13])).
% 1.11/0.43 thf(f97,plain,(
% 1.11/0.43 ( ! [X0 : $tType] : ((c_2Ebool_2EF = ((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)))) )),
% 1.11/0.43 inference(cnf_transformation,[],[f13])).
% 1.11/0.43 thf(f98,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X1 : X0] : ((((c_2Eoption_2ETHE @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = X1)) )),
% 1.11/0.43 inference(cnf_transformation,[],[f14])).
% 1.11/0.43 thf(f99,plain,(
% 1.11/0.43 ( ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : (X1 > X2 > X0),X4 : tyop_2Eoption_2Eoption @ X1,X5 : tyop_2Eoption_2Eoption @ X2] : ((((c_2Eoption_2EOPTION__MAP2 @ X0 @ X1 @ X2 @ X3 @ X4 @ X5)) = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ X0 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ X1 @ X4) @ (c_2Eoption_2EIS__SOME @ X2 @ X5)) @ (c_2Eoption_2ESOME @ X0 @ (X3 @ (c_2Eoption_2ETHE @ X1 @ X4) @ (c_2Eoption_2ETHE @ X2 @ X5))) @ c_2Eoption_2ENONE @ X0)))) )),
% 1.11/0.43 inference(cnf_transformation,[],[f15])).
% 1.11/0.43 thf(f100,plain,(
% 1.11/0.43 (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ c_2Eoption_2ENONE @ sK3 @ c_2Eoption_2ENONE @ sK4))) | (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ c_2Eoption_2ENONE @ sK3 @ (c_2Eoption_2ESOME @ sK4 @ sK5)))) | (c_2Eoption_2ENONE @ sK2 != ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ (c_2Eoption_2ESOME @ sK3 @ sK6) @ c_2Eoption_2ENONE @ sK4))) | (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ (c_2Eoption_2ESOME @ sK3 @ sK6) @ (c_2Eoption_2ESOME @ sK4 @ sK5))) != ((c_2Eoption_2ESOME @ sK2 @ (sK7 @ sK6 @ sK5))))),
% 1.11/0.43 inference(cnf_transformation,[],[f57])).
% 1.11/0.43 thf(f101,definition,(
% 1.11/0.43 ($true != $false)),
% 1.11/0.43 introduced(theory,[fool_distinctness_axiom])).
% 1.11/0.43 thf(f102,definition,(
% 1.11/0.43 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.11/0.43 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.11/0.43 thf(f109,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ $true @ X1 @ X2)) = X1)) )),
% 1.11/0.43 inference(definition_unfolding,[],[f92,f74])).
% 1.11/0.43 thf(f110,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X1 : X0] : ((((c_2Eoption_2EIS__SOME @ X0 @ (c_2Eoption_2ESOME @ X0 @ X1))) = $true)) )),
% 1.11/0.43 inference(definition_unfolding,[],[f96,f74])).
% 1.11/0.43 thf(f111,plain,(
% 1.11/0.43 ( ! [X0 : $o] : (($true = ((c_2Ebool_2E_2F_5C @ X0 @ $true))) | ($true != X0)) )),
% 1.11/0.43 inference(equality_resolution,[],[f60])).
% 1.11/0.43 thf(f112,plain,(
% 1.11/0.43 ($true = ((c_2Ebool_2E_2F_5C @ $true @ $true)))),
% 1.11/0.43 inference(equality_resolution,[],[f111])).
% 1.11/0.43 thf(f130,definition,(
% 1.11/0.43 (sF8 = c_2Eoption_2ENONE @ sK2)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 1.11/0.43 thf(f131,plain,(
% 1.11/0.43 (c_2Eoption_2ENONE @ sK2 = sF8)),
% 1.11/0.43 inference(reorient_equations,[],[f130])).
% 1.11/0.43 thf(f132,definition,(
% 1.11/0.43 (sF9 = c_2Eoption_2ENONE @ sK3)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF9])],[function_definition])).
% 1.11/0.43 thf(f133,plain,(
% 1.11/0.43 (c_2Eoption_2ENONE @ sK3 = sF9)),
% 1.11/0.43 inference(reorient_equations,[],[f132])).
% 1.11/0.43 thf(f134,definition,(
% 1.11/0.43 (sF10 = c_2Eoption_2ENONE @ sK4)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF10])],[function_definition])).
% 1.11/0.43 thf(f135,plain,(
% 1.11/0.43 (c_2Eoption_2ENONE @ sK4 = sF10)),
% 1.11/0.43 inference(reorient_equations,[],[f134])).
% 1.11/0.43 thf(f136,definition,(
% 1.11/0.43 (sF11 = ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF9 @ sF10)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF11])],[function_definition])).
% 1.11/0.43 thf(f137,plain,(
% 1.11/0.43 (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF9 @ sF10)) = sF11)),
% 1.11/0.43 inference(reorient_equations,[],[f136])).
% 1.11/0.43 thf(f138,definition,(
% 1.11/0.43 (sF12 = ((c_2Eoption_2ESOME @ sK4 @ sK5)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF12])],[function_definition])).
% 1.11/0.43 thf(f139,plain,(
% 1.11/0.43 (((c_2Eoption_2ESOME @ sK4 @ sK5)) = sF12)),
% 1.11/0.43 inference(reorient_equations,[],[f138])).
% 1.11/0.43 thf(f140,definition,(
% 1.11/0.43 (sF13 = ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF9 @ sF12)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF13])],[function_definition])).
% 1.11/0.43 thf(f141,plain,(
% 1.11/0.43 (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF9 @ sF12)) = sF13)),
% 1.11/0.43 inference(reorient_equations,[],[f140])).
% 1.11/0.43 thf(f142,definition,(
% 1.11/0.43 (sF14 = ((c_2Eoption_2ESOME @ sK3 @ sK6)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF14])],[function_definition])).
% 1.11/0.43 thf(f143,plain,(
% 1.11/0.43 (((c_2Eoption_2ESOME @ sK3 @ sK6)) = sF14)),
% 1.11/0.43 inference(reorient_equations,[],[f142])).
% 1.11/0.43 thf(f144,definition,(
% 1.11/0.43 (sF15 = ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF14 @ sF10)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF15])],[function_definition])).
% 1.11/0.43 thf(f145,plain,(
% 1.11/0.43 (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF14 @ sF10)) = sF15)),
% 1.11/0.43 inference(reorient_equations,[],[f144])).
% 1.11/0.43 thf(f146,definition,(
% 1.11/0.43 (sF16 = ((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF14 @ sF12)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF16])],[function_definition])).
% 1.11/0.43 thf(f147,plain,(
% 1.11/0.43 (((c_2Eoption_2EOPTION__MAP2 @ sK2 @ sK3 @ sK4 @ sK7 @ sF14 @ sF12)) = sF16)),
% 1.11/0.43 inference(reorient_equations,[],[f146])).
% 1.11/0.43 thf(f148,definition,(
% 1.11/0.43 (sF17 = ((sK7 @ sK6 @ sK5)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF17])],[function_definition])).
% 1.11/0.43 thf(f149,plain,(
% 1.11/0.43 (((sK7 @ sK6 @ sK5)) = sF17)),
% 1.11/0.43 inference(reorient_equations,[],[f148])).
% 1.11/0.43 thf(f150,definition,(
% 1.11/0.43 (sF18 = ((c_2Eoption_2ESOME @ sK2 @ sF17)))),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[sF18])],[function_definition])).
% 1.11/0.43 thf(f151,plain,(
% 1.11/0.43 (((c_2Eoption_2ESOME @ sK2 @ sF17)) = sF18)),
% 1.11/0.43 inference(reorient_equations,[],[f150])).
% 1.11/0.43 thf(f152,plain,(
% 1.11/0.43 (sF8 != sF11) | (sF8 != sF13) | (sF8 != sF15) | (sF16 != sF18)),
% 1.11/0.43 inference(definition_folding,[],[f100,f151,f149,f147,f139,f143,f145,f135,f143,f131,f141,f139,f133,f131,f137,f135,f133,f131])).
% 1.11/0.43 thf(f153,plain,(
% 1.11/0.43 ( ! [X0 : $tType] : ((c_2Ebool_2EF = $true) | (((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)) = $false)) )),
% 1.11/0.43 inference(iff_proxy_clausification,[],[f97])).
% 1.11/0.43 thf(f160,definition,(
% 1.11/0.43 spl19_1 <=> (sF16 = sF18)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_1])],[avatar_definition])).
% 1.11/0.43 thf(f162,plain,(
% 1.11/0.43 (sF16 != sF18) | spl19_1),
% 1.11/0.43 inference(avatar_component_clause,[],[f160])).
% 1.11/0.43 thf(f164,definition,(
% 1.11/0.43 spl19_2 <=> (sF8 = sF15)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_2])],[avatar_definition])).
% 1.11/0.43 thf(f168,definition,(
% 1.11/0.43 spl19_3 <=> (sF8 = sF13)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition])).
% 1.11/0.43 thf(f170,plain,(
% 1.11/0.43 (sF8 != sF13) | spl19_3),
% 1.11/0.43 inference(avatar_component_clause,[],[f168])).
% 1.11/0.43 thf(f172,definition,(
% 1.11/0.43 spl19_4 <=> (sF8 = sF11)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_4])],[avatar_definition])).
% 1.11/0.43 thf(f175,plain,(
% 1.11/0.43 ~spl19_1 | ~spl19_2 | ~spl19_3 | ~spl19_4),
% 1.11/0.43 inference(avatar_split_clause,[],[f152,f172,f168,f164,f160])).
% 1.11/0.43 thf(f180,definition,(
% 1.11/0.43 spl19_6 <=> (c_2Ebool_2EF = $false)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_6])],[avatar_definition])).
% 1.11/0.43 thf(f182,plain,(
% 1.11/0.43 (c_2Ebool_2EF = $false) | ~spl19_6),
% 1.11/0.43 inference(avatar_component_clause,[],[f180])).
% 1.11/0.43 thf(f185,definition,(
% 1.11/0.43 spl19_7 <=> ! [X0 : $tType] : (((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)) = $false)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition])).
% 1.11/0.43 thf(f186,plain,(
% 1.11/0.43 ( ! [X0 : $tType] : ((((c_2Eoption_2EIS__SOME @ X0 @ c_2Eoption_2ENONE @ X0)) = $false)) ) | ~spl19_7),
% 1.11/0.43 inference(avatar_component_clause,[],[f185])).
% 1.11/0.43 thf(f188,definition,(
% 1.11/0.43 spl19_8 <=> (c_2Ebool_2EF = $true)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_8])],[avatar_definition])).
% 1.11/0.43 thf(f189,plain,(
% 1.11/0.43 (c_2Ebool_2EF != $true) | spl19_8),
% 1.11/0.43 inference(avatar_component_clause,[],[f188])).
% 1.11/0.43 thf(f191,plain,(
% 1.11/0.43 spl19_7 | spl19_8),
% 1.11/0.43 inference(avatar_split_clause,[],[f153,f188,f185])).
% 1.11/0.43 thf(f193,definition,(
% 1.11/0.43 spl19_9 <=> ! [X0 : $o] : ($true = X0)),
% 1.11/0.43 introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition])).
% 1.11/0.43 thf(f194,plain,(
% 1.11/0.43 ( ! [X0 : $o] : (($true = X0)) ) | ~spl19_9),
% 1.11/0.43 inference(avatar_component_clause,[],[f193])).
% 1.11/0.43 thf(f196,plain,(
% 1.11/0.43 ~spl19_8 | spl19_9),
% 1.11/0.43 inference(avatar_split_clause,[],[f85,f193,f188])).
% 1.11/0.43 thf(f197,plain,(
% 1.11/0.43 (sF11 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF9) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF10)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ c_2Eoption_2ENONE @ sK2)))),
% 1.11/0.43 inference(forward_demodulation,[],[f137,f99])).
% 1.11/0.43 thf(f198,plain,(
% 1.11/0.43 (sF13 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF9) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ c_2Eoption_2ENONE @ sK2)))),
% 1.11/0.43 inference(forward_demodulation,[],[f141,f99])).
% 1.11/0.43 thf(f199,plain,(
% 1.11/0.43 (sF15 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF10)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ c_2Eoption_2ENONE @ sK2)))),
% 1.11/0.43 inference(forward_demodulation,[],[f145,f99])).
% 1.11/0.43 thf(f200,plain,(
% 1.11/0.43 (sF16 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ c_2Eoption_2ENONE @ sK2)))),
% 1.11/0.43 inference(forward_demodulation,[],[f147,f99])).
% 1.11/0.43 thf(f201,plain,(
% 1.11/0.43 (sF11 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF9) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF10)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ sF8)))),
% 1.11/0.43 inference(forward_demodulation,[],[f197,f131])).
% 1.11/0.43 thf(f202,plain,(
% 1.11/0.43 (sF13 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF9) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ sF8)))),
% 1.11/0.43 inference(forward_demodulation,[],[f198,f131])).
% 1.11/0.43 thf(f203,plain,(
% 1.11/0.43 (sF15 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF10)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ sF8)))),
% 1.11/0.43 inference(forward_demodulation,[],[f199,f131])).
% 1.11/0.43 thf(f204,plain,(
% 1.11/0.43 (sF16 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ (c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)) @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ sF8)))),
% 1.11/0.43 inference(forward_demodulation,[],[f200,f131])).
% 1.11/0.43 thf(f207,plain,(
% 1.11/0.43 ($true != $true) | (c_2Ebool_2EF = $false) | spl19_8),
% 1.11/0.43 inference(constrained_superposition,[],[f189,f102])).
% 1.11/0.43 thf(f209,plain,(
% 1.11/0.43 (c_2Ebool_2EF = $false) | spl19_8),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f207])).
% 1.11/0.43 thf(f214,plain,(
% 1.11/0.43 spl19_6 | spl19_8),
% 1.11/0.43 inference(avatar_split_clause,[],[f209,f188,f180])).
% 1.11/0.43 thf(f244,plain,(
% 1.11/0.43 (sK5 = ((c_2Eoption_2ETHE @ sK4 @ sF12)))),
% 1.11/0.43 inference(constrained_superposition,[],[f98,f139])).
% 1.11/0.43 thf(f245,plain,(
% 1.11/0.43 (sK6 = ((c_2Eoption_2ETHE @ sK3 @ sF14)))),
% 1.11/0.43 inference(constrained_superposition,[],[f98,f143])).
% 1.11/0.43 thf(f249,plain,(
% 1.11/0.43 ($true = ((c_2Eoption_2EIS__SOME @ sK4 @ sF12)))),
% 1.11/0.43 inference(constrained_superposition,[],[f110,f139])).
% 1.11/0.43 thf(f250,plain,(
% 1.11/0.43 ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF14)))),
% 1.11/0.43 inference(constrained_superposition,[],[f110,f143])).
% 1.11/0.43 thf(f252,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : (($true != $true) | ($true = X0) | (((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $false)) )),
% 1.11/0.43 inference(constrained_superposition,[],[f58,f102])).
% 1.11/0.43 thf(f253,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $false) | ($true = X0)) )),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f252])).
% 1.11/0.43 thf(f254,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : (($true != $true) | ($true = X1) | (((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $false)) )),
% 1.11/0.43 inference(constrained_superposition,[],[f59,f102])).
% 1.11/0.43 thf(f255,plain,(
% 1.11/0.43 ( ! [X0 : $o,X1 : $o] : ((((c_2Ebool_2E_2F_5C @ X0 @ X1)) = $false) | ($true = X1)) )),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f254])).
% 1.11/0.43 thf(f272,plain,(
% 1.11/0.43 ($false = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9))) | ~spl19_7),
% 1.11/0.43 inference(constrained_superposition,[],[f186,f133])).
% 1.11/0.43 thf(f273,plain,(
% 1.11/0.43 ($false = ((c_2Eoption_2EIS__SOME @ sK4 @ sF10))) | ~spl19_7),
% 1.11/0.43 inference(constrained_superposition,[],[f186,f135])).
% 1.11/0.43 thf(f415,plain,(
% 1.11/0.43 ( ! [X0 : $o] : (($false != X0)) ) | ~spl19_9),
% 1.11/0.43 inference(constrained_superposition,[],[f101,f194])).
% 1.11/0.43 thf(f424,plain,(
% 1.11/0.43 ( ! [X2 : X0,X1 : X0] : (($true != $true) | (X1 = X2)) ) | ~spl19_9),
% 1.11/0.43 inference(constrained_superposition,[],[f68,f194])).
% 1.11/0.43 thf(f444,plain,(
% 1.11/0.43 ( ! [X2 : X0,X1 : X0] : ((X1 = X2)) ) | ~spl19_9),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f424])).
% 1.11/0.43 thf(f473,plain,(
% 1.11/0.43 $false | ~spl19_9),
% 1.11/0.43 inference(forward_subsumption_resolution,[],[f415,f444])).
% 1.11/0.43 thf(f474,plain,(
% 1.11/0.43 ~spl19_9),
% 1.11/0.43 inference(avatar_contradiction_clause,[],[f473])).
% 1.11/0.43 thf(f513,plain,(
% 1.11/0.43 ( ! [X0 : $tType,X2 : X0,X1 : X0] : ((((c_2Ebool_2ECOND @ X0 @ $false @ X1 @ X2)) = X2)) ) | ~spl19_6),
% 1.11/0.43 inference(constrained_superposition,[],[f93,f182])).
% 1.11/0.43 thf(f796,plain,(
% 1.11/0.43 (sF11 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ $false @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ sF8))) | ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9)))),
% 1.11/0.43 inference(constrained_superposition,[],[f201,f253])).
% 1.11/0.43 thf(f797,plain,(
% 1.11/0.43 (sF13 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ $false @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF9) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ sF8))) | ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9)))),
% 1.11/0.43 inference(constrained_superposition,[],[f202,f253])).
% 1.11/0.43 thf(f816,plain,(
% 1.11/0.43 (sF8 = sF13) | ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9))) | ~spl19_6),
% 1.11/0.43 inference(forward_demodulation,[],[f797,f513])).
% 1.11/0.43 thf(f817,plain,(
% 1.11/0.43 (sF8 = sF11) | ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9))) | ~spl19_6),
% 1.11/0.43 inference(forward_demodulation,[],[f796,f513])).
% 1.11/0.43 thf(f818,plain,(
% 1.11/0.43 ($true = ((c_2Eoption_2EIS__SOME @ sK3 @ sF9))) | (spl19_3 | ~spl19_6)),
% 1.11/0.43 inference(forward_subsumption_resolution,[],[f816,f170])).
% 1.11/0.43 thf(f819,plain,(
% 1.11/0.43 ($true = $false) | (sF8 = sF11) | (~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(forward_demodulation,[],[f817,f272])).
% 1.11/0.43 thf(f820,plain,(
% 1.11/0.43 (sF8 = sF11) | (~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f819])).
% 1.11/0.43 thf(f821,plain,(
% 1.11/0.43 ($true = $false) | (spl19_3 | ~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(forward_demodulation,[],[f818,f272])).
% 1.11/0.43 thf(f822,plain,(
% 1.11/0.43 $false | (spl19_3 | ~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f821])).
% 1.11/0.43 thf(f823,plain,(
% 1.11/0.43 spl19_3 | ~spl19_6 | ~spl19_7),
% 1.11/0.43 inference(avatar_contradiction_clause,[],[f822])).
% 1.11/0.43 thf(f824,plain,(
% 1.11/0.43 spl19_4 | ~spl19_6 | ~spl19_7),
% 1.11/0.43 inference(avatar_split_clause,[],[f820,f185,f180,f172])).
% 1.11/0.43 thf(f857,plain,(
% 1.11/0.43 (sF15 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ $false @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF10))) @ sF8))) | ($true = ((c_2Eoption_2EIS__SOME @ sK4 @ sF10)))),
% 1.11/0.43 inference(constrained_superposition,[],[f203,f255])).
% 1.11/0.43 thf(f859,plain,(
% 1.11/0.43 (sF8 = sF15) | ($true = ((c_2Eoption_2EIS__SOME @ sK4 @ sF10))) | ~spl19_6),
% 1.11/0.43 inference(forward_demodulation,[],[f857,f513])).
% 1.11/0.43 thf(f865,plain,(
% 1.11/0.43 ($true = $false) | (sF8 = sF15) | (~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(forward_demodulation,[],[f859,f273])).
% 1.11/0.43 thf(f866,plain,(
% 1.11/0.43 (sF8 = sF15) | (~spl19_6 | ~spl19_7)),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f865])).
% 1.11/0.43 thf(f872,plain,(
% 1.11/0.43 spl19_2 | ~spl19_6 | ~spl19_7),
% 1.11/0.43 inference(avatar_split_clause,[],[f866,f185,f180,f164])).
% 1.11/0.43 thf(f891,plain,(
% 1.11/0.43 (sF16 = ((c_2Ebool_2ECOND @ tyop_2Eoption_2Eoption @ sK2 @ $true @ (c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF12))) @ sF8))) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(constrained_superposition,[],[f204,f102])).
% 1.11/0.43 thf(f894,plain,(
% 1.11/0.43 (sF16 = ((c_2Eoption_2ESOME @ sK2 @ (sK7 @ (c_2Eoption_2ETHE @ sK3 @ sF14) @ (c_2Eoption_2ETHE @ sK4 @ sF12))))) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(forward_demodulation,[],[f891,f109])).
% 1.11/0.43 thf(f901,plain,(
% 1.11/0.43 (sF16 = ((c_2Eoption_2ESOME @ sK2 @ (sK7 @ sK6 @ (c_2Eoption_2ETHE @ sK4 @ sF12))))) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(forward_demodulation,[],[f894,f245])).
% 1.11/0.43 thf(f908,plain,(
% 1.11/0.43 (((c_2Eoption_2ESOME @ sK2 @ (sK7 @ sK6 @ sK5))) = sF16) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(forward_demodulation,[],[f901,f244])).
% 1.11/0.43 thf(f915,plain,(
% 1.11/0.43 (sF16 = ((c_2Eoption_2ESOME @ sK2 @ sF17))) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(forward_demodulation,[],[f908,f149])).
% 1.11/0.43 thf(f922,plain,(
% 1.11/0.43 (sF16 = sF18) | ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12))))),
% 1.11/0.43 inference(forward_demodulation,[],[f915,f151])).
% 1.11/0.43 thf(f929,plain,(
% 1.11/0.43 ($false = ((c_2Ebool_2E_2F_5C @ (c_2Eoption_2EIS__SOME @ sK3 @ sF14) @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)))) | spl19_1),
% 1.11/0.43 inference(forward_subsumption_resolution,[],[f922,f162])).
% 1.11/0.43 thf(f936,plain,(
% 1.11/0.43 ($false = ((c_2Ebool_2E_2F_5C @ $true @ (c_2Eoption_2EIS__SOME @ sK4 @ sF12)))) | spl19_1),
% 1.11/0.43 inference(forward_demodulation,[],[f929,f250])).
% 1.11/0.43 thf(f937,plain,(
% 1.11/0.43 ($false = ((c_2Ebool_2E_2F_5C @ $true @ $true))) | spl19_1),
% 1.11/0.43 inference(forward_demodulation,[],[f936,f249])).
% 1.11/0.43 thf(f940,plain,(
% 1.11/0.43 ($true = $false) | spl19_1),
% 1.11/0.43 inference(constrained_superposition,[],[f937,f112])).
% 1.11/0.43 thf(f948,plain,(
% 1.11/0.43 $false | spl19_1),
% 1.11/0.43 inference(trivial_inequality_removal,[],[f940])).
% 1.11/0.43 thf(f949,plain,(
% 1.11/0.43 spl19_1),
% 1.11/0.43 inference(avatar_contradiction_clause,[],[f948])).
% 1.11/0.43 cnf(s1, plain, ~spl19_1 | ~spl19_2 | ~spl19_3 | ~spl19_4, inference(sat_conversion,[],[f175])).
% 1.11/0.43 cnf(s3, plain, spl19_7 | spl19_8, inference(sat_conversion,[],[f191])).
% 1.11/0.43 cnf(s5, plain, ~spl19_8 | spl19_9, inference(sat_conversion,[],[f196])).
% 1.11/0.43 cnf(s6, plain, spl19_6 | spl19_8, inference(sat_conversion,[],[f214])).
% 1.11/0.43 cnf(s24, plain, ~spl19_9, inference(sat_conversion,[],[f474])).
% 1.11/0.43 cnf(s51, plain, spl19_3 | ~spl19_6 | ~spl19_7, inference(sat_conversion,[],[f823])).
% 1.11/0.43 cnf(s52, plain, spl19_4 | ~spl19_6 | ~spl19_7, inference(sat_conversion,[],[f824])).
% 1.11/0.43 cnf(s53, plain, spl19_2 | ~spl19_6 | ~spl19_7, inference(sat_conversion,[],[f872])).
% 1.11/0.43 cnf(s56, plain, spl19_1, inference(sat_conversion,[],[f949])).
% 1.11/0.43 cnf(s86, plain, ~spl19_8, inference(rat,[],[s5,s24])).
% 1.11/0.43 cnf(s87, plain, spl19_6, inference(rat,[],[s6,s86])).
% 1.11/0.43 cnf(s88, plain, spl19_7, inference(rat,[],[s3,s86])).
% 1.11/0.43 cnf(s90, plain, spl19_2, inference(rat,[],[s53,s87,s88])).
% 1.11/0.43 cnf(s91, plain, spl19_4, inference(rat,[],[s52,s87,s88])).
% 1.11/0.43 cnf(s92, plain, spl19_3, inference(rat,[],[s51,s87,s88])).
% 1.11/0.43 cnf(s93, plain, $false, inference(rat,[],[s1,s91,s92,s90,s56])).
% 1.11/0.43 thf(f951,plain,(
% 1.11/0.43 $false),
% 1.11/0.43 inference(avatar_sat_refutation,[],[s93])).
% 1.11/0.43 % SZS output end Proof for theBenchmark
% 1.11/0.43 % (511572)------------------------------
% 1.11/0.43 % (511572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.11/0.43 % (511572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.11/0.43 % (511572)CaDiCaL version: 2.1.3
% 1.11/0.43 % (511572)Termination reason: Refutation
% 1.11/0.43 % (511572)Time elapsed: 0.048 s
% 1.11/0.43 % (511572)Peak memory usage: 13 MB
% 1.11/0.43 % (511572)Instructions burned: 68 (million)
% 1.11/0.43 % (511542)Success in time 0.203 s
% 1.11/0.43 % Vampire exiting
%------------------------------------------------------------------------------