%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW474^1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:40:22 AM UTC 2026
% Result : Theorem 162.16s 41.15s
% Output : Refutation 162.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474^1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n011.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 16:06:02 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 3.61/0.97 % (270074)Will run a generic schedule for satisfiability detection.
% 3.61/0.97 % (270084)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4212764897:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.61/0.97 % (270080)% WARNING: option uhcvi not known.
% 3.61/0.97 % (270079)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=519305566_2999 on theBenchmark for (2999ds/0Mi)
% 3.61/0.97 % (270080)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=26798962:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.61/0.97 % (270081)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1190018802:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.61/0.97 % (270082)dis+10_1_sil=32000:sp=arity:random_seed=2958097429:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.61/0.97 % (270083)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3363332573:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.61/0.97 % (270085)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2722079918:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.61/0.97 % (270080)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.61/0.97 % (270083)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.61/0.97 % (270084)Instruction limit reached!
% 3.61/0.97 % (270084)------------------------------
% 3.61/0.97 % (270084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.97 % (270084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.97 % (270084)CaDiCaL version: 2.1.3
% 3.61/0.97 % (270084)Termination reason: Instruction limit
% 3.61/0.97 % (270084)Termination phase: Saturation
% 3.61/0.97 % (270084)Time elapsed: 0.031 s
% 3.61/0.97 % (270084)Peak memory usage: 13 MB
% 3.61/0.97 % (270084)Instructions burned: 134 (million)
% 3.61/0.97 % Exception at run slice level
% 3.61/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.61/0.97 % (270080)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.61/0.97 % (270093)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2053009042:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.61/0.97 % (270082)Instruction limit reached!
% 3.61/0.97 % (270082)------------------------------
% 3.61/0.97 % (270082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.97 % (270082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.97 % (270082)CaDiCaL version: 2.1.3
% 3.61/0.97 % (270082)Termination reason: Instruction limit
% 3.61/0.97 % (270082)Termination phase: Saturation
% 3.61/0.97 % (270082)Time elapsed: 0.045 s
% 3.61/0.97 % (270082)Peak memory usage: 12 MB
% 3.61/0.97 % (270082)Instructions burned: 103 (million)
% 3.61/0.97 % (270083)Instruction limit reached!
% 3.61/0.97 % (270083)------------------------------
% 3.61/0.97 % (270083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.97 % (270083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.97 % (270083)CaDiCaL version: 2.1.3
% 3.61/0.97 % (270083)Termination reason: Instruction limit
% 3.61/0.97 % (270083)Termination phase: Saturation
% 3.61/0.97 % (270083)Time elapsed: 0.050 s
% 3.61/0.97 % (270083)Peak memory usage: 13 MB
% 3.61/0.97 % (270083)Instructions burned: 118 (million)
% 3.61/0.97 % (270094)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1093876491:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.61/0.97 % Exception at run slice level
% 3.61/0.97 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.61/0.97 % (270098)ott-21_1_sil=16000:fs=off:random_seed=790303593:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.61/0.97 % (270096)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=527742608:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.61/0.97 % (270099)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=740198164:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.61/0.97 % (270085)Instruction limit reached!
% 3.61/0.97 % (270085)------------------------------
% 3.61/0.97 % (270085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.22/2.98 % (270085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/2.98 % (270085)CaDiCaL version: 2.1.3
% 17.22/2.98 % (270085)Termination reason: Instruction limit
% 17.22/2.98 % (270085)Termination phase: Saturation
% 17.22/2.98 % (270085)Time elapsed: 0.073 s
% 17.22/2.98 % (270085)Peak memory usage: 14 MB
% 17.22/2.98 % (270085)Instructions burned: 159 (million)
% 17.22/2.98 % (270096)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.22/2.98 % (270103)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1174565509:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.22/2.98 % (270096)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 17.22/2.98 % (270098)Instruction limit reached!
% 17.22/2.98 % (270098)------------------------------
% 17.22/2.98 % (270098)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.22/2.98 % (270098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/2.98 % (270098)CaDiCaL version: 2.1.3
% 17.22/2.98 % (270098)Termination reason: Instruction limit
% 17.22/2.98 % (270098)Termination phase: Saturation
% 17.22/2.98 % (270098)Time elapsed: 0.044 s
% 17.22/2.98 % (270098)Peak memory usage: 13 MB
% 17.22/2.98 % (270098)Instructions burned: 184 (million)
% 17.22/2.98 % (270094)Instruction limit reached!
% 17.22/2.98 % (270094)------------------------------
% 17.22/2.98 % (270094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.22/2.98 % (270094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/2.98 % (270094)CaDiCaL version: 2.1.3
% 17.22/2.98 % (270094)Termination reason: Instruction limit
% 17.22/2.98 % (270094)Termination phase: Saturation
% 17.22/2.98 % (270094)Time elapsed: 0.060 s
% 17.22/2.98 % (270094)Peak memory usage: 13 MB
% 17.22/2.98 % (270094)Instructions burned: 132 (million)
% 17.22/2.98 % (270105)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2858611549:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 17.22/2.98 % Exception at run slice level
% 17.22/2.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.22/2.98 % (270106)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2453534652:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 17.22/2.98 % (270108)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=4081731870: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)
% 17.22/2.98 % (270108)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.22/2.98 % Exception at run slice level
% 17.22/2.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.22/2.98 % (270111)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2142791425:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 17.22/2.98 % (270111)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.22/2.98 % (270099)Instruction limit reached!
% 17.22/2.98 % (270099)------------------------------
% 17.22/2.98 % (270099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.22/2.98 % (270099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.22/2.98 % (270099)CaDiCaL version: 2.1.3
% 17.22/2.98 % (270099)Termination reason: Instruction limit
% 17.22/2.98 % (270099)Termination phase: Saturation
% 17.22/2.98 % (270099)Time elapsed: 0.242 s
% 17.22/2.98 % (270099)Peak memory usage: 15 MB
% 17.22/2.98 % (270099)Instructions burned: 478 (million)
% 17.22/2.98 % (270113)fmb+10_1_sil=64000:random_seed=2379891395:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 17.22/2.98 % (270113)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.22/2.98 % Exception at run slice level
% 17.22/2.98 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.22/2.98 % (270115)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=720735272:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 17.22/2.98 % (270096)Instruction limit reached!
% 17.22/2.98 % (270096)------------------------------
% 17.22/2.98 % (270096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.22/2.98 % (270096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.66/5.31 % (270096)CaDiCaL version: 2.1.3
% 35.66/5.31 % (270096)Termination reason: Instruction limit
% 35.66/5.31 % (270096)Termination phase: Saturation
% 35.66/5.31 % (270096)Time elapsed: 0.324 s
% 35.66/5.31 % (270096)Peak memory usage: 17 MB
% 35.66/5.31 % (270096)Instructions burned: 686 (million)
% 35.66/5.31 % (270117)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1599466133:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 35.66/5.31 % (270105)Instruction limit reached!
% 35.66/5.31 % (270105)------------------------------
% 35.66/5.31 % (270105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.66/5.31 % (270105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.66/5.31 % (270105)CaDiCaL version: 2.1.3
% 35.66/5.31 % (270105)Termination reason: Instruction limit
% 35.66/5.31 % (270105)Termination phase: Saturation
% 35.66/5.31 % (270105)Time elapsed: 0.295 s
% 35.66/5.31 % (270105)Peak memory usage: 20 MB
% 35.66/5.31 % (270105)Instructions burned: 1181 (million)
% 35.66/5.31 % Exception at run slice level
% 35.66/5.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.66/5.31 % (270119)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3038237198:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 35.66/5.31 % (270119)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.66/5.31 % (270120)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2530005427:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 35.66/5.31 % Exception at run slice level
% 35.66/5.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.66/5.31 % (270123)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=132628043:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 35.66/5.31 % (270120)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 35.66/5.31 % (270120)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.66/5.31 % (270108)Instruction limit reached!
% 35.66/5.31 % (270108)------------------------------
% 35.66/5.31 % (270108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.66/5.31 % (270108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.66/5.31 % (270108)CaDiCaL version: 2.1.3
% 35.66/5.31 % (270108)Termination reason: Instruction limit
% 35.66/5.31 % (270108)Termination phase: Saturation
% 35.66/5.31 % (270108)Time elapsed: 0.335 s
% 35.66/5.31 % (270108)Peak memory usage: 18 MB
% 35.66/5.31 % (270108)Instructions burned: 692 (million)
% 35.66/5.31 % Exception at run slice level
% 35.66/5.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.66/5.31 % (270125)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4169236258:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 35.66/5.31 % (270126)ott-2_1_sil=16000:newcnf=on:random_seed=4074629558:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 35.66/5.31 % (270126)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.66/5.31 % Exception at run slice level
% 35.66/5.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.66/5.31 % (270129)ott+10_1_sil=32000:tgt=ground:random_seed=3149302654:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 35.66/5.31 % (270111)Instruction limit reached!
% 35.66/5.31 % (270111)------------------------------
% 35.66/5.31 % (270111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.66/5.31 % (270111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.66/5.31 % (270111)CaDiCaL version: 2.1.3
% 35.66/5.31 % (270111)Termination reason: Instruction limit
% 35.66/5.31 % (270111)Termination phase: Saturation
% 35.66/5.31 % (270111)Time elapsed: 0.420 s
% 35.66/5.31 % (270111)Peak memory usage: 19 MB
% 35.66/5.31 % (270111)Instructions burned: 879 (million)
% 35.66/5.31 % (270131)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3710397843:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 35.66/5.31 % Exception at run slice level
% 35.66/5.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.66/5.31 % (270133)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2442579803:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 107.46/15.40 % (270133)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 107.46/15.40 % (270126)Instruction limit reached!
% 107.46/15.40 % (270126)------------------------------
% 107.46/15.40 % (270126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.46/15.40 % (270126)CaDiCaL version: 2.1.3
% 107.46/15.40 % (270126)Termination reason: Instruction limit
% 107.46/15.40 % (270126)Termination phase: Saturation
% 107.46/15.40 % (270126)Time elapsed: 0.406 s
% 107.46/15.40 % (270126)Peak memory usage: 17 MB
% 107.46/15.40 % (270126)Instructions burned: 870 (million)
% 107.46/15.40 % (270135)dis+21_1_sil=32000:sas=cadical:random_seed=3075155046:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 107.46/15.40 % (270120)Instruction limit reached!
% 107.46/15.40 % (270120)------------------------------
% 107.46/15.40 % (270120)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.46/15.40 % (270120)CaDiCaL version: 2.1.3
% 107.46/15.40 % (270120)Termination reason: Instruction limit
% 107.46/15.40 % (270120)Termination phase: Saturation
% 107.46/15.40 % (270120)Time elapsed: 0.724 s
% 107.46/15.40 % (270120)Peak memory usage: 21 MB
% 107.46/15.40 % (270120)Instructions burned: 1472 (million)
% 107.46/15.40 % (270137)ott+11_1_sil=16000:gs=on:random_seed=3984095176:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 107.46/15.40 % (270137)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 107.46/15.40 % (270119)Instruction limit reached!
% 107.46/15.40 % (270119)------------------------------
% 107.46/15.40 % (270119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.46/15.40 % (270119)CaDiCaL version: 2.1.3
% 107.46/15.40 % (270119)Termination reason: Instruction limit
% 107.46/15.40 % (270119)Termination phase: Saturation
% 107.46/15.40 % (270119)Time elapsed: 1.257 s
% 107.46/15.40 % (270119)Peak memory usage: 35 MB
% 107.46/15.40 % (270119)Instructions burned: 5134 (million)
% 107.46/15.40 % (270139)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1302365223:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 107.46/15.40 % Exception at run slice level
% 107.46/15.40 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 107.46/15.40 % (270141)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4231157565:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 107.46/15.40 % (270137)Instruction limit reached!
% 107.46/15.40 % (270137)------------------------------
% 107.46/15.40 % (270137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.46/15.40 % (270137)CaDiCaL version: 2.1.3
% 107.46/15.40 % (270137)Termination reason: Instruction limit
% 107.46/15.40 % (270137)Termination phase: Saturation
% 107.46/15.40 % (270137)Time elapsed: 1.085 s
% 107.46/15.40 % (270137)Peak memory usage: 24 MB
% 107.46/15.40 % (270137)Instructions burned: 2253 (million)
% 107.46/15.40 % (270143)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2544821547:i=29340_2976 on theBenchmark for (2976ds/29340Mi)
% 107.46/15.40 % (270133)Instruction limit reached!
% 107.46/15.40 % (270133)------------------------------
% 107.46/15.40 % (270133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.46/15.40 % (270133)CaDiCaL version: 2.1.3
% 107.46/15.40 % (270133)Termination reason: Instruction limit
% 107.46/15.40 % (270133)Termination phase: Saturation
% 107.46/15.40 % (270133)Time elapsed: 1.623 s
% 107.46/15.40 % (270133)Peak memory usage: 27 MB
% 107.46/15.40 % (270133)Instructions burned: 3514 (million)
% 107.46/15.40 % (270145)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3372215450:i=5211_2976 on theBenchmark for (2976ds/5211Mi)
% 107.46/15.40 % (270135)Instruction limit reached!
% 107.46/15.40 % (270135)------------------------------
% 107.46/15.40 % (270135)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 107.46/15.40 % (270135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.53/16.18 % (270135)CaDiCaL version: 2.1.3
% 112.53/16.18 % (270135)Termination reason: Instruction limit
% 112.53/16.18 % (270135)Termination phase: Saturation
% 112.53/16.18 % (270135)Time elapsed: 1.745 s
% 112.53/16.18 % (270135)Peak memory usage: 28 MB
% 112.53/16.18 % (270135)Instructions burned: 3773 (million)
% 112.53/16.18 % (270147)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1588911798:i=5497:nm=2_2972 on theBenchmark for (2972ds/5497Mi)
% 112.53/16.18 % Exception at run slice level
% 112.53/16.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 112.53/16.18 % (270149)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3948129122:fmbsr=2:i=46332_2972 on theBenchmark for (2972ds/46332Mi)
% 112.53/16.18 % Exception at run slice level
% 112.53/16.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 112.53/16.18 % (270151)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=704395031:i=14071_2971 on theBenchmark for (2971ds/14071Mi)
% 112.53/16.18 % Exception at run slice level
% 112.53/16.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 112.53/16.18 % (270153)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=712062887:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi)
% 112.53/16.18 % (270141)Instruction limit reached!
% 112.53/16.18 % (270141)------------------------------
% 112.53/16.18 % (270141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.53/16.18 % (270141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.53/16.18 % (270141)CaDiCaL version: 2.1.3
% 112.53/16.18 % (270141)Termination reason: Instruction limit
% 112.53/16.18 % (270141)Termination phase: Saturation
% 112.53/16.18 % (270141)Time elapsed: 1.185 s
% 112.53/16.18 % (270141)Peak memory usage: 31 MB
% 112.53/16.18 % (270141)Instructions burned: 4593 (million)
% 112.53/16.18 % (270155)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2005128834:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi)
% 112.53/16.18 % (270129)Instruction limit reached!
% 112.53/16.18 % (270129)------------------------------
% 112.53/16.18 % (270129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.53/16.18 % (270129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.53/16.18 % (270129)CaDiCaL version: 2.1.3
% 112.53/16.18 % (270129)Termination reason: Instruction limit
% 112.53/16.18 % (270129)Termination phase: Saturation
% 112.53/16.18 % (270129)Time elapsed: 2.399 s
% 112.53/16.18 % (270129)Peak memory usage: 36 MB
% 112.53/16.18 % (270129)Instructions burned: 5114 (million)
% 112.53/16.18 % (270157)dis+10_16:1_sil=16000:random_seed=3654194297:i=9155:fsr=off_2969 on theBenchmark for (2969ds/9155Mi)
% 112.53/16.18 % (270145)Instruction limit reached!
% 112.53/16.18 % (270145)------------------------------
% 112.53/16.18 % (270145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.53/16.18 % (270145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.53/16.18 % (270145)CaDiCaL version: 2.1.3
% 112.53/16.18 % (270145)Termination reason: Instruction limit
% 112.53/16.18 % (270145)Termination phase: Saturation
% 112.53/16.18 % (270145)Time elapsed: 2.523 s
% 112.53/16.18 % (270145)Peak memory usage: 41 MB
% 112.53/16.18 % (270145)Instructions burned: 5211 (million)
% 112.53/16.18 % (270159)ott-3_8_sil=64000:random_seed=4143043398:i=20139:bs=on_2950 on theBenchmark for (2950ds/20139Mi)
% 112.53/16.18 % (270155)Instruction limit reached!
% 112.53/16.18 % (270155)------------------------------
% 112.53/16.18 % (270155)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 112.53/16.18 % (270155)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.53/16.18 % (270155)CaDiCaL version: 2.1.3
% 112.53/16.18 % (270155)Termination reason: Instruction limit
% 112.53/16.18 % (270155)Termination phase: Saturation
% 112.53/16.18 % (270155)Time elapsed: 2.054 s
% 112.53/16.18 % (270155)Peak memory usage: 56 MB
% 112.53/16.18 % (270155)Instructions burned: 8177 (million)
% 112.53/16.18 % (270161)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2844449433:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi)
% 112.53/16.18 % Exception at run slice level
% 112.53/16.18 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 112.53/16.18 % (270163)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2576708525:i=11404_2949 on theBenchmark for (2949ds/11404Mi)
% 116.86/16.91 % (270157)Instruction limit reached!
% 116.86/16.91 % (270157)------------------------------
% 116.86/16.91 % (270157)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270157)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270157)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270157)Termination reason: Instruction limit
% 116.86/16.91 % (270157)Termination phase: Saturation
% 116.86/16.91 % (270157)Time elapsed: 4.318 s
% 116.86/16.91 % (270157)Peak memory usage: 53 MB
% 116.86/16.91 % (270157)Instructions burned: 9156 (million)
% 116.86/16.91 % (270165)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=962931541:i=14134_2926 on theBenchmark for (2926ds/14134Mi)
% 116.86/16.91 % (270165)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 116.86/16.91 % (270163)Instruction limit reached!
% 116.86/16.91 % (270163)------------------------------
% 116.86/16.91 % (270163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270163)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270163)Termination reason: Instruction limit
% 116.86/16.91 % (270163)Termination phase: Saturation
% 116.86/16.91 % (270163)Time elapsed: 2.931 s
% 116.86/16.91 % (270163)Peak memory usage: 86 MB
% 116.86/16.91 % (270163)Instructions burned: 11405 (million)
% 116.86/16.91 % (270167)dis+33_16_sil=32000:sac=on:random_seed=3027594997:i=15851:nm=0_2919 on theBenchmark for (2919ds/15851Mi)
% 116.86/16.91 % (270167)Instruction limit reached!
% 116.86/16.91 % (270167)------------------------------
% 116.86/16.91 % (270167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270167)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270167)Termination reason: Instruction limit
% 116.86/16.91 % (270167)Termination phase: Saturation
% 116.86/16.91 % (270167)Time elapsed: 2.772 s
% 116.86/16.91 % (270167)Peak memory usage: 24 MB
% 116.86/16.91 % (270167)Instructions burned: 15857 (million)
% 116.86/16.91 % (270169)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=837358042:avsq=on:i=17627:add=on:amm=off_2892 on theBenchmark for (2892ds/17627Mi)
% 116.86/16.91 % (270165)Instruction limit reached!
% 116.86/16.91 % (270165)------------------------------
% 116.86/16.91 % (270165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270165)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270165)Termination reason: Instruction limit
% 116.86/16.91 % (270165)Termination phase: Saturation
% 116.86/16.91 % (270165)Time elapsed: 6.494 s
% 116.86/16.91 % (270165)Peak memory usage: 83 MB
% 116.86/16.91 % (270165)Instructions burned: 14134 (million)
% 116.86/16.91 % (270400)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1581420605:s2a=on:i=53295_2861 on theBenchmark for (2861ds/53295Mi)
% 116.86/16.91 % (270159)Instruction limit reached!
% 116.86/16.91 % (270159)------------------------------
% 116.86/16.91 % (270159)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270159)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270159)Termination reason: Instruction limit
% 116.86/16.91 % (270159)Termination phase: Saturation
% 116.86/16.91 % (270159)Time elapsed: 9.405 s
% 116.86/16.91 % (270159)Peak memory usage: 67 MB
% 116.86/16.91 % (270159)Instructions burned: 20141 (million)
% 116.86/16.91 % (270534)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=537303228:i=26857:ins=20_2856 on theBenchmark for (2856ds/26857Mi)
% 116.86/16.91 % Exception at run slice level
% 116.86/16.91 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 116.86/16.91 % (270536)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2179312073:i=28120:bs=on:fsr=off_2856 on theBenchmark for (2856ds/28120Mi)
% 116.86/16.91 % (270153)Instruction limit reached!
% 116.86/16.91 % (270153)------------------------------
% 116.86/16.91 % (270153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 116.86/16.91 % (270153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.86/16.91 % (270153)CaDiCaL version: 2.1.3
% 116.86/16.91 % (270153)Termination reason: Instruction limit
% 116.86/16.91 % (270153)Termination phase: Saturation
% 116.86/16.91 % (270153)Time elapsed: 12.245 s
% 131.13/18.80 % (270153)Peak memory usage: 96 MB
% 131.13/18.80 % (270153)Instructions burned: 22566 (million)
% 131.13/18.80 % (270538)fmb+10_1_sil=256000:fmbss=7:random_seed=1057185023:fmbsr=1.6:i=182295_2848 on theBenchmark for (2848ds/182295Mi)
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270540)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3882092706:i=44625:gsp=on_2847 on theBenchmark for (2847ds/44625Mi)
% 131.13/18.80 % (270540)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 131.13/18.80 % (270540)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270542)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=578592411:i=160505_2847 on theBenchmark for (2847ds/160505Mi)
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270544)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1489028901:fmbsr=1.3:i=225729_2846 on theBenchmark for (2846ds/225729Mi)
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270546)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=2914486937:fmbsr=2:i=185024:ins=7_2846 on theBenchmark for (2846ds/185024Mi)
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270548)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=409558901:rtra=on_2845 on theBenchmark for (2845ds/0Mi)
% 131.13/18.80 % Exception at run slice level
% 131.13/18.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 131.13/18.80 % (270550)% WARNING: option uhcvi not known.
% 131.13/18.80 % (270550)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3910575073:i=271062:add=off:rtra=on:rawr=on_2845 on theBenchmark for (2845ds/271062Mi)
% 131.13/18.80 % (270550)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 131.13/18.80 % (270550)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 131.13/18.80 % (270143)Instruction limit reached!
% 131.13/18.80 % (270143)------------------------------
% 131.13/18.80 % (270143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.13/18.80 % (270143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.13/18.80 % (270143)CaDiCaL version: 2.1.3
% 131.13/18.80 % (270143)Termination reason: Instruction limit
% 131.13/18.80 % (270143)Termination phase: Saturation
% 131.13/18.80 % (270143)Time elapsed: 13.414 s
% 131.13/18.80 % (270143)Peak memory usage: 96 MB
% 131.13/18.80 % (270143)Instructions burned: 29341 (million)
% 131.13/18.80 % (270552)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2543104148:i=176048:add=on:rtra=on:rawr=on_2842 on theBenchmark for (2842ds/176048Mi)
% 131.13/18.80 % (270169)Instruction limit reached!
% 131.13/18.80 % (270169)------------------------------
% 131.13/18.80 % (270169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.13/18.80 % (270169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.13/18.80 % (270169)CaDiCaL version: 2.1.3
% 131.13/18.80 % (270169)Termination reason: Instruction limit
% 131.13/18.80 % (270169)Termination phase: Saturation
% 131.13/18.80 % (270169)Time elapsed: 5.072 s
% 131.13/18.80 % (270169)Peak memory usage: 88 MB
% 131.13/18.80 % (270169)Instructions burned: 17631 (million)
% 131.13/18.80 % (270554)dis+10_1_sil=32000:si=on:sp=arity:random_seed=873455586:i=206:fgj=on:rtra=on_2841 on theBenchmark for (2841ds/206Mi)
% 131.13/18.80 % (270554)Instruction limit reached!
% 131.13/18.80 % (270554)------------------------------
% 131.13/18.80 % (270554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 131.13/18.80 % (270554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 131.13/18.80 % (270554)CaDiCaL version: 2.1.3
% 131.13/18.80 % (270554)Termination reason: Instruction limit
% 131.13/18.80 % (270554)Termination phase: Saturation
% 131.13/18.80 % (270554)Time elapsed: 0.052 s
% 159.57/22.87 % (270554)Peak memory usage: 13 MB
% 159.57/22.87 % (270554)Instructions burned: 206 (million)
% 159.57/22.87 % (270556)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1334859805:i=232:rtra=on_2840 on theBenchmark for (2840ds/232Mi)
% 159.57/22.87 % (270556)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 159.57/22.87 % (270556)Instruction limit reached!
% 159.57/22.87 % (270556)------------------------------
% 159.57/22.87 % (270556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.57/22.87 % (270556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.57/22.87 % (270556)CaDiCaL version: 2.1.3
% 159.57/22.87 % (270556)Termination reason: Instruction limit
% 159.57/22.87 % (270556)Termination phase: Saturation
% 159.57/22.87 % (270556)Time elapsed: 0.060 s
% 159.57/22.87 % (270556)Peak memory usage: 14 MB
% 159.57/22.87 % (270556)Instructions burned: 234 (million)
% 159.57/22.87 % (270558)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3072461047:i=262:rtra=on_2839 on theBenchmark for (2839ds/262Mi)
% 159.57/22.87 % (270558)Instruction limit reached!
% 159.57/22.87 % (270558)------------------------------
% 159.57/22.87 % (270558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.57/22.87 % (270558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.57/22.87 % (270558)CaDiCaL version: 2.1.3
% 159.57/22.87 % (270558)Termination reason: Instruction limit
% 159.57/22.87 % (270558)Termination phase: Saturation
% 159.57/22.87 % (270558)Time elapsed: 0.069 s
% 159.57/22.87 % (270558)Peak memory usage: 14 MB
% 159.57/22.87 % (270558)Instructions burned: 266 (million)
% 159.57/22.87 % (270560)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2177172664:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2838 on theBenchmark for (2838ds/318Mi)
% 159.57/22.87 % (270560)Instruction limit reached!
% 159.57/22.87 % (270560)------------------------------
% 159.57/22.87 % (270560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.57/22.87 % (270560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.57/22.87 % (270560)CaDiCaL version: 2.1.3
% 159.57/22.87 % (270560)Termination reason: Instruction limit
% 159.57/22.87 % (270560)Termination phase: Saturation
% 159.57/22.87 % (270560)Time elapsed: 0.083 s
% 159.57/22.87 % (270560)Peak memory usage: 15 MB
% 159.57/22.87 % (270560)Instructions burned: 321 (million)
% 159.57/22.87 % (270562)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3612489001:i=1428:nm=2:rtra=on_2838 on theBenchmark for (2838ds/1428Mi)
% 159.57/22.87 % Exception at run slice level
% 159.57/22.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 159.57/22.87 % (270564)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=414380583:i=262:bd=preordered:rtra=on:fsd=on_2837 on theBenchmark for (2837ds/262Mi)
% 159.57/22.87 % (270564)Instruction limit reached!
% 159.57/22.87 % (270564)------------------------------
% 159.57/22.87 % (270564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.57/22.87 % (270564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.57/22.87 % (270564)CaDiCaL version: 2.1.3
% 159.57/22.87 % (270564)Termination reason: Instruction limit
% 159.57/22.87 % (270564)Termination phase: Saturation
% 159.57/22.87 % (270564)Time elapsed: 0.075 s
% 159.57/22.87 % (270564)Peak memory usage: 14 MB
% 159.57/22.87 % (270564)Instructions burned: 265 (million)
% 159.57/22.87 % (270566)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1913879615:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2836 on theBenchmark for (2836ds/1368Mi)
% 159.57/22.87 % (270566)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 159.57/22.87 % (270566)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 159.57/22.87 % (270566)Instruction limit reached!
% 159.57/22.87 % (270566)------------------------------
% 159.57/22.87 % (270566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 159.57/22.87 % (270566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.57/22.87 % (270566)CaDiCaL version: 2.1.3
% 159.57/22.87 % (270566)Termination reason: Instruction limit
% 159.57/22.87 % (270566)Termination phase: Saturation
% 159.57/22.87 % (270566)Time elapsed: 0.346 s
% 159.57/22.87 % (270566)Peak memory usage: 19 MB
% 159.57/22.87 % (270566)Instructions burned: 1371 (million)
% 159.57/22.87 % (270568)ott-21_1_sil=16000:si=on:fs=off:random_seed=1782852583:i=360:av=off:fsr=off:rtra=on_2833 on theBenchmark for (2833ds/360Mi)
% 215.33/30.65 % (270568)Instruction limit reached!
% 215.33/30.65 % (270568)------------------------------
% 215.33/30.65 % (270568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.33/30.65 % (270568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.33/30.65 % (270568)CaDiCaL version: 2.1.3
% 215.33/30.65 % (270568)Termination reason: Instruction limit
% 215.33/30.65 % (270568)Termination phase: Saturation
% 215.33/30.65 % (270568)Time elapsed: 0.088 s
% 215.33/30.65 % (270568)Peak memory usage: 14 MB
% 215.33/30.65 % (270568)Instructions burned: 363 (million)
% 215.33/30.65 % (270570)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1193303614:i=954:bd=all:rtra=on_2832 on theBenchmark for (2832ds/954Mi)
% 215.33/30.65 % (270570)Instruction limit reached!
% 215.33/30.65 % (270570)------------------------------
% 215.33/30.65 % (270570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.33/30.65 % (270570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.33/30.65 % (270570)CaDiCaL version: 2.1.3
% 215.33/30.65 % (270570)Termination reason: Instruction limit
% 215.33/30.65 % (270570)Termination phase: Saturation
% 215.33/30.65 % (270570)Time elapsed: 0.258 s
% 215.33/30.65 % (270570)Peak memory usage: 17 MB
% 215.33/30.65 % (270570)Instructions burned: 957 (million)
% 215.33/30.65 % (270572)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=841815795:fmbsr=1.3:i=1730:ins=25:rtra=on_2829 on theBenchmark for (2829ds/1730Mi)
% 215.33/30.65 % Exception at run slice level
% 215.33/30.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 215.33/30.65 % (270574)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=125284702:i=2358:rtra=on_2829 on theBenchmark for (2829ds/2358Mi)
% 215.33/30.65 % (270574)Instruction limit reached!
% 215.33/30.65 % (270574)------------------------------
% 215.33/30.65 % (270574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.33/30.65 % (270574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.33/30.65 % (270574)CaDiCaL version: 2.1.3
% 215.33/30.65 % (270574)Termination reason: Instruction limit
% 215.33/30.65 % (270574)Termination phase: Saturation
% 215.33/30.65 % (270574)Time elapsed: 0.606 s
% 215.33/30.65 % (270574)Peak memory usage: 26 MB
% 215.33/30.65 % (270574)Instructions burned: 2360 (million)
% 215.33/30.65 % (270576)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=979893128:i=1778:ins=1:rtra=on_2823 on theBenchmark for (2823ds/1778Mi)
% 215.33/30.65 % Exception at run slice level
% 215.33/30.65 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 215.33/30.65 % (270578)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2508165285:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/1384Mi)
% 215.33/30.65 % (270578)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 215.33/30.65 % (270578)Instruction limit reached!
% 215.33/30.65 % (270578)------------------------------
% 215.33/30.65 % (270578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.33/30.65 % (270578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.33/30.65 % (270578)CaDiCaL version: 2.1.3
% 215.33/30.65 % (270578)Termination reason: Instruction limit
% 215.33/30.65 % (270578)Termination phase: Saturation
% 215.33/30.65 % (270578)Time elapsed: 0.364 s
% 215.33/30.65 % (270578)Peak memory usage: 22 MB
% 215.33/30.65 % (270578)Instructions burned: 1385 (million)
% 215.33/30.65 % (270580)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=383426539:i=1758:kws=inv_precedence:fsr=off:rtra=on_2819 on theBenchmark for (2819ds/1758Mi)
% 215.33/30.65 % (270580)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 215.33/30.65 % (270580)Instruction limit reached!
% 215.33/30.65 % (270580)------------------------------
% 215.33/30.65 % (270580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.33/30.65 % (270580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.33/30.65 % (270580)CaDiCaL version: 2.1.3
% 215.33/30.65 % (270580)Termination reason: Instruction limit
% 215.33/30.65 % (270580)Termination phase: Saturation
% 215.33/30.65 % (270580)Time elapsed: 0.455 s
% 162.16/41.15 % (270580)Peak memory usage: 23 MB
% 162.16/41.15 % (270580)Instructions burned: 1759 (million)
% 162.16/41.15 % (270582)fmb+10_1_sil=64000:si=on:random_seed=2046478535:i=44122:nm=2:rtra=on:gsp=on_2814 on theBenchmark for (2814ds/44122Mi)
% 162.16/41.15 % (270582)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270584)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=1176093564:i=19030:nm=5:rtra=on_2814 on theBenchmark for (2814ds/19030Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270586)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=164982834:fmbsr=1.7:i=1840:rtra=on_2813 on theBenchmark for (2813ds/1840Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270588)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3509218545:i=10262:rtra=on_2813 on theBenchmark for (2813ds/10262Mi)
% 162.16/41.15 % (270588)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 162.16/41.15 % (270588)Instruction limit reached!
% 162.16/41.15 % (270588)------------------------------
% 162.16/41.15 % (270588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270588)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270588)Termination reason: Instruction limit
% 162.16/41.15 % (270588)Termination phase: Saturation
% 162.16/41.15 % (270588)Time elapsed: 2.622 s
% 162.16/41.15 % (270588)Peak memory usage: 48 MB
% 162.16/41.15 % (270588)Instructions burned: 10266 (million)
% 162.16/41.15 % (270590)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3305323688:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2786 on theBenchmark for (2786ds/2944Mi)
% 162.16/41.15 % (270590)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 162.16/41.15 % (270590)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 162.16/41.15 % (270590)Instruction limit reached!
% 162.16/41.15 % (270590)------------------------------
% 162.16/41.15 % (270590)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270590)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270590)Termination reason: Instruction limit
% 162.16/41.15 % (270590)Termination phase: Saturation
% 162.16/41.15 % (270590)Time elapsed: 0.787 s
% 162.16/41.15 % (270590)Peak memory usage: 25 MB
% 162.16/41.15 % (270590)Instructions burned: 2945 (million)
% 162.16/41.15 % (270592)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1729023253:i=12648:rtra=on_2778 on theBenchmark for (2778ds/12648Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270594)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=450966487:fmbsr=2.30978:i=4348:rtra=on_2778 on theBenchmark for (2778ds/4348Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270596)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=643176020:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2778 on theBenchmark for (2778ds/1738Mi)
% 162.16/41.15 % (270596)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 162.16/41.15 % (270596)Instruction limit reached!
% 162.16/41.15 % (270596)------------------------------
% 162.16/41.15 % (270596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270596)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270596)Termination reason: Instruction limit
% 162.16/41.15 % (270596)Termination phase: Saturation
% 162.16/41.15 % (270596)Time elapsed: 0.442 s
% 162.16/41.15 % (270596)Peak memory usage: 22 MB
% 162.16/41.15 % (270596)Instructions burned: 1740 (million)
% 162.16/41.15 % (270598)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1881562550:i=10228:av=off:rtra=on_2773 on theBenchmark for (2773ds/10228Mi)
% 162.16/41.15 % (270598)Instruction limit reached!
% 162.16/41.15 % (270598)------------------------------
% 162.16/41.15 % (270598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270598)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270598)Termination reason: Instruction limit
% 162.16/41.15 % (270598)Termination phase: Saturation
% 162.16/41.15 % (270598)Time elapsed: 2.641 s
% 162.16/41.15 % (270598)Peak memory usage: 47 MB
% 162.16/41.15 % (270598)Instructions burned: 10228 (million)
% 162.16/41.15 % (270600)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=3846467471:i=108564:rtra=on_2747 on theBenchmark for (2747ds/108564Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270602)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=3857180920:i=7024:aac=none:rtra=on_2746 on theBenchmark for (2746ds/7024Mi)
% 162.16/41.15 % (270602)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 162.16/41.15 % (270536)Instruction limit reached!
% 162.16/41.15 % (270536)------------------------------
% 162.16/41.15 % (270536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270536)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270536)Termination reason: Instruction limit
% 162.16/41.15 % (270536)Termination phase: Saturation
% 162.16/41.15 % (270536)Time elapsed: 12.399 s
% 162.16/41.15 % (270536)Peak memory usage: 66 MB
% 162.16/41.15 % (270536)Instructions burned: 28121 (million)
% 162.16/41.15 % (270604)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=1351558371:i=7546:rtra=on:amm=off_2731 on theBenchmark for (2731ds/7546Mi)
% 162.16/41.15 % (270602)Instruction limit reached!
% 162.16/41.15 % (270602)------------------------------
% 162.16/41.15 % (270602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270602)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270602)Termination reason: Instruction limit
% 162.16/41.15 % (270602)Termination phase: Saturation
% 162.16/41.15 % (270602)Time elapsed: 1.750 s
% 162.16/41.15 % (270602)Peak memory usage: 39 MB
% 162.16/41.15 % (270602)Instructions burned: 7024 (million)
% 162.16/41.15 % (270606)ott+11_1_sil=16000:si=on:gs=on:random_seed=3606495868:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2729 on theBenchmark for (2729ds/4502Mi)
% 162.16/41.15 % (270606)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 162.16/41.15 % (270606)Instruction limit reached!
% 162.16/41.15 % (270606)------------------------------
% 162.16/41.15 % (270606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270606)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270606)Termination reason: Instruction limit
% 162.16/41.15 % (270606)Termination phase: Saturation
% 162.16/41.15 % (270606)Time elapsed: 1.202 s
% 162.16/41.15 % (270606)Peak memory usage: 31 MB
% 162.16/41.15 % (270606)Instructions burned: 4503 (million)
% 162.16/41.15 % (270742)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=225608388:fmbsr=1.6:i=135068:rtra=on_2717 on theBenchmark for (2717ds/135068Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270751)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1848940542:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2716 on theBenchmark for (2716ds/9182Mi)
% 162.16/41.15 % (270604)Instruction limit reached!
% 162.16/41.15 % (270604)------------------------------
% 162.16/41.15 % (270604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270604)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270604)Termination reason: Instruction limit
% 162.16/41.15 % (270604)Termination phase: Saturation
% 162.16/41.15 % (270604)Time elapsed: 3.570 s
% 162.16/41.15 % (270604)Peak memory usage: 41 MB
% 162.16/41.15 % (270604)Instructions burned: 7548 (million)
% 162.16/41.15 % (270973)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=1229606660:i=58680:rtra=on_2695 on theBenchmark for (2695ds/58680Mi)
% 162.16/41.15 % (270751)Instruction limit reached!
% 162.16/41.15 % (270751)------------------------------
% 162.16/41.15 % (270751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270751)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270751)Termination reason: Instruction limit
% 162.16/41.15 % (270751)Termination phase: Saturation
% 162.16/41.15 % (270751)Time elapsed: 2.494 s
% 162.16/41.15 % (270751)Peak memory usage: 39 MB
% 162.16/41.15 % (270751)Instructions burned: 9183 (million)
% 162.16/41.15 % (270975)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=2367891985:i=10422:rtra=on_2691 on theBenchmark for (2691ds/10422Mi)
% 162.16/41.15 % (270975)Instruction limit reached!
% 162.16/41.15 % (270975)------------------------------
% 162.16/41.15 % (270975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270975)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270975)Termination reason: Instruction limit
% 162.16/41.15 % (270975)Termination phase: Saturation
% 162.16/41.15 % (270975)Time elapsed: 2.673 s
% 162.16/41.15 % (270975)Peak memory usage: 58 MB
% 162.16/41.15 % (270975)Instructions burned: 10425 (million)
% 162.16/41.15 % (270977)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=675990584:i=10994:nm=2:rtra=on_2664 on theBenchmark for (2664ds/10994Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270979)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=2333108528:fmbsr=2:i=92664:rtra=on_2664 on theBenchmark for (2664ds/92664Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270981)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=2468391015:i=28142:rtra=on_2664 on theBenchmark for (2664ds/28142Mi)
% 162.16/41.15 % Exception at run slice level
% 162.16/41.15 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 162.16/41.15 % (270983)dis+10_161_sil=128000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=760156264:i=45130:add=on:rtra=on:rawr=on_2663 on theBenchmark for (2663ds/45130Mi)
% 162.16/41.15 % (270400)Instruction limit reached!
% 162.16/41.15 % (270400)------------------------------
% 162.16/41.15 % (270400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.15 % (270400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.15 % (270400)CaDiCaL version: 2.1.3
% 162.16/41.15 % (270400)Termination reason: Instruction limit
% 162.16/41.15 % (270400)Termination phase: Saturation
% 162.16/41.15 % (270400)Time elapsed: 25.135 s
% 162.16/41.15 % (270400)Peak memory usage: 163 MB
% 162.16/41.15 % (270400)Instructions burned: 53295 (million)
% 162.16/41.15 % (270985)ott+4_1_sil=16000:si=on:sp=arity:gs=on:random_seed=3064490933:i=16346:av=off:rtra=on_2609 on theBenchmark for (2609ds/16346Mi)
% 162.16/41.15 % (270550) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-270074-270550"...
% 162.16/41.15 % (270550)...printing done.
% 162.16/41.15 % (270550)Refutation found. Thanks to Tanya!
% 162.16/41.15 % SZS status Theorem for theBenchmark
% 162.16/41.15 % SZS output start Proof for theBenchmark
% 162.16/41.15 thf(type_def_5, type, com: $tType).
% 162.16/41.15 thf(type_def_6, type, pname: $tType).
% 162.16/41.15 thf(type_def_7, type, hoare_1262092251_state: $tType).
% 162.16/41.15 thf(type_def_8, type, option_com: $tType).
% 162.16/41.15 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 162.16/41.15 thf(func_def_0, type, wt: (com > $o)).
% 162.16/41.15 thf(func_def_1, type, wT_bodies: $o).
% 162.16/41.15 thf(func_def_2, type, body: (pname > option_com)).
% 162.16/41.15 thf(func_def_3, type, body_1: (pname > com)).
% 162.16/41.15 thf(func_def_4, type, finite1648353812_o_o_o: (((((pname > $o) > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_5, type, finite734360985_o_o_o: (((((hoare_1262092251_state > $o) > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_6, type, finite1066544169me_o_o: ((((pname > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_7, type, finite1303896758te_o_o: ((((hoare_1262092251_state > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_8, type, finite297249702name_o: (((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_9, type, finite1423311111tate_o: (((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_10, type, finite_finite_pname: ((pname > $o) > $o)).
% 162.16/41.15 thf(func_def_11, type, finite1178804552_state: ((hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_12, type, hoare_Mirabelle_MGT: (com > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_13, type, hoare_930741239_state: ((hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_14, type, hoare_1821564147gleton: $o).
% 162.16/41.15 thf(func_def_15, type, dom_pname_o_com: (((pname > $o) > option_com) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_16, type, dom_Ho1489634536_o_com: (((hoare_1262092251_state > $o) > option_com) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_17, type, dom_pname_com: ((pname > option_com) > pname > $o)).
% 162.16/41.15 thf(func_def_18, type, some_com: (com > option_com)).
% 162.16/41.15 thf(func_def_19, type, the_com: (option_com > com)).
% 162.16/41.15 thf(func_def_20, type, bot_bot_pname_o_o_o: (((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_21, type, bot_bo388435036_o_o_o: (((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_22, type, bot_bot_pname_o_o: ((pname > $o) > $o)).
% 162.16/41.15 thf(func_def_23, type, bot_bo1962689075te_o_o: ((hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_24, type, bot_bot_pname_o: (pname > $o)).
% 162.16/41.15 thf(func_def_25, type, bot_bo113204042tate_o: (hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_26, type, ord_le1828183645_o_o_o: ((((pname > $o) > $o) > $o) > (((pname > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_27, type, ord_le1891858320_o_o_o: ((((hoare_1262092251_state > $o) > $o) > $o) > (((hoare_1262092251_state > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_28, type, ord_le1205211808me_o_o: (((pname > $o) > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_29, type, ord_le2012720639te_o_o: (((hoare_1262092251_state > $o) > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_30, type, ord_less_eq_pname_o: ((pname > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_31, type, ord_le870406270tate_o: ((hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_32, type, collect_pname_o_o_o: (((((pname > $o) > $o) > $o) > $o) > (((pname > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_33, type, collec101077467_o_o_o: (((((hoare_1262092251_state > $o) > $o) > $o) > $o) > (((hoare_1262092251_state > $o) > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_34, type, collect_pname_o_o: ((((pname > $o) > $o) > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_35, type, collec341954548te_o_o: ((((hoare_1262092251_state > $o) > $o) > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_36, type, collect_pname_o: (((pname > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_37, type, collec313158217tate_o: (((hoare_1262092251_state > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_38, type, collect_pname: ((pname > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_39, type, collec1121927558_state: ((hoare_1262092251_state > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_40, type, image_471733107_pname: ((((pname > $o) > $o) > pname) > (((pname > $o) > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_41, type, image_1036078444_state: ((((pname > $o) > $o) > hoare_1262092251_state) > (((pname > $o) > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_42, type, image_893364936_pname: ((((hoare_1262092251_state > $o) > $o) > pname) > (((hoare_1262092251_state > $o) > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_43, type, image_165349207_state: ((((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state) > (((hoare_1262092251_state > $o) > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_44, type, image_pname_o_pname: (((pname > $o) > pname) > ((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_45, type, image_1476171975_state: (((pname > $o) > hoare_1262092251_state) > ((pname > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_46, type, image_1820530197_pname: (((hoare_1262092251_state > $o) > pname) > ((hoare_1262092251_state > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_47, type, image_234589002_state: (((hoare_1262092251_state > $o) > hoare_1262092251_state) > ((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_48, type, image_504089495me_o_o: ((pname > (pname > $o) > $o) > (pname > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_49, type, image_827868872te_o_o: ((pname > (hoare_1262092251_state > $o) > $o) > (pname > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_50, type, image_pname_pname_o: ((pname > pname > $o) > (pname > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_51, type, image_518521461tate_o: ((pname > hoare_1262092251_state > $o) > (pname > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_52, type, image_pname_pname: ((pname > pname) > (pname > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_53, type, image_669833818_state: ((pname > hoare_1262092251_state) > (pname > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_54, type, image_333245000me_o_o: ((hoare_1262092251_state > (pname > $o) > $o) > (hoare_1262092251_state > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_55, type, image_1731108951te_o_o: ((hoare_1262092251_state > (hoare_1262092251_state > $o) > $o) > (hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_56, type, image_1320925383name_o: ((hoare_1262092251_state > pname > $o) > (hoare_1262092251_state > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_57, type, image_1403668518tate_o: ((hoare_1262092251_state > hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_58, type, image_202231862_pname: ((hoare_1262092251_state > pname) > (hoare_1262092251_state > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_59, type, insert_pname_o_o: (((pname > $o) > $o) > (((pname > $o) > $o) > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_60, type, insert1691644879te_o_o: (((hoare_1262092251_state > $o) > $o) > (((hoare_1262092251_state > $o) > $o) > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_61, type, insert_pname_o: ((pname > $o) > ((pname > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_62, type, insert1042460334tate_o: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_63, type, insert_pname: (pname > (pname > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_64, type, insert81609953_state: (hoare_1262092251_state > (hoare_1262092251_state > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_65, type, fequal_pname_o: ((pname > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_66, type, fequal1529404211tate_o: ((hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_67, type, fequal_pname: (pname > pname > $o)).
% 162.16/41.15 thf(func_def_68, type, fequal1925511196_state: (hoare_1262092251_state > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_69, type, member_pname_o: ((pname > $o) > ((pname > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_70, type, member907417095tate_o: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > $o) > $o)).
% 162.16/41.15 thf(func_def_71, type, member_pname: (pname > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_72, type, member5164104_state: (hoare_1262092251_state > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_73, type, fa: (hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_74, type, pn: pname).
% 162.16/41.15 thf(func_def_75, type, y: com).
% 162.16/41.15 thf(func_def_77, type, vAND: ($o > $o > $o)).
% 162.16/41.15 thf(func_def_78, type, vIMP: ($o > $o > $o)).
% 162.16/41.15 thf(func_def_79, type, vNOT: ($o > $o)).
% 162.16/41.15 thf(func_def_80, type, vOR: ($o > $o > $o)).
% 162.16/41.15 thf(func_def_83, type, db0: !>[X0: $tType]:(X0)).
% 162.16/41.15 thf(func_def_84, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 162.16/41.15 thf(func_def_85, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 162.16/41.15 thf(func_def_86, type, sK0: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_87, type, sK1: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_88, type, sK2: ((((pname > $o) > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_89, type, sK3: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_90, type, sK4: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_91, type, sK5: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_92, type, sK6: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_93, type, sK7: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_94, type, sK8: ((hoare_1262092251_state > $o) > (pname > hoare_1262092251_state) > (pname > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_95, type, sK9: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_96, type, sK10: ((pname > $o) > ((pname > $o) > $o) > pname)).
% 162.16/41.15 thf(func_def_97, type, sK11: ((pname > $o) > ((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_98, type, sK12: ((((pname > $o) > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_99, type, sK13: ((pname > $o) > (pname > hoare_1262092251_state) > hoare_1262092251_state > pname)).
% 162.16/41.15 thf(func_def_100, type, sK14: (hoare_1262092251_state > (pname > $o) > (pname > hoare_1262092251_state) > pname)).
% 162.16/41.15 thf(func_def_101, type, sK15: ((hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_102, type, sK16: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_103, type, sK17: ((pname > $o) > (pname > $o) > pname)).
% 162.16/41.15 thf(func_def_104, type, sK18: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_105, type, sK19: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_106, type, sK20: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_107, type, sK21: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_108, type, sK22: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_109, type, sK23: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_110, type, sK24: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_111, type, sK25: (pname > com)).
% 162.16/41.15 thf(func_def_112, type, sK26: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_113, type, sK27: ((((pname > $o) > $o) > $o) > ((pname > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_114, type, sK28: ((((pname > $o) > $o) > $o) > ((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_115, type, sK29: ((((hoare_1262092251_state > $o) > $o) > $o) > ((hoare_1262092251_state > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_116, type, sK30: ((((hoare_1262092251_state > $o) > $o) > $o) > ((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_117, type, sK31: ((hoare_1262092251_state > $o) > (pname > hoare_1262092251_state) > (pname > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_118, type, sK32: ((hoare_1262092251_state > $o) > pname)).
% 162.16/41.15 thf(func_def_119, type, sK33: ((((hoare_1262092251_state > $o) > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_120, type, sK34: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_121, type, sK35: ((((hoare_1262092251_state > $o) > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_122, type, sK36: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_123, type, sK37: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_124, type, sK38: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_125, type, db1: !>[X0: $tType]:(X0)).
% 162.16/41.15 thf(func_def_127, type, sK40: ((pname > $o) > pname > pname)).
% 162.16/41.15 thf(func_def_128, type, sK41: ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_129, type, sK42: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_130, type, sK43: ((((pname > $o) > $o) > $o) > (pname > $o) > $o)).
% 162.16/41.15 thf(func_def_131, type, sK44: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_132, type, sK45: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_133, type, sK46: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_134, type, sK47: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_135, type, sK48: (hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_136, type, sK49: (pname > pname)).
% 162.16/41.15 thf(func_def_137, type, sK50: ((pname > hoare_1262092251_state) > (pname > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_138, type, sK51: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_139, type, sK52: pname).
% 162.16/41.15 thf(func_def_140, type, sK53: ((((hoare_1262092251_state > $o) > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_141, type, sK54: (pname > (pname > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_142, type, sK55: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_143, type, sK56: ((pname > pname > hoare_1262092251_state) > pname > pname)).
% 162.16/41.15 thf(func_def_144, type, sK57: (pname > (pname > pname > $o) > pname)).
% 162.16/41.15 thf(func_def_145, type, sK58: pname).
% 162.16/41.15 thf(func_def_146, type, sK59: (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_147, type, sK60: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_148, type, sK61: (pname > pname > pname)).
% 162.16/41.15 thf(func_def_149, type, sK62: (pname > pname)).
% 162.16/41.15 thf(func_def_150, type, sK63: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_151, type, sK64: (pname > pname)).
% 162.16/41.15 thf(func_def_152, type, sK65: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_153, type, sK66: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_154, type, db2: !>[X0: $tType]:(X0)).
% 162.16/41.15 thf(func_def_155, type, sK67: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_156, type, sK68: pname).
% 162.16/41.15 thf(func_def_157, type, sK69: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_158, type, sK70: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_159, type, sK71: (pname > pname)).
% 162.16/41.15 thf(func_def_160, type, sK72: (pname > pname)).
% 162.16/41.15 thf(func_def_161, type, sK73: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_162, type, sK74: ((hoare_1262092251_state > $o) > (hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_163, type, sK75: ((pname > $o) > pname > (pname > $o) > pname)).
% 162.16/41.15 thf(func_def_164, type, sK76: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_165, type, sK77: (pname > pname)).
% 162.16/41.15 thf(func_def_166, type, sK78: (pname > pname)).
% 162.16/41.15 thf(func_def_167, type, sK79: (option_com > pname)).
% 162.16/41.15 thf(func_def_168, type, sK80: (pname > pname)).
% 162.16/41.15 thf(func_def_169, type, sK81: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_170, type, sK82: (pname > pname)).
% 162.16/41.15 thf(func_def_171, type, sK83: (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_172, type, sK84: (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_173, type, sK85: (pname > pname > pname > pname > pname)).
% 162.16/41.15 thf(func_def_174, type, sK86: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_175, type, sK87: (pname > pname > pname > pname > pname)).
% 162.16/41.15 thf(func_def_176, type, sK88: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_177, type, sK89: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_178, type, sK90: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_179, type, sK91: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_180, type, sK92: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_181, type, sK93: (pname > pname)).
% 162.16/41.15 thf(func_def_182, type, sK94: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_183, type, sK95: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_184, type, sK96: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_185, type, sK97: ((pname > $o) > pname > pname)).
% 162.16/41.15 thf(func_def_186, type, sK98: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_187, type, sK99: pname).
% 162.16/41.15 thf(func_def_188, type, sK100: ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_189, type, sK101: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_190, type, sK102: ((pname > hoare_1262092251_state) > (pname > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_191, type, sK103: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_192, type, sK104: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_193, type, sK105: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_194, type, sK106: (pname > pname)).
% 162.16/41.15 thf(func_def_195, type, sK107: (hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_196, type, sK108: ((hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_197, type, sK109: ((pname > $o) > pname)).
% 162.16/41.15 thf(func_def_198, type, sK110: (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_199, type, sK111: (((pname > $o) > $o) > pname > $o)).
% 162.16/41.15 thf(func_def_200, type, sK112: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_201, type, sK113: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_202, type, sK114: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_203, type, sK115: ((pname > $o) > ((pname > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_204, type, sK116: ((pname > $o) > ((pname > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_205, type, sK117: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_206, type, sK118: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_207, type, sK119: ((pname > $o) > ((pname > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_208, type, sK120: (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_209, type, sK121: (pname > pname > pname)).
% 162.16/41.15 thf(func_def_210, type, sK122: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_211, type, sK123: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_212, type, sK124: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_213, type, sK125: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_214, type, sK126: (pname > (pname > hoare_1262092251_state) > (pname > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_215, type, sK127: (hoare_1262092251_state > (hoare_1262092251_state > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_216, type, sK128: (pname > (pname > pname > option_com) > pname)).
% 162.16/41.15 thf(func_def_217, type, sK129: (option_com > pname)).
% 162.16/41.15 thf(func_def_218, type, sK130: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_219, type, sK131: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_220, type, sK132: (option_com > pname)).
% 162.16/41.15 thf(func_def_221, type, sK133: ((pname > $o) > pname > pname)).
% 162.16/41.15 thf(func_def_222, type, sK134: (hoare_1262092251_state > pname)).
% 162.16/41.15 thf(func_def_223, type, sK135: (hoare_1262092251_state > pname > $o)).
% 162.16/41.15 thf(func_def_224, type, sK136: (hoare_1262092251_state > hoare_1262092251_state > $o)).
% 162.16/41.15 thf(func_def_225, type, sK137: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_226, type, sK138: ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_227, type, sK139: ((pname > $o) > pname > pname)).
% 162.16/41.15 thf(func_def_228, type, sK140: (hoare_1262092251_state > (hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_229, type, sK141: (pname > (pname > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_230, type, sK142: (pname > (pname > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_231, type, sK143: (hoare_1262092251_state > (hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_232, type, sK144: ((hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > (hoare_1262092251_state > hoare_1262092251_state > $o) > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_233, type, sK145: ((pname > hoare_1262092251_state > hoare_1262092251_state) > (pname > hoare_1262092251_state > hoare_1262092251_state) > (pname > hoare_1262092251_state > $o) > (pname > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_234, type, sK146: ((hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > (hoare_1262092251_state > hoare_1262092251_state > $o) > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_235, type, sK147: ((pname > hoare_1262092251_state > hoare_1262092251_state) > (pname > hoare_1262092251_state > hoare_1262092251_state) > (pname > hoare_1262092251_state > $o) > (pname > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_236, type, sK148: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_237, type, sK149: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_238, type, sK150: (hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_239, type, sK151: (hoare_1262092251_state > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_240, type, sK152: ((pname > $o) > ((pname > $o) > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_241, type, sK153: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_242, type, sK154: ((pname > $o) > ((pname > $o) > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_243, type, sK155: ((hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_244, type, sK156: (hoare_1262092251_state > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_245, type, sK157: (pname > (pname > hoare_1262092251_state > hoare_1262092251_state) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_246, type, sK158: (((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_247, type, sK159: (((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > $o) > ((hoare_1262092251_state > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_248, type, sK160: (((pname > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((pname > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((pname > $o) > hoare_1262092251_state > $o) > ((pname > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_249, type, sK161: (((pname > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((pname > $o) > hoare_1262092251_state > hoare_1262092251_state) > ((pname > $o) > hoare_1262092251_state > $o) > ((pname > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_250, type, sK162: (pname > pname > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_251, type, sK163: (pname > pname > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_252, type, sK164: (pname > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_253, type, sK165: (pname > pname > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_254, type, sK166: ((((hoare_1262092251_state > $o) > $o) > $o) > (((hoare_1262092251_state > $o) > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_255, type, sK167: ((((hoare_1262092251_state > $o) > $o) > $o) > (((hoare_1262092251_state > $o) > $o) > $o) > (hoare_1262092251_state > $o) > $o)).
% 162.16/41.15 thf(func_def_256, type, sK168: hoare_1262092251_state).
% 162.16/41.15 thf(func_def_257, type, sK169: (pname > (pname > hoare_1262092251_state > hoare_1262092251_state) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_258, type, sK170: (hoare_1262092251_state > (hoare_1262092251_state > hoare_1262092251_state > hoare_1262092251_state) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_259, type, sK171: ((((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((pname > $o) > $o) > hoare_1262092251_state > $o) > (((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_260, type, sK172: ((((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((pname > $o) > $o) > hoare_1262092251_state > $o) > (((pname > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_261, type, sK173: ((((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(func_def_262, type, sK174: ((((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > $o) > (((hoare_1262092251_state > $o) > $o) > hoare_1262092251_state > hoare_1262092251_state > $o) > hoare_1262092251_state)).
% 162.16/41.15 thf(f4,axiom,(
% 162.16/41.15 ! [X2 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o),X0 : (hoare_1262092251_state > $o)] : ((hoare_930741239_state @ X1 @ X2) => ((ord_le870406270tate_o @ X1 @ X0) => (hoare_930741239_state @ X0 @ X2)))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_thin)).
% 162.16/41.15 thf(f34,axiom,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o)] : (ord_le870406270tate_o @ bot_bo113204042tate_o @ X0)),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_empty__subsetI)).
% 162.16/41.15 thf(f104,axiom,(
% 162.16/41.15 ! [X0 : com] : (hoare_1821564147gleton => (wT_bodies => ((wt @ X0) => (hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o)))))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_MGF)).
% 162.16/41.15 thf(f167,axiom,(
% 162.16/41.15 (((collec1121927558_state @ (^[X0 : hoare_1262092251_state] : ($false)))) = bot_bo113204042tate_o)),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_empty__def)).
% 162.16/41.15 thf(f256,axiom,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o)] : (((collec1121927558_state @ X0)) = X0)),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_Collect__def)).
% 162.16/41.15 thf(f285,axiom,(
% 162.16/41.15 ! [X0 : hoare_1262092251_state] : (((collec1121927558_state @ (fequal1925511196_state @ X0))) = ((insert81609953_state @ X0 @ bot_bo113204042tate_o)))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_singleton__conv2)).
% 162.16/41.15 thf(f289,axiom,(
% 162.16/41.15 ! [X1 : com,X0 : pname] : (wT_bodies => ((((body @ X0)) = ((some_com @ X1))) => (wt @ X1)))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_288_WT__bodiesD)).
% 162.16/41.15 thf(f309,axiom,(
% 162.16/41.15 hoare_1821564147gleton),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 162.16/41.15 thf(f310,axiom,(
% 162.16/41.15 wT_bodies),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 162.16/41.15 thf(f314,axiom,(
% 162.16/41.15 (((body @ pn)) = ((some_com @ y)))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5)).
% 162.16/41.15 thf(f316,conjecture,(
% 162.16/41.15 (hoare_930741239_state @ (image_669833818_state @ (^[X0 : pname] : ((hoare_Mirabelle_MGT @ (body_1 @ X0)))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))),
% 162.16/41.15 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_7)).
% 162.16/41.15 thf(f317,negated_conjecture,(
% 162.16/41.15 ~(hoare_930741239_state @ (image_669833818_state @ (^[X0 : pname] : ((hoare_Mirabelle_MGT @ (body_1 @ X0)))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))),
% 162.16/41.15 inference(negated_conjecture,[status(cth)],[f316])).
% 162.16/41.15 thf(f422,plain,(
% 162.16/41.15 wT_bodies),
% 162.16/41.15 inference(rectify,[],[f310])).
% 162.16/41.15 thf(f423,plain,(
% 162.16/41.15 (wT_bodies = $true)),
% 162.16/41.15 inference(fool_elimination,[],[f422])).
% 162.16/41.15 thf(f436,plain,(
% 162.16/41.15 ~(hoare_930741239_state @ (image_669833818_state @ (^[X0 : pname] : ((hoare_Mirabelle_MGT @ (body_1 @ X0)))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))),
% 162.16/41.15 inference(rectify,[],[f317])).
% 162.16/41.15 thf(f437,plain,(
% 162.16/41.15 ~ (((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))) = $true)),
% 162.16/41.15 inference(fool_elimination,[],[f436])).
% 162.16/41.15 thf(f492,plain,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o),X2 : (hoare_1262092251_state > $o)] : ((hoare_930741239_state @ X1 @ X0) => ((ord_le870406270tate_o @ X1 @ X2) => (hoare_930741239_state @ X2 @ X0)))),
% 162.16/41.15 inference(rectify,[],[f4])).
% 162.16/41.15 thf(f493,plain,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o),X2 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : ((((hoare_930741239_state @ X1 @ X0)) = $true) => ((((ord_le870406270tate_o @ X1 @ X2)) = $true) => ($true = ((hoare_930741239_state @ X2 @ X0)))))),
% 162.16/41.15 inference(fool_elimination,[],[f492])).
% 162.16/41.15 thf(f542,plain,(
% 162.16/41.15 (((collec1121927558_state @ (^[X0 : hoare_1262092251_state] : ($false)))) = bot_bo113204042tate_o)),
% 162.16/41.15 inference(rectify,[],[f167])).
% 162.16/41.15 thf(f543,plain,(
% 162.16/41.15 (bot_bo113204042tate_o = ((collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false)))))),
% 162.16/41.15 inference(fool_elimination,[],[f542])).
% 162.16/41.15 thf(f590,plain,(
% 162.16/41.15 ! [X0 : com,X1 : pname] : (wT_bodies => ((((some_com @ X0)) = ((body @ X1))) => (wt @ X0)))),
% 162.16/41.15 inference(rectify,[],[f289])).
% 162.16/41.15 thf(f591,plain,(
% 162.16/41.15 ! [X0 : com,X1 : pname] : ((wT_bodies = $true) => ((((some_com @ X0)) = ((body @ X1))) => (((wt @ X0)) = $true)))),
% 162.16/41.15 inference(fool_elimination,[],[f590])).
% 162.16/41.15 thf(f634,plain,(
% 162.16/41.15 hoare_1821564147gleton),
% 162.16/41.15 inference(rectify,[],[f309])).
% 162.16/41.15 thf(f635,plain,(
% 162.16/41.15 (hoare_1821564147gleton = $true)),
% 162.16/41.15 inference(fool_elimination,[],[f634])).
% 162.16/41.15 thf(f702,plain,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o)] : (ord_le870406270tate_o @ bot_bo113204042tate_o @ X0)),
% 162.16/41.15 inference(rectify,[],[f34])).
% 162.16/41.15 thf(f703,plain,(
% 162.16/41.15 ! [X0 : (hoare_1262092251_state > $o)] : (((ord_le870406270tate_o @ bot_bo113204042tate_o @ X0)) = $true)),
% 162.16/41.15 inference(fool_elimination,[],[f702])).
% 162.16/41.15 thf(f866,plain,(
% 162.16/41.15 ! [X0 : com] : (hoare_1821564147gleton => (wT_bodies => ((wt @ X0) => (hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o)))))),
% 162.16/41.15 inference(rectify,[],[f104])).
% 162.16/41.15 thf(f867,plain,(
% 162.16/41.15 ! [X0 : com] : ((hoare_1821564147gleton = $true) => ((wT_bodies = $true) => ((((wt @ X0)) = $true) => (((hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o))) = $true))))),
% 162.16/41.16 inference(fool_elimination,[],[f866])).
% 162.16/41.16 thf(f909,plain,(
% 162.16/41.16 (((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))) != $true)),
% 162.16/41.16 inference(flattening,[],[f437])).
% 162.16/41.16 thf(f979,plain,(
% 162.16/41.16 ! [X0 : com,X1 : pname] : (((((wt @ X0)) = $true) | (((some_com @ X0)) != ((body @ X1)))) | (wT_bodies != $true))),
% 162.16/41.16 inference(ennf_transformation,[],[f591])).
% 162.16/41.16 thf(f980,plain,(
% 162.16/41.16 ! [X1 : pname,X0 : com] : ((((wt @ X0)) = $true) | (wT_bodies != $true) | (((some_com @ X0)) != ((body @ X1))))),
% 162.16/41.16 inference(flattening,[],[f979])).
% 162.16/41.16 thf(f1101,plain,(
% 162.16/41.16 ! [X0 : (hoare_1262092251_state > $o),X2 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : ((($true = ((hoare_930741239_state @ X2 @ X0))) | (((ord_le870406270tate_o @ X1 @ X2)) != $true)) | (((hoare_930741239_state @ X1 @ X0)) != $true))),
% 162.16/41.16 inference(ennf_transformation,[],[f493])).
% 162.16/41.16 thf(f1102,plain,(
% 162.16/41.16 ! [X2 : (hoare_1262092251_state > $o),X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ X1 @ X2)) != $true) | (((hoare_930741239_state @ X1 @ X0)) != $true) | ($true = ((hoare_930741239_state @ X2 @ X0))))),
% 162.16/41.16 inference(flattening,[],[f1101])).
% 162.16/41.16 thf(f1118,plain,(
% 162.16/41.16 ! [X0 : com] : ((((((hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o))) = $true) | (((wt @ X0)) != $true)) | (wT_bodies != $true)) | (hoare_1821564147gleton != $true))),
% 162.16/41.16 inference(ennf_transformation,[],[f867])).
% 162.16/41.16 thf(f1119,plain,(
% 162.16/41.16 ! [X0 : com] : ((hoare_1821564147gleton != $true) | (wT_bodies != $true) | (((hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o))) = $true) | (((wt @ X0)) != $true))),
% 162.16/41.16 inference(flattening,[],[f1118])).
% 162.16/41.16 thf(f1380,plain,(
% 162.16/41.16 ! [X0 : pname,X1 : com] : ((((wt @ X1)) = $true) | (wT_bodies != $true) | (((body @ X0)) != ((some_com @ X1))))),
% 162.16/41.16 inference(rectify,[],[f980])).
% 162.16/41.16 thf(f1413,plain,(
% 162.16/41.16 ! [X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o),X2 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ X2 @ X0)) != $true) | (((hoare_930741239_state @ X2 @ X1)) != $true) | (((hoare_930741239_state @ X0 @ X1)) = $true))),
% 162.16/41.16 inference(rectify,[],[f1102])).
% 162.16/41.16 thf(f1694,plain,(
% 162.16/41.16 (hoare_1821564147gleton = $true)),
% 162.16/41.16 inference(cnf_transformation,[],[f635])).
% 162.16/41.16 thf(f1713,plain,(
% 162.16/41.16 (wT_bodies = $true)),
% 162.16/41.16 inference(cnf_transformation,[],[f423])).
% 162.16/41.16 thf(f1729,plain,(
% 162.16/41.16 (((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ bot_bo113204042tate_o))) != $true)),
% 162.16/41.16 inference(cnf_transformation,[],[f909])).
% 162.16/41.16 thf(f1731,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : ((((collec1121927558_state @ X0)) = X0)) )),
% 162.16/41.16 inference(cnf_transformation,[],[f256])).
% 162.16/41.16 thf(f1741,plain,(
% 162.16/41.16 ( ! [X0 : pname,X1 : com] : ((((wt @ X1)) = $true) | (wT_bodies != $true) | (((body @ X0)) != ((some_com @ X1)))) )),
% 162.16/41.16 inference(cnf_transformation,[],[f1380])).
% 162.16/41.16 thf(f1750,plain,(
% 162.16/41.16 (bot_bo113204042tate_o = ((collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false)))))),
% 162.16/41.16 inference(cnf_transformation,[],[f543])).
% 162.16/41.16 thf(f1783,plain,(
% 162.16/41.16 ( ! [X2 : (hoare_1262092251_state > $o),X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ X2 @ X0)) != $true) | (((hoare_930741239_state @ X2 @ X1)) != $true) | (((hoare_930741239_state @ X0 @ X1)) = $true)) )),
% 162.16/41.16 inference(cnf_transformation,[],[f1413])).
% 162.16/41.16 thf(f1804,plain,(
% 162.16/41.16 (((body @ pn)) = ((some_com @ y)))),
% 162.16/41.16 inference(cnf_transformation,[],[f314])).
% 162.16/41.16 thf(f1820,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((hoare_1821564147gleton != $true) | (wT_bodies != $true) | (((hoare_930741239_state @ bot_bo113204042tate_o @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ bot_bo113204042tate_o))) = $true) | (((wt @ X0)) != $true)) )),
% 162.16/41.16 inference(cnf_transformation,[],[f1119])).
% 162.16/41.16 thf(f1825,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ bot_bo113204042tate_o @ X0)) = $true)) )),
% 162.16/41.16 inference(cnf_transformation,[],[f703])).
% 162.16/41.16 thf(f1911,plain,(
% 162.16/41.16 ( ! [X0 : hoare_1262092251_state] : ((((insert81609953_state @ X0 @ bot_bo113204042tate_o)) = ((collec1121927558_state @ (fequal1925511196_state @ X0))))) )),
% 162.16/41.16 inference(cnf_transformation,[],[f285])).
% 162.16/41.16 thf(f1932,definition,(
% 162.16/41.16 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 162.16/41.16 introduced(theory,[fool_exhaustiveness_axiom])).
% 162.16/41.16 thf(f2021,plain,(
% 162.16/41.16 ($true != ((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false)))))))),
% 162.16/41.16 inference(definition_unfolding,[],[f1729,f1750])).
% 162.16/41.16 thf(f2026,plain,(
% 162.16/41.16 ( ! [X0 : pname,X1 : com] : (($true != $true) | (((body @ X0)) != ((some_com @ X1))) | (((wt @ X1)) = $true)) )),
% 162.16/41.16 inference(definition_unfolding,[],[f1741,f1713])).
% 162.16/41.16 thf(f2053,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((((wt @ X0)) != $true) | ($true = ((hoare_930741239_state @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))))))) | ($true != $true) | ($true != $true)) )),
% 162.16/41.16 inference(definition_unfolding,[],[f1820,f1694,f1713,f1750,f1750])).
% 162.16/41.16 thf(f2056,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))) @ X0)) = $true)) )),
% 162.16/41.16 inference(definition_unfolding,[],[f1825,f1750])).
% 162.16/41.16 thf(f2104,plain,(
% 162.16/41.16 ( ! [X0 : hoare_1262092251_state] : ((((collec1121927558_state @ (fequal1925511196_state @ X0))) = ((insert81609953_state @ X0 @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))))))) )),
% 162.16/41.16 inference(definition_unfolding,[],[f1911,f1750])).
% 162.16/41.16 thf(f2196,plain,(
% 162.16/41.16 ( ! [X0 : pname,X1 : com] : ((((body @ X0)) != ((some_com @ X1))) | (((wt @ X1)) = $true)) )),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f2026])).
% 162.16/41.16 thf(f2209,plain,(
% 162.16/41.16 ( ! [X0 : com] : (($true = ((hoare_930741239_state @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))))))) | ($true != $true) | (((wt @ X0)) != $true)) )),
% 162.16/41.16 inference(duplicate_literal_removal,[],[f2053])).
% 162.16/41.16 thf(f2210,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((((wt @ X0)) != $true) | ($true = ((hoare_930741239_state @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false))) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ (collec1121927558_state @ (^[Y0 : hoare_1262092251_state]: ($false)))))))) )),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f2209])).
% 162.16/41.16 thf(f2228,plain,(
% 162.16/41.16 ($true != ((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ (^[Y0 : hoare_1262092251_state]: ($false))))))),
% 162.16/41.16 inference(constrained_superposition,[],[f2021,f1731])).
% 162.16/41.16 thf(f2237,plain,(
% 162.16/41.16 ($false = ((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ (^[Y0 : hoare_1262092251_state]: ($false)))))) | ($true != $true)),
% 162.16/41.16 inference(constrained_superposition,[],[f2228,f1932])).
% 162.16/41.16 thf(f2238,plain,(
% 162.16/41.16 ($false = ((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ y) @ (^[Y0 : hoare_1262092251_state]: ($false))))))),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f2237])).
% 162.16/41.16 thf(f2253,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((((some_com @ y)) != ((some_com @ X0))) | (((wt @ X0)) = $true)) )),
% 162.16/41.16 inference(constrained_superposition,[],[f2196,f1804])).
% 162.16/41.16 thf(f2260,plain,(
% 162.16/41.16 (((wt @ y)) = $true)),
% 162.16/41.16 inference(equality_resolution,[],[f2253])).
% 162.16/41.16 thf(f2360,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : ((((ord_le870406270tate_o @ (^[Y0 : hoare_1262092251_state]: ($false)) @ X0)) = $true)) )),
% 162.16/41.16 inference(forward_demodulation,[],[f2056,f1731])).
% 162.16/41.16 thf(f8450,plain,(
% 162.16/41.16 ( ! [X0 : hoare_1262092251_state] : ((((collec1121927558_state @ (fequal1925511196_state @ X0))) = ((insert81609953_state @ X0 @ (^[Y0 : hoare_1262092251_state]: ($false)))))) )),
% 162.16/41.16 inference(forward_demodulation,[],[f2104,f1731])).
% 162.16/41.16 thf(f8451,plain,(
% 162.16/41.16 ( ! [X0 : hoare_1262092251_state] : ((((fequal1925511196_state @ X0)) = ((insert81609953_state @ X0 @ (^[Y0 : hoare_1262092251_state]: ($false)))))) )),
% 162.16/41.16 inference(forward_demodulation,[],[f8450,f1731])).
% 162.16/41.16 thf(f8453,plain,(
% 162.16/41.16 ($false = ((hoare_930741239_state @ (image_669833818_state @ (^[Y0 : pname]: (hoare_Mirabelle_MGT @ (body_1 @ Y0))) @ (dom_pname_com @ body)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))))),
% 162.16/41.16 inference(constrained_superposition,[],[f2238,f8451])).
% 162.16/41.16 thf(f18095,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : ((((hoare_930741239_state @ X0 @ X1)) = $true) | ($true != $true) | ($true != ((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ X1)))) )),
% 162.16/41.16 inference(constrained_superposition,[],[f1783,f2360])).
% 162.16/41.16 thf(f18115,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o),X1 : (hoare_1262092251_state > $o)] : (($true != ((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ X1))) | (((hoare_930741239_state @ X0 @ X1)) = $true)) )),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f18095])).
% 162.16/41.16 thf(f27576,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (insert81609953_state @ (hoare_Mirabelle_MGT @ X0) @ (^[Y0 : hoare_1262092251_state]: ($false))))) = $true) | (((wt @ X0)) != $true)) )),
% 162.16/41.16 inference(forward_demodulation,[],[f2210,f1731])).
% 162.16/41.16 thf(f27577,plain,(
% 162.16/41.16 ( ! [X0 : com] : ((((wt @ X0)) != $true) | ($true = ((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ X0)))))) )),
% 162.16/41.16 inference(forward_demodulation,[],[f27576,f8451])).
% 162.16/41.16 thf(f27579,plain,(
% 162.16/41.16 ( ! [X0 : com] : (($true = ((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ X0))))) | ($true != $true) | (((wt @ X0)) = $false)) )),
% 162.16/41.16 inference(constrained_superposition,[],[f27577,f1932])).
% 162.16/41.16 thf(f27628,plain,(
% 162.16/41.16 ( ! [X0 : com] : (($true = ((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ X0))))) | (((wt @ X0)) = $false)) )),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f27579])).
% 162.16/41.16 thf(f225451,definition,(
% 162.16/41.16 spl39_771 <=> (((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))) = $true)),
% 162.16/41.16 introduced(definition,[new_symbols(definition,[spl39_771])],[avatar_definition])).
% 162.16/41.16 thf(f225452,plain,(
% 162.16/41.16 (((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))) = $true) | ~spl39_771),
% 162.16/41.16 inference(avatar_component_clause,[],[f225451])).
% 162.16/41.16 thf(f225453,plain,(
% 162.16/41.16 (((hoare_930741239_state @ (^[Y0 : hoare_1262092251_state]: ($false)) @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))) != $true) | spl39_771),
% 162.16/41.16 inference(avatar_component_clause,[],[f225451])).
% 162.16/41.16 thf(f236669,plain,(
% 162.16/41.16 ($false = ((wt @ y))) | ($true != $true) | spl39_771),
% 162.16/41.16 inference(constrained_superposition,[],[f225453,f27628])).
% 162.16/41.16 thf(f236793,plain,(
% 162.16/41.16 ($false = ((wt @ y))) | spl39_771),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f236669])).
% 162.16/41.16 thf(f236801,plain,(
% 162.16/41.16 ($false = $true) | spl39_771),
% 162.16/41.16 inference(constrained_superposition,[],[f236793,f2260])).
% 162.16/41.16 thf(f237043,plain,(
% 162.16/41.16 $false | spl39_771),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f236801])).
% 162.16/41.16 thf(f237044,plain,(
% 162.16/41.16 spl39_771),
% 162.16/41.16 inference(avatar_contradiction_clause,[],[f237043])).
% 162.16/41.16 thf(f237175,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : (($true != $true) | ($true = ((hoare_930741239_state @ X0 @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))))) ) | ~spl39_771),
% 162.16/41.16 inference(constrained_superposition,[],[f18115,f225452])).
% 162.16/41.16 thf(f237400,plain,(
% 162.16/41.16 ( ! [X0 : (hoare_1262092251_state > $o)] : (($true = ((hoare_930741239_state @ X0 @ (fequal1925511196_state @ (hoare_Mirabelle_MGT @ y)))))) ) | ~spl39_771),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f237175])).
% 162.16/41.16 thf(f237745,plain,(
% 162.16/41.16 ($false = $true) | ~spl39_771),
% 162.16/41.16 inference(constrained_superposition,[],[f8453,f237400])).
% 162.16/41.16 thf(f237992,plain,(
% 162.16/41.16 $false | ~spl39_771),
% 162.16/41.16 inference(trivial_inequality_removal,[],[f237745])).
% 162.16/41.16 thf(f237993,plain,(
% 162.16/41.16 ~spl39_771),
% 162.16/41.16 inference(avatar_contradiction_clause,[],[f237992])).
% 162.16/41.16 cnf(s3110, plain, spl39_771, inference(sat_conversion,[],[f237044])).
% 162.16/41.16 cnf(s3116, plain, ~spl39_771, inference(sat_conversion,[],[f237993])).
% 162.16/41.16 cnf(s3119, plain, $false, inference(rat,[],[s3110,s3116])).
% 162.16/41.16 thf(f238018,plain,(
% 162.16/41.16 $false),
% 162.16/41.16 inference(avatar_sat_refutation,[],[s3119])).
% 162.16/41.16 % SZS output end Proof for theBenchmark
% 162.16/41.16 % (270550)------------------------------
% 162.16/41.16 % (270550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 162.16/41.16 % (270550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.16/41.16 % (270550)CaDiCaL version: 2.1.3
% 162.16/41.16 % (270550)Termination reason: Refutation
% 162.16/41.16 % (270550)Time elapsed: 25.343 s
% 162.16/41.16 % (270550)Peak memory usage: 148 MB
% 162.16/41.16 % (270550)Instructions burned: 52674 (million)
% 162.16/41.16 % (270074)Success in time 40.918 s
% 162.16/41.16 % Vampire exiting
%------------------------------------------------------------------------------