%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP087^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:10:39 AM UTC 2026
% Result : Theorem 216.34s 30.76s
% Output : Refutation 216.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP087^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n017.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 19:47:37 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.99/1.35 % (809638)Will run a generic schedule for satisfiability detection.
% 6.99/1.35 % (809656)% WARNING: option uhcvi not known.
% 6.99/1.35 % (809658)dis+10_1_sil=32000:sp=arity:random_seed=353475171:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.99/1.35 % (809655)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3331357393_2999 on theBenchmark for (2999ds/0Mi)
% 6.99/1.35 % (809656)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3540896115:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.99/1.35 % (809657)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=995149603:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.99/1.35 % (809660)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2848934071:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.99/1.35 % (809659)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4000757706:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.99/1.35 % (809661)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2420883353:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.99/1.35 % (809656)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.99/1.35 % (809659)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.99/1.35 % (809658)Instruction limit reached!
% 6.99/1.35 % (809658)------------------------------
% 6.99/1.35 % (809658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.35 % (809658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.35 % (809658)CaDiCaL version: 2.1.3
% 6.99/1.35 % (809658)Termination reason: Instruction limit
% 6.99/1.35 % (809658)Termination phase: Property scanning
% 6.99/1.35 % (809658)Time elapsed: 0.044 s
% 6.99/1.35 % (809658)Peak memory usage: 11 MB
% 6.99/1.35 % (809658)Instructions burned: 104 (million)
% 6.99/1.35 % (809659)Instruction limit reached!
% 6.99/1.35 % (809659)------------------------------
% 6.99/1.35 % (809659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.35 % (809659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.35 % (809659)CaDiCaL version: 2.1.3
% 6.99/1.35 % (809659)Termination reason: Instruction limit
% 6.99/1.35 % (809659)Termination phase: Property scanning
% 6.99/1.35 % (809659)Time elapsed: 0.049 s
% 6.99/1.35 % (809659)Peak memory usage: 11 MB
% 6.99/1.35 % (809659)Instructions burned: 118 (million)
% 6.99/1.35 % Exception at run slice level
% 6.99/1.35 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.99/1.35 % (809660)Instruction limit reached!
% 6.99/1.35 % (809660)------------------------------
% 6.99/1.35 % (809660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.35 % (809660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.35 % (809656)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.99/1.35 % (809660)CaDiCaL version: 2.1.3
% 6.99/1.35 % (809660)Termination reason: Instruction limit
% 6.99/1.35 % (809660)Termination phase: Saturation
% 6.99/1.35 % (809660)Time elapsed: 0.055 s
% 6.99/1.35 % (809660)Peak memory usage: 11 MB
% 6.99/1.35 % (809660)Instructions burned: 132 (million)
% 6.99/1.35 % (809695)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2212718812:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.99/1.35 % (809700)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3411383725:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.99/1.35 % (809661)Instruction limit reached!
% 6.99/1.35 % (809661)------------------------------
% 6.99/1.35 % (809661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.99/1.35 % (809661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.99/1.35 % (809661)CaDiCaL version: 2.1.3
% 6.99/1.35 % (809661)Termination reason: Instruction limit
% 6.99/1.35 % (809661)Termination phase: Saturation
% 6.99/1.35 % (809661)Time elapsed: 0.066 s
% 6.99/1.35 % (809661)Peak memory usage: 12 MB
% 6.99/1.35 % (809661)Instructions burned: 160 (million)
% 6.99/1.35 % (809703)ott-21_1_sil=16000:fs=off:random_seed=3784350818:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 6.99/1.35 % (809701)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=2741869677:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 35.13/5.27 % (809707)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=747423267:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 35.13/5.27 % (809700)Instruction limit reached!
% 35.13/5.27 % (809700)------------------------------
% 35.13/5.27 % (809700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.13/5.27 % (809700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.13/5.27 % (809700)CaDiCaL version: 2.1.3
% 35.13/5.27 % (809700)Termination reason: Instruction limit
% 35.13/5.27 % (809700)Termination phase: Saturation
% 35.13/5.27 % (809700)Time elapsed: 0.030 s
% 35.13/5.27 % (809700)Peak memory usage: 13 MB
% 35.13/5.27 % (809700)Instructions burned: 135 (million)
% 35.13/5.27 % (809716)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1793179538:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 35.13/5.27 % (809701)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.13/5.27 % Exception at run slice level
% 35.13/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.13/5.27 % (809724)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3637172558:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 35.13/5.27 % Exception at run slice level
% 35.13/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.13/5.27 % (809701)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.13/5.27 % (809731)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1493749929:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 35.13/5.27 % (809703)Instruction limit reached!
% 35.13/5.27 % (809703)------------------------------
% 35.13/5.27 % (809703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.13/5.27 % (809703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.13/5.27 % (809703)CaDiCaL version: 2.1.3
% 35.13/5.27 % (809703)Termination reason: Instruction limit
% 35.13/5.27 % (809703)Termination phase: Saturation
% 35.13/5.27 % (809703)Time elapsed: 0.078 s
% 35.13/5.27 % (809703)Peak memory usage: 13 MB
% 35.13/5.27 % (809703)Instructions burned: 185 (million)
% 35.13/5.27 % (809734)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3473583845:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 35.13/5.27 % Exception at run slice level
% 35.13/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.13/5.27 % (809734)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.13/5.27 % (809749)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3813467015:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 35.13/5.27 % (809749)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.13/5.27 % (809707)Instruction limit reached!
% 35.13/5.27 % (809707)------------------------------
% 35.13/5.27 % (809707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.13/5.27 % (809707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.13/5.27 % (809707)CaDiCaL version: 2.1.3
% 35.13/5.27 % (809707)Termination reason: Instruction limit
% 35.13/5.27 % (809707)Termination phase: Saturation
% 35.13/5.27 % (809707)Time elapsed: 0.233 s
% 35.13/5.27 % (809707)Peak memory usage: 15 MB
% 35.13/5.27 % (809707)Instructions burned: 478 (million)
% 35.13/5.27 % (809774)fmb+10_1_sil=64000:random_seed=1770512867:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 35.13/5.27 % (809774)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 35.13/5.27 % Exception at run slice level
% 35.13/5.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.13/5.27 % (809701)Instruction limit reached!
% 35.13/5.27 % (809701)------------------------------
% 35.13/5.27 % (809701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.13/5.27 % (809701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.13/5.27 % (809701)CaDiCaL version: 2.1.3
% 35.13/5.27 % (809701)Termination reason: Instruction limit
% 86.90/12.52 % (809701)Termination phase: Saturation
% 86.90/12.52 % (809701)Time elapsed: 0.345 s
% 86.90/12.52 % (809701)Peak memory usage: 16 MB
% 86.90/12.52 % (809701)Instructions burned: 684 (million)
% 86.90/12.52 % (809794)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4216164097:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 86.90/12.52 % (809796)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1815771895:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 86.90/12.52 % Exception at run slice level
% 86.90/12.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 86.90/12.52 % Exception at run slice level
% 86.90/12.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 86.90/12.52 % (809809)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=683079445:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 86.90/12.52 % (809734)Instruction limit reached!
% 86.90/12.52 % (809734)------------------------------
% 86.90/12.52 % (809734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.90/12.52 % (809734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.90/12.52 % (809734)CaDiCaL version: 2.1.3
% 86.90/12.52 % (809734)Termination reason: Instruction limit
% 86.90/12.52 % (809734)Termination phase: Saturation
% 86.90/12.52 % (809734)Time elapsed: 0.406 s
% 86.90/12.52 % (809734)Peak memory usage: 19 MB
% 86.90/12.52 % (809734)Instructions burned: 693 (million)
% 86.90/12.52 % (809815)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1642367912:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 86.90/12.52 % (809809)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 86.90/12.52 % (809819)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2237647416:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 86.90/12.52 % (809815)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 86.90/12.52 % (809815)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 86.90/12.52 % Exception at run slice level
% 86.90/12.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 86.90/12.52 % (809827)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2550875740:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 86.90/12.52 % (809749)Instruction limit reached!
% 86.90/12.52 % (809749)------------------------------
% 86.90/12.52 % (809749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.90/12.52 % (809749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.90/12.52 % (809749)CaDiCaL version: 2.1.3
% 86.90/12.52 % (809749)Termination reason: Instruction limit
% 86.90/12.52 % (809749)Termination phase: Saturation
% 86.90/12.52 % (809749)Time elapsed: 0.586 s
% 86.90/12.52 % (809749)Peak memory usage: 18 MB
% 86.90/12.52 % (809749)Instructions burned: 879 (million)
% 86.90/12.52 % (809831)ott-2_1_sil=16000:newcnf=on:random_seed=4249160227:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 86.90/12.52 % Exception at run slice level
% 86.90/12.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 86.90/12.52 % (809831)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 86.90/12.52 % (809724)Instruction limit reached!
% 86.90/12.52 % (809724)------------------------------
% 86.90/12.52 % (809724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 86.90/12.52 % (809724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.90/12.52 % (809724)CaDiCaL version: 2.1.3
% 86.90/12.52 % (809724)Termination reason: Instruction limit
% 86.90/12.52 % (809724)Termination phase: Saturation
% 86.90/12.52 % (809724)Time elapsed: 0.742 s
% 86.90/12.52 % (809724)Peak memory usage: 22 MB
% 86.90/12.52 % (809724)Instructions burned: 1180 (million)
% 86.90/12.52 % (809835)ott+10_1_sil=32000:tgt=ground:random_seed=898292017:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi)
% 86.90/12.52 % (809837)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=576244946:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 86.90/12.52 % Exception at run slice level
% 86.90/12.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 86.90/12.52 % (809845)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1762884077:i=3512:aac=none_2989 on theBenchmark for (2989ds/3512Mi)
% 197.62/28.10 % (809845)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 197.62/28.10 % (809831)Instruction limit reached!
% 197.62/28.10 % (809831)------------------------------
% 197.62/28.10 % (809831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.62/28.10 % (809831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.62/28.10 % (809831)CaDiCaL version: 2.1.3
% 197.62/28.10 % (809831)Termination reason: Instruction limit
% 197.62/28.10 % (809831)Termination phase: Saturation
% 197.62/28.10 % (809831)Time elapsed: 0.594 s
% 197.62/28.10 % (809831)Peak memory usage: 20 MB
% 197.62/28.10 % (809831)Instructions burned: 869 (million)
% 197.62/28.10 % (809857)dis+21_1_sil=32000:sas=cadical:random_seed=3124197933:i=3773:amm=off_2985 on theBenchmark for (2985ds/3773Mi)
% 197.62/28.10 % (809815)Instruction limit reached!
% 197.62/28.10 % (809815)------------------------------
% 197.62/28.10 % (809815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.62/28.10 % (809815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.62/28.10 % (809815)CaDiCaL version: 2.1.3
% 197.62/28.10 % (809815)Termination reason: Instruction limit
% 197.62/28.10 % (809815)Termination phase: Saturation
% 197.62/28.10 % (809815)Time elapsed: 1.213 s
% 197.62/28.10 % (809815)Peak memory usage: 17 MB
% 197.62/28.10 % (809815)Instructions burned: 1473 (million)
% 197.62/28.10 % (809867)ott+11_1_sil=16000:gs=on:random_seed=1129134482:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2981 on theBenchmark for (2981ds/2251Mi)
% 197.62/28.10 % (809867)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 197.62/28.10 % (809867)Instruction limit reached!
% 197.62/28.10 % (809867)------------------------------
% 197.62/28.10 % (809867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.62/28.10 % (809867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.62/28.10 % (809867)CaDiCaL version: 2.1.3
% 197.62/28.10 % (809867)Termination reason: Instruction limit
% 197.62/28.10 % (809867)Termination phase: Saturation
% 197.62/28.10 % (809867)Time elapsed: 1.696 s
% 197.62/28.10 % (809867)Peak memory usage: 20 MB
% 197.62/28.10 % (809867)Instructions burned: 2251 (million)
% 197.62/28.10 % (809875)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3139085572:fmbsr=1.6:i=67534_2964 on theBenchmark for (2964ds/67534Mi)
% 197.62/28.10 % Exception at run slice level
% 197.62/28.10 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 197.62/28.10 % (809877)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3241512900:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2963 on theBenchmark for (2963ds/4591Mi)
% 197.62/28.10 % (809845)Instruction limit reached!
% 197.62/28.10 % (809845)------------------------------
% 197.62/28.10 % (809845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.62/28.10 % (809845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.62/28.10 % (809845)CaDiCaL version: 2.1.3
% 197.62/28.10 % (809845)Termination reason: Instruction limit
% 197.62/28.10 % (809845)Termination phase: Saturation
% 197.62/28.10 % (809845)Time elapsed: 2.802 s
% 197.62/28.10 % (809845)Peak memory usage: 28 MB
% 197.62/28.10 % (809845)Instructions burned: 3512 (million)
% 197.62/28.10 % (809879)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3735149614:i=29340_2960 on theBenchmark for (2960ds/29340Mi)
% 197.62/28.10 % (809857)Instruction limit reached!
% 197.62/28.10 % (809857)------------------------------
% 197.62/28.10 % (809857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 197.62/28.10 % (809857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.62/28.10 % (809857)CaDiCaL version: 2.1.3
% 197.62/28.10 % (809857)Termination reason: Instruction limit
% 197.62/28.10 % (809857)Termination phase: Saturation
% 197.62/28.10 % (809857)Time elapsed: 3.128 s
% 197.62/28.10 % (809857)Peak memory usage: 28 MB
% 197.62/28.10 % (809857)Instructions burned: 3773 (million)
% 197.62/28.10 % (809885)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1489637962:i=5211_2953 on theBenchmark for (2953ds/5211Mi)
% 197.62/28.10 % (809809)Instruction limit reached!
% 197.62/28.10 % (809809)------------------------------
% 197.62/28.10 % (809809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809809)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809809)Termination reason: Instruction limit
% 216.34/30.76 % (809809)Termination phase: Saturation
% 216.34/30.76 % (809809)Time elapsed: 4.400 s
% 216.34/30.76 % (809809)Peak memory usage: 28 MB
% 216.34/30.76 % (809809)Instructions burned: 5131 (million)
% 216.34/30.76 % (809887)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=393726358:i=5497:nm=2_2949 on theBenchmark for (2949ds/5497Mi)
% 216.34/30.76 % (809835)Instruction limit reached!
% 216.34/30.76 % (809835)------------------------------
% 216.34/30.76 % (809835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809835)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809835)Termination reason: Instruction limit
% 216.34/30.76 % (809835)Termination phase: Saturation
% 216.34/30.76 % (809835)Time elapsed: 4.197 s
% 216.34/30.76 % (809835)Peak memory usage: 45 MB
% 216.34/30.76 % (809835)Instructions burned: 5114 (million)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809889)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=975754649:fmbsr=2:i=46332_2948 on theBenchmark for (2948ds/46332Mi)
% 216.34/30.76 % (809890)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=418229826:i=14071_2948 on theBenchmark for (2948ds/14071Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809893)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2777048416:i=22565:add=on:rawr=on_2947 on theBenchmark for (2947ds/22565Mi)
% 216.34/30.76 % (809894)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3389514020:i=8173:av=off_2947 on theBenchmark for (2947ds/8173Mi)
% 216.34/30.76 % (809877)Instruction limit reached!
% 216.34/30.76 % (809877)------------------------------
% 216.34/30.76 % (809877)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809877)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809877)Termination reason: Instruction limit
% 216.34/30.76 % (809877)Termination phase: Saturation
% 216.34/30.76 % (809877)Time elapsed: 4.022 s
% 216.34/30.76 % (809877)Peak memory usage: 31 MB
% 216.34/30.76 % (809877)Instructions burned: 4591 (million)
% 216.34/30.76 % (809909)dis+10_16:1_sil=16000:random_seed=2390738976:i=9155:fsr=off_2922 on theBenchmark for (2922ds/9155Mi)
% 216.34/30.76 % (809885)Instruction limit reached!
% 216.34/30.76 % (809885)------------------------------
% 216.34/30.76 % (809885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809885)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809885)Termination reason: Instruction limit
% 216.34/30.76 % (809885)Termination phase: Saturation
% 216.34/30.76 % (809885)Time elapsed: 4.441 s
% 216.34/30.76 % (809885)Peak memory usage: 43 MB
% 216.34/30.76 % (809885)Instructions burned: 5212 (million)
% 216.34/30.76 % (809913)ott-3_8_sil=64000:random_seed=1391665082:i=20139:bs=on_2909 on theBenchmark for (2909ds/20139Mi)
% 216.34/30.76 % (809894)Instruction limit reached!
% 216.34/30.76 % (809894)------------------------------
% 216.34/30.76 % (809894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809894)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809894)Termination reason: Instruction limit
% 216.34/30.76 % (809894)Termination phase: Saturation
% 216.34/30.76 % (809894)Time elapsed: 6.786 s
% 216.34/30.76 % (809894)Peak memory usage: 46 MB
% 216.34/30.76 % (809894)Instructions burned: 8173 (million)
% 216.34/30.76 % (809919)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3324908268:fmbsr=2:i=32576_2878 on theBenchmark for (2878ds/32576Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809921)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=660987723:i=11404_2877 on theBenchmark for (2877ds/11404Mi)
% 216.34/30.76 % (809909)Instruction limit reached!
% 216.34/30.76 % (809909)------------------------------
% 216.34/30.76 % (809909)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809909)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809909)Termination reason: Instruction limit
% 216.34/30.76 % (809909)Termination phase: Saturation
% 216.34/30.76 % (809909)Time elapsed: 7.857 s
% 216.34/30.76 % (809909)Peak memory usage: 45 MB
% 216.34/30.76 % (809909)Instructions burned: 9156 (million)
% 216.34/30.76 % (809928)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3979228893:i=14134_2843 on theBenchmark for (2843ds/14134Mi)
% 216.34/30.76 % (809928)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 216.34/30.76 % (809893)Instruction limit reached!
% 216.34/30.76 % (809893)------------------------------
% 216.34/30.76 % (809893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809893)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809893)Termination reason: Instruction limit
% 216.34/30.76 % (809893)Termination phase: Saturation
% 216.34/30.76 % (809893)Time elapsed: 12.141 s
% 216.34/30.76 % (809893)Peak memory usage: 22 MB
% 216.34/30.76 % (809893)Instructions burned: 22566 (million)
% 216.34/30.76 % (809930)dis+33_16_sil=32000:sac=on:random_seed=1004798051:i=15851:nm=0_2825 on theBenchmark for (2825ds/15851Mi)
% 216.34/30.76 % (809921)Instruction limit reached!
% 216.34/30.76 % (809921)------------------------------
% 216.34/30.76 % (809921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809921)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809921)Termination reason: Instruction limit
% 216.34/30.76 % (809921)Termination phase: Saturation
% 216.34/30.76 % (809921)Time elapsed: 9.610 s
% 216.34/30.76 % (809921)Peak memory usage: 71 MB
% 216.34/30.76 % (809921)Instructions burned: 11404 (million)
% 216.34/30.76 % (809954)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=560425261:avsq=on:i=17627:add=on:amm=off_2780 on theBenchmark for (2780ds/17627Mi)
% 216.34/30.76 % (809913)Instruction limit reached!
% 216.34/30.76 % (809913)------------------------------
% 216.34/30.76 % (809913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809913)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809913)Termination reason: Instruction limit
% 216.34/30.76 % (809913)Termination phase: Saturation
% 216.34/30.76 % (809913)Time elapsed: 16.124 s
% 216.34/30.76 % (809913)Peak memory usage: 50 MB
% 216.34/30.76 % (809913)Instructions burned: 20141 (million)
% 216.34/30.76 % (809958)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1732921725:s2a=on:i=53295_2747 on theBenchmark for (2747ds/53295Mi)
% 216.34/30.76 % (809879)Instruction limit reached!
% 216.34/30.76 % (809879)------------------------------
% 216.34/30.76 % (809879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809879)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809879)Termination reason: Instruction limit
% 216.34/30.76 % (809879)Termination phase: Saturation
% 216.34/30.76 % (809879)Time elapsed: 22.134 s
% 216.34/30.76 % (809879)Peak memory usage: 35 MB
% 216.34/30.76 % (809879)Instructions burned: 29341 (million)
% 216.34/30.76 % (809960)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3939411631:i=26857:ins=20_2739 on theBenchmark for (2739ds/26857Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809962)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2863398204:i=28120:bs=on:fsr=off_2737 on theBenchmark for (2737ds/28120Mi)
% 216.34/30.76 % (809928)Instruction limit reached!
% 216.34/30.76 % (809928)------------------------------
% 216.34/30.76 % (809928)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809928)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809928)Termination reason: Instruction limit
% 216.34/30.76 % (809928)Termination phase: Saturation
% 216.34/30.76 % (809928)Time elapsed: 12.186 s
% 216.34/30.76 % (809928)Peak memory usage: 77 MB
% 216.34/30.76 % (809928)Instructions burned: 14135 (million)
% 216.34/30.76 % (809970)fmb+10_1_sil=256000:fmbss=7:random_seed=804987707:fmbsr=1.6:i=182295_2721 on theBenchmark for (2721ds/182295Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809974)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=906837308:i=44625:gsp=on_2720 on theBenchmark for (2720ds/44625Mi)
% 216.34/30.76 % (809974)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 216.34/30.76 % (809974)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809976)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=512059935:i=160505_2719 on theBenchmark for (2719ds/160505Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809978)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1082420663:fmbsr=1.3:i=225729_2718 on theBenchmark for (2718ds/225729Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809981)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2673845611:fmbsr=2:i=185024:ins=7_2718 on theBenchmark for (2718ds/185024Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809984)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2278634591:rtra=on_2717 on theBenchmark for (2717ds/0Mi)
% 216.34/30.76 % Exception at run slice level
% 216.34/30.76 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 216.34/30.76 % (809988)% WARNING: option uhcvi not known.
% 216.34/30.76 % (809988)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1013991925:i=271062:add=off:rtra=on:rawr=on_2716 on theBenchmark for (2716ds/271062Mi)
% 216.34/30.76 % (809988)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 216.34/30.76 % (809988)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 216.34/30.76 % (809930)Instruction limit reached!
% 216.34/30.76 % (809930)------------------------------
% 216.34/30.76 % (809930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.76 % (809930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.76 % (809930)CaDiCaL version: 2.1.3
% 216.34/30.76 % (809930)Termination reason: Instruction limit
% 216.34/30.76 % (809930)Termination phase: Saturation
% 216.34/30.76 % (809930)Time elapsed: 12.748 s
% 216.34/30.76 % (809930)Peak memory usage: 39 MB
% 216.34/30.76 % (809930)Instructions burned: 15851 (million)
% 216.34/30.76 % (810000)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=144497737:i=176048:add=on:rtra=on:rawr=on_2697 on theBenchmark for (2697ds/176048Mi)
% 216.34/30.76 % (809656) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-809638-809656"...
% 216.34/30.76 % (809656)...printing done.
% 216.34/30.76 % (809656)Refutation found. Thanks to Tanya!
% 216.34/30.76 % SZS status Theorem for theBenchmark
% 216.34/30.76 % SZS output start Proof for theBenchmark
% 216.34/30.76 thf(type_def_5, type, secrecy_Expression: $tType).
% 216.34/30.76 thf(type_def_6, type, secrecy_Secrets: $tType).
% 216.34/30.76 thf(type_def_7, type, secrecy_specID: $tType).
% 216.34/30.76 thf(type_def_8, type, secrecy_chanID: $tType).
% 216.34/30.76 thf(type_def_9, type, secrecy_Keys: $tType).
% 216.34/30.76 thf(type_def_10, type, secrecy_KS: $tType).
% 216.34/30.76 thf(type_def_11, type, list: $tType > $tType).
% 216.34/30.76 thf(type_def_12, type, set: $tType > $tType).
% 216.34/30.76 thf(type_def_13, type, nat: $tType).
% 216.34/30.76 thf(type_def_14, type, sTfun: ($tType * $tType) > $tType).
% 216.34/30.76 thf(func_def_0, type, bounded_lattice: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_2, type, bot: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_3, type, ord: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_4, type, order: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_5, type, linorder: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_6, type, preorder: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_7, type, order_bot: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_8, type, bounde1808546759up_bot: !>[X0: $tType]:($o)).
% 216.34/30.76 thf(func_def_9, type, localSecrets: (secrecy_specID > set @ secrecy_KS)).
% 216.34/30.76 thf(func_def_10, type, knowle1667810483orrect: (secrecy_specID > secrecy_KS > $o)).
% 216.34/30.76 thf(func_def_11, type, knowle1437066798e_know: (secrecy_specID > secrecy_KS > $o)).
% 216.34/30.76 thf(func_def_12, type, sup_sup: !>[X0: $tType]:((X0 > X0 > X0))).
% 216.34/30.76 thf(func_def_13, type, mem: !>[X0: $tType]:((X0 > list @ X0 > $o))).
% 216.34/30.76 thf(func_def_14, type, bot_bot: !>[X0: $tType]:(X0)).
% 216.34/30.76 thf(func_def_15, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 216.34/30.76 thf(func_def_16, type, correctCompositionKS: (secrecy_specID > $o)).
% 216.34/30.76 thf(func_def_17, type, correc17873122onKeys: (secrecy_specID > $o)).
% 216.34/30.76 thf(func_def_18, type, eout: (secrecy_specID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_19, type, eoutM: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_20, type, exprChannel: (secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_21, type, ine: (secrecy_specID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_22, type, ineM: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_23, type, ine_exprChannelSet: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_24, type, ine_ex1303305700Single: (secrecy_specID > secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_25, type, notSpe1586871396tsExpr: (secrecy_specID > list @ secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_26, type, out_exprChannelSet: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_27, type, out_ex985543062Single: (secrecy_specID > secrecy_chanID > secrecy_Expression > $o)).
% 216.34/30.76 thf(func_def_28, type, specKeys: (secrecy_specID > set @ secrecy_Keys)).
% 216.34/30.76 thf(func_def_29, type, specKeysSecrets: (secrecy_specID > set @ secrecy_KS)).
% 216.34/30.76 thf(func_def_30, type, specSecrets: (secrecy_specID > set @ secrecy_Secrets)).
% 216.34/30.76 thf(func_def_31, type, secrecy_kE: (secrecy_Keys > secrecy_Expression)).
% 216.34/30.76 thf(func_def_32, type, secrecy_sE: (secrecy_Secrets > secrecy_Expression)).
% 216.34/30.76 thf(func_def_33, type, secrec1016742679ession: (secrecy_KS > secrecy_Expression)).
% 216.34/30.76 thf(func_def_34, type, secrecy_kKS: (secrecy_Keys > secrecy_KS)).
% 216.34/30.76 thf(func_def_35, type, secrecy_sKS: (secrecy_Secrets > secrecy_KS)).
% 216.34/30.76 thf(func_def_36, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 216.34/30.76 thf(func_def_37, type, insert: !>[X0: $tType]:((X0 > set @ X0 > set @ X0))).
% 216.34/30.76 thf(func_def_38, type, is_empty: !>[X0: $tType]:((set @ X0 > $o))).
% 216.34/30.76 thf(func_def_39, type, is_singleton: !>[X0: $tType]:((set @ X0 > $o))).
% 216.34/30.76 thf(func_def_40, type, the_elem: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.76 thf(func_def_41, type, correctCompositionIn: (secrecy_specID > $o)).
% 216.34/30.76 thf(func_def_42, type, correc965049635ionLoc: (secrecy_specID > $o)).
% 216.34/30.76 thf(func_def_43, type, correc990227761ionOut: (secrecy_specID > $o)).
% 216.34/30.76 thf(func_def_44, type, inStream: (secrecy_specID > set @ secrecy_chanID > $o)).
% 216.34/30.76 thf(func_def_45, type, ins: (secrecy_specID > set @ secrecy_chanID)).
% 216.34/30.76 thf(func_def_46, type, loc: (secrecy_specID > set @ secrecy_chanID)).
% 216.34/30.76 thf(func_def_47, type, locStream: (secrecy_specID > set @ secrecy_chanID > $o)).
% 216.34/30.76 thf(func_def_48, type, out: (secrecy_specID > set @ secrecy_chanID)).
% 216.34/30.76 thf(func_def_49, type, subcomponents: (secrecy_specID > set @ secrecy_specID)).
% 216.34/30.76 thf(func_def_50, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 216.34/30.76 thf(func_def_51, type, p: secrecy_specID).
% 216.34/30.76 thf(func_def_52, type, pq: secrecy_specID).
% 216.34/30.76 thf(func_def_53, type, q: secrecy_specID).
% 216.34/30.76 thf(func_def_54, type, key: secrecy_Keys).
% 216.34/30.76 thf(func_def_55, type, m: secrecy_KS).
% 216.34/30.76 thf(func_def_59, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 216.34/30.76 thf(func_def_60, type, vOR: ($o > $o > $o)).
% 216.34/30.76 thf(func_def_61, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 216.34/30.76 thf(func_def_62, type, vNOT: ($o > $o)).
% 216.34/30.76 thf(func_def_63, type, db0: !>[X0: $tType]:(X0)).
% 216.34/30.76 thf(func_def_64, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 216.34/30.76 thf(func_def_65, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 216.34/30.76 thf(func_def_66, type, vAND: ($o > $o > $o)).
% 216.34/30.76 thf(func_def_67, type, vIMP: ($o > $o > $o)).
% 216.34/30.76 thf(func_def_68, type, db1: !>[X0: $tType]:(X0)).
% 216.34/30.76 thf(func_def_69, type, db2: !>[X0: $tType]:(X0)).
% 216.34/30.76 thf(func_def_70, type, db3: !>[X0: $tType]:(X0)).
% 216.34/30.76 thf(func_def_71, type, sP0: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 216.34/30.76 thf(func_def_72, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 216.34/30.76 thf(func_def_73, type, sP2: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 216.34/30.76 thf(func_def_74, type, sK3: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.76 thf(func_def_75, type, sK4: !>[X0: $tType]:((set @ X0 > X0 > set @ X0))).
% 216.34/30.76 thf(func_def_76, type, sK5: !>[X0: $tType]:((set @ X0 > X0 > set @ X0))).
% 216.34/30.76 thf(func_def_77, type, sK6: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_78, type, sK7: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_79, type, sK8: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.76 thf(func_def_80, type, sK9: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.76 thf(func_def_81, type, sK10: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.76 thf(func_def_82, type, sK11: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_83, type, sK12: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_84, type, sK13: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_85, type, sK14: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_86, type, sK15: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_87, type, sK16: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_88, type, sK17: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_89, type, sK18: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_90, type, sK19: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_91, type, sK20: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_92, type, sK21: (secrecy_KS > secrecy_Secrets)).
% 216.34/30.76 thf(func_def_93, type, sK22: (secrecy_KS > secrecy_Keys)).
% 216.34/30.76 thf(func_def_94, type, sK23: ((secrecy_KS > $o) > secrecy_Secrets)).
% 216.34/30.76 thf(func_def_95, type, sK24: ((secrecy_KS > $o) > secrecy_Keys)).
% 216.34/30.76 thf(func_def_96, type, sK25: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_Secrets)).
% 216.34/30.76 thf(func_def_97, type, sK26: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_Keys)).
% 216.34/30.76 thf(func_def_98, type, sK27: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_Secrets)).
% 216.34/30.76 thf(func_def_99, type, sK28: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_Keys)).
% 216.34/30.76 thf(func_def_100, type, sK29: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_101, type, sK30: (secrecy_Keys > secrecy_specID > secrecy_specID)).
% 216.34/30.76 thf(func_def_102, type, sK31: (secrecy_Secrets > secrecy_specID > secrecy_specID)).
% 216.34/30.76 thf(func_def_103, type, sK32: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_104, type, sK33: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_105, type, sK34: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_106, type, sK35: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_107, type, sK36: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_108, type, sK37: (set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_109, type, sK38: (secrecy_Keys > secrecy_specID > secrecy_specID)).
% 216.34/30.76 thf(func_def_110, type, sK39: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 216.34/30.76 thf(func_def_111, type, sK40: !>[X0: $tType]:((set @ X0 > set @ X0 > set @ X0 > set @ X0))).
% 216.34/30.76 thf(func_def_112, type, sK41: !>[X0: $tType]:((set @ X0 > set @ X0 > set @ X0 > set @ X0))).
% 216.34/30.76 thf(func_def_113, type, sK42: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_114, type, sK43: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_115, type, sK44: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_116, type, sK45: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_117, type, sK46: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 216.34/30.76 thf(func_def_118, type, sK47: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 216.34/30.76 thf(func_def_119, type, sK48: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_120, type, sK49: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_121, type, sK50: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 216.34/30.76 thf(func_def_122, type, sK51: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 216.34/30.76 thf(func_def_123, type, sK52: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_124, type, sK53: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_125, type, sK54: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 216.34/30.76 thf(func_def_126, type, sK55: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_127, type, sK56: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 216.34/30.76 thf(func_def_128, type, sK57: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_129, type, sK58: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_130, type, sK59: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_131, type, sK60: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_132, type, sK61: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_133, type, sK62: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_134, type, sK63: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_135, type, sK64: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_136, type, sK65: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_137, type, sK66: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_138, type, sK67: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_139, type, sK68: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_140, type, sK69: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_141, type, sK70: (secrecy_specID > secrecy_Expression > secrecy_chanID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_142, type, sK71: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_143, type, sK72: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_144, type, sK73: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_145, type, sK74: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_146, type, sK75: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_147, type, sK76: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_148, type, sK77: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_149, type, sK78: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_150, type, sK79: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_151, type, sK80: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_152, type, sK81: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_153, type, sK82: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_154, type, sK83: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_155, type, sK84: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_156, type, sK85: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_157, type, sK86: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_158, type, sK87: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_159, type, sK88: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_160, type, sK89: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_161, type, sK90: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_162, type, sK91: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_163, type, sK92: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_164, type, sK93: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_165, type, sK94: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_166, type, sK95: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_167, type, sK96: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_168, type, sK97: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_169, type, sK98: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_170, type, sK99: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_171, type, sK100: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_172, type, sK101: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_173, type, sK102: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_174, type, sK103: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_175, type, sK104: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_176, type, sK105: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_177, type, sK106: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_178, type, sK107: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_179, type, sK108: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_180, type, sK109: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_181, type, sK110: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_182, type, sK111: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_183, type, sK112: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_184, type, sK113: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_185, type, sK114: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_186, type, sK115: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_187, type, sK116: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_188, type, sK117: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_189, type, sK118: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_190, type, sK119: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_191, type, sK120: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_192, type, sK121: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_193, type, sK122: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_194, type, sK123: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_195, type, sK124: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.76 thf(func_def_196, type, sK125: (secrecy_specID > secrecy_Expression > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_197, type, sK126: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_198, type, sK127: (secrecy_specID > secrecy_Expression > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.76 thf(func_def_199, type, sK128: (secrecy_specID > secrecy_Expression > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_200, type, sK129: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_201, type, sK130: (secrecy_specID > secrecy_Expression > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_202, type, sK131: (secrecy_Expression > secrecy_specID > secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_203, type, sK132: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_204, type, sK133: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_205, type, sK134: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_206, type, sK135: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_207, type, sK136: (secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_208, type, sK137: (set @ secrecy_chanID > set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_209, type, sK138: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_210, type, sK139: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_211, type, sK140: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_212, type, sK141: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_213, type, sK142: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_214, type, sK143: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_215, type, sK144: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_216, type, sK145: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_217, type, sK146: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_218, type, sK147: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_219, type, sK148: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_220, type, sK149: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_221, type, sK150: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_222, type, sK151: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_223, type, sK152: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_224, type, sK153: (secrecy_KS > secrecy_specID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_225, type, sK154: (secrecy_specID > secrecy_Secrets > secrecy_chanID)).
% 216.34/30.77 thf(func_def_226, type, sK155: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_227, type, sK156: (secrecy_specID > secrecy_Secrets > secrecy_chanID)).
% 216.34/30.77 thf(func_def_228, type, sK157: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_229, type, sK158: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_230, type, sK159: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_231, type, sK160: (secrecy_specID > secrecy_Secrets > secrecy_chanID)).
% 216.34/30.77 thf(func_def_232, type, sK161: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_233, type, sK162: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_234, type, sK163: (secrecy_specID > secrecy_Secrets > secrecy_chanID)).
% 216.34/30.77 thf(func_def_235, type, sK164: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_236, type, sK165: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_237, type, sK166: (secrecy_Secrets > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_238, type, sK167: !>[X0: $tType]:((set @ X0 > set @ X0 > (X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_239, type, sK168: !>[X0: $tType]:((set @ X0 > (X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_240, type, sK169: !>[X0: $tType]:((set @ X0 > (X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_241, type, sK170: !>[X0: $tType]:((set @ X0 > (X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_242, type, sK171: !>[X0: $tType]:((set @ X0 > (X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_243, type, sK172: !>[X0: $tType]:((set @ X0 > (X0 > $o) > set @ X0 > X0))).
% 216.34/30.77 thf(func_def_244, type, sK173: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_245, type, sK174: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_246, type, sK175: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_247, type, sK176: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_248, type, sK177: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_249, type, sK178: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_250, type, sK179: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_251, type, sK180: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_252, type, sK181: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_253, type, sK182: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_254, type, sK183: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_255, type, sK184: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_256, type, sK185: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_257, type, sK186: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_258, type, sK187: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_259, type, sK188: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_260, type, sK189: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_261, type, sK190: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_262, type, sK191: (secrecy_Expression > secrecy_specID > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_263, type, sK192: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_264, type, sK193: (secrecy_Expression > secrecy_specID > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_265, type, sK194: (secrecy_Expression > secrecy_specID > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_266, type, sK195: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_267, type, sK196: (secrecy_Expression > secrecy_specID > set @ secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_268, type, sK197: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_269, type, sK198: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_270, type, sK199: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_271, type, sK200: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_272, type, sK201: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_273, type, sK202: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_274, type, sK203: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_275, type, sK204: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_276, type, sK205: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_277, type, sK206: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_278, type, sK207: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_279, type, sK208: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_280, type, sK209: (secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_281, type, sK210: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_282, type, sK211: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_283, type, sK212: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_284, type, sK213: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_285, type, sK214: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_286, type, sK215: (secrecy_Expression > set @ secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_287, type, sK216: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_288, type, sK217: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_289, type, sK218: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_290, type, sK219: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_291, type, sK220: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_292, type, sK221: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_293, type, sK222: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_294, type, sK223: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_295, type, sK224: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_296, type, sK225: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_297, type, sK226: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_298, type, sK227: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_299, type, sK228: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_300, type, sK229: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_301, type, sK230: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_302, type, sK231: (secrecy_specID > set @ secrecy_chanID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_303, type, sK232: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_304, type, sK233: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_305, type, sK234: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_306, type, sK235: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_307, type, sK236: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_308, type, sK237: (secrecy_specID > secrecy_Keys > secrecy_chanID)).
% 216.34/30.77 thf(func_def_309, type, sK238: (secrecy_Expression > secrecy_specID > secrecy_chanID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_310, type, sK239: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_311, type, sK240: (secrecy_Expression > secrecy_chanID > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_312, type, sK241: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_313, type, sK242: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_314, type, sK243: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_315, type, sK244: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_316, type, sK245: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_317, type, sK246: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_318, type, sK247: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_319, type, sK248: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_320, type, sK249: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_321, type, sK250: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_322, type, sK251: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_323, type, sK252: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_324, type, sK253: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_325, type, sK254: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_326, type, sK255: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_327, type, sK256: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_328, type, sK257: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_329, type, sK258: (secrecy_Keys > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_330, type, sK259: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_331, type, sK260: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_332, type, sK261: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_333, type, sK262: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_334, type, sK263: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_335, type, sK264: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_336, type, sK265: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_337, type, sK266: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_338, type, sK267: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_339, type, sK268: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_340, type, sK269: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_341, type, sK270: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_342, type, sK271: (secrecy_Expression > secrecy_specID > secrecy_chanID)).
% 216.34/30.77 thf(func_def_343, type, sK272: secrecy_chanID).
% 216.34/30.77 thf(func_def_344, type, sK273: secrecy_chanID).
% 216.34/30.77 thf(func_def_345, type, sK274: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_346, type, sK275: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_347, type, sK276: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_348, type, sK277: (set @ secrecy_chanID > secrecy_specID > secrecy_Expression > secrecy_chanID)).
% 216.34/30.77 thf(func_def_349, type, sK278: secrecy_chanID).
% 216.34/30.77 thf(func_def_350, type, sK279: !>[X0: $tType]:((X0 > X0))).
% 216.34/30.77 thf(func_def_351, type, sK280: !>[X0: $tType]:((X0 > set @ X0 > X0 > set @ X0 > set @ X0))).
% 216.34/30.77 thf(func_def_352, type, sK281: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_353, type, sK282: !>[X0: $tType]:(((X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_354, type, sK283: !>[X0: $tType]:(((X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_355, type, sK284: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_357, type, db4: !>[X0: $tType]:(X0)).
% 216.34/30.77 thf(func_def_358, type, db5: !>[X0: $tType]:(X0)).
% 216.34/30.77 thf(func_def_359, type, sK286: !>[X0: $tType]:((set @ X0 > X0))).
% 216.34/30.77 thf(func_def_360, type, sK287: !>[X0: $tType]:(((X0 > $o) > X0))).
% 216.34/30.77 thf(func_def_361, type, sK288: !>[X0: $tType]:((set @ X0 > set @ X0 > X0))).
% 216.34/30.77 thf(f1,axiom,(
% 216.34/30.77 (correctCompositionKS @ pq)),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_cCompKS)).
% 216.34/30.77 thf(f2,axiom,(
% 216.34/30.77 ~(member @ secrecy_KS @ m @ (specKeysSecrets @ q))),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_notKSQ)).
% 216.34/30.77 thf(f3,axiom,(
% 216.34/30.77 ~(member @ secrecy_KS @ m @ (specKeysSecrets @ p))),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_notKSP)).
% 216.34/30.77 thf(f4,axiom,(
% 216.34/30.77 (((subcomponents @ pq)) = ((insert @ secrecy_specID @ p @ (insert @ secrecy_specID @ q @ bot_bot @ set @ secrecy_specID))))),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_subPQ)).
% 216.34/30.77 thf(f8,axiom,(
% 216.34/30.77 ! [X0 : secrecy_specID,X1 : secrecy_specID,X2 : secrecy_specID,X3 : secrecy_KS] : ((((subcomponents @ X0)) = ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))) => ((correctCompositionKS @ X0) => ((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0)) => ((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2)) | (member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))))))),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_correctCompositionKS__PQ)).
% 216.34/30.77 thf(f285,conjecture,(
% 216.34/30.77 ~(member @ secrecy_KS @ m @ (specKeysSecrets @ pq))),
% 216.34/30.77 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 216.34/30.77 thf(f286,negated_conjecture,(
% 216.34/30.77 ~ ~(member @ secrecy_KS @ m @ (specKeysSecrets @ pq))),
% 216.34/30.77 inference(negated_conjecture,[status(cth)],[f285])).
% 216.34/30.77 thf(f287,plain,(
% 216.34/30.77 (correctCompositionKS @ pq)),
% 216.34/30.77 inference(rectify,[],[f1])).
% 216.34/30.77 thf(f288,plain,(
% 216.34/30.77 (((correctCompositionKS @ pq)) = $true)),
% 216.34/30.77 inference(fool_elimination,[],[f287])).
% 216.34/30.77 thf(f289,plain,(
% 216.34/30.77 ~(member @ secrecy_KS @ m @ (specKeysSecrets @ q))),
% 216.34/30.77 inference(rectify,[],[f2])).
% 216.34/30.77 thf(f290,plain,(
% 216.34/30.77 ~ (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) = $true)),
% 216.34/30.77 inference(fool_elimination,[],[f289])).
% 216.34/30.77 thf(f291,plain,(
% 216.34/30.77 ~(member @ secrecy_KS @ m @ (specKeysSecrets @ p))),
% 216.34/30.77 inference(rectify,[],[f3])).
% 216.34/30.77 thf(f292,plain,(
% 216.34/30.77 ~ (((member @ secrecy_KS @ m @ (specKeysSecrets @ p))) = $true)),
% 216.34/30.77 inference(fool_elimination,[],[f291])).
% 216.34/30.77 thf(f297,plain,(
% 216.34/30.77 ! [X0 : secrecy_specID,X1 : secrecy_specID,X2 : secrecy_specID,X3 : secrecy_KS] : ((((subcomponents @ X0)) = ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))) => ((correctCompositionKS @ X0) => ((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0)) => ((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2)) | (member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))))))),
% 216.34/30.77 inference(rectify,[],[f8])).
% 216.34/30.77 thf(f298,plain,(
% 216.34/30.77 ! [X0 : secrecy_specID,X1 : secrecy_specID,X2 : secrecy_specID,X3 : secrecy_KS] : ((((subcomponents @ X0)) = ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))) => ((((correctCompositionKS @ X0)) = $true) => ((((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0))) = $true) => ((((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2))) = $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))) = $true)))))),
% 216.34/30.77 inference(fool_elimination,[],[f297])).
% 216.34/30.77 thf(f788,plain,(
% 216.34/30.77 ~ ~(member @ secrecy_KS @ m @ (specKeysSecrets @ pq))),
% 216.34/30.77 inference(rectify,[],[f286])).
% 216.34/30.77 thf(f789,plain,(
% 216.34/30.77 ~ ~ (((member @ secrecy_KS @ m @ (specKeysSecrets @ pq))) = $true)),
% 216.34/30.77 inference(fool_elimination,[],[f788])).
% 216.34/30.77 thf(f790,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) != $true)),
% 216.34/30.77 inference(flattening,[],[f290])).
% 216.34/30.77 thf(f791,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ p))) != $true)),
% 216.34/30.77 inference(flattening,[],[f292])).
% 216.34/30.77 thf(f868,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ pq))) = $true)),
% 216.34/30.77 inference(flattening,[],[f789])).
% 216.34/30.77 thf(f869,plain,(
% 216.34/30.77 ! [X0 : secrecy_specID,X1 : secrecy_specID,X2 : secrecy_specID,X3 : secrecy_KS] : (((((((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2))) = $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))) = $true)) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0))) != $true)) | (((correctCompositionKS @ X0)) != $true)) | (((subcomponents @ X0)) != ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))))),
% 216.34/30.77 inference(ennf_transformation,[],[f298])).
% 216.34/30.77 thf(f870,plain,(
% 216.34/30.77 ! [X0 : secrecy_specID,X1 : secrecy_specID,X2 : secrecy_specID,X3 : secrecy_KS] : ((((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2))) = $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))) = $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0))) != $true) | (((correctCompositionKS @ X0)) != $true) | (((subcomponents @ X0)) != ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))))),
% 216.34/30.77 inference(flattening,[],[f869])).
% 216.34/30.77 thf(f1203,plain,(
% 216.34/30.77 (((correctCompositionKS @ pq)) = $true)),
% 216.34/30.77 inference(cnf_transformation,[],[f288])).
% 216.34/30.77 thf(f1204,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) != $true)),
% 216.34/30.77 inference(cnf_transformation,[],[f790])).
% 216.34/30.77 thf(f1205,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ p))) != $true)),
% 216.34/30.77 inference(cnf_transformation,[],[f791])).
% 216.34/30.77 thf(f1206,plain,(
% 216.34/30.77 (((subcomponents @ pq)) = ((insert @ secrecy_specID @ p @ (insert @ secrecy_specID @ q @ bot_bot @ set @ secrecy_specID))))),
% 216.34/30.77 inference(cnf_transformation,[],[f4])).
% 216.34/30.77 thf(f1210,plain,(
% 216.34/30.77 ( ! [X2 : secrecy_specID,X3 : secrecy_KS,X0 : secrecy_specID,X1 : secrecy_specID] : ((((subcomponents @ X0)) != ((insert @ secrecy_specID @ X1 @ (insert @ secrecy_specID @ X2 @ bot_bot @ set @ secrecy_specID)))) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X1))) = $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X0))) != $true) | (((correctCompositionKS @ X0)) != $true) | (((member @ secrecy_KS @ X3 @ (specKeysSecrets @ X2))) = $true)) )),
% 216.34/30.77 inference(cnf_transformation,[],[f870])).
% 216.34/30.77 thf(f1568,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ pq))) = $true)),
% 216.34/30.77 inference(cnf_transformation,[],[f868])).
% 216.34/30.77 thf(f17908,plain,(
% 216.34/30.77 ( ! [X0 : secrecy_specID,X1 : secrecy_KS] : (($true != ((member @ secrecy_KS @ X1 @ (specKeysSecrets @ X0)))) | ($true = ((member @ secrecy_KS @ X1 @ (specKeysSecrets @ p)))) | (((subcomponents @ pq)) != ((subcomponents @ X0))) | (((correctCompositionKS @ X0)) != $true) | ($true = ((member @ secrecy_KS @ X1 @ (specKeysSecrets @ q))))) )),
% 216.34/30.77 inference(constrained_superposition,[],[f1210,f1206])).
% 216.34/30.77 thf(f302631,plain,(
% 216.34/30.77 ($true != $true) | (((member @ secrecy_KS @ m @ (specKeysSecrets @ p))) = $true) | (((subcomponents @ pq)) != ((subcomponents @ pq))) | (((correctCompositionKS @ pq)) != $true) | (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) = $true)),
% 216.34/30.77 inference(constrained_superposition,[],[f17908,f1568])).
% 216.34/30.77 thf(f302654,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ p))) = $true) | (((correctCompositionKS @ pq)) != $true) | (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) = $true)),
% 216.34/30.77 inference(trivial_inequality_removal,[],[f302631])).
% 216.34/30.77 thf(f302719,plain,(
% 216.34/30.77 (((correctCompositionKS @ pq)) != $true) | (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) = $true)),
% 216.34/30.77 inference(forward_subsumption_resolution,[],[f302654,f1205])).
% 216.34/30.77 thf(f302729,plain,(
% 216.34/30.77 (((member @ secrecy_KS @ m @ (specKeysSecrets @ q))) = $true)),
% 216.34/30.77 inference(forward_subsumption_resolution,[],[f302719,f1203])).
% 216.34/30.77 thf(f302731,plain,(
% 216.34/30.77 $false),
% 216.34/30.77 inference(forward_subsumption_resolution,[],[f302729,f1204])).
% 216.34/30.77 % SZS output end Proof for theBenchmark
% 216.34/30.77 % (809656)------------------------------
% 216.34/30.77 % (809656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 216.34/30.77 % (809656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.34/30.77 % (809656)CaDiCaL version: 2.1.3
% 216.34/30.77 % (809656)Termination reason: Refutation
% 216.34/30.77 % (809656)Time elapsed: 30.412 s
% 216.34/30.77 % (809656)Peak memory usage: 178 MB
% 216.34/30.77 % (809656)Instructions burned: 68344 (million)
% 216.34/30.77 % (809638)Success in time 30.517 s
% 216.34/30.77 % Vampire exiting
%------------------------------------------------------------------------------