%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP059^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:10:33 AM UTC 2026
% Result : Theorem 205.63s 29.24s
% Output : Refutation 205.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP059^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n010.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 19:45:04 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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.39/1.03 % (3318630)Will run a generic schedule for satisfiability detection.
% 4.39/1.03 % (3318647)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2053335354:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.39/1.03 % (3318646)% WARNING: option uhcvi not known.
% 4.39/1.03 % (3318648)dis+10_1_sil=32000:sp=arity:random_seed=2621308870:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.39/1.03 % (3318645)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1420448022_2999 on theBenchmark for (2999ds/0Mi)
% 4.39/1.03 % (3318646)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2943644966:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.39/1.03 % (3318650)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4134619751:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.39/1.03 % (3318652)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1061370150:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.39/1.03 % (3318651)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2974481981:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.39/1.03 % (3318646)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.39/1.03 % (3318650)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.39/1.03 % Exception at run slice level
% 4.39/1.03 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.39/1.03 % (3318646)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.39/1.03 % (3318648)Instruction limit reached!
% 4.39/1.03 % (3318648)------------------------------
% 4.39/1.03 % (3318648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/1.03 % (3318648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/1.03 % (3318648)CaDiCaL version: 2.1.3
% 4.39/1.03 % (3318648)Termination reason: Instruction limit
% 4.39/1.03 % (3318648)Termination phase: Saturation
% 4.39/1.03 % (3318648)Time elapsed: 0.044 s
% 4.39/1.03 % (3318648)Peak memory usage: 12 MB
% 4.39/1.03 % (3318648)Instructions burned: 103 (million)
% 4.39/1.03 % (3318685)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2646846782:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.39/1.03 % (3318650)Instruction limit reached!
% 4.39/1.03 % (3318650)------------------------------
% 4.39/1.03 % (3318650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/1.03 % (3318650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/1.03 % (3318650)CaDiCaL version: 2.1.3
% 4.39/1.03 % (3318650)Termination reason: Instruction limit
% 4.39/1.03 % (3318650)Termination phase: Saturation
% 4.39/1.03 % (3318650)Time elapsed: 0.052 s
% 4.39/1.03 % (3318650)Peak memory usage: 13 MB
% 4.39/1.03 % (3318650)Instructions burned: 116 (million)
% 4.39/1.03 % (3318651)Instruction limit reached!
% 4.39/1.03 % (3318651)------------------------------
% 4.39/1.03 % (3318651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/1.03 % (3318651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/1.03 % (3318651)CaDiCaL version: 2.1.3
% 4.39/1.03 % (3318651)Termination reason: Instruction limit
% 4.39/1.03 % (3318651)Termination phase: Saturation
% 4.39/1.03 % (3318651)Time elapsed: 0.059 s
% 4.39/1.03 % (3318651)Peak memory usage: 13 MB
% 4.39/1.03 % (3318651)Instructions burned: 132 (million)
% 4.39/1.03 % (3318689)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3616788920:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.39/1.03 % (3318691)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=2096564098:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.39/1.03 % (3318652)Instruction limit reached!
% 4.39/1.03 % (3318652)------------------------------
% 4.39/1.03 % (3318652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.39/1.03 % (3318652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.39/1.03 % (3318652)CaDiCaL version: 2.1.3
% 4.39/1.03 % (3318652)Termination reason: Instruction limit
% 4.39/1.03 % (3318652)Termination phase: Saturation
% 4.39/1.03 % (3318652)Time elapsed: 0.077 s
% 4.39/1.03 % (3318652)Peak memory usage: 14 MB
% 4.39/1.03 % (3318652)Instructions burned: 159 (million)
% 19.90/3.06 % (3318692)ott-21_1_sil=16000:fs=off:random_seed=4035214339:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 19.90/3.06 % Exception at run slice level
% 19.90/3.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.90/3.06 % (3318691)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 19.90/3.06 % (3318696)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3045160959:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.90/3.06 % (3318697)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2691372967:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 19.90/3.06 % (3318691)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 19.90/3.06 % (3318689)Instruction limit reached!
% 19.90/3.06 % (3318689)------------------------------
% 19.90/3.06 % (3318689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.06 % (3318689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.06 % (3318689)CaDiCaL version: 2.1.3
% 19.90/3.06 % (3318689)Termination reason: Instruction limit
% 19.90/3.06 % (3318689)Termination phase: Saturation
% 19.90/3.06 % (3318689)Time elapsed: 0.062 s
% 19.90/3.06 % (3318689)Peak memory usage: 13 MB
% 19.90/3.06 % (3318689)Instructions burned: 132 (million)
% 19.90/3.06 % Exception at run slice level
% 19.90/3.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.90/3.06 % (3318700)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3089064693:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 19.90/3.06 % (3318701)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3866603273:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 19.90/3.06 % (3318692)Instruction limit reached!
% 19.90/3.06 % (3318692)------------------------------
% 19.90/3.06 % (3318692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.06 % (3318692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.06 % (3318692)CaDiCaL version: 2.1.3
% 19.90/3.06 % (3318692)Termination reason: Instruction limit
% 19.90/3.06 % (3318692)Termination phase: Saturation
% 19.90/3.06 % (3318692)Time elapsed: 0.078 s
% 19.90/3.06 % (3318692)Peak memory usage: 13 MB
% 19.90/3.06 % (3318692)Instructions burned: 181 (million)
% 19.90/3.06 % (3318704)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=3460515488: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)
% 19.90/3.06 % Exception at run slice level
% 19.90/3.06 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.90/3.06 % (3318704)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 19.90/3.06 % (3318706)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=553593269:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 19.90/3.06 % (3318706)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 19.90/3.06 % (3318696)Instruction limit reached!
% 19.90/3.06 % (3318696)------------------------------
% 19.90/3.06 % (3318696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.06 % (3318696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.06 % (3318696)CaDiCaL version: 2.1.3
% 19.90/3.06 % (3318696)Termination reason: Instruction limit
% 19.90/3.06 % (3318696)Termination phase: Saturation
% 19.90/3.06 % (3318696)Time elapsed: 0.258 s
% 19.90/3.06 % (3318696)Peak memory usage: 14 MB
% 19.90/3.06 % (3318696)Instructions burned: 478 (million)
% 19.90/3.06 % (3318691)Instruction limit reached!
% 19.90/3.06 % (3318691)------------------------------
% 19.90/3.06 % (3318691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.90/3.06 % (3318691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.90/3.06 % (3318691)CaDiCaL version: 2.1.3
% 19.90/3.06 % (3318691)Termination reason: Instruction limit
% 19.90/3.06 % (3318691)Termination phase: Saturation
% 19.90/3.06 % (3318691)Time elapsed: 0.303 s
% 19.90/3.06 % (3318691)Peak memory usage: 15 MB
% 19.90/3.06 % (3318691)Instructions burned: 685 (million)
% 19.90/3.06 % (3318708)fmb+10_1_sil=64000:random_seed=412557323:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 50.17/7.31 % (3318710)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3118234349:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 50.17/7.31 % (3318708)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 50.17/7.31 % Exception at run slice level
% 50.17/7.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 50.17/7.31 % Exception at run slice level
% 50.17/7.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 50.17/7.31 % (3318712)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1983749166:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 50.17/7.31 % (3318714)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=776376269:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 50.17/7.31 % (3318714)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 50.17/7.31 % Exception at run slice level
% 50.17/7.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 50.17/7.31 % (3318716)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2024414201:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 50.17/7.31 % (3318716)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 50.17/7.31 % (3318716)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 50.17/7.31 % (3318704)Instruction limit reached!
% 50.17/7.31 % (3318704)------------------------------
% 50.17/7.31 % (3318704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.17/7.31 % (3318704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.17/7.31 % (3318704)CaDiCaL version: 2.1.3
% 50.17/7.31 % (3318704)Termination reason: Instruction limit
% 50.17/7.31 % (3318704)Termination phase: Saturation
% 50.17/7.31 % (3318704)Time elapsed: 0.341 s
% 50.17/7.31 % (3318704)Peak memory usage: 16 MB
% 50.17/7.31 % (3318704)Instructions burned: 693 (million)
% 50.17/7.31 % (3318718)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=843394844:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 50.17/7.31 % Exception at run slice level
% 50.17/7.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 50.17/7.31 % (3318720)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1955033460:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 50.17/7.31 % Exception at run slice level
% 50.17/7.31 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 50.17/7.31 % (3318722)ott-2_1_sil=16000:newcnf=on:random_seed=3557143666:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 50.17/7.31 % (3318706)Instruction limit reached!
% 50.17/7.31 % (3318706)------------------------------
% 50.17/7.31 % (3318706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.17/7.31 % (3318706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.17/7.31 % (3318706)CaDiCaL version: 2.1.3
% 50.17/7.31 % (3318706)Termination reason: Instruction limit
% 50.17/7.31 % (3318706)Termination phase: Saturation
% 50.17/7.31 % (3318706)Time elapsed: 0.436 s
% 50.17/7.31 % (3318706)Peak memory usage: 18 MB
% 50.17/7.31 % (3318706)Instructions burned: 881 (million)
% 50.17/7.31 % (3318722)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 50.17/7.31 % (3318724)ott+10_1_sil=32000:tgt=ground:random_seed=2692962225:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 50.17/7.31 % (3318700)Instruction limit reached!
% 50.17/7.31 % (3318700)------------------------------
% 50.17/7.31 % (3318700)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 50.17/7.31 % (3318700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.17/7.31 % (3318700)CaDiCaL version: 2.1.3
% 50.17/7.31 % (3318700)Termination reason: Instruction limit
% 50.17/7.31 % (3318700)Termination phase: Saturation
% 50.17/7.31 % (3318700)Time elapsed: 0.564 s
% 50.17/7.31 % (3318700)Peak memory usage: 19 MB
% 50.17/7.31 % (3318700)Instructions burned: 1179 (million)
% 50.17/7.31 % (3318726)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3689402924:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 50.17/7.31 % Exception at run slice level
% 111.22/16.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 111.22/16.02 % (3318728)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=921612099:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 111.22/16.02 % (3318728)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 111.22/16.02 % (3318722)Instruction limit reached!
% 111.22/16.02 % (3318722)------------------------------
% 111.22/16.02 % (3318722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 111.22/16.02 % (3318722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.22/16.02 % (3318722)CaDiCaL version: 2.1.3
% 111.22/16.02 % (3318722)Termination reason: Instruction limit
% 111.22/16.02 % (3318722)Termination phase: Saturation
% 111.22/16.02 % (3318722)Time elapsed: 0.409 s
% 111.22/16.02 % (3318722)Peak memory usage: 17 MB
% 111.22/16.02 % (3318722)Instructions burned: 871 (million)
% 111.22/16.02 % (3318730)dis+21_1_sil=32000:sas=cadical:random_seed=21655615:i=3773:amm=off_2989 on theBenchmark for (2989ds/3773Mi)
% 111.22/16.02 % (3318716)Instruction limit reached!
% 111.22/16.02 % (3318716)------------------------------
% 111.22/16.02 % (3318716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 111.22/16.02 % (3318716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.22/16.02 % (3318716)CaDiCaL version: 2.1.3
% 111.22/16.02 % (3318716)Termination reason: Instruction limit
% 111.22/16.02 % (3318716)Termination phase: Saturation
% 111.22/16.02 % (3318716)Time elapsed: 0.637 s
% 111.22/16.02 % (3318716)Peak memory usage: 16 MB
% 111.22/16.02 % (3318716)Instructions burned: 1474 (million)
% 111.22/16.02 % (3318732)ott+11_1_sil=16000:gs=on:random_seed=942498746:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 111.22/16.02 % (3318732)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 111.22/16.02 % (3318732)Instruction limit reached!
% 111.22/16.02 % (3318732)------------------------------
% 111.22/16.02 % (3318732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 111.22/16.02 % (3318732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.22/16.02 % (3318732)CaDiCaL version: 2.1.3
% 111.22/16.02 % (3318732)Termination reason: Instruction limit
% 111.22/16.02 % (3318732)Termination phase: Saturation
% 111.22/16.02 % (3318732)Time elapsed: 1.053 s
% 111.22/16.02 % (3318732)Peak memory usage: 19 MB
% 111.22/16.02 % (3318732)Instructions burned: 2252 (million)
% 111.22/16.02 % (3318734)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=59720882:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi)
% 111.22/16.02 % Exception at run slice level
% 111.22/16.02 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 111.22/16.02 % (3318736)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2870001538:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2977 on theBenchmark for (2977ds/4591Mi)
% 111.22/16.02 % (3318728)Instruction limit reached!
% 111.22/16.02 % (3318728)------------------------------
% 111.22/16.02 % (3318728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 111.22/16.02 % (3318728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.22/16.02 % (3318728)CaDiCaL version: 2.1.3
% 111.22/16.02 % (3318728)Termination reason: Instruction limit
% 111.22/16.02 % (3318728)Termination phase: Saturation
% 111.22/16.02 % (3318728)Time elapsed: 1.613 s
% 111.22/16.02 % (3318728)Peak memory usage: 27 MB
% 111.22/16.02 % (3318728)Instructions burned: 3513 (million)
% 111.22/16.02 % (3318738)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3243249211:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 111.22/16.02 % (3318714)Instruction limit reached!
% 111.22/16.02 % (3318714)------------------------------
% 111.22/16.02 % (3318714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 111.22/16.02 % (3318714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.22/16.02 % (3318714)CaDiCaL version: 2.1.3
% 111.22/16.02 % (3318714)Termination reason: Instruction limit
% 111.22/16.02 % (3318714)Termination phase: Saturation
% 111.22/16.02 % (3318714)Time elapsed: 2.348 s
% 111.22/16.02 % (3318714)Peak memory usage: 30 MB
% 111.22/16.02 % (3318714)Instructions burned: 5131 (million)
% 111.22/16.02 % (3318730)Instruction limit reached!
% 111.22/16.02 % (3318730)------------------------------
% 111.22/16.02 % (3318730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.72/20.25 % (3318730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.72/20.25 % (3318730)CaDiCaL version: 2.1.3
% 141.72/20.25 % (3318730)Termination reason: Instruction limit
% 141.72/20.25 % (3318730)Termination phase: Saturation
% 141.72/20.25 % (3318730)Time elapsed: 1.731 s
% 141.72/20.25 % (3318730)Peak memory usage: 29 MB
% 141.72/20.25 % (3318730)Instructions burned: 3773 (million)
% 141.72/20.25 % (3318740)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=421705335:i=5211_2971 on theBenchmark for (2971ds/5211Mi)
% 141.72/20.25 % (3318741)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4171522643:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi)
% 141.72/20.25 % Exception at run slice level
% 141.72/20.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 141.72/20.25 % (3318744)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3722507171:fmbsr=2:i=46332_2971 on theBenchmark for (2971ds/46332Mi)
% 141.72/20.25 % Exception at run slice level
% 141.72/20.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 141.72/20.25 % (3318746)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2896658559:i=14071_2970 on theBenchmark for (2970ds/14071Mi)
% 141.72/20.25 % Exception at run slice level
% 141.72/20.25 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 141.72/20.25 % (3318748)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2645084084:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi)
% 141.72/20.25 % (3318724)Instruction limit reached!
% 141.72/20.25 % (3318724)------------------------------
% 141.72/20.25 % (3318724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.72/20.25 % (3318724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.72/20.25 % (3318724)CaDiCaL version: 2.1.3
% 141.72/20.25 % (3318724)Termination reason: Instruction limit
% 141.72/20.25 % (3318724)Termination phase: Saturation
% 141.72/20.25 % (3318724)Time elapsed: 2.427 s
% 141.72/20.25 % (3318724)Peak memory usage: 43 MB
% 141.72/20.25 % (3318724)Instructions burned: 5115 (million)
% 141.72/20.25 % (3318750)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3778759440:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi)
% 141.72/20.25 % (3318736)Instruction limit reached!
% 141.72/20.25 % (3318736)------------------------------
% 141.72/20.25 % (3318736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.72/20.25 % (3318736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.72/20.25 % (3318736)CaDiCaL version: 2.1.3
% 141.72/20.25 % (3318736)Termination reason: Instruction limit
% 141.72/20.25 % (3318736)Termination phase: Saturation
% 141.72/20.25 % (3318736)Time elapsed: 2.211 s
% 141.72/20.25 % (3318736)Peak memory usage: 27 MB
% 141.72/20.25 % (3318736)Instructions burned: 4591 (million)
% 141.72/20.25 % (3318752)dis+10_16:1_sil=16000:random_seed=2344179649:i=9155:fsr=off_2955 on theBenchmark for (2955ds/9155Mi)
% 141.72/20.25 % (3318740)Instruction limit reached!
% 141.72/20.25 % (3318740)------------------------------
% 141.72/20.25 % (3318740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.72/20.25 % (3318740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.72/20.25 % (3318740)CaDiCaL version: 2.1.3
% 141.72/20.25 % (3318740)Termination reason: Instruction limit
% 141.72/20.25 % (3318740)Termination phase: Saturation
% 141.72/20.25 % (3318740)Time elapsed: 2.440 s
% 141.72/20.25 % (3318740)Peak memory usage: 40 MB
% 141.72/20.25 % (3318740)Instructions burned: 5213 (million)
% 141.72/20.25 % (3318754)ott-3_8_sil=64000:random_seed=2106376221:i=20139:bs=on_2947 on theBenchmark for (2947ds/20139Mi)
% 141.72/20.25 % (3318750)Instruction limit reached!
% 141.72/20.25 % (3318750)------------------------------
% 141.72/20.25 % (3318750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 141.72/20.25 % (3318750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.72/20.25 % (3318750)CaDiCaL version: 2.1.3
% 141.72/20.25 % (3318750)Termination reason: Instruction limit
% 141.72/20.25 % (3318750)Termination phase: Saturation
% 141.72/20.25 % (3318750)Time elapsed: 3.908 s
% 141.72/20.25 % (3318750)Peak memory usage: 54 MB
% 141.72/20.25 % (3318750)Instructions burned: 8174 (million)
% 141.72/20.25 % (3318756)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=518609152:fmbsr=2:i=32576_2929 on theBenchmark for (2929ds/32576Mi)
% 150.96/21.53 % Exception at run slice level
% 150.96/21.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.96/21.53 % (3318758)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=804989413:i=11404_2928 on theBenchmark for (2928ds/11404Mi)
% 150.96/21.53 % (3318752)Instruction limit reached!
% 150.96/21.53 % (3318752)------------------------------
% 150.96/21.53 % (3318752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.96/21.53 % (3318752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.96/21.53 % (3318752)CaDiCaL version: 2.1.3
% 150.96/21.53 % (3318752)Termination reason: Instruction limit
% 150.96/21.53 % (3318752)Termination phase: Saturation
% 150.96/21.53 % (3318752)Time elapsed: 4.173 s
% 150.96/21.53 % (3318752)Peak memory usage: 42 MB
% 150.96/21.53 % (3318752)Instructions burned: 9155 (million)
% 150.96/21.53 % (3318760)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3517707959:i=14134_2913 on theBenchmark for (2913ds/14134Mi)
% 150.96/21.53 % (3318760)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 150.96/21.53 % (3318758)Instruction limit reached!
% 150.96/21.53 % (3318758)------------------------------
% 150.96/21.53 % (3318758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.96/21.53 % (3318758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.96/21.53 % (3318758)CaDiCaL version: 2.1.3
% 150.96/21.53 % (3318758)Termination reason: Instruction limit
% 150.96/21.53 % (3318758)Termination phase: Saturation
% 150.96/21.53 % (3318758)Time elapsed: 5.636 s
% 150.96/21.53 % (3318758)Peak memory usage: 72 MB
% 150.96/21.53 % (3318758)Instructions burned: 11405 (million)
% 150.96/21.53 % (3318762)dis+33_16_sil=32000:sac=on:random_seed=3300861690:i=15851:nm=0_2872 on theBenchmark for (2872ds/15851Mi)
% 150.96/21.53 % (3318754)Instruction limit reached!
% 150.96/21.53 % (3318754)------------------------------
% 150.96/21.53 % (3318754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.96/21.53 % (3318754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.96/21.53 % (3318754)CaDiCaL version: 2.1.3
% 150.96/21.53 % (3318754)Termination reason: Instruction limit
% 150.96/21.53 % (3318754)Termination phase: Saturation
% 150.96/21.53 % (3318754)Time elapsed: 8.531 s
% 150.96/21.53 % (3318754)Peak memory usage: 44 MB
% 150.96/21.53 % (3318754)Instructions burned: 20141 (million)
% 150.96/21.53 % (3318880)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2888488109:avsq=on:i=17627:add=on:amm=off_2861 on theBenchmark for (2861ds/17627Mi)
% 150.96/21.53 % (3318738)Instruction limit reached!
% 150.96/21.53 % (3318738)------------------------------
% 150.96/21.53 % (3318738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.96/21.53 % (3318738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.96/21.53 % (3318738)CaDiCaL version: 2.1.3
% 150.96/21.53 % (3318738)Termination reason: Instruction limit
% 150.96/21.53 % (3318738)Termination phase: Saturation
% 150.96/21.53 % (3318738)Time elapsed: 11.790 s
% 150.96/21.53 % (3318738)Peak memory usage: 151 MB
% 150.96/21.53 % (3318738)Instructions burned: 29342 (million)
% 150.96/21.53 % (3318985)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1908798705:s2a=on:i=53295_2857 on theBenchmark for (2857ds/53295Mi)
% 150.96/21.53 % (3318748)Instruction limit reached!
% 150.96/21.53 % (3318748)------------------------------
% 150.96/21.53 % (3318748)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.96/21.53 % (3318748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.96/21.53 % (3318748)CaDiCaL version: 2.1.3
% 150.96/21.53 % (3318748)Termination reason: Instruction limit
% 150.96/21.53 % (3318748)Termination phase: Saturation
% 150.96/21.53 % (3318748)Time elapsed: 11.485 s
% 150.96/21.53 % (3318748)Peak memory usage: 264 MB
% 150.96/21.53 % (3318748)Instructions burned: 22566 (million)
% 150.96/21.53 % (3319036)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3052048479:i=26857:ins=20_2854 on theBenchmark for (2854ds/26857Mi)
% 150.96/21.53 % Exception at run slice level
% 150.96/21.53 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 150.96/21.53 % (3319056)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=1944179895:i=28120:bs=on:fsr=off_2853 on theBenchmark for (2853ds/28120Mi)
% 150.96/21.53 % (3318760)Instruction limit reached!
% 150.96/21.53 % (3318760)------------------------------
% 150.96/21.53 % (3318760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.15/24.30 % (3318760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.15/24.30 % (3318760)CaDiCaL version: 2.1.3
% 170.15/24.30 % (3318760)Termination reason: Instruction limit
% 170.15/24.30 % (3318760)Termination phase: Saturation
% 170.15/24.30 % (3318760)Time elapsed: 7.072 s
% 170.15/24.30 % (3318760)Peak memory usage: 80 MB
% 170.15/24.30 % (3318760)Instructions burned: 14136 (million)
% 170.15/24.30 % (3319241)fmb+10_1_sil=256000:fmbss=7:random_seed=2819386465:fmbsr=1.6:i=182295_2842 on theBenchmark for (2842ds/182295Mi)
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319270)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=3329567161:i=44625:gsp=on_2841 on theBenchmark for (2841ds/44625Mi)
% 170.15/24.30 % (3319270)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 170.15/24.30 % (3319270)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319278)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1824950589:i=160505_2841 on theBenchmark for (2841ds/160505Mi)
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319280)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=256085864:fmbsr=1.3:i=225729_2840 on theBenchmark for (2840ds/225729Mi)
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319282)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=3755615306:fmbsr=2:i=185024:ins=7_2840 on theBenchmark for (2840ds/185024Mi)
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319284)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=432108255:rtra=on_2839 on theBenchmark for (2839ds/0Mi)
% 170.15/24.30 % Exception at run slice level
% 170.15/24.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 170.15/24.30 % (3319286)% WARNING: option uhcvi not known.
% 170.15/24.30 % (3319286)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2978198677:i=271062:add=off:rtra=on:rawr=on_2839 on theBenchmark for (2839ds/271062Mi)
% 170.15/24.30 % (3319286)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 170.15/24.30 % (3319286)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 170.15/24.30 % (3318880)Instruction limit reached!
% 170.15/24.30 % (3318880)------------------------------
% 170.15/24.30 % (3318880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.15/24.30 % (3318880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.15/24.30 % (3318880)CaDiCaL version: 2.1.3
% 170.15/24.30 % (3318880)Termination reason: Instruction limit
% 170.15/24.30 % (3318880)Termination phase: Saturation
% 170.15/24.30 % (3318880)Time elapsed: 5.757 s
% 170.15/24.30 % (3318880)Peak memory usage: 18 MB
% 170.15/24.30 % (3318880)Instructions burned: 17631 (million)
% 170.15/24.30 % (3319289)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=730461564:i=176048:add=on:rtra=on:rawr=on_2803 on theBenchmark for (2803ds/176048Mi)
% 170.15/24.30 % (3318762)Instruction limit reached!
% 170.15/24.30 % (3318762)------------------------------
% 170.15/24.30 % (3318762)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 170.15/24.30 % (3318762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 170.15/24.30 % (3318762)CaDiCaL version: 2.1.3
% 170.15/24.30 % (3318762)Termination reason: Instruction limit
% 170.15/24.30 % (3318762)Termination phase: Saturation
% 170.15/24.30 % (3318762)Time elapsed: 7.107 s
% 170.15/24.30 % (3318762)Peak memory usage: 40 MB
% 170.15/24.30 % (3318762)Instructions burned: 15852 (million)
% 170.15/24.30 % (3319291)dis+10_1_sil=32000:si=on:sp=arity:random_seed=2021639378:i=206:fgj=on:rtra=on_2800 on theBenchmark for (2800ds/206Mi)
% 170.15/24.30 % (3319291)Instruction limit reached!
% 170.15/24.30 % (3319291)------------------------------
% 190.96/27.14 % (3319291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 190.96/27.14 % (3319291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.96/27.14 % (3319291)CaDiCaL version: 2.1.3
% 190.96/27.14 % (3319291)Termination reason: Instruction limit
% 190.96/27.14 % (3319291)Termination phase: Saturation
% 190.96/27.14 % (3319291)Time elapsed: 0.098 s
% 190.96/27.14 % (3319291)Peak memory usage: 13 MB
% 190.96/27.14 % (3319291)Instructions burned: 207 (million)
% 190.96/27.14 % (3319293)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=2559823176:i=232:rtra=on_2799 on theBenchmark for (2799ds/232Mi)
% 190.96/27.14 % (3319293)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 190.96/27.14 % (3319293)Instruction limit reached!
% 190.96/27.14 % (3319293)------------------------------
% 190.96/27.14 % (3319293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 190.96/27.14 % (3319293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.96/27.14 % (3319293)CaDiCaL version: 2.1.3
% 190.96/27.14 % (3319293)Termination reason: Instruction limit
% 190.96/27.14 % (3319293)Termination phase: Saturation
% 190.96/27.14 % (3319293)Time elapsed: 0.112 s
% 190.96/27.14 % (3319293)Peak memory usage: 14 MB
% 190.96/27.14 % (3319293)Instructions burned: 232 (million)
% 190.96/27.14 % (3319295)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3834026801:i=262:rtra=on_2798 on theBenchmark for (2798ds/262Mi)
% 190.96/27.14 % (3319295)Instruction limit reached!
% 190.96/27.14 % (3319295)------------------------------
% 190.96/27.14 % (3319295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 190.96/27.14 % (3319295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.96/27.14 % (3319295)CaDiCaL version: 2.1.3
% 190.96/27.14 % (3319295)Termination reason: Instruction limit
% 190.96/27.14 % (3319295)Termination phase: Saturation
% 190.96/27.14 % (3319295)Time elapsed: 0.128 s
% 190.96/27.14 % (3319295)Peak memory usage: 14 MB
% 190.96/27.14 % (3319295)Instructions burned: 263 (million)
% 190.96/27.14 % (3319297)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2629192630:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2797 on theBenchmark for (2797ds/318Mi)
% 190.96/27.14 % (3319297)Instruction limit reached!
% 190.96/27.14 % (3319297)------------------------------
% 190.96/27.14 % (3319297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 190.96/27.14 % (3319297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.96/27.14 % (3319297)CaDiCaL version: 2.1.3
% 190.96/27.14 % (3319297)Termination reason: Instruction limit
% 190.96/27.14 % (3319297)Termination phase: Saturation
% 190.96/27.14 % (3319297)Time elapsed: 0.134 s
% 190.96/27.14 % (3319297)Peak memory usage: 14 MB
% 190.96/27.14 % (3319297)Instructions burned: 319 (million)
% 190.96/27.14 % (3319299)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4161322166:i=1428:nm=2:rtra=on_2795 on theBenchmark for (2795ds/1428Mi)
% 190.96/27.14 % Exception at run slice level
% 190.96/27.14 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 190.96/27.14 % (3319301)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=3277869363:i=262:bd=preordered:rtra=on:fsd=on_2794 on theBenchmark for (2794ds/262Mi)
% 190.96/27.14 % (3319301)Instruction limit reached!
% 190.96/27.14 % (3319301)------------------------------
% 190.96/27.14 % (3319301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 190.96/27.14 % (3319301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 190.96/27.14 % (3319301)CaDiCaL version: 2.1.3
% 190.96/27.14 % (3319301)Termination reason: Instruction limit
% 190.96/27.14 % (3319301)Termination phase: Saturation
% 190.96/27.14 % (3319301)Time elapsed: 0.131 s
% 190.96/27.14 % (3319301)Peak memory usage: 13 MB
% 190.96/27.14 % (3319301)Instructions burned: 263 (million)
% 190.96/27.14 % (3319303)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=620836217:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2793 on theBenchmark for (2793ds/1368Mi)
% 190.96/27.14 % (3319303)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 190.96/27.14 % (3319303)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 190.96/27.14 % (3319303)Instruction limit reached!
% 190.96/27.14 % (3319303)------------------------------
% 190.96/27.14 % (3319303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319303)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319303)Termination reason: Instruction limit
% 205.63/29.24 % (3319303)Termination phase: Saturation
% 205.63/29.24 % (3319303)Time elapsed: 0.619 s
% 205.63/29.24 % (3319303)Peak memory usage: 16 MB
% 205.63/29.24 % (3319303)Instructions burned: 1370 (million)
% 205.63/29.24 % (3319305)ott-21_1_sil=16000:si=on:fs=off:random_seed=4051301013:i=360:av=off:fsr=off:rtra=on_2787 on theBenchmark for (2787ds/360Mi)
% 205.63/29.24 % (3319305)Instruction limit reached!
% 205.63/29.24 % (3319305)------------------------------
% 205.63/29.24 % (3319305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319305)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319305)Termination reason: Instruction limit
% 205.63/29.24 % (3319305)Termination phase: Saturation
% 205.63/29.24 % (3319305)Time elapsed: 0.159 s
% 205.63/29.24 % (3319305)Peak memory usage: 13 MB
% 205.63/29.24 % (3319305)Instructions burned: 360 (million)
% 205.63/29.24 % (3319307)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=985390947:i=954:bd=all:rtra=on_2785 on theBenchmark for (2785ds/954Mi)
% 205.63/29.24 % (3319307)Instruction limit reached!
% 205.63/29.24 % (3319307)------------------------------
% 205.63/29.24 % (3319307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319307)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319307)Termination reason: Instruction limit
% 205.63/29.24 % (3319307)Termination phase: Saturation
% 205.63/29.24 % (3319307)Time elapsed: 0.462 s
% 205.63/29.24 % (3319307)Peak memory usage: 15 MB
% 205.63/29.24 % (3319307)Instructions burned: 955 (million)
% 205.63/29.24 % (3319309)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=3567862353:fmbsr=1.3:i=1730:ins=25:rtra=on_2780 on theBenchmark for (2780ds/1730Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319311)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=422019580:i=2358:rtra=on_2779 on theBenchmark for (2779ds/2358Mi)
% 205.63/29.24 % (3319311)Instruction limit reached!
% 205.63/29.24 % (3319311)------------------------------
% 205.63/29.24 % (3319311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319311)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319311)Termination reason: Instruction limit
% 205.63/29.24 % (3319311)Termination phase: Saturation
% 205.63/29.24 % (3319311)Time elapsed: 1.197 s
% 205.63/29.24 % (3319311)Peak memory usage: 24 MB
% 205.63/29.24 % (3319311)Instructions burned: 2358 (million)
% 205.63/29.24 % (3319313)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=308323329:i=1778:ins=1:rtra=on_2767 on theBenchmark for (2767ds/1778Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319315)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=2394003229:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2767 on theBenchmark for (2767ds/1384Mi)
% 205.63/29.24 % (3319315)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 205.63/29.24 % (3319315)Instruction limit reached!
% 205.63/29.24 % (3319315)------------------------------
% 205.63/29.24 % (3319315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319315)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319315)Termination reason: Instruction limit
% 205.63/29.24 % (3319315)Termination phase: Saturation
% 205.63/29.24 % (3319315)Time elapsed: 0.726 s
% 205.63/29.24 % (3319315)Peak memory usage: 17 MB
% 205.63/29.24 % (3319315)Instructions burned: 1385 (million)
% 205.63/29.24 % (3319317)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=1385216848:i=1758:kws=inv_precedence:fsr=off:rtra=on_2759 on theBenchmark for (2759ds/1758Mi)
% 205.63/29.24 % (3319317)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 205.63/29.24 % (3318647)Instruction limit reached!
% 205.63/29.24 % (3318647)------------------------------
% 205.63/29.24 % (3318647)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3318647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3318647)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3318647)Termination reason: Instruction limit
% 205.63/29.24 % (3318647)Termination phase: Saturation
% 205.63/29.24 % (3318647)Time elapsed: 24.150 s
% 205.63/29.24 % (3318647)Peak memory usage: 672 MB
% 205.63/29.24 % (3318647)Instructions burned: 88027 (million)
% 205.63/29.24 % (3319319)fmb+10_1_sil=64000:si=on:random_seed=1001442764:i=44122:nm=2:rtra=on:gsp=on_2757 on theBenchmark for (2757ds/44122Mi)
% 205.63/29.24 % (3319319)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319321)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=3681758498:i=19030:nm=5:rtra=on_2757 on theBenchmark for (2757ds/19030Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319323)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=136425373:fmbsr=1.7:i=1840:rtra=on_2757 on theBenchmark for (2757ds/1840Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319325)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=2570404769:i=10262:rtra=on_2756 on theBenchmark for (2756ds/10262Mi)
% 205.63/29.24 % (3319325)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 205.63/29.24 % (3319317)Instruction limit reached!
% 205.63/29.24 % (3319317)------------------------------
% 205.63/29.24 % (3319317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319317)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319317)Termination reason: Instruction limit
% 205.63/29.24 % (3319317)Termination phase: Saturation
% 205.63/29.24 % (3319317)Time elapsed: 0.864 s
% 205.63/29.24 % (3319317)Peak memory usage: 24 MB
% 205.63/29.24 % (3319317)Instructions burned: 1758 (million)
% 205.63/29.24 % (3319327)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2625698441:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2750 on theBenchmark for (2750ds/2944Mi)
% 205.63/29.24 % (3319327)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 205.63/29.24 % (3319327)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 205.63/29.24 % (3319327)Instruction limit reached!
% 205.63/29.24 % (3319327)------------------------------
% 205.63/29.24 % (3319327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319327)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319327)Termination reason: Instruction limit
% 205.63/29.24 % (3319327)Termination phase: Saturation
% 205.63/29.24 % (3319327)Time elapsed: 1.412 s
% 205.63/29.24 % (3319327)Peak memory usage: 19 MB
% 205.63/29.24 % (3319327)Instructions burned: 2944 (million)
% 205.63/29.24 % (3319329)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=1401029980:i=12648:rtra=on_2736 on theBenchmark for (2736ds/12648Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319331)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=2269578899:fmbsr=2.30978:i=4348:rtra=on_2735 on theBenchmark for (2735ds/4348Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319333)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=1555309546:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2735 on theBenchmark for (2735ds/1738Mi)
% 205.63/29.24 % (3319333)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 205.63/29.24 % (3319325)Instruction limit reached!
% 205.63/29.24 % (3319325)------------------------------
% 205.63/29.24 % (3319325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319325)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319325)Termination reason: Instruction limit
% 205.63/29.24 % (3319325)Termination phase: Saturation
% 205.63/29.24 % (3319325)Time elapsed: 2.588 s
% 205.63/29.24 % (3319325)Peak memory usage: 37 MB
% 205.63/29.24 % (3319325)Instructions burned: 10262 (million)
% 205.63/29.24 % (3319335)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=4034137828:i=10228:av=off:rtra=on_2730 on theBenchmark for (2730ds/10228Mi)
% 205.63/29.24 % (3319333)Instruction limit reached!
% 205.63/29.24 % (3319333)------------------------------
% 205.63/29.24 % (3319333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319333)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319333)Termination reason: Instruction limit
% 205.63/29.24 % (3319333)Termination phase: Saturation
% 205.63/29.24 % (3319333)Time elapsed: 0.865 s
% 205.63/29.24 % (3319333)Peak memory usage: 23 MB
% 205.63/29.24 % (3319333)Instructions burned: 1739 (million)
% 205.63/29.24 % (3319337)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=1443938803:i=108564:rtra=on_2726 on theBenchmark for (2726ds/108564Mi)
% 205.63/29.24 % Exception at run slice level
% 205.63/29.24 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 205.63/29.24 % (3319339)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=2600571685:i=7024:aac=none:rtra=on_2726 on theBenchmark for (2726ds/7024Mi)
% 205.63/29.24 % (3319056)Instruction limit reached!
% 205.63/29.24 % (3319056)------------------------------
% 205.63/29.24 % (3319056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319056)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319056)Termination reason: Instruction limit
% 205.63/29.24 % (3319056)Termination phase: Saturation
% 205.63/29.24 % (3319056)Time elapsed: 12.764 s
% 205.63/29.24 % (3319056)Peak memory usage: 53 MB
% 205.63/29.24 % (3319056)Instructions burned: 28120 (million)
% 205.63/29.24 % (3319339)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 205.63/29.24 % (3319341)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3031886487:i=7546:rtra=on:amm=off_2725 on theBenchmark for (2725ds/7546Mi)
% 205.63/29.24 % (3319335) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3318630-3319335"...
% 205.63/29.24 % (3319335)...printing done.
% 205.63/29.24 % (3319335)Refutation found. Thanks to Tanya!
% 205.63/29.24 % SZS status Theorem for theBenchmark
% 205.63/29.24 % SZS output start Proof for theBenchmark
% 205.63/29.24 thf(type_def_5, type, list_c1059388851t_unit: $tType).
% 205.63/29.24 thf(type_def_6, type, config256849571t_unit: $tType).
% 205.63/29.24 thf(type_def_7, type, list_message_p_v: $tType).
% 205.63/29.24 thf(type_def_8, type, set_message_p_v: $tType).
% 205.63/29.24 thf(type_def_9, type, message_p_v: $tType).
% 205.63/29.24 thf(type_def_10, type, nat: $tType).
% 205.63/29.24 thf(type_def_11, type, p: $tType).
% 205.63/29.24 thf(type_def_12, type, sTfun: ($tType * $tType) > $tType).
% 205.63/29.24 thf(func_def_0, type, msgs_p1029620568t_unit: (config256849571t_unit > message_p_v > nat)).
% 205.63/29.24 thf(func_def_1, type, enabled_p_v_s: (config256849571t_unit > message_p_v > $o)).
% 205.63/29.24 thf(func_def_2, type, isReceiverOf_p_v: (p > message_p_v > $o)).
% 205.63/29.24 thf(func_def_3, type, firstO1414030372_p_v_s: (list_c1059388851t_unit > list_message_p_v > message_p_v > nat > $o)).
% 205.63/29.24 thf(func_def_4, type, minus_minus_nat: (nat > nat > nat)).
% 205.63/29.24 thf(func_def_5, type, one_one_nat: nat).
% 205.63/29.24 thf(func_def_6, type, zero_zero_nat: nat).
% 205.63/29.24 thf(func_def_7, type, prefix1615116500t_unit: (list_c1059388851t_unit > list_c1059388851t_unit > $o)).
% 205.63/29.24 thf(func_def_8, type, prefix47729710ge_p_v: (list_message_p_v > list_message_p_v > $o)).
% 205.63/29.24 thf(func_def_9, type, last_c571238084t_unit: (list_c1059388851t_unit > config256849571t_unit)).
% 205.63/29.24 thf(func_def_10, type, last_message_p_v: (list_message_p_v > message_p_v)).
% 205.63/29.24 thf(func_def_11, type, nil_co1338500125t_unit: list_c1059388851t_unit).
% 205.63/29.24 thf(func_def_12, type, nil_message_p_v: list_message_p_v).
% 205.63/29.24 thf(func_def_13, type, nth_co1649820636t_unit: (list_c1059388851t_unit > nat > config256849571t_unit)).
% 205.63/29.24 thf(func_def_14, type, nth_message_p_v: (list_message_p_v > nat > message_p_v)).
% 205.63/29.24 thf(func_def_15, type, suc: (nat > nat)).
% 205.63/29.24 thf(func_def_16, type, size_s1406904903t_unit: (list_c1059388851t_unit > nat)).
% 205.63/29.24 thf(func_def_17, type, size_s1168481041ge_p_v: (list_message_p_v > nat)).
% 205.63/29.24 thf(func_def_18, type, ord_less_nat: (nat > nat > $o)).
% 205.63/29.24 thf(func_def_19, type, ord_less_eq_nat: (nat > nat > $o)).
% 205.63/29.24 thf(func_def_20, type, member_message_p_v: (message_p_v > set_message_p_v > $o)).
% 205.63/29.24 thf(func_def_21, type, fe: (nat > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_22, type, firstOccSet: (nat > set_message_p_v)).
% 205.63/29.24 thf(func_def_23, type, ft: (nat > list_message_p_v)).
% 205.63/29.24 thf(func_def_24, type, index: nat).
% 205.63/29.24 thf(func_def_25, type, msgInSet: message_p_v).
% 205.63/29.24 thf(func_def_26, type, msg: message_p_v).
% 205.63/29.24 thf(func_def_27, type, n0: nat).
% 205.63/29.24 thf(func_def_28, type, n1: nat).
% 205.63/29.24 thf(func_def_29, type, nMsg: nat).
% 205.63/29.24 thf(func_def_30, type, n: nat).
% 205.63/29.24 thf(func_def_31, type, p2: p).
% 205.63/29.24 thf(func_def_35, type, vAND: ($o > $o > $o)).
% 205.63/29.24 thf(func_def_36, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 205.63/29.24 thf(func_def_37, type, vIMP: ($o > $o > $o)).
% 205.63/29.24 thf(func_def_38, type, db0: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_39, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 205.63/29.24 thf(func_def_40, type, db1: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_41, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 205.63/29.24 thf(func_def_42, type, db2: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_43, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 205.63/29.24 thf(func_def_44, type, vOR: ($o > $o > $o)).
% 205.63/29.24 thf(func_def_45, type, vNOT: ($o > $o)).
% 205.63/29.24 thf(func_def_46, type, sP0: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > $o)).
% 205.63/29.24 thf(func_def_47, type, sP1: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > $o)).
% 205.63/29.24 thf(func_def_48, type, sK2: (nat > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_49, type, sK3: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_50, type, sK4: ((nat > $o) > nat > nat > nat)).
% 205.63/29.24 thf(func_def_51, type, sK5: nat).
% 205.63/29.24 thf(func_def_52, type, sK6: p).
% 205.63/29.24 thf(func_def_53, type, sK7: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_54, type, sK8: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_55, type, sK9: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_56, type, sK10: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_57, type, sK11: (nat > nat)).
% 205.63/29.24 thf(func_def_58, type, sK12: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_59, type, sK13: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_60, type, sK14: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_61, type, sK15: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_62, type, sK16: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_63, type, sK17: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_64, type, sK18: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_65, type, sK19: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_66, type, sK20: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_67, type, sK21: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_68, type, sK22: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_69, type, sK23: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_70, type, sK24: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_71, type, sK25: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_72, type, sK26: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_73, type, sK27: (nat > nat)).
% 205.63/29.24 thf(func_def_74, type, sK28: ((nat > $o) > nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_75, type, sK29: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_76, type, sK30: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_77, type, sK31: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_78, type, sK32: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_79, type, sK33: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_80, type, sK34: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_81, type, sK35: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_82, type, sK36: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_83, type, sK37: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_84, type, sK38: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_85, type, sK39: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > (config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_86, type, sK40: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_87, type, sK41: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_88, type, sK42: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_89, type, sK43: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_message_p_v)).
% 205.63/29.24 thf(func_def_90, type, sK44: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > config256849571t_unit)).
% 205.63/29.24 thf(func_def_91, type, sK45: ((config256849571t_unit > (list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit) > (list_c1059388851t_unit > list_message_p_v > list_message_p_v) > nat > $o) > list_c1059388851t_unit > list_message_p_v > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_92, type, sK46: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_93, type, sK47: (list_message_p_v > list_message_p_v > nat)).
% 205.63/29.24 thf(func_def_94, type, sK48: ((list_c1059388851t_unit > $o) > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_95, type, sK49: (nat > nat > nat)).
% 205.63/29.24 thf(func_def_96, type, sK50: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_97, type, sK51: ((list_message_p_v > $o) > list_message_p_v)).
% 205.63/29.24 thf(func_def_98, type, sK52: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_99, type, sK53: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_100, type, sK54: (nat > nat > message_p_v > nat)).
% 205.63/29.24 thf(func_def_101, type, sK55: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_102, type, sK56: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_103, type, sK57: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_104, type, sK58: nat).
% 205.63/29.24 thf(func_def_105, type, sK59: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_106, type, sK60: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_107, type, sK61: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_108, type, sK62: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_109, type, sK63: (nat > nat)).
% 205.63/29.24 thf(func_def_110, type, sK64: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_111, type, sK65: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_112, type, sK66: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_113, type, sK67: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_114, type, sK68: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_115, type, sK69: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_116, type, sK70: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_117, type, sK71: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_118, type, sK72: ((nat > nat) > nat)).
% 205.63/29.24 thf(func_def_119, type, sK73: nat).
% 205.63/29.24 thf(func_def_120, type, sK74: nat).
% 205.63/29.24 thf(func_def_121, type, sK75: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_122, type, sK76: (nat > (nat > $o) > nat > nat)).
% 205.63/29.24 thf(func_def_123, type, sK77: (list_c1059388851t_unit > list_c1059388851t_unit > nat)).
% 205.63/29.24 thf(func_def_124, type, sK78: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_125, type, sK79: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_126, type, sK80: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_127, type, sK81: ((nat > nat > $o) > nat)).
% 205.63/29.24 thf(func_def_128, type, sK82: ((nat > $o) > nat > nat)).
% 205.63/29.24 thf(func_def_129, type, sK83: p).
% 205.63/29.24 thf(func_def_130, type, sK84: (nat > nat)).
% 205.63/29.24 thf(func_def_131, type, sK85: ((nat > $o) > nat > nat)).
% 205.63/29.24 thf(func_def_132, type, sK86: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_133, type, sK87: (nat > nat > nat)).
% 205.63/29.24 thf(func_def_134, type, sK88: (nat > list_message_p_v)).
% 205.63/29.24 thf(func_def_135, type, sK89: ((nat > $o) > nat)).
% 205.63/29.24 thf(func_def_136, type, sF90: nat).
% 205.63/29.24 thf(func_def_137, type, sF91: nat).
% 205.63/29.24 thf(func_def_138, type, sF92: list_c1059388851t_unit).
% 205.63/29.24 thf(func_def_139, type, sF93: nat).
% 205.63/29.24 thf(func_def_140, type, sF94: nat).
% 205.63/29.24 thf(func_def_141, type, sF95: $o).
% 205.63/29.24 thf(func_def_142, type, sK96: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_143, type, sK97: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_144, type, sK98: (nat > (nat > config256849571t_unit > $o) > list_c1059388851t_unit)).
% 205.63/29.24 thf(func_def_145, type, sK99: (nat > (nat > config256849571t_unit > $o) > nat)).
% 205.63/29.24 thf(func_def_146, type, sK100: (list_c1059388851t_unit > nat > (nat > config256849571t_unit > $o) > nat)).
% 205.63/29.24 thf(func_def_147, type, sK101: ((nat > config256849571t_unit > $o) > nat > config256849571t_unit)).
% 205.63/29.24 thf(func_def_148, type, sK102: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_149, type, sK103: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_150, type, sK104: (nat > nat)).
% 205.63/29.24 thf(func_def_151, type, sK105: (nat > nat > nat)).
% 205.63/29.24 thf(func_def_152, type, sK106: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_153, type, sK107: (nat > (nat > $o) > nat)).
% 205.63/29.24 thf(func_def_154, type, sK108: ((nat > $o) > nat > nat)).
% 205.63/29.24 thf(func_def_155, type, sK109: ((nat > $o) > nat > nat)).
% 205.63/29.24 thf(func_def_156, type, sK110: (list_message_p_v > nat > (nat > message_p_v > $o) > nat)).
% 205.63/29.24 thf(func_def_157, type, sK111: ((nat > message_p_v > $o) > nat > message_p_v)).
% 205.63/29.24 thf(func_def_158, type, sK112: (nat > (nat > message_p_v > $o) > list_message_p_v)).
% 205.63/29.24 thf(func_def_159, type, sK113: (nat > (nat > message_p_v > $o) > nat)).
% 205.63/29.24 thf(func_def_160, type, sK114: (nat > nat > nat)).
% 205.63/29.24 thf(func_def_161, type, db3: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_162, type, db6: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_163, type, db5: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(func_def_164, type, db4: !>[X0: $tType]:(X0)).
% 205.63/29.24 thf(f1,axiom,(
% 205.63/29.24 (ord_less_nat @ zero_zero_nat @ nMsg)),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_AssumpOcc6_I1_J)).
% 205.63/29.24 thf(f4,axiom,(
% 205.63/29.24 (firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_AssumptionSubset_I3_J)).
% 205.63/29.24 thf(f5,axiom,(
% 205.63/29.24 ! [X0 : nat] : ((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0) => (ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index))))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_SmallIndex)).
% 205.63/29.24 thf(f22,axiom,(
% 205.63/29.24 ! [X0 : nat] : (((minus_minus_nat @ X0 @ zero_zero_nat)) = X0)),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_diff__zero)).
% 205.63/29.24 thf(f34,axiom,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((X0 != X1) => (~(ord_less_nat @ X0 @ X1) => (ord_less_nat @ X1 @ X0)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_linorder__neqE__nat)).
% 205.63/29.24 thf(f38,axiom,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_nat @ X0 @ X1) => (X0 != X1))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_less__not__refl3)).
% 205.63/29.24 thf(f71,axiom,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_nat @ X0 @ X1) | (X0 = X1) = ((ord_less_nat @ X0 @ (suc @ X1))))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_less__Suc__eq)).
% 205.63/29.24 thf(f94,axiom,(
% 205.63/29.24 ! [X0 : nat] : ((ord_less_nat @ zero_zero_nat @ X0) => ? [X1 : nat] : (X0 = ((suc @ X1))))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_gr0__implies__Suc)).
% 205.63/29.24 thf(f119,axiom,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (((minus_minus_nat @ X1 @ (minus_minus_nat @ X1 @ X0))) = X0))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_diff__diff__cancel)).
% 205.63/29.24 thf(f126,axiom,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (((minus_minus_nat @ X0 @ X1)) = zero_zero_nat))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_diff__is__0__eq_H)).
% 205.63/29.24 thf(f128,axiom,(
% 205.63/29.24 ! [X0 : nat] : (((minus_minus_nat @ (suc @ X0) @ one_one_nat)) = X0)),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_diff__Suc__1)).
% 205.63/29.24 thf(f139,axiom,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) | (ord_less_eq_nat @ X0 @ X1))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_nat__le__linear)).
% 205.63/29.24 thf(f153,axiom,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (ord_less_eq_nat @ X0 @ (suc @ X1)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_le__SucI)).
% 205.63/29.24 thf(f188,axiom,(
% 205.63/29.24 ((^[X0 : nat] : ((ord_less_eq_nat @ (suc @ X0)))) = ord_less_nat)),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_less__eq__Suc__le)).
% 205.63/29.24 thf(f189,axiom,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (ord_less_nat @ X0 @ (suc @ X1)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_le__imp__less__Suc)).
% 205.63/29.24 thf(f194,axiom,(
% 205.63/29.24 (one_one_nat = ((suc @ zero_zero_nat)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_One__nat__def)).
% 205.63/29.24 thf(f195,axiom,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : (((minus_minus_nat @ X0 @ (suc @ X1))) = ((minus_minus_nat @ (minus_minus_nat @ X0 @ one_one_nat) @ X1)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_diff__Suc__eq__diff__pred)).
% 205.63/29.24 thf(f245,conjecture,(
% 205.63/29.24 (ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 205.63/29.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 205.63/29.24 thf(f246,negated_conjecture,(
% 205.63/29.24 ~(ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 205.63/29.24 inference(negated_conjecture,[status(cth)],[f245])).
% 205.63/29.24 thf(f265,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X0 @ X1) => (ord_less_eq_nat @ X0 @ (suc @ X1)))),
% 205.63/29.24 inference(rectify,[],[f153])).
% 205.63/29.24 thf(f266,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) = $true) => (((ord_less_eq_nat @ X0 @ (suc @ X1))) = $true))),
% 205.63/29.24 inference(fool_elimination,[],[f265])).
% 205.63/29.24 thf(f273,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_nat @ X0 @ X1) | (X0 = X1) = ((ord_less_nat @ X0 @ (suc @ X1))))),
% 205.63/29.24 inference(rectify,[],[f71])).
% 205.63/29.24 thf(f274,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : (((ord_less_nat @ X0 @ (suc @ X1))) = (((X0 = X1) | (ord_less_nat @ X0 @ X1))))),
% 205.63/29.24 inference(fool_elimination,[],[f273])).
% 205.63/29.24 thf(f303,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) => (zero_zero_nat = ((minus_minus_nat @ X1 @ X0))))),
% 205.63/29.24 inference(rectify,[],[f126])).
% 205.63/29.24 thf(f304,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) => (zero_zero_nat = ((minus_minus_nat @ X1 @ X0))))),
% 205.63/29.24 inference(fool_elimination,[],[f303])).
% 205.63/29.24 thf(f305,plain,(
% 205.63/29.24 (firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)),
% 205.63/29.24 inference(rectify,[],[f4])).
% 205.63/29.24 thf(f306,plain,(
% 205.63/29.24 (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true)),
% 205.63/29.24 inference(fool_elimination,[],[f305])).
% 205.63/29.24 thf(f344,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) => (ord_less_nat @ X1 @ (suc @ X0)))),
% 205.63/29.24 inference(rectify,[],[f189])).
% 205.63/29.24 thf(f345,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) => (((ord_less_nat @ X1 @ (suc @ X0))) = $true))),
% 205.63/29.24 inference(fool_elimination,[],[f344])).
% 205.63/29.24 thf(f368,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_nat @ X0 @ X1) => (X0 != X1))),
% 205.63/29.24 inference(rectify,[],[f38])).
% 205.63/29.24 thf(f369,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X0 @ X1)) = $true) => (X0 != X1))),
% 205.63/29.24 inference(fool_elimination,[],[f368])).
% 205.63/29.24 thf(f390,plain,(
% 205.63/29.24 ~(ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))),
% 205.63/29.24 inference(rectify,[],[f246])).
% 205.63/29.24 thf(f391,plain,(
% 205.63/29.24 ~ (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) = $true)),
% 205.63/29.24 inference(fool_elimination,[],[f390])).
% 205.63/29.24 thf(f446,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~(ord_less_nat @ X1 @ X0) => (ord_less_nat @ X0 @ X1)))),
% 205.63/29.24 inference(rectify,[],[f34])).
% 205.63/29.24 thf(f447,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~ (((ord_less_nat @ X1 @ X0)) = $true) => (((ord_less_nat @ X0 @ X1)) = $true)))),
% 205.63/29.24 inference(fool_elimination,[],[f446])).
% 205.63/29.24 thf(f462,plain,(
% 205.63/29.24 ! [X0 : nat] : ((ord_less_nat @ zero_zero_nat @ X0) => ? [X1 : nat] : (X0 = ((suc @ X1))))),
% 205.63/29.24 inference(rectify,[],[f94])).
% 205.63/29.24 thf(f463,plain,(
% 205.63/29.24 ! [X0 : nat] : ((((ord_less_nat @ zero_zero_nat @ X0)) = $true) => ? [X1 : nat] : (((suc @ X1)) = X0))),
% 205.63/29.24 inference(fool_elimination,[],[f462])).
% 205.63/29.24 thf(f480,plain,(
% 205.63/29.24 ! [X0 : nat] : ((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0) => (ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index))))),
% 205.63/29.24 inference(rectify,[],[f5])).
% 205.63/29.24 thf(f481,plain,(
% 205.63/29.24 ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) = $true) => (((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true))),
% 205.63/29.24 inference(fool_elimination,[],[f480])).
% 205.63/29.24 thf(f492,plain,(
% 205.63/29.24 (ord_less_nat @ zero_zero_nat @ nMsg)),
% 205.63/29.24 inference(rectify,[],[f1])).
% 205.63/29.24 thf(f493,plain,(
% 205.63/29.24 (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true)),
% 205.63/29.24 inference(fool_elimination,[],[f492])).
% 205.63/29.24 thf(f529,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) => (((minus_minus_nat @ X0 @ (minus_minus_nat @ X0 @ X1))) = X1))),
% 205.63/29.24 inference(rectify,[],[f119])).
% 205.63/29.24 thf(f530,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) => (((minus_minus_nat @ X0 @ (minus_minus_nat @ X0 @ X1))) = X1))),
% 205.63/29.24 inference(fool_elimination,[],[f529])).
% 205.63/29.24 thf(f546,plain,(
% 205.63/29.24 (ord_less_nat = (^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))))),
% 205.63/29.24 inference(fool_elimination,[],[f188])).
% 205.63/29.24 thf(f565,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((ord_less_eq_nat @ X1 @ X0) | (ord_less_eq_nat @ X0 @ X1))),
% 205.63/29.24 inference(rectify,[],[f139])).
% 205.63/29.24 thf(f566,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) | (((ord_less_eq_nat @ X0 @ X1)) = $true))),
% 205.63/29.24 inference(fool_elimination,[],[f565])).
% 205.63/29.24 thf(f640,plain,(
% 205.63/29.24 (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true)),
% 205.63/29.24 inference(flattening,[],[f391])).
% 205.63/29.24 thf(f647,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((X0 != X1) => ((((ord_less_nat @ X1 @ X0)) != $true) => (((ord_less_nat @ X0 @ X1)) = $true)))),
% 205.63/29.24 inference(flattening,[],[f447])).
% 205.63/29.24 thf(f651,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : (((minus_minus_nat @ X1 @ (suc @ X0))) = ((minus_minus_nat @ (minus_minus_nat @ X1 @ one_one_nat) @ X0)))),
% 205.63/29.24 inference(rectify,[],[f195])).
% 205.63/29.24 thf(f684,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) != $true) | (((ord_less_eq_nat @ X0 @ (suc @ X1))) = $true))),
% 205.63/29.24 inference(ennf_transformation,[],[f266])).
% 205.63/29.24 thf(f685,plain,(
% 205.63/29.24 ! [X0 : nat] : (? [X1 : nat] : (((suc @ X1)) = X0) | (((ord_less_nat @ zero_zero_nat @ X0)) != $true))),
% 205.63/29.24 inference(ennf_transformation,[],[f463])).
% 205.63/29.24 thf(f693,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : (((((ord_less_nat @ X0 @ X1)) = $true) | (((ord_less_nat @ X1 @ X0)) = $true)) | (X0 = X1))),
% 205.63/29.24 inference(ennf_transformation,[],[f647])).
% 205.63/29.24 thf(f694,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_nat @ X1 @ X0)) = $true) | (((ord_less_nat @ X0 @ X1)) = $true) | (X0 = X1))),
% 205.63/29.24 inference(flattening,[],[f693])).
% 205.63/29.24 thf(f710,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((minus_minus_nat @ X0 @ (minus_minus_nat @ X0 @ X1))) = X1))),
% 205.63/29.24 inference(ennf_transformation,[],[f530])).
% 205.63/29.24 thf(f729,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((((ord_less_nat @ X0 @ X1)) != $true) | (X0 != X1))),
% 205.63/29.24 inference(ennf_transformation,[],[f369])).
% 205.63/29.24 thf(f755,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_nat @ X1 @ (suc @ X0))) = $true))),
% 205.63/29.24 inference(ennf_transformation,[],[f345])).
% 205.63/29.24 thf(f807,plain,(
% 205.63/29.24 ! [X0 : nat] : ((((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true) | (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true))),
% 205.63/29.24 inference(ennf_transformation,[],[f481])).
% 205.63/29.24 thf(f810,plain,(
% 205.63/29.24 ! [X1 : nat,X0 : nat] : ((zero_zero_nat = ((minus_minus_nat @ X1 @ X0))) | (((ord_less_eq_nat @ X1 @ X0)) != $true))),
% 205.63/29.24 inference(ennf_transformation,[],[f304])).
% 205.63/29.24 thf(f898,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((zero_zero_nat = ((minus_minus_nat @ X0 @ X1))) | (((ord_less_eq_nat @ X0 @ X1)) != $true))),
% 205.63/29.24 inference(rectify,[],[f810])).
% 205.63/29.24 thf(f910,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X1 @ X0)) != $true) | (X0 != X1))),
% 205.63/29.24 inference(rectify,[],[f729])).
% 205.63/29.24 thf(f920,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) != $true) | (((minus_minus_nat @ X1 @ (minus_minus_nat @ X1 @ X0))) = X0))),
% 205.63/29.24 inference(rectify,[],[f710])).
% 205.63/29.24 thf(f922,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) = $true) | (((ord_less_eq_nat @ X1 @ X0)) = $true))),
% 205.63/29.24 inference(rectify,[],[f566])).
% 205.63/29.24 thf(f935,plain,(
% 205.63/29.24 ! [X0 : nat] : ((((suc @ (sK63 @ X0))) = X0) | (((ord_less_nat @ zero_zero_nat @ X0)) != $true))),
% 205.63/29.24 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK2 @ X0)],[f685])).
% 205.63/29.24 thf(f938,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_eq_nat @ X1 @ (suc @ X0))) = $true))),
% 205.63/29.24 inference(rectify,[],[f684])).
% 205.63/29.24 thf(f954,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X0 @ X1)) = $true) | (((ord_less_nat @ X1 @ X0)) = $true) | (X0 = X1))),
% 205.63/29.24 inference(rectify,[],[f694])).
% 205.63/29.24 thf(f964,plain,(
% 205.63/29.24 ! [X0 : nat,X1 : nat] : (((ord_less_nat @ X1 @ (suc @ X0))) = (((X1 = X0) | (ord_less_nat @ X1 @ X0))))),
% 205.63/29.24 inference(rectify,[],[f274])).
% 205.63/29.24 thf(f1001,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((ord_less_nat @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true) | (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f807])).
% 205.63/29.24 thf(f1059,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((minus_minus_nat @ (suc @ X0) @ one_one_nat)) = X0)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f128])).
% 205.63/29.24 thf(f1087,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_nat @ X1 @ (suc @ X0))) = $true)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f755])).
% 205.63/29.24 thf(f1099,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) != $true) | (zero_zero_nat = ((minus_minus_nat @ X0 @ X1)))) )),
% 205.63/29.24 inference(cnf_transformation,[],[f898])).
% 205.63/29.24 thf(f1114,plain,(
% 205.63/29.24 (((ord_less_nat @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true)),
% 205.63/29.24 inference(cnf_transformation,[],[f640])).
% 205.63/29.24 thf(f1127,plain,(
% 205.63/29.24 (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ nMsg)) = $true)),
% 205.63/29.24 inference(cnf_transformation,[],[f306])).
% 205.63/29.24 thf(f1134,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X1 @ X0)) != $true) | (X0 != X1)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f910])).
% 205.63/29.24 thf(f1141,plain,(
% 205.63/29.24 (((ord_less_nat @ zero_zero_nat @ nMsg)) = $true)),
% 205.63/29.24 inference(cnf_transformation,[],[f493])).
% 205.63/29.24 thf(f1162,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((minus_minus_nat @ X1 @ (suc @ X0))) = ((minus_minus_nat @ (minus_minus_nat @ X1 @ one_one_nat) @ X0)))) )),
% 205.63/29.24 inference(cnf_transformation,[],[f651])).
% 205.63/29.24 thf(f1170,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X0 @ X1)) != $true) | (((minus_minus_nat @ X1 @ (minus_minus_nat @ X1 @ X0))) = X0)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f920])).
% 205.63/29.24 thf(f1179,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) = $true) | (((ord_less_eq_nat @ X0 @ X1)) = $true)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f922])).
% 205.63/29.24 thf(f1187,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((minus_minus_nat @ X0 @ zero_zero_nat)) = X0)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f22])).
% 205.63/29.24 thf(f1212,plain,(
% 205.63/29.24 (ord_less_nat = (^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))))),
% 205.63/29.24 inference(cnf_transformation,[],[f546])).
% 205.63/29.24 thf(f1214,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((suc @ (sK63 @ X0))) = X0) | (((ord_less_nat @ zero_zero_nat @ X0)) != $true)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f935])).
% 205.63/29.24 thf(f1219,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_eq_nat @ X1 @ (suc @ X0))) = $true)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f938])).
% 205.63/29.24 thf(f1251,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X0 @ X1)) = $true) | (((ord_less_nat @ X1 @ X0)) = $true) | (X0 = X1)) )),
% 205.63/29.24 inference(cnf_transformation,[],[f954])).
% 205.63/29.24 thf(f1259,plain,(
% 205.63/29.24 (((suc @ zero_zero_nat)) = one_one_nat)),
% 205.63/29.24 inference(cnf_transformation,[],[f194])).
% 205.63/29.24 thf(f1270,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_nat @ X1 @ (suc @ X0))) = (((X1 = X0) | (ord_less_nat @ X1 @ X0))))) )),
% 205.63/29.24 inference(cnf_transformation,[],[f964])).
% 205.63/29.24 thf(f1305,plain,(
% 205.63/29.24 ( ! [X0 : nat] : (((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X0 @ (size_s1406904903t_unit @ (fe @ index)))) = $true) | (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true)) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1001,f1212])).
% 205.63/29.24 thf(f1350,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : (($true = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ (suc @ X0)))) | (((ord_less_eq_nat @ X1 @ X0)) != $true)) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1087,f1212])).
% 205.63/29.24 thf(f1359,plain,(
% 205.63/29.24 ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ (minus_minus_nat @ nMsg @ (suc @ zero_zero_nat)) @ (minus_minus_nat @ (size_s1406904903t_unit @ (fe @ index)) @ (suc @ zero_zero_nat)))) != $true)),
% 205.63/29.24 inference(definition_unfolding,[],[f1114,f1212])).
% 205.63/29.24 thf(f1369,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : (((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ X0)) != $true) | (X0 != X1)) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1134,f1212])).
% 205.63/29.24 thf(f1371,plain,(
% 205.63/29.24 ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ zero_zero_nat @ nMsg)) = $true)),
% 205.63/29.24 inference(definition_unfolding,[],[f1141,f1212])).
% 205.63/29.24 thf(f1407,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((suc @ (sK63 @ X0))) = X0) | ($true != (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ zero_zero_nat @ X0)))) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1214,f1212])).
% 205.63/29.24 thf(f1423,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((X0 = X1) | ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ X0)) = $true) | ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X0 @ X1)) = $true)) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1251,f1212,f1212])).
% 205.63/29.24 thf(f1429,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : (((((X1 = X0) | ((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ X0))) = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ (suc @ X0))))) )),
% 205.63/29.24 inference(definition_unfolding,[],[f1270,f1212,f1212])).
% 205.63/29.24 thf(f1447,plain,(
% 205.63/29.24 ( ! [X1 : nat] : (((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ X1)) != $true)) )),
% 205.63/29.24 inference(equality_resolution,[],[f1369])).
% 205.63/29.24 thf(f1452,definition,(
% 205.63/29.24 (sF90 = ((suc @ zero_zero_nat)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF90])],[function_definition])).
% 205.63/29.24 thf(f1453,plain,(
% 205.63/29.24 (((suc @ zero_zero_nat)) = sF90)),
% 205.63/29.24 inference(reorient_equations,[],[f1452])).
% 205.63/29.24 thf(f1454,definition,(
% 205.63/29.24 (sF91 = ((minus_minus_nat @ nMsg @ sF90)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF91])],[function_definition])).
% 205.63/29.24 thf(f1455,plain,(
% 205.63/29.24 (((minus_minus_nat @ nMsg @ sF90)) = sF91)),
% 205.63/29.24 inference(reorient_equations,[],[f1454])).
% 205.63/29.24 thf(f1456,definition,(
% 205.63/29.24 (sF92 = ((fe @ index)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF92])],[function_definition])).
% 205.63/29.24 thf(f1457,plain,(
% 205.63/29.24 (((fe @ index)) = sF92)),
% 205.63/29.24 inference(reorient_equations,[],[f1456])).
% 205.63/29.24 thf(f1458,definition,(
% 205.63/29.24 (sF93 = ((size_s1406904903t_unit @ sF92)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF93])],[function_definition])).
% 205.63/29.24 thf(f1459,plain,(
% 205.63/29.24 (((size_s1406904903t_unit @ sF92)) = sF93)),
% 205.63/29.24 inference(reorient_equations,[],[f1458])).
% 205.63/29.24 thf(f1460,definition,(
% 205.63/29.24 (sF94 = ((minus_minus_nat @ sF93 @ sF90)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF94])],[function_definition])).
% 205.63/29.24 thf(f1461,definition,(
% 205.63/29.24 (sF95 = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ sF91 @ sF94)))),
% 205.63/29.24 introduced(definition,[new_symbols(definition,[sF95])],[function_definition])).
% 205.63/29.24 thf(f1462,plain,(
% 205.63/29.24 ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ sF91 @ sF94)) = sF95)),
% 205.63/29.24 inference(reorient_equations,[],[f1461])).
% 205.63/29.24 thf(f1463,plain,(
% 205.63/29.24 ($true != sF95)),
% 205.63/29.24 inference(definition_folding,[],[f1359,f1462,f1460,f1453,f1459,f1457,f1455,f1453])).
% 205.63/29.24 thf(f1467,plain,(
% 205.63/29.24 ( ! [X1 : nat] : (($true != ((ord_less_eq_nat @ (suc @ X1) @ X1)))) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1447])).
% 205.63/29.24 thf(f1675,plain,(
% 205.63/29.24 ($true = sF95) | ((((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ sF91 @ sF94)) = $false)),
% 205.63/29.24 inference(iff_proxy_clausification,[],[f1462])).
% 205.63/29.24 thf(f1676,plain,(
% 205.63/29.24 ($true = sF95) | (((ord_less_eq_nat @ (suc @ sF91) @ sF94)) = $false)),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1675])).
% 205.63/29.24 thf(f1687,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : (((((X1 = X0) | ((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ X0))) = $false) | ($true = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ (suc @ X0))))) )),
% 205.63/29.24 inference(iff_proxy_clausification,[],[f1429])).
% 205.63/29.24 thf(f1689,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((X1 = X0)) = $false) | ($true = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ (suc @ X0))))) )),
% 205.63/29.24 inference(or_proxy_clausification,[],[f1687])).
% 205.63/29.24 thf(f1690,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : (($true = (((^[Y0 : nat]: (ord_less_eq_nat @ (suc @ Y0))) @ X1 @ (suc @ X0)))) | (X0 != X1)) )),
% 205.63/29.24 inference(equality_proxy_clausification,[],[f1689])).
% 205.63/29.24 thf(f1691,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((X0 != X1) | (((ord_less_eq_nat @ (suc @ X1) @ (suc @ X0))) = $true)) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1690])).
% 205.63/29.24 thf(f1852,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ X1 @ X0)) != $true) | (((ord_less_eq_nat @ (suc @ X1) @ (suc @ X0))) = $true)) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1350])).
% 205.63/29.24 thf(f1862,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((ord_less_eq_nat @ (suc @ zero_zero_nat) @ X0)) != $true) | (((suc @ (sK63 @ X0))) = X0)) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1407])).
% 205.63/29.24 thf(f1894,plain,(
% 205.63/29.24 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq_nat @ (suc @ X1) @ X0)) = $true) | (((ord_less_eq_nat @ (suc @ X0) @ X1)) = $true) | (X0 = X1)) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1423])).
% 205.63/29.24 thf(f1950,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((ord_less_eq_nat @ (suc @ X0) @ (size_s1406904903t_unit @ (fe @ index)))) = $true) | (((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true)) )),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1305])).
% 205.63/29.24 thf(f1955,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ zero_zero_nat) @ nMsg)) = $true)),
% 205.63/29.24 inference(beta-eta_normalization,[],[f1371])).
% 205.63/29.24 thf(f1981,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ sF91) @ sF94)) = $false)),
% 205.63/29.24 inference(forward_subsumption_resolution,[],[f1676,f1463])).
% 205.63/29.24 thf(f1992,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((ord_less_eq_nat @ sF90 @ X0)) != $true) | (((suc @ (sK63 @ X0))) = X0)) )),
% 205.63/29.24 inference(forward_demodulation,[],[f1862,f1453])).
% 205.63/29.24 thf(f1996,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true) | (((ord_less_eq_nat @ (suc @ X0) @ (size_s1406904903t_unit @ sF92))) = $true)) )),
% 205.63/29.24 inference(forward_demodulation,[],[f1950,f1457])).
% 205.63/29.24 thf(f1998,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ sF90 @ nMsg)) = $true)),
% 205.63/29.24 inference(forward_demodulation,[],[f1955,f1453])).
% 205.63/29.24 thf(f2003,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((firstO1414030372_p_v_s @ (fe @ (suc @ index)) @ (ft @ (suc @ index)) @ msg @ X0)) != $true) | (((ord_less_eq_nat @ (suc @ X0) @ sF93)) = $true)) )),
% 205.63/29.24 inference(forward_demodulation,[],[f1996,f1459])).
% 205.63/29.24 thf(f2026,plain,(
% 205.63/29.24 (one_one_nat = sF90)),
% 205.63/29.24 inference(constrained_superposition,[],[f1259,f1453])).
% 205.63/29.24 thf(f2039,plain,(
% 205.63/29.24 (((minus_minus_nat @ nMsg @ one_one_nat)) = sF91)),
% 205.63/29.24 inference(constrained_superposition,[],[f1455,f2026])).
% 205.63/29.24 thf(f2040,plain,(
% 205.63/29.24 (((minus_minus_nat @ sF93 @ one_one_nat)) = sF94)),
% 205.63/29.24 inference(constrained_superposition,[],[f1460,f2026])).
% 205.63/29.24 thf(f2750,plain,(
% 205.63/29.24 (nMsg = ((suc @ (sK63 @ nMsg)))) | ($true != $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1992,f1998])).
% 205.63/29.24 thf(f2754,plain,(
% 205.63/29.24 (nMsg = ((suc @ (sK63 @ nMsg))))),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f2750])).
% 205.63/29.24 thf(f2886,plain,(
% 205.63/29.24 (((minus_minus_nat @ nMsg @ one_one_nat)) = ((sK63 @ nMsg)))),
% 205.63/29.24 inference(constrained_superposition,[],[f1059,f2754])).
% 205.63/29.24 thf(f2897,plain,(
% 205.63/29.24 (((sK63 @ nMsg)) = sF91)),
% 205.63/29.24 inference(forward_demodulation,[],[f2886,f2039])).
% 205.63/29.24 thf(f2959,plain,(
% 205.63/29.24 (nMsg = ((suc @ sF91)))),
% 205.63/29.24 inference(constrained_superposition,[],[f2754,f2897])).
% 205.63/29.24 thf(f2970,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ sF94 @ (suc @ sF91))) = $true) | ($false = $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1981,f1179])).
% 205.63/29.24 thf(f3006,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ sF94 @ (suc @ sF91))) = $true)),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f2970])).
% 205.63/29.24 thf(f3046,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ sF94 @ nMsg)) = $true)),
% 205.63/29.24 inference(forward_demodulation,[],[f3006,f2959])).
% 205.63/29.24 thf(f3052,plain,(
% 205.63/29.24 (zero_zero_nat = ((minus_minus_nat @ sF94 @ nMsg))) | ($true != $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1099,f3046])).
% 205.63/29.24 thf(f3066,plain,(
% 205.63/29.24 (zero_zero_nat = ((minus_minus_nat @ sF94 @ nMsg)))),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f3052])).
% 205.63/29.24 thf(f5751,plain,(
% 205.63/29.24 ( ! [X0 : nat] : ((((minus_minus_nat @ sF93 @ (suc @ X0))) = ((minus_minus_nat @ sF94 @ X0)))) )),
% 205.63/29.24 inference(constrained_superposition,[],[f1162,f2040])).
% 205.63/29.24 thf(f6470,plain,(
% 205.63/29.24 (sF94 = sF91) | (((ord_less_eq_nat @ (suc @ sF94) @ sF91)) = $true) | ($false = $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1894,f1981])).
% 205.63/29.24 thf(f6621,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ sF94) @ sF91)) = $true) | (sF94 = sF91)),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f6470])).
% 205.63/29.24 thf(f6728,plain,(
% 205.63/29.24 ($true = ((ord_less_eq_nat @ (suc @ sF94) @ (suc @ sF91)))) | (sF94 = sF91) | ($true != $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1219,f6621])).
% 205.63/29.24 thf(f6789,plain,(
% 205.63/29.24 ($true = ((ord_less_eq_nat @ (suc @ sF94) @ (suc @ sF91)))) | (sF94 = sF91)),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f6728])).
% 205.63/29.24 thf(f6811,plain,(
% 205.63/29.24 ($true = ((ord_less_eq_nat @ (suc @ sF94) @ (suc @ sF91))))),
% 205.63/29.24 inference(forward_subsumption_resolution,[],[f6789,f1691])).
% 205.63/29.24 thf(f6813,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ sF94) @ nMsg)) = $true)),
% 205.63/29.24 inference(forward_demodulation,[],[f6811,f2959])).
% 205.63/29.24 thf(f8659,plain,(
% 205.63/29.24 ($true != $true) | (((ord_less_eq_nat @ (suc @ (suc @ sF94)) @ (suc @ nMsg))) = $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f1852,f6813])).
% 205.63/29.24 thf(f8758,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ (suc @ sF94)) @ (suc @ nMsg))) = $true)),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f8659])).
% 205.63/29.24 thf(f15641,plain,(
% 205.63/29.24 ($true != $true) | (((ord_less_eq_nat @ (suc @ nMsg) @ sF93)) = $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f2003,f1127])).
% 205.63/29.24 thf(f15642,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ nMsg) @ sF93)) = $true)),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f15641])).
% 205.63/29.24 thf(f31577,plain,(
% 205.63/29.24 ($true != $true) | (((minus_minus_nat @ sF93 @ (minus_minus_nat @ sF93 @ (suc @ nMsg)))) = ((suc @ nMsg)))),
% 205.63/29.24 inference(constrained_superposition,[],[f1170,f15642])).
% 205.63/29.24 thf(f31769,plain,(
% 205.63/29.24 (((minus_minus_nat @ sF93 @ (minus_minus_nat @ sF93 @ (suc @ nMsg)))) = ((suc @ nMsg)))),
% 205.63/29.24 inference(trivial_inequality_removal,[],[f31577])).
% 205.63/29.24 thf(f31835,plain,(
% 205.63/29.24 (((suc @ nMsg)) = ((minus_minus_nat @ sF93 @ (minus_minus_nat @ sF94 @ nMsg))))),
% 205.63/29.24 inference(forward_demodulation,[],[f31769,f5751])).
% 205.63/29.24 thf(f31841,plain,(
% 205.63/29.24 (((suc @ nMsg)) = ((minus_minus_nat @ sF93 @ zero_zero_nat)))),
% 205.63/29.24 inference(forward_demodulation,[],[f31835,f3066])).
% 205.63/29.24 thf(f31845,plain,(
% 205.63/29.24 (((suc @ nMsg)) = sF93)),
% 205.63/29.24 inference(forward_demodulation,[],[f31841,f1187])).
% 205.63/29.24 thf(f31874,plain,(
% 205.63/29.24 (nMsg = ((minus_minus_nat @ sF93 @ one_one_nat)))),
% 205.63/29.24 inference(constrained_superposition,[],[f1059,f31845])).
% 205.63/29.24 thf(f33963,plain,(
% 205.63/29.24 (nMsg = sF94)),
% 205.63/29.24 inference(constrained_superposition,[],[f2040,f31874])).
% 205.63/29.24 thf(f34384,plain,(
% 205.63/29.24 (((ord_less_eq_nat @ (suc @ (suc @ nMsg)) @ (suc @ nMsg))) = $true)),
% 205.63/29.24 inference(constrained_superposition,[],[f8758,f33963])).
% 205.63/29.24 thf(f34442,plain,(
% 205.63/29.24 $false),
% 205.63/29.24 inference(forward_subsumption_resolution,[],[f34384,f1467])).
% 205.63/29.24 % SZS output end Proof for theBenchmark
% 205.63/29.24 % (3319335)------------------------------
% 205.63/29.24 % (3319335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 205.63/29.24 % (3319335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 205.63/29.24 % (3319335)CaDiCaL version: 2.1.3
% 205.63/29.24 % (3319335)Termination reason: Refutation
% 205.63/29.24 % (3319335)Time elapsed: 2.053 s
% 205.63/29.24 % (3319335)Peak memory usage: 57 MB
% 205.63/29.24 % (3319335)Instructions burned: 7850 (million)
% 205.63/29.24 % (3318630)Success in time 29.005 s
% 205.63/29.24 % Vampire exiting
%------------------------------------------------------------------------------