%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW470^1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:21 AM UTC 2026
% Result : Theorem 7.21s 1.37s
% Output : Refutation 7.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470^1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 16:04:45 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.25/1.01 % (2854595)Will run a generic schedule for satisfiability detection.
% 4.25/1.01 % (2854611)% WARNING: option uhcvi not known.
% 4.25/1.01 % (2854611)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2774952576:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.25/1.01 % (2854611)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.25/1.01 % (2854610)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2485165477_2999 on theBenchmark for (2999ds/0Mi)
% 4.25/1.01 % (2854615)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2572387677:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.25/1.01 % (2854612)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1548069586:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.25/1.01 % (2854613)dis+10_1_sil=32000:sp=arity:random_seed=1387727385:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.25/1.01 % (2854616)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2768778644:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.25/1.01 % (2854617)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=398457539:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.25/1.01 % (2854611)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.25/1.01 % (2854615)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.25/1.01 % Exception at run slice level
% 4.25/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.25/1.01 % (2854625)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1878935711:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.25/1.01 % Exception at run slice level
% 4.25/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.25/1.01 % (2854613)Instruction limit reached!
% 4.25/1.01 % (2854613)------------------------------
% 4.25/1.01 % (2854613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.01 % (2854613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.01 % (2854613)CaDiCaL version: 2.1.3
% 4.25/1.01 % (2854613)Termination reason: Instruction limit
% 4.25/1.01 % (2854613)Termination phase: Saturation
% 4.25/1.01 % (2854613)Time elapsed: 0.051 s
% 4.25/1.01 % (2854613)Peak memory usage: 12 MB
% 4.25/1.01 % (2854613)Instructions burned: 105 (million)
% 4.25/1.01 % (2854615)Instruction limit reached!
% 4.25/1.01 % (2854615)------------------------------
% 4.25/1.01 % (2854615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.01 % (2854615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.01 % (2854615)CaDiCaL version: 2.1.3
% 4.25/1.01 % (2854615)Termination reason: Instruction limit
% 4.25/1.01 % (2854615)Termination phase: Saturation
% 4.25/1.01 % (2854615)Time elapsed: 0.057 s
% 4.25/1.01 % (2854615)Peak memory usage: 13 MB
% 4.25/1.01 % (2854615)Instructions burned: 116 (million)
% 4.25/1.01 % (2854616)Instruction limit reached!
% 4.25/1.01 % (2854616)------------------------------
% 4.25/1.01 % (2854616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.01 % (2854616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.25/1.01 % (2854616)CaDiCaL version: 2.1.3
% 4.25/1.01 % (2854616)Termination reason: Instruction limit
% 4.25/1.01 % (2854616)Termination phase: Saturation
% 4.25/1.01 % (2854616)Time elapsed: 0.064 s
% 4.25/1.01 % (2854616)Peak memory usage: 13 MB
% 4.25/1.01 % (2854616)Instructions burned: 131 (million)
% 4.25/1.01 % (2854627)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=7020412:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.25/1.01 % (2854628)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=812708369:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.25/1.01 % (2854629)ott-21_1_sil=16000:fs=off:random_seed=647710429:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.25/1.01 % (2854617)Instruction limit reached!
% 4.25/1.01 % (2854617)------------------------------
% 4.25/1.01 % (2854617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.25/1.01 % (2854617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854617)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854617)Termination reason: Instruction limit
% 7.21/1.37 % (2854617)Termination phase: Saturation
% 7.21/1.37 % (2854617)Time elapsed: 0.078 s
% 7.21/1.37 % (2854617)Peak memory usage: 13 MB
% 7.21/1.37 % (2854617)Instructions burned: 160 (million)
% 7.21/1.37 % (2854628)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.21/1.37 % (2854630)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2812611441:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.21/1.37 % (2854628)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.21/1.37 % (2854634)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2959736755:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854637)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=925610154:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.21/1.37 % (2854627)Instruction limit reached!
% 7.21/1.37 % (2854627)------------------------------
% 7.21/1.37 % (2854627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854627)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854627)Termination reason: Instruction limit
% 7.21/1.37 % (2854627)Termination phase: Saturation
% 7.21/1.37 % (2854627)Time elapsed: 0.067 s
% 7.21/1.37 % (2854627)Peak memory usage: 13 MB
% 7.21/1.37 % (2854627)Instructions burned: 132 (million)
% 7.21/1.37 % (2854639)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3209349852:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.21/1.37 % (2854629)Instruction limit reached!
% 7.21/1.37 % (2854629)------------------------------
% 7.21/1.37 % (2854629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854629)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854629)Termination reason: Instruction limit
% 7.21/1.37 % (2854629)Termination phase: Saturation
% 7.21/1.37 % (2854629)Time elapsed: 0.084 s
% 7.21/1.37 % (2854629)Peak memory usage: 13 MB
% 7.21/1.37 % (2854629)Instructions burned: 180 (million)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854641)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=1199055410:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 7.21/1.37 % (2854641)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.21/1.37 % (2854642)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4290732206:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 7.21/1.37 % (2854642)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.21/1.37 % (2854630)Instruction limit reached!
% 7.21/1.37 % (2854630)------------------------------
% 7.21/1.37 % (2854630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854630)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854630)Termination reason: Instruction limit
% 7.21/1.37 % (2854630)Termination phase: Saturation
% 7.21/1.37 % (2854630)Time elapsed: 0.248 s
% 7.21/1.37 % (2854630)Peak memory usage: 14 MB
% 7.21/1.37 % (2854630)Instructions burned: 477 (million)
% 7.21/1.37 % (2854645)fmb+10_1_sil=64000:random_seed=1602936232:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 7.21/1.37 % (2854645)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854647)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2119234289:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 7.21/1.37 % (2854628)Instruction limit reached!
% 7.21/1.37 % (2854628)------------------------------
% 7.21/1.37 % (2854628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854628)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854628)Termination reason: Instruction limit
% 7.21/1.37 % (2854628)Termination phase: Saturation
% 7.21/1.37 % (2854628)Time elapsed: 0.325 s
% 7.21/1.37 % (2854628)Peak memory usage: 16 MB
% 7.21/1.37 % (2854628)Instructions burned: 685 (million)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854649)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2239037978:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 7.21/1.37 % (2854650)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=265935797:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 7.21/1.37 % (2854650)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854653)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4249495310:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 7.21/1.37 % (2854653)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.21/1.37 % (2854653)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.21/1.37 % (2854641)Instruction limit reached!
% 7.21/1.37 % (2854641)------------------------------
% 7.21/1.37 % (2854641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854641)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854641)Termination reason: Instruction limit
% 7.21/1.37 % (2854641)Termination phase: Saturation
% 7.21/1.37 % (2854641)Time elapsed: 0.336 s
% 7.21/1.37 % (2854641)Peak memory usage: 18 MB
% 7.21/1.37 % (2854641)Instructions burned: 694 (million)
% 7.21/1.37 % (2854655)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3030781895:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854657)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1044276999:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854659)ott-2_1_sil=16000:newcnf=on:random_seed=293413649:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 7.21/1.37 % (2854659)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.21/1.37 % (2854642)Instruction limit reached!
% 7.21/1.37 % (2854642)------------------------------
% 7.21/1.37 % (2854642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854642)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854642)Termination reason: Instruction limit
% 7.21/1.37 % (2854642)Termination phase: Saturation
% 7.21/1.37 % (2854642)Time elapsed: 0.430 s
% 7.21/1.37 % (2854642)Peak memory usage: 18 MB
% 7.21/1.37 % (2854642)Instructions burned: 880 (million)
% 7.21/1.37 % (2854661)ott+10_1_sil=32000:tgt=ground:random_seed=971060382:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 7.21/1.37 % (2854637)Instruction limit reached!
% 7.21/1.37 % (2854637)------------------------------
% 7.21/1.37 % (2854637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854637)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854637)Termination reason: Instruction limit
% 7.21/1.37 % (2854637)Termination phase: Saturation
% 7.21/1.37 % (2854637)Time elapsed: 0.557 s
% 7.21/1.37 % (2854637)Peak memory usage: 19 MB
% 7.21/1.37 % (2854637)Instructions burned: 1180 (million)
% 7.21/1.37 % (2854663)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1919215609:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 7.21/1.37 % Exception at run slice level
% 7.21/1.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.21/1.37 % (2854665)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2234389335:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 7.21/1.37 % (2854665)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.21/1.37 % (2854659)Instruction limit reached!
% 7.21/1.37 % (2854659)------------------------------
% 7.21/1.37 % (2854659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854659)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854659)Termination reason: Instruction limit
% 7.21/1.37 % (2854659)Termination phase: Saturation
% 7.21/1.37 % (2854659)Time elapsed: 0.406 s
% 7.21/1.37 % (2854659)Peak memory usage: 16 MB
% 7.21/1.37 % (2854659)Instructions burned: 870 (million)
% 7.21/1.37 % (2854667)dis+21_1_sil=32000:sas=cadical:random_seed=324900805:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 7.21/1.37 % (2854611) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2854595-2854611"...
% 7.21/1.37 % (2854611)...printing done.
% 7.21/1.37 % (2854611)Refutation found. Thanks to Tanya!
% 7.21/1.37 % SZS status Theorem for theBenchmark
% 7.21/1.37 % SZS output start Proof for theBenchmark
% 7.21/1.37 thf(type_def_5, type, x_a: $tType).
% 7.21/1.37 thf(type_def_6, type, com: $tType).
% 7.21/1.37 thf(type_def_7, type, state: $tType).
% 7.21/1.37 thf(type_def_8, type, hoare_669141180iple_a: $tType).
% 7.21/1.37 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 7.21/1.37 thf(func_def_0, type, skip: com).
% 7.21/1.37 thf(func_def_1, type, semi: (com > com > com)).
% 7.21/1.37 thf(func_def_2, type, ex: ((hoare_669141180iple_a > $o) > $o)).
% 7.21/1.37 thf(func_def_3, type, finite957651855iple_a: ((hoare_669141180iple_a > $o) > $o)).
% 7.21/1.37 thf(func_def_4, type, finite840267660iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_5, type, finite684844060iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_6, type, finite590756294iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_7, type, finite972428089iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o)).
% 7.21/1.37 thf(func_def_8, type, finite252461622iple_a: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o)).
% 7.21/1.37 thf(func_def_9, type, the_Ho49089901iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_10, type, hoare_2128652938rivs_a: ((hoare_669141180iple_a > $o) > (hoare_669141180iple_a > $o) > $o)).
% 7.21/1.37 thf(func_def_11, type, hoare_1295064928iple_a: ((x_a > state > $o) > com > (x_a > state > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_12, type, bot_bo280939947le_a_o: (hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_13, type, bot_bot_o: $o).
% 7.21/1.37 thf(func_def_14, type, collec1717965009iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_15, type, insert175534902iple_a: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_16, type, the_el738790235iple_a: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_17, type, fequal182287803iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_18, type, member1016246415iple_a: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > $o)).
% 7.21/1.37 thf(func_def_19, type, g: (hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_20, type, p: (x_a > state > $o)).
% 7.21/1.37 thf(func_def_21, type, b: (state > $o)).
% 7.21/1.37 thf(func_def_22, type, c: com).
% 7.21/1.37 thf(func_def_24, type, vAND: ($o > $o > $o)).
% 7.21/1.37 thf(func_def_25, type, vIMP: ($o > $o > $o)).
% 7.21/1.37 thf(func_def_26, type, vNOT: ($o > $o)).
% 7.21/1.37 thf(func_def_27, type, vOR: ($o > $o > $o)).
% 7.21/1.37 thf(func_def_30, type, db1: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_31, type, db0: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_32, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.21/1.37 thf(func_def_33, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.21/1.37 thf(func_def_34, type, sP0: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_35, type, sK1: ((x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > x_a)).
% 7.21/1.37 thf(func_def_36, type, sK2: ((x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > state)).
% 7.21/1.37 thf(func_def_37, type, sK3: ((x_a > state > $o) > (x_a > state > $o) > x_a)).
% 7.21/1.37 thf(func_def_38, type, sK4: ((x_a > state > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_39, type, sK5: ((x_a > state > $o) > (x_a > state > $o) > x_a)).
% 7.21/1.37 thf(func_def_40, type, sK6: ((x_a > state > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_41, type, sK7: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > x_a)).
% 7.21/1.37 thf(func_def_42, type, sK8: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_43, type, sK9: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_44, type, sK10: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_45, type, sK11: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_46, type, sK12: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_47, type, sK13: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_48, type, sK14: (hoare_669141180iple_a > x_a > state > $o)).
% 7.21/1.37 thf(func_def_49, type, sK15: (hoare_669141180iple_a > com)).
% 7.21/1.37 thf(func_def_50, type, sK16: (hoare_669141180iple_a > x_a > state > $o)).
% 7.21/1.37 thf(func_def_51, type, sK17: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_52, type, sK18: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_53, type, sK19: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_54, type, sK20: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_55, type, sK21: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_56, type, sK22: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_57, type, sK23: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_58, type, sK24: ((x_a > state > $o) > com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > x_a)).
% 7.21/1.37 thf(func_def_59, type, sK25: ((x_a > state > $o) > com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_60, type, sK26: ((x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > state)).
% 7.21/1.37 thf(func_def_61, type, sK27: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_62, type, sK28: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_63, type, sK29: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_64, type, sK30: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_65, type, sK31: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_66, type, sK32: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_67, type, sK33: (((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_68, type, sK34: (((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_69, type, sK35: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_70, type, sK36: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_71, type, sK37: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_72, type, sK38: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_73, type, sK39: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_74, type, sK40: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_75, type, sK41: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_76, type, sK42: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_77, type, sK43: (((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_78, type, sK44: (((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a > $o)).
% 7.21/1.37 thf(func_def_79, type, sK45: (((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_81, type, sK47: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_82, type, sK48: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_83, type, sK49: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_84, type, sK50: (hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_85, type, sK51: (hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_86, type, db2: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_87, type, db3: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_88, type, db4: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_89, type, sK52: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_90, type, sK53: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_91, type, sK54: (hoare_669141180iple_a > (hoare_669141180iple_a > $o) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_92, type, sK55: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_93, type, sK56: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_94, type, sK57: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_95, type, sK58: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_96, type, sK59: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_97, type, sK60: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_98, type, sK61: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_99, type, sK62: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_100, type, sK63: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_101, type, sK64: ((hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_102, type, sK65: ((hoare_669141180iple_a > hoare_669141180iple_a > $o) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_103, type, sK66: hoare_669141180iple_a).
% 7.21/1.37 thf(func_def_104, type, sK67: hoare_669141180iple_a).
% 7.21/1.37 thf(func_def_105, type, sK68: hoare_669141180iple_a).
% 7.21/1.37 thf(func_def_106, type, sK69: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_107, type, db6: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_108, type, db5: !>[X0: $tType]:(X0)).
% 7.21/1.37 thf(func_def_109, type, sK70: ((hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_110, type, sK71: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_111, type, sK72: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_112, type, sK73: ((hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_113, type, sK74: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(func_def_114, type, sK75: ((hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > hoare_669141180iple_a > $o) > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a > $o) > hoare_669141180iple_a)).
% 7.21/1.37 thf(f6,axiom,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : (! [X4 : x_a,X5 : state] : ((X3 @ X4 @ X5) => (hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X6 : x_a, X7 : state] : ((X7 = X5))) @ X1 @ (^[X8 : x_a] : ((X2 @ X4)))) @ bot_bo280939947le_a_o))) => (hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o)))),
% 7.21/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_escape)).
% 7.21/1.37 thf(f13,axiom,(
% 7.21/1.37 ! [X0 : hoare_669141180iple_a] : (((collec1717965009iple_a @ (fequal182287803iple_a @ X0))) = ((insert175534902iple_a @ X0 @ bot_bo280939947le_a_o)))),
% 7.21/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_singleton__conv2)).
% 7.21/1.37 thf(f23,axiom,(
% 7.21/1.37 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[X0 : hoare_669141180iple_a] : ($false)))))),
% 7.21/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_empty__def)).
% 7.21/1.37 thf(f75,axiom,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o)] : (((collec1717965009iple_a @ X0)) = X0)),
% 7.21/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_Collect__def)).
% 7.21/1.37 thf(f98,conjecture,(
% 7.21/1.37 (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X0 : x_a, X1 : state] : (((p @ X0 @ X1) & (~ (b @ X1)))))) @ bot_bo280939947le_a_o))),
% 7.21/1.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 7.21/1.37 thf(f99,negated_conjecture,(
% 7.21/1.37 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X0 : x_a, X1 : state] : (((p @ X0 @ X1) & (~ (b @ X1)))))) @ bot_bo280939947le_a_o))),
% 7.21/1.37 inference(negated_conjecture,[status(cth)],[f98])).
% 7.21/1.37 thf(f108,plain,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : (! [X4 : x_a,X5 : state] : ((X3 @ X4 @ X5) => (hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X6 : x_a, X7 : state] : ((X7 = X5))) @ X1 @ (^[X8 : x_a] : ((X2 @ X4)))) @ bot_bo280939947le_a_o))) => (hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o)))),
% 7.21/1.37 inference(rectify,[],[f6])).
% 7.21/1.37 thf(f109,plain,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : (! [X4 : x_a,X5 : state] : ((((X3 @ X4 @ X5)) = $true) => ($true = ((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: (X5 = Y1)))) @ X1 @ (^[Y0 : x_a]: (X2 @ X4))) @ bot_bo280939947le_a_o))))) => (((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o))) = $true))),
% 7.21/1.37 inference(fool_elimination,[],[f108])).
% 7.21/1.37 thf(f140,plain,(
% 7.21/1.37 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[X0 : hoare_669141180iple_a] : ($false)))))),
% 7.21/1.37 inference(rectify,[],[f23])).
% 7.21/1.37 thf(f141,plain,(
% 7.21/1.37 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))),
% 7.21/1.37 inference(fool_elimination,[],[f140])).
% 7.21/1.37 thf(f258,plain,(
% 7.21/1.37 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X2 : x_a, X3 : state] : (((p @ X2 @ X3) & (~ (b @ X3)))))) @ bot_bo280939947le_a_o))),
% 7.21/1.37 inference(rectify,[],[f99])).
% 7.21/1.37 thf(f259,plain,(
% 7.21/1.37 ~ ($true = ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))))),
% 7.21/1.37 inference(fool_elimination,[],[f258])).
% 7.21/1.37 thf(f283,plain,(
% 7.21/1.37 ($true != ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))))),
% 7.21/1.37 inference(flattening,[],[f259])).
% 7.21/1.37 thf(f289,plain,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o))) = $true) | ? [X4 : x_a,X5 : state] : (($true != ((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: (X5 = Y1)))) @ X1 @ (^[Y0 : x_a]: (X2 @ X4))) @ bot_bo280939947le_a_o)))) & (((X3 @ X4 @ X5)) = $true)))),
% 7.21/1.37 inference(ennf_transformation,[],[f109])).
% 7.21/1.37 thf(f357,plain,(
% 7.21/1.37 ! [X0 : (hoare_669141180iple_a > $o),X1 : com,X2 : (x_a > state > $o),X3 : (x_a > state > $o)] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o))) = $true) | (($true != ((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ((sK2 @ X3 @ X2 @ X1 @ X0) = Y1)))) @ X1 @ (^[Y0 : x_a]: (X2 @ (sK1 @ X3 @ X2 @ X1 @ X0)))) @ bot_bo280939947le_a_o)))) & ($true = ((X3 @ (sK1 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))))))),
% 7.21/1.37 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X5,sK2 @ X3 @ X2 @ X1 @ X0),skolemize(X5,sK2 @ X3 @ X2 @ X1 @ X0)],[f289])).
% 7.21/1.37 thf(f424,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : ((((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ bot_bo280939947le_a_o))) = $true) | ($true = ((X3 @ (sK1 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))))) )),
% 7.21/1.37 inference(cnf_transformation,[],[f357])).
% 7.21/1.37 thf(f437,plain,(
% 7.21/1.37 ( ! [X0 : hoare_669141180iple_a] : ((((collec1717965009iple_a @ (fequal182287803iple_a @ X0))) = ((insert175534902iple_a @ X0 @ bot_bo280939947le_a_o)))) )),
% 7.21/1.37 inference(cnf_transformation,[],[f13])).
% 7.21/1.37 thf(f453,plain,(
% 7.21/1.37 (bot_bo280939947le_a_o = ((collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))),
% 7.21/1.37 inference(cnf_transformation,[],[f141])).
% 7.21/1.37 thf(f531,plain,(
% 7.21/1.37 ( ! [X0 : (hoare_669141180iple_a > $o)] : ((((collec1717965009iple_a @ X0)) = X0)) )),
% 7.21/1.37 inference(cnf_transformation,[],[f75])).
% 7.21/1.37 thf(f583,plain,(
% 7.21/1.37 ($true != ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o))))),
% 7.21/1.37 inference(cnf_transformation,[],[f283])).
% 7.21/1.37 thf(f585,definition,(
% 7.21/1.37 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 7.21/1.37 introduced(theory,[fool_exhaustiveness_axiom])).
% 7.21/1.37 thf(f591,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = ((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) | ($true = ((X3 @ (sK1 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))))) )),
% 7.21/1.37 inference(definition_unfolding,[],[f424,f453])).
% 7.21/1.37 thf(f600,plain,(
% 7.21/1.37 ( ! [X0 : hoare_669141180iple_a] : ((((collec1717965009iple_a @ (fequal182287803iple_a @ X0))) = ((insert175534902iple_a @ X0 @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) )),
% 7.21/1.37 inference(definition_unfolding,[],[f437,f453])).
% 7.21/1.37 thf(f673,plain,(
% 7.21/1.37 ($true != ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))))),
% 7.21/1.37 inference(definition_unfolding,[],[f583,f453])).
% 7.21/1.37 thf(f751,plain,(
% 7.21/1.37 ($true != $true) | ($false = ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))))),
% 7.21/1.37 inference(constrained_superposition,[],[f673,f585])).
% 7.21/1.37 thf(f752,plain,(
% 7.21/1.37 ($false = ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))))),
% 7.21/1.37 inference(trivial_inequality_removal,[],[f751])).
% 7.21/1.37 thf(f757,plain,(
% 7.21/1.37 ($false = ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (^[Y0 : hoare_669141180iple_a]: ($false))))))),
% 7.21/1.37 inference(constrained_superposition,[],[f752,f531])).
% 7.21/1.37 thf(f2218,plain,(
% 7.21/1.37 ( ! [X0 : hoare_669141180iple_a] : ((((collec1717965009iple_a @ (fequal182287803iple_a @ X0))) = ((insert175534902iple_a @ X0 @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) )),
% 7.21/1.37 inference(forward_demodulation,[],[f600,f531])).
% 7.21/1.37 thf(f2219,plain,(
% 7.21/1.37 ( ! [X0 : hoare_669141180iple_a] : ((((fequal182287803iple_a @ X0)) = ((insert175534902iple_a @ X0 @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) )),
% 7.21/1.37 inference(forward_demodulation,[],[f2218,f531])).
% 7.21/1.37 thf(f2347,plain,(
% 7.21/1.37 ($false = ((hoare_2128652938rivs_a @ g @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1)))))))))))),
% 7.21/1.37 inference(constrained_superposition,[],[f757,f2219])).
% 7.21/1.37 thf(f7143,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = ((hoare_2128652938rivs_a @ X0 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2) @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) | ($true = ((X3 @ (sK1 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0))))) )),
% 7.21/1.37 inference(forward_demodulation,[],[f591,f531])).
% 7.21/1.37 thf(f7144,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X3 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = ((X3 @ (sK1 @ X3 @ X2 @ X1 @ X0) @ (sK2 @ X3 @ X2 @ X1 @ X0)))) | ($true = ((hoare_2128652938rivs_a @ X0 @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ X3 @ X1 @ X2)))))) )),
% 7.21/1.37 inference(forward_demodulation,[],[f7143,f2219])).
% 7.21/1.37 thf(f7146,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = (((^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ (sK1 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ X2 @ X1 @ X0) @ (sK2 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ X2 @ X1 @ X0)))) | ($true = ((hoare_2128652938rivs_a @ X0 @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ X1 @ X2)))))) )),
% 7.21/1.37 inference(primitive_instantiation,[],[f7144])).
% 7.21/1.37 thf(f7423,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = $false) | ($true = ((hoare_2128652938rivs_a @ X0 @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ X1 @ X2)))))) )),
% 7.21/1.37 inference(beta-eta_normalization,[],[f7146])).
% 7.21/1.37 thf(f7424,plain,(
% 7.21/1.37 ( ! [X2 : (x_a > state > $o),X0 : (hoare_669141180iple_a > $o),X1 : com] : (($true = ((hoare_2128652938rivs_a @ X0 @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ X1 @ X2)))))) )),
% 7.21/1.37 inference(trivial_inequality_removal,[],[f7423])).
% 7.21/1.37 thf(f21289,plain,(
% 7.21/1.37 ($true = $false)),
% 7.21/1.37 inference(constrained_superposition,[],[f2347,f7424])).
% 7.21/1.37 thf(f21321,plain,(
% 7.21/1.37 $false),
% 7.21/1.37 inference(trivial_inequality_removal,[],[f21289])).
% 7.21/1.37 % SZS output end Proof for theBenchmark
% 7.21/1.37 % (2854611)------------------------------
% 7.21/1.37 % (2854611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.21/1.37 % (2854611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.21/1.37 % (2854611)CaDiCaL version: 2.1.3
% 7.21/1.37 % (2854611)Termination reason: Refutation
% 7.21/1.37 % (2854611)Time elapsed: 1.091 s
% 7.21/1.37 % (2854611)Peak memory usage: 30 MB
% 7.21/1.37 % (2854611)Instructions burned: 4427 (million)
% 7.21/1.37 % (2854595)Success in time 1.13 s
% 7.21/1.37 % Vampire exiting
%------------------------------------------------------------------------------