%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW637_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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 : Tue Sep 29 01:40:34 PM UTC 2026
% Result : Theorem 117.35s 16.97s
% Output : Refutation 117.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW637_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.27 % Computer : n007.cluster.edu
% 0.11/0.27 % Model : x86_64 x86_64
% 0.11/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.27 % Memory : 8046.5625MB
% 0.11/0.27 % OS : Linux 6.8.0-71-generic
% 0.11/0.27 % CPULimit : 300
% 0.11/0.27 % WCLimit : 300
% 0.11/0.27 % DateTime : Mon Sep 28 14:21:10 UTC 2026
% 0.11/0.27 % CPUTime :
% 0.11/0.27 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.27/0.31 Running first-order model finding
% 0.27/0.31 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.87/1.16 % (2415628)Will run a generic schedule for satisfiability detection.
% 5.87/1.16 % (2415633)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2764495267_2999 on theBenchmark for (2999ds/0Mi)
% 5.87/1.16 % (2415633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.87/1.16 % (2415633)Terminated due to inappropriate strategy.
% 5.87/1.16 % (2415633)------------------------------
% 5.87/1.16 % (2415633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.16 % (2415633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.16 % (2415633)CaDiCaL version: 2.1.3
% 5.87/1.16 % (2415633)Termination reason: Inappropriate
% 5.87/1.16 % (2415633)Time elapsed: 0.004 s
% 5.87/1.16 % (2415633)Peak memory usage: 11 MB
% 5.87/1.16 % (2415633)Instructions burned: 6 (million)
% 5.87/1.16 % (2415633)------------------------------
% 5.87/1.16 % (2415633)------------------------------
% 5.87/1.16 % (2415634)% WARNING: option uhcvi not known.
% 5.87/1.16 % (2415636)dis+10_1_sil=32000:sp=arity:random_seed=79823184:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.87/1.16 % (2415637)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2905773410:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.87/1.16 % (2415635)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1138705843:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.87/1.16 % (2415634)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3465547609:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.87/1.16 % (2415639)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2625743931:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.87/1.16 % (2415638)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2413504558:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.87/1.16 % (2415641)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2849107988:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.87/1.16 % (2415641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.87/1.16 % (2415641)Terminated due to inappropriate strategy.
% 5.87/1.16 % (2415641)------------------------------
% 5.87/1.16 % (2415641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.16 % (2415641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.16 % (2415641)CaDiCaL version: 2.1.3
% 5.87/1.16 % (2415641)Termination reason: Inappropriate
% 5.87/1.16 % (2415641)Time elapsed: 0.003 s
% 5.87/1.16 % (2415641)Peak memory usage: 11 MB
% 5.87/1.16 % (2415641)Instructions burned: 5 (million)
% 5.87/1.16 % (2415641)------------------------------
% 5.87/1.16 % (2415641)------------------------------
% 5.87/1.16 % (2415649)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3095325623:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.87/1.16 % (2415636)Instruction limit reached!
% 5.87/1.16 % (2415636)------------------------------
% 5.87/1.16 % (2415636)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.16 % (2415636)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.16 % (2415636)CaDiCaL version: 2.1.3
% 5.87/1.16 % (2415636)Termination reason: Instruction limit
% 5.87/1.16 % (2415636)Termination phase: Saturation
% 5.87/1.16 % (2415636)Time elapsed: 0.106 s
% 5.87/1.16 % (2415636)Peak memory usage: 13 MB
% 5.87/1.16 % (2415636)Instructions burned: 103 (million)
% 5.87/1.16 % (2415649)Instruction limit reached!
% 5.87/1.16 % (2415649)------------------------------
% 5.87/1.16 % (2415649)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.16 % (2415649)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.16 % (2415649)CaDiCaL version: 2.1.3
% 5.87/1.16 % (2415649)Termination reason: Instruction limit
% 5.87/1.16 % (2415649)Termination phase: Saturation
% 5.87/1.16 % (2415649)Time elapsed: 0.074 s
% 5.87/1.16 % (2415649)Peak memory usage: 13 MB
% 5.87/1.16 % (2415649)Instructions burned: 131 (million)
% 5.87/1.16 % (2415637)Instruction limit reached!
% 5.87/1.16 % (2415637)------------------------------
% 5.87/1.16 % (2415637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.87/1.16 % (2415637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.87/1.16 % (2415637)CaDiCaL version: 2.1.3
% 5.87/1.16 % (2415637)Termination reason: Instruction limit
% 9.00/1.83 % (2415637)Termination phase: Saturation
% 9.00/1.83 % (2415637)Time elapsed: 0.116 s
% 9.00/1.83 % (2415637)Peak memory usage: 13 MB
% 9.00/1.83 % (2415637)Instructions burned: 116 (million)
% 9.00/1.83 % (2415652)ott-21_1_sil=16000:fs=off:random_seed=1161742732:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.00/1.83 % (2415638)Instruction limit reached!
% 9.00/1.83 % (2415638)------------------------------
% 9.00/1.83 % (2415638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.00/1.83 % (2415638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.00/1.83 % (2415638)CaDiCaL version: 2.1.3
% 9.00/1.83 % (2415638)Termination reason: Instruction limit
% 9.00/1.83 % (2415638)Termination phase: Saturation
% 9.00/1.83 % (2415638)Time elapsed: 0.140 s
% 9.00/1.83 % (2415638)Peak memory usage: 13 MB
% 9.00/1.83 % (2415638)Instructions burned: 131 (million)
% 9.00/1.83 % (2415651)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=3584228454:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.00/1.83 % (2415653)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2550443413:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 9.00/1.83 % (2415656)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3443005911:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 9.00/1.83 % (2415656)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.00/1.83 % (2415656)Terminated due to inappropriate strategy.
% 9.00/1.83 % (2415656)------------------------------
% 9.00/1.83 % (2415656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.00/1.83 % (2415656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.00/1.83 % (2415656)CaDiCaL version: 2.1.3
% 9.00/1.83 % (2415656)Termination reason: Inappropriate
% 9.00/1.83 % (2415656)Time elapsed: 0.003 s
% 9.00/1.83 % (2415656)Peak memory usage: 10 MB
% 9.00/1.83 % (2415656)Instructions burned: 4 (million)
% 9.00/1.83 % (2415656)------------------------------
% 9.00/1.83 % (2415656)------------------------------
% 9.00/1.83 % (2415639)Instruction limit reached!
% 9.00/1.83 % (2415639)------------------------------
% 9.00/1.83 % (2415639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.00/1.83 % (2415639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.00/1.83 % (2415639)CaDiCaL version: 2.1.3
% 9.00/1.83 % (2415639)Termination reason: Instruction limit
% 9.00/1.83 % (2415639)Termination phase: Saturation
% 9.00/1.83 % (2415639)Time elapsed: 0.179 s
% 9.00/1.83 % (2415639)Peak memory usage: 14 MB
% 9.00/1.83 % (2415639)Instructions burned: 159 (million)
% 9.00/1.83 % (2415659)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=889284781:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 9.00/1.83 % (2415660)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3915361702:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 9.00/1.83 % (2415652)Instruction limit reached!
% 9.00/1.83 % (2415652)------------------------------
% 9.00/1.83 % (2415652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.00/1.83 % (2415652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.00/1.83 % (2415652)CaDiCaL version: 2.1.3
% 9.00/1.83 % (2415652)Termination reason: Instruction limit
% 9.00/1.83 % (2415652)Termination phase: Saturation
% 9.00/1.83 % (2415652)Time elapsed: 0.087 s
% 9.00/1.83 % (2415652)Peak memory usage: 13 MB
% 9.00/1.83 % (2415652)Instructions burned: 182 (million)
% 9.00/1.83 % (2415660)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 9.00/1.83 % (2415660)Terminated due to inappropriate strategy.
% 9.00/1.83 % (2415660)------------------------------
% 9.00/1.83 % (2415660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.00/1.83 % (2415660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.00/1.83 % (2415660)CaDiCaL version: 2.1.3
% 9.00/1.83 % (2415660)Termination reason: Inappropriate
% 9.00/1.83 % (2415660)Time elapsed: 0.007 s
% 9.00/1.83 % (2415660)Peak memory usage: 10 MB
% 9.00/1.83 % (2415660)Instructions burned: 5 (million)
% 9.00/1.83 % (2415660)------------------------------
% 9.00/1.83 % (2415660)------------------------------
% 9.00/1.83 % (2415663)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=1183151322:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 35.54/5.36 % (2415664)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4139326498:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 35.54/5.36 % (2415653)Instruction limit reached!
% 35.54/5.36 % (2415653)------------------------------
% 35.54/5.36 % (2415653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.54/5.36 % (2415653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/5.36 % (2415653)CaDiCaL version: 2.1.3
% 35.54/5.36 % (2415653)Termination reason: Instruction limit
% 35.54/5.36 % (2415653)Termination phase: Saturation
% 35.54/5.36 % (2415653)Time elapsed: 0.438 s
% 35.54/5.36 % (2415653)Peak memory usage: 14 MB
% 35.54/5.36 % (2415653)Instructions burned: 478 (million)
% 35.54/5.36 % (2415663)Instruction limit reached!
% 35.54/5.36 % (2415663)------------------------------
% 35.54/5.36 % (2415663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.54/5.36 % (2415663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/5.36 % (2415663)CaDiCaL version: 2.1.3
% 35.54/5.36 % (2415663)Termination reason: Instruction limit
% 35.54/5.36 % (2415663)Termination phase: Saturation
% 35.54/5.36 % (2415663)Time elapsed: 0.353 s
% 35.54/5.36 % (2415663)Peak memory usage: 17 MB
% 35.54/5.36 % (2415663)Instructions burned: 692 (million)
% 35.54/5.36 % (2415667)fmb+10_1_sil=64000:random_seed=3582993908:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 35.54/5.36 % (2415667)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.54/5.36 % (2415667)Terminated due to inappropriate strategy.
% 35.54/5.36 % (2415667)------------------------------
% 35.54/5.36 % (2415667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.54/5.36 % (2415667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/5.36 % (2415667)CaDiCaL version: 2.1.3
% 35.54/5.36 % (2415667)Termination reason: Inappropriate
% 35.54/5.36 % (2415667)Time elapsed: 0.004 s
% 35.54/5.36 % (2415667)Peak memory usage: 10 MB
% 35.54/5.36 % (2415667)Instructions burned: 6 (million)
% 35.54/5.36 % (2415667)------------------------------
% 35.54/5.36 % (2415667)------------------------------
% 35.54/5.36 % (2415668)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3274546556:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 35.54/5.36 % (2415668)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.54/5.36 % (2415668)Terminated due to inappropriate strategy.
% 35.54/5.36 % (2415668)------------------------------
% 35.54/5.36 % (2415668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.54/5.36 % (2415668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/5.36 % (2415668)CaDiCaL version: 2.1.3
% 35.54/5.36 % (2415668)Termination reason: Inappropriate
% 35.54/5.36 % (2415668)Time elapsed: 0.006 s
% 35.54/5.36 % (2415668)Peak memory usage: 10 MB
% 35.54/5.36 % (2415668)Instructions burned: 5 (million)
% 35.54/5.36 % (2415668)------------------------------
% 35.54/5.36 % (2415668)------------------------------
% 35.54/5.36 % (2415670)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2793352068:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 35.54/5.36 % (2415670)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 35.54/5.36 % (2415670)Terminated due to inappropriate strategy.
% 35.54/5.36 % (2415670)------------------------------
% 35.54/5.36 % (2415670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.54/5.36 % (2415670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.54/5.36 % (2415670)CaDiCaL version: 2.1.3
% 35.54/5.36 % (2415670)Termination reason: Inappropriate
% 35.54/5.36 % (2415670)Time elapsed: 0.003 s
% 35.54/5.36 % (2415670)Peak memory usage: 10 MB
% 35.54/5.36 % (2415670)Instructions burned: 5 (million)
% 35.54/5.36 % (2415670)------------------------------
% 35.54/5.36 % (2415670)------------------------------
% 35.54/5.36 % (2415672)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2144174949:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 35.54/5.36 % (2415674)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=260212738:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 35.54/5.36 % (2415651)Instruction limit reached!
% 35.54/5.36 % (2415651)------------------------------
% 53.30/7.83 % (2415651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415651)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415651)Termination reason: Instruction limit
% 53.30/7.83 % (2415651)Termination phase: Saturation
% 53.30/7.83 % (2415651)Time elapsed: 0.661 s
% 53.30/7.83 % (2415651)Peak memory usage: 17 MB
% 53.30/7.83 % (2415651)Instructions burned: 684 (million)
% 53.30/7.83 % (2415677)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=946312665:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 53.30/7.83 % (2415677)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 53.30/7.83 % (2415677)Terminated due to inappropriate strategy.
% 53.30/7.83 % (2415677)------------------------------
% 53.30/7.83 % (2415677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415677)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415677)Termination reason: Inappropriate
% 53.30/7.83 % (2415677)Time elapsed: 0.007 s
% 53.30/7.83 % (2415677)Peak memory usage: 11 MB
% 53.30/7.83 % (2415677)Instructions burned: 6 (million)
% 53.30/7.83 % (2415677)------------------------------
% 53.30/7.83 % (2415677)------------------------------
% 53.30/7.83 % (2415679)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=115202580:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 53.30/7.83 % (2415679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 53.30/7.83 % (2415679)Terminated due to inappropriate strategy.
% 53.30/7.83 % (2415679)------------------------------
% 53.30/7.83 % (2415679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415679)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415679)Termination reason: Inappropriate
% 53.30/7.83 % (2415679)Time elapsed: 0.004 s
% 53.30/7.83 % (2415679)Peak memory usage: 10 MB
% 53.30/7.83 % (2415679)Instructions burned: 5 (million)
% 53.30/7.83 % (2415679)------------------------------
% 53.30/7.83 % (2415679)------------------------------
% 53.30/7.83 % (2415681)ott-2_1_sil=16000:newcnf=on:random_seed=3284431078:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 53.30/7.83 % (2415664)Instruction limit reached!
% 53.30/7.83 % (2415664)------------------------------
% 53.30/7.83 % (2415664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415664)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415664)Termination reason: Instruction limit
% 53.30/7.83 % (2415664)Termination phase: Saturation
% 53.30/7.83 % (2415664)Time elapsed: 0.852 s
% 53.30/7.83 % (2415664)Peak memory usage: 20 MB
% 53.30/7.83 % (2415664)Instructions burned: 879 (million)
% 53.30/7.83 % (2415683)ott+10_1_sil=32000:tgt=ground:random_seed=3860096231:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 53.30/7.83 % (2415659)Instruction limit reached!
% 53.30/7.83 % (2415659)------------------------------
% 53.30/7.83 % (2415659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415659)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415659)Termination reason: Instruction limit
% 53.30/7.83 % (2415659)Termination phase: Saturation
% 53.30/7.83 % (2415659)Time elapsed: 1.250 s
% 53.30/7.83 % (2415659)Peak memory usage: 22 MB
% 53.30/7.83 % (2415659)Instructions burned: 1180 (million)
% 53.30/7.83 % (2415685)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3596127608:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 53.30/7.83 % (2415685)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 53.30/7.83 % (2415685)Terminated due to inappropriate strategy.
% 53.30/7.83 % (2415685)------------------------------
% 53.30/7.83 % (2415685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.30/7.83 % (2415685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.30/7.83 % (2415685)CaDiCaL version: 2.1.3
% 53.30/7.83 % (2415685)Termination reason: Inappropriate
% 53.30/7.83 % (2415685)Time elapsed: 0.005 s
% 53.30/7.83 % (2415685)Peak memory usage: 11 MB
% 53.30/7.83 % (2415685)Instructions burned: 6 (million)
% 117.35/16.97 % (2415685)------------------------------
% 117.35/16.97 % (2415685)------------------------------
% 117.35/16.97 % (2415687)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2905916986:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi)
% 117.35/16.97 % (2415681)Instruction limit reached!
% 117.35/16.97 % (2415681)------------------------------
% 117.35/16.97 % (2415681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415681)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415681)Termination reason: Instruction limit
% 117.35/16.97 % (2415681)Termination phase: Saturation
% 117.35/16.97 % (2415681)Time elapsed: 0.766 s
% 117.35/16.97 % (2415681)Peak memory usage: 15 MB
% 117.35/16.97 % (2415681)Instructions burned: 869 (million)
% 117.35/16.97 % (2415689)dis+21_1_sil=32000:sas=cadical:random_seed=236148992:i=3773:amm=off_2982 on theBenchmark for (2982ds/3773Mi)
% 117.35/16.97 % (2415674)Instruction limit reached!
% 117.35/16.97 % (2415674)------------------------------
% 117.35/16.97 % (2415674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415674)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415674)Termination reason: Instruction limit
% 117.35/16.97 % (2415674)Termination phase: Saturation
% 117.35/16.97 % (2415674)Time elapsed: 1.355 s
% 117.35/16.97 % (2415674)Peak memory usage: 24 MB
% 117.35/16.97 % (2415674)Instructions burned: 1473 (million)
% 117.35/16.97 % (2415691)ott+11_1_sil=16000:gs=on:random_seed=3951207681:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2979 on theBenchmark for (2979ds/2251Mi)
% 117.35/16.97 % (2415672)Instruction limit reached!
% 117.35/16.97 % (2415672)------------------------------
% 117.35/16.97 % (2415672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415672)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415672)Termination reason: Instruction limit
% 117.35/16.97 % (2415672)Termination phase: Saturation
% 117.35/16.97 % (2415672)Time elapsed: 2.603 s
% 117.35/16.97 % (2415672)Peak memory usage: 40 MB
% 117.35/16.97 % (2415672)Instructions burned: 5132 (million)
% 117.35/16.97 % (2415695)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2978281167:fmbsr=1.6:i=67534_2966 on theBenchmark for (2966ds/67534Mi)
% 117.35/16.97 % (2415695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.35/16.97 % (2415695)Terminated due to inappropriate strategy.
% 117.35/16.97 % (2415695)------------------------------
% 117.35/16.97 % (2415695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415695)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415695)Termination reason: Inappropriate
% 117.35/16.97 % (2415695)Time elapsed: 0.005 s
% 117.35/16.97 % (2415695)Peak memory usage: 11 MB
% 117.35/16.97 % (2415695)Instructions burned: 5 (million)
% 117.35/16.97 % (2415695)------------------------------
% 117.35/16.97 % (2415695)------------------------------
% 117.35/16.97 % (2415697)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3055967611:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2966 on theBenchmark for (2966ds/4591Mi)
% 117.35/16.97 % (2415691)Instruction limit reached!
% 117.35/16.97 % (2415691)------------------------------
% 117.35/16.97 % (2415691)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415691)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415691)Termination reason: Instruction limit
% 117.35/16.97 % (2415691)Termination phase: Saturation
% 117.35/16.97 % (2415691)Time elapsed: 1.771 s
% 117.35/16.97 % (2415691)Peak memory usage: 22 MB
% 117.35/16.97 % (2415691)Instructions burned: 2252 (million)
% 117.35/16.97 % (2415699)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4180153346:i=29340_2961 on theBenchmark for (2961ds/29340Mi)
% 117.35/16.97 % (2415687)Instruction limit reached!
% 117.35/16.97 % (2415687)------------------------------
% 117.35/16.97 % (2415687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415687)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415687)Termination reason: Instruction limit
% 117.35/16.97 % (2415687)Termination phase: Saturation
% 117.35/16.97 % (2415687)Time elapsed: 3.487 s
% 117.35/16.97 % (2415687)Peak memory usage: 36 MB
% 117.35/16.97 % (2415687)Instructions burned: 3513 (million)
% 117.35/16.97 % (2415703)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1678733373:i=5211_2949 on theBenchmark for (2949ds/5211Mi)
% 117.35/16.97 % (2415689)Instruction limit reached!
% 117.35/16.97 % (2415689)------------------------------
% 117.35/16.97 % (2415689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415689)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415689)Termination reason: Instruction limit
% 117.35/16.97 % (2415689)Termination phase: Saturation
% 117.35/16.97 % (2415689)Time elapsed: 3.460 s
% 117.35/16.97 % (2415689)Peak memory usage: 34 MB
% 117.35/16.97 % (2415689)Instructions burned: 3773 (million)
% 117.35/16.97 % (2415705)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=310970545:i=5497:nm=2_2947 on theBenchmark for (2947ds/5497Mi)
% 117.35/16.97 % (2415705)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.35/16.97 % (2415705)Terminated due to inappropriate strategy.
% 117.35/16.97 % (2415705)------------------------------
% 117.35/16.97 % (2415705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415705)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415705)Termination reason: Inappropriate
% 117.35/16.97 % (2415705)Time elapsed: 0.007 s
% 117.35/16.97 % (2415705)Peak memory usage: 11 MB
% 117.35/16.97 % (2415705)Instructions burned: 7 (million)
% 117.35/16.97 % (2415705)------------------------------
% 117.35/16.97 % (2415705)------------------------------
% 117.35/16.97 % (2415707)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=848346700:fmbsr=2:i=46332_2947 on theBenchmark for (2947ds/46332Mi)
% 117.35/16.97 % (2415707)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.35/16.97 % (2415707)Terminated due to inappropriate strategy.
% 117.35/16.97 % (2415707)------------------------------
% 117.35/16.97 % (2415707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415707)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415707)Termination reason: Inappropriate
% 117.35/16.97 % (2415707)Time elapsed: 0.005 s
% 117.35/16.97 % (2415707)Peak memory usage: 11 MB
% 117.35/16.97 % (2415707)Instructions burned: 5 (million)
% 117.35/16.97 % (2415707)------------------------------
% 117.35/16.97 % (2415707)------------------------------
% 117.35/16.97 % (2415709)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1057774563:i=14071_2947 on theBenchmark for (2947ds/14071Mi)
% 117.35/16.97 % (2415709)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.35/16.97 % (2415709)Terminated due to inappropriate strategy.
% 117.35/16.97 % (2415709)------------------------------
% 117.35/16.97 % (2415709)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415709)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415709)Termination reason: Inappropriate
% 117.35/16.97 % (2415709)Time elapsed: 0.006 s
% 117.35/16.97 % (2415709)Peak memory usage: 11 MB
% 117.35/16.97 % (2415709)Instructions burned: 5 (million)
% 117.35/16.97 % (2415709)------------------------------
% 117.35/16.97 % (2415709)------------------------------
% 117.35/16.97 % (2415711)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4107335378:i=22565:add=on:rawr=on_2946 on theBenchmark for (2946ds/22565Mi)
% 117.35/16.97 % (2415683)Instruction limit reached!
% 117.35/16.97 % (2415683)------------------------------
% 117.35/16.97 % (2415683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415683)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415683)Termination reason: Instruction limit
% 117.35/16.97 % (2415683)Termination phase: Saturation
% 117.35/16.97 % (2415683)Time elapsed: 5.338 s
% 117.35/16.97 % (2415683)Peak memory usage: 34 MB
% 117.35/16.97 % (2415683)Instructions burned: 5114 (million)
% 117.35/16.97 % (2415715)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=636184659:i=8173:av=off_2934 on theBenchmark for (2934ds/8173Mi)
% 117.35/16.97 % (2415697)Instruction limit reached!
% 117.35/16.97 % (2415697)------------------------------
% 117.35/16.97 % (2415697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415697)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415697)Termination reason: Instruction limit
% 117.35/16.97 % (2415697)Termination phase: Saturation
% 117.35/16.97 % (2415697)Time elapsed: 4.151 s
% 117.35/16.97 % (2415697)Peak memory usage: 37 MB
% 117.35/16.97 % (2415697)Instructions burned: 4591 (million)
% 117.35/16.97 % (2415721)dis+10_16:1_sil=16000:random_seed=3201379226:i=9155:fsr=off_2924 on theBenchmark for (2924ds/9155Mi)
% 117.35/16.97 % (2415703)Instruction limit reached!
% 117.35/16.97 % (2415703)------------------------------
% 117.35/16.97 % (2415703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415703)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415703)Termination reason: Instruction limit
% 117.35/16.97 % (2415703)Termination phase: Saturation
% 117.35/16.97 % (2415703)Time elapsed: 4.570 s
% 117.35/16.97 % (2415703)Peak memory usage: 48 MB
% 117.35/16.97 % (2415703)Instructions burned: 5213 (million)
% 117.35/16.97 % (2415737)ott-3_8_sil=64000:random_seed=1970860667:i=20139:bs=on_2903 on theBenchmark for (2903ds/20139Mi)
% 117.35/16.97 % (2415715)Instruction limit reached!
% 117.35/16.97 % (2415715)------------------------------
% 117.35/16.97 % (2415715)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415715)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415715)Termination reason: Instruction limit
% 117.35/16.97 % (2415715)Termination phase: Saturation
% 117.35/16.97 % (2415715)Time elapsed: 8.661 s
% 117.35/16.97 % (2415715)Peak memory usage: 59 MB
% 117.35/16.97 % (2415715)Instructions burned: 8173 (million)
% 117.35/16.97 % (2415739)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=543467753:fmbsr=2:i=32576_2847 on theBenchmark for (2847ds/32576Mi)
% 117.35/16.97 % (2415739)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 117.35/16.97 % (2415739)Terminated due to inappropriate strategy.
% 117.35/16.97 % (2415739)------------------------------
% 117.35/16.97 % (2415739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415739)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415739)Termination reason: Inappropriate
% 117.35/16.97 % (2415739)Time elapsed: 0.004 s
% 117.35/16.97 % (2415739)Peak memory usage: 11 MB
% 117.35/16.97 % (2415739)Instructions burned: 6 (million)
% 117.35/16.97 % (2415739)------------------------------
% 117.35/16.97 % (2415739)------------------------------
% 117.35/16.97 % (2415741)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3732886649:i=11404_2847 on theBenchmark for (2847ds/11404Mi)
% 117.35/16.97 % (2415721)Instruction limit reached!
% 117.35/16.97 % (2415721)------------------------------
% 117.35/16.97 % (2415721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415721)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415721)Termination reason: Instruction limit
% 117.35/16.97 % (2415721)Termination phase: Saturation
% 117.35/16.97 % (2415721)Time elapsed: 8.278 s
% 117.35/16.97 % (2415721)Peak memory usage: 55 MB
% 117.35/16.97 % (2415721)Instructions burned: 9155 (million)
% 117.35/16.97 % (2415743)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3000816904:i=14134_2841 on theBenchmark for (2841ds/14134Mi)
% 117.35/16.97 % (2415743) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2415628-2415743"...
% 117.35/16.97 % (2415743)...printing done.
% 117.35/16.97 % (2415743)Refutation found. Thanks to Tanya!
% 117.35/16.97 % SZS status Theorem for theBenchmark
% 117.35/16.97 % SZS output start Proof for theBenchmark
% 117.35/16.97 tff(type_def_5, type, uni: $tType).
% 117.35/16.97 tff(type_def_6, type, ty: $tType).
% 117.35/16.97 tff(type_def_7, type, bool: $tType).
% 117.35/16.97 tff(type_def_8, type, tuple0: $tType).
% 117.35/16.97 tff(type_def_9, type, a: $tType).
% 117.35/16.97 tff(type_def_10, type, tree_int: $tType).
% 117.35/16.97 tff(type_def_11, type, list_int: $tType).
% 117.35/16.97 tff(type_def_12, type, tree_a1: $tType).
% 117.35/16.97 tff(func_def_0, type, witness: ty > uni).
% 117.35/16.97 tff(func_def_1, type, int: ty).
% 117.35/16.97 tff(func_def_2, type, real: ty).
% 117.35/16.97 tff(func_def_3, type, bool1: ty).
% 117.35/16.97 tff(func_def_4, type, true: bool).
% 117.35/16.97 tff(func_def_5, type, false: bool).
% 117.35/16.97 tff(func_def_6, type, match_bool: (ty * bool * uni * uni) > uni).
% 117.35/16.97 tff(func_def_7, type, tuple01: ty).
% 117.35/16.97 tff(func_def_8, type, tuple02: tuple0).
% 117.35/16.97 tff(func_def_9, type, qtmark: ty).
% 117.35/16.97 tff(func_def_10, type, list: ty > ty).
% 117.35/16.97 tff(func_def_11, type, nil: ty > uni).
% 117.35/16.97 tff(func_def_12, type, cons: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_13, type, match_list: (ty * ty * uni * uni * uni) > uni).
% 117.35/16.97 tff(func_def_14, type, cons_proj_1: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_15, type, cons_proj_2: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_16, type, infix_plpl: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_19, type, length: (ty * uni) > $int).
% 117.35/16.97 tff(func_def_22, type, tree: ty > ty).
% 117.35/16.97 tff(func_def_23, type, leaf: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_24, type, node: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_25, type, match_tree: (ty * ty * uni * uni * uni) > uni).
% 117.35/16.97 tff(func_def_26, type, leaf_proj_1: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_27, type, node_proj_1: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_28, type, node_proj_2: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_29, type, labels: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_30, type, ref: ty > ty).
% 117.35/16.97 tff(func_def_31, type, mk_ref: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_32, type, contents: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_33, type, a1: ty).
% 117.35/16.97 tff(func_def_34, type, t2tb: tree_int > uni).
% 117.35/16.97 tff(func_def_35, type, tb2t: uni > tree_int).
% 117.35/16.97 tff(func_def_36, type, t2tb1: list_int > uni).
% 117.35/16.97 tff(func_def_37, type, tb2t1: uni > list_int).
% 117.35/16.97 tff(func_def_38, type, t2tb2: tree_a1 > uni).
% 117.35/16.97 tff(func_def_39, type, tb2t2: uni > tree_a1).
% 117.35/16.97 tff(func_def_40, type, t2tb3: $int > uni).
% 117.35/16.97 tff(func_def_41, type, tb2t3: uni > $int).
% 117.35/16.97 tff(func_def_43, type, sK2: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_44, type, sK3: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_45, type, sK4: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_46, type, sK5: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_47, type, sK6: (ty * uni) > uni).
% 117.35/16.97 tff(func_def_48, type, sK7: (ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_49, type, sK8: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_50, type, sK9: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_51, type, sK10: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_52, type, sK11: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_53, type, sK12: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_54, type, sK13: (ty * ty * uni * uni) > uni).
% 117.35/16.97 tff(func_def_55, type, sK14: $int).
% 117.35/16.97 tff(func_def_56, type, sK15: tree_a1).
% 117.35/16.97 tff(func_def_57, type, sK16: tree_a1).
% 117.35/16.97 tff(func_def_58, type, sK17: $int).
% 117.35/16.97 tff(func_def_59, type, sK18: tree_int).
% 117.35/16.97 tff(func_def_60, type, sK19: $int).
% 117.35/16.97 tff(func_def_61, type, sK20: tree_int).
% 117.35/16.97 tff(func_def_62, type, sK21: $int).
% 117.35/16.97 tff(pred_def_1, type, sort: (ty * uni) > $o).
% 117.35/16.97 tff(pred_def_2, type, mem: (ty * uni * uni) > $o).
% 117.35/16.97 tff(pred_def_4, type, distinct: (ty * uni) > $o).
% 117.35/16.97 tff(pred_def_5, type, same_shape: (ty * ty * uni * uni) > $o).
% 117.35/16.97 tff(pred_def_7, type, sP0: (ty * uni) > $o).
% 117.35/16.97 tff(pred_def_8, type, sP1: (ty * ty * uni * uni) > $o).
% 117.35/16.97 tff(f35,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : (distinct(X0,X1) => (distinct(X0,X2) => (! [X3 : uni] : (sort(X0,X3) => (mem(X0,X3,X1) => ~mem(X0,X3,X2))) => distinct(X0,infix_plpl(X0,X1,X2)))))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',distinct_append)).
% 117.35/16.97 tff(f41,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni,X3 : uni] : leaf(X0,X1) != node(X0,X2,X3)),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',leaf_Node)).
% 117.35/16.97 tff(f45,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : node_proj_1(X0,node(X0,X1,X2)) = X1),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',node_proj_1_def)).
% 117.35/16.97 tff(f47,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : node_proj_2(X0,node(X0,X1,X2)) = X2),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',node_proj_2_def)).
% 117.35/16.97 tff(f48,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni] : (X1 = leaf(X0,leaf_proj_1(X0,X1)) | X1 = node(X0,node_proj_1(X0,X1),node_proj_2(X0,X1)))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tree_inversion)).
% 117.35/16.97 tff(f50,axiom,(
% 117.35/16.97 ! [X0 : ty] : (! [X1 : uni] : labels(X0,leaf(X0,X1)) = cons(X0,X1,nil(X0)) & ! [X1 : uni,X2 : uni] : labels(X0,node(X0,X1,X2)) = infix_plpl(X0,labels(X0,X1),labels(X0,X2)))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',labels_def)).
% 117.35/16.97 tff(f52,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni,X3 : uni] : (mem(X0,X1,labels(X0,node(X0,X2,X3))) <=> (mem(X0,X1,labels(X0,X2)) | mem(X0,X1,labels(X0,X3))))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',labels_Node)).
% 117.35/16.97 tff(f54,axiom,(
% 117.35/16.97 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : (same_shape(X1,X0,X2,X4) => (same_shape(X1,X0,X3,X5) => same_shape(X1,X0,node(X0,X2,X3),node(X1,X4,X5))))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_shape_Node)).
% 117.35/16.97 tff(f70,axiom,(
% 117.35/16.97 ! [X0 : $int] : tb2t3(t2tb3(X0)) = X0),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL3)).
% 117.35/16.97 tff(f71,axiom,(
% 117.35/16.97 ! [X0 : uni] : t2tb3(tb2t3(X0)) = X0),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR3)).
% 117.35/16.97 tff(f72,conjecture,(
% 117.35/16.97 ! [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : ((same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & $lesseq(X0,X3) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X4))) => ($less(X0,X5) & $lesseq(X5,X3)))) => ! [X6 : $int,X7 : tree_int] : ((same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & $lesseq(X3,X6) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X7))) => ($less(X3,X5) & $lesseq(X5,X6)))) => (same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) & distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) & $lesseq(X0,X6) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4)))) => ($less(X0,X5) & $lesseq(X5,X6))))))),
% 117.35/16.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_relabel)).
% 117.35/16.97 tff(f73,negated_conjecture,(
% 117.35/16.97 ~ ! [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : ((same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & $lesseq(X0,X3) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X4))) => ($less(X0,X5) & $lesseq(X5,X3)))) => ! [X6 : $int,X7 : tree_int] : ((same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & $lesseq(X3,X6) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X7))) => ($less(X3,X5) & $lesseq(X5,X6)))) => (same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) & distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) & $lesseq(X0,X6) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4)))) => ($less(X0,X5) & $lesseq(X5,X6))))))),
% 117.35/16.97 inference(negated_conjecture,[status(cth)],[f72])).
% 117.35/16.97 tff(f76,plain,(
% 117.35/16.97 ~ ! [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : ((same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & ~$less(X3,X0) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X4))) => ($less(X0,X5) & ~$less(X3,X5)))) => ! [X6 : $int,X7 : tree_int] : ((same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & ~$less(X6,X3) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X7))) => ($less(X3,X5) & ~$less(X6,X5)))) => (same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) & distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) & ~$less(X6,X0) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,node(int,t2tb(X7),t2tb(X4)))) => ($less(X0,X5) & ~$less(X6,X5))))))),
% 117.35/16.97 inference(theory_normalization,[],[f73])).
% 117.35/16.97 tff(f83,definition,(
% 117.35/16.97 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X0,X2) | ~$less(X1,X2) | ~$less(X0,X1)) )),
% 117.35/16.97 introduced(theory,[tha_transitivity])).
% 117.35/16.97 tff(f84,definition,(
% 117.35/16.97 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 117.35/16.97 introduced(theory,[tha_order_totality])).
% 117.35/16.97 tff(f96,plain,(
% 117.35/16.97 ! [X0 : ty] : (! [X1 : uni] : labels(X0,leaf(X0,X1)) = cons(X0,X1,nil(X0)) & ! [X2 : uni,X3 : uni] : labels(X0,node(X0,X2,X3)) = infix_plpl(X0,labels(X0,X2),labels(X0,X3)))),
% 117.35/16.97 inference(rectify,[],[f50])).
% 117.35/16.97 tff(f97,plain,(
% 117.35/16.97 ~ ! [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : ((same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & ~$less(X3,X0) & ! [X5 : $int] : (mem(int,t2tb3(X5),labels(int,t2tb(X4))) => ($less(X0,X5) & ~$less(X3,X5)))) => ! [X6 : $int,X7 : tree_int] : ((same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & ~$less(X6,X3) & ! [X8 : $int] : (mem(int,t2tb3(X8),labels(int,t2tb(X7))) => ($less(X3,X8) & ~$less(X6,X8)))) => (same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) & distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) & ~$less(X6,X0) & ! [X9 : $int] : (mem(int,t2tb3(X9),labels(int,node(int,t2tb(X7),t2tb(X4)))) => ($less(X0,X9) & ~$less(X6,X9))))))),
% 117.35/16.97 inference(rectify,[],[f76])).
% 117.35/16.97 tff(f111,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : (((distinct(X0,infix_plpl(X0,X1,X2)) | ? [X3 : uni] : ((mem(X0,X3,X2) & mem(X0,X3,X1)) & sort(X0,X3))) | ~distinct(X0,X2)) | ~distinct(X0,X1))),
% 117.35/16.97 inference(ennf_transformation,[],[f35])).
% 117.35/16.97 tff(f112,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : (distinct(X0,infix_plpl(X0,X1,X2)) | ? [X3 : uni] : (mem(X0,X3,X2) & mem(X0,X3,X1) & sort(X0,X3)) | ~distinct(X0,X2) | ~distinct(X0,X1))),
% 117.35/16.97 inference(flattening,[],[f111])).
% 117.35/16.97 tff(f118,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : ((same_shape(X1,X0,node(X0,X2,X3),node(X1,X4,X5)) | ~same_shape(X1,X0,X3,X5)) | ~same_shape(X1,X0,X2,X4))),
% 117.35/16.97 inference(ennf_transformation,[],[f54])).
% 117.35/16.97 tff(f119,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : ty,X2 : uni,X3 : uni,X4 : uni,X5 : uni] : (same_shape(X1,X0,node(X0,X2,X3),node(X1,X4,X5)) | ~same_shape(X1,X0,X3,X5) | ~same_shape(X1,X0,X2,X4))),
% 117.35/16.97 inference(flattening,[],[f118])).
% 117.35/16.97 tff(f124,plain,(
% 117.35/16.97 ? [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : (? [X6 : $int,X7 : tree_int] : ((~same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) | ~distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) | $less(X6,X0) | ? [X9 : $int] : ((~$less(X0,X9) | $less(X6,X9)) & mem(int,t2tb3(X9),labels(int,node(int,t2tb(X7),t2tb(X4)))))) & (same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & ~$less(X6,X3) & ! [X8 : $int] : (($less(X3,X8) & ~$less(X6,X8)) | ~mem(int,t2tb3(X8),labels(int,t2tb(X7)))))) & (same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & ~$less(X3,X0) & ! [X5 : $int] : (($less(X0,X5) & ~$less(X3,X5)) | ~mem(int,t2tb3(X5),labels(int,t2tb(X4))))))),
% 117.35/16.97 inference(ennf_transformation,[],[f97])).
% 117.35/16.97 tff(f125,plain,(
% 117.35/16.97 ? [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : (? [X6 : $int,X7 : tree_int] : ((~same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X7),t2tb(X4))) | ~distinct(int,labels(int,node(int,t2tb(X7),t2tb(X4)))) | $less(X6,X0) | ? [X9 : $int] : ((~$less(X0,X9) | $less(X6,X9)) & mem(int,t2tb3(X9),labels(int,node(int,t2tb(X7),t2tb(X4)))))) & same_shape(int,a1,t2tb2(X1),t2tb(X7)) & distinct(int,labels(int,t2tb(X7))) & ~$less(X6,X3) & ! [X8 : $int] : (($less(X3,X8) & ~$less(X6,X8)) | ~mem(int,t2tb3(X8),labels(int,t2tb(X7))))) & same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & ~$less(X3,X0) & ! [X5 : $int] : (($less(X0,X5) & ~$less(X3,X5)) | ~mem(int,t2tb3(X5),labels(int,t2tb(X4)))))),
% 117.35/16.97 inference(flattening,[],[f124])).
% 117.35/16.97 tff(f140,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni] : (distinct(X0,infix_plpl(X0,X1,X2)) | (mem(X0,sK7(X0,X1,X2),X2) & mem(X0,sK7(X0,X1,X2),X1) & sort(X0,sK7(X0,X1,X2))) | ~distinct(X0,X2) | ~distinct(X0,X1))),
% 117.35/16.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X3,sK7(X0,X1,X2))],[f112])).
% 117.35/16.97 tff(f142,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni,X3 : uni] : ((mem(X0,X1,labels(X0,node(X0,X2,X3))) | (~mem(X0,X1,labels(X0,X2)) & ~mem(X0,X1,labels(X0,X3)))) & ((mem(X0,X1,labels(X0,X2)) | mem(X0,X1,labels(X0,X3))) | ~mem(X0,X1,labels(X0,node(X0,X2,X3)))))),
% 117.35/16.97 inference(nnf_transformation,[],[f52])).
% 117.35/16.97 tff(f143,plain,(
% 117.35/16.97 ! [X0 : ty,X1 : uni,X2 : uni,X3 : uni] : ((mem(X0,X1,labels(X0,node(X0,X2,X3))) | (~mem(X0,X1,labels(X0,X2)) & ~mem(X0,X1,labels(X0,X3)))) & (mem(X0,X1,labels(X0,X2)) | mem(X0,X1,labels(X0,X3)) | ~mem(X0,X1,labels(X0,node(X0,X2,X3)))))),
% 117.35/16.97 inference(flattening,[],[f142])).
% 117.35/16.97 tff(f148,plain,(
% 117.35/16.97 ? [X0 : $int,X1 : tree_a1,X2 : tree_a1,X3 : $int,X4 : tree_int] : (? [X5 : $int,X6 : tree_int] : ((~same_shape(int,a1,node(a1,t2tb2(X1),t2tb2(X2)),node(int,t2tb(X6),t2tb(X4))) | ~distinct(int,labels(int,node(int,t2tb(X6),t2tb(X4)))) | $less(X5,X0) | ? [X7 : $int] : ((~$less(X0,X7) | $less(X5,X7)) & mem(int,t2tb3(X7),labels(int,node(int,t2tb(X6),t2tb(X4)))))) & same_shape(int,a1,t2tb2(X1),t2tb(X6)) & distinct(int,labels(int,t2tb(X6))) & ~$less(X5,X3) & ! [X8 : $int] : (($less(X3,X8) & ~$less(X5,X8)) | ~mem(int,t2tb3(X8),labels(int,t2tb(X6))))) & same_shape(int,a1,t2tb2(X2),t2tb(X4)) & distinct(int,labels(int,t2tb(X4))) & ~$less(X3,X0) & ! [X9 : $int] : (($less(X0,X9) & ~$less(X3,X9)) | ~mem(int,t2tb3(X9),labels(int,t2tb(X4)))))),
% 117.35/16.97 inference(rectify,[],[f125])).
% 117.35/16.97 tff(f149,plain,(
% 117.35/16.97 ((~same_shape(int,a1,node(a1,t2tb2(sK15),t2tb2(sK16)),node(int,t2tb(sK20),t2tb(sK18))) | ~distinct(int,labels(int,node(int,t2tb(sK20),t2tb(sK18)))) | $less(sK19,sK14) | ((~$less(sK14,sK21) | $less(sK19,sK21)) & mem(int,t2tb3(sK21),labels(int,node(int,t2tb(sK20),t2tb(sK18)))))) & same_shape(int,a1,t2tb2(sK15),t2tb(sK20)) & distinct(int,labels(int,t2tb(sK20))) & ~$less(sK19,sK17) & ! [X8 : $int] : (($less(sK17,X8) & ~$less(sK19,X8)) | ~mem(int,t2tb3(X8),labels(int,t2tb(sK20))))) & same_shape(int,a1,t2tb2(sK16),t2tb(sK18)) & distinct(int,labels(int,t2tb(sK18))) & ~$less(sK17,sK14) & ! [X9 : $int] : (($less(sK14,X9) & ~$less(sK17,X9)) | ~mem(int,t2tb3(X9),labels(int,t2tb(sK18))))),
% 117.35/16.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21]),skolemize(X0,sK14),skolemize(X1,sK15),skolemize(X2,sK16),skolemize(X3,sK17),skolemize(X4,sK18),skolemize(X5,sK19),skolemize(X6,sK20),skolemize(X7,sK21)],[f148])).
% 117.35/16.97 tff(f201,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (distinct(X0,infix_plpl(X0,X1,X2)) | mem(X0,sK7(X0,X1,X2),X1) | ~distinct(X0,X2) | ~distinct(X0,X1)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f140])).
% 117.35/16.97 tff(f202,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (distinct(X0,infix_plpl(X0,X1,X2)) | mem(X0,sK7(X0,X1,X2),X2) | ~distinct(X0,X2) | ~distinct(X0,X1)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f140])).
% 117.35/16.97 tff(f208,plain,(
% 117.35/16.97 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (leaf(X0,X1) != node(X0,X2,X3)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f41])).
% 117.35/16.97 tff(f212,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (node_proj_1(X0,node(X0,X1,X2)) = X1) )),
% 117.35/16.97 inference(cnf_transformation,[],[f45])).
% 117.35/16.97 tff(f214,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (node_proj_2(X0,node(X0,X1,X2)) = X2) )),
% 117.35/16.97 inference(cnf_transformation,[],[f47])).
% 117.35/16.97 tff(f215,plain,(
% 117.35/16.97 ( ! [X0 : ty,X1 : uni] : (node(X0,node_proj_1(X0,X1),node_proj_2(X0,X1)) = X1 | leaf(X0,leaf_proj_1(X0,X1)) = X1) )),
% 117.35/16.97 inference(cnf_transformation,[],[f48])).
% 117.35/16.97 tff(f217,plain,(
% 117.35/16.97 ( ! [X2 : uni,X3 : uni,X0 : ty] : (labels(X0,node(X0,X2,X3)) = infix_plpl(X0,labels(X0,X2),labels(X0,X3))) )),
% 117.35/16.97 inference(cnf_transformation,[],[f96])).
% 117.35/16.97 tff(f221,plain,(
% 117.35/16.97 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : uni] : (~mem(X0,X1,labels(X0,node(X0,X2,X3))) | mem(X0,X1,labels(X0,X3)) | mem(X0,X1,labels(X0,X2))) )),
% 117.35/16.97 inference(cnf_transformation,[],[f143])).
% 117.35/16.97 tff(f225,plain,(
% 117.35/16.97 ( ! [X2 : uni,X3 : uni,X0 : ty,X1 : ty,X4 : uni,X5 : uni] : (same_shape(X1,X0,node(X0,X2,X3),node(X1,X4,X5)) | ~same_shape(X1,X0,X3,X5) | ~same_shape(X1,X0,X2,X4)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f119])).
% 117.35/16.97 tff(f252,plain,(
% 117.35/16.97 ( ! [X0 : $int] : (tb2t3(t2tb3(X0)) = X0) )),
% 117.35/16.97 inference(cnf_transformation,[],[f70])).
% 117.35/16.97 tff(f253,plain,(
% 117.35/16.97 ( ! [X0 : uni] : (t2tb3(tb2t3(X0)) = X0) )),
% 117.35/16.97 inference(cnf_transformation,[],[f71])).
% 117.35/16.97 tff(f254,plain,(
% 117.35/16.97 ( ! [X9 : $int] : (~mem(int,t2tb3(X9),labels(int,t2tb(sK18))) | ~$less(sK17,X9)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f255,plain,(
% 117.35/16.97 ( ! [X9 : $int] : (~mem(int,t2tb3(X9),labels(int,t2tb(sK18))) | $less(sK14,X9)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f256,plain,(
% 117.35/16.97 ~$less(sK17,sK14)),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f257,plain,(
% 117.35/16.97 distinct(int,labels(int,t2tb(sK18)))),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f258,plain,(
% 117.35/16.97 same_shape(int,a1,t2tb2(sK16),t2tb(sK18))),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f259,plain,(
% 117.35/16.97 ( ! [X8 : $int] : (~mem(int,t2tb3(X8),labels(int,t2tb(sK20))) | ~$less(sK19,X8)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f260,plain,(
% 117.35/16.97 ( ! [X8 : $int] : (~mem(int,t2tb3(X8),labels(int,t2tb(sK20))) | $less(sK17,X8)) )),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f261,plain,(
% 117.35/16.97 ~$less(sK19,sK17)),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f262,plain,(
% 117.35/16.97 distinct(int,labels(int,t2tb(sK20)))),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f263,plain,(
% 117.35/16.97 same_shape(int,a1,t2tb2(sK15),t2tb(sK20))),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f264,plain,(
% 117.35/16.97 ~same_shape(int,a1,node(a1,t2tb2(sK15),t2tb2(sK16)),node(int,t2tb(sK20),t2tb(sK18))) | ~distinct(int,labels(int,node(int,t2tb(sK20),t2tb(sK18)))) | $less(sK19,sK14) | mem(int,t2tb3(sK21),labels(int,node(int,t2tb(sK20),t2tb(sK18))))),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f265,plain,(
% 117.35/16.97 ~same_shape(int,a1,node(a1,t2tb2(sK15),t2tb2(sK16)),node(int,t2tb(sK20),t2tb(sK18))) | ~distinct(int,labels(int,node(int,t2tb(sK20),t2tb(sK18)))) | $less(sK19,sK14) | ~$less(sK14,sK21) | $less(sK19,sK21)),
% 117.35/16.97 inference(cnf_transformation,[],[f149])).
% 117.35/16.97 tff(f276,definition,(
% 117.35/16.97 spl22_1 <=> $less(sK19,sK21)),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition])).
% 117.35/16.97 tff(f278,plain,(
% 117.35/16.97 $less(sK19,sK21) | ~spl22_1),
% 117.35/16.97 inference(avatar_component_clause,[],[f276])).
% 117.35/16.97 tff(f280,definition,(
% 117.35/16.97 spl22_2 <=> $less(sK14,sK21)),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_2])],[avatar_definition])).
% 117.35/16.97 tff(f282,plain,(
% 117.35/16.97 ~$less(sK14,sK21) | spl22_2),
% 117.35/16.97 inference(avatar_component_clause,[],[f280])).
% 117.35/16.97 tff(f284,definition,(
% 117.35/16.97 spl22_3 <=> $less(sK19,sK14)),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_3])],[avatar_definition])).
% 117.35/16.97 tff(f286,plain,(
% 117.35/16.97 $less(sK19,sK14) | ~spl22_3),
% 117.35/16.97 inference(avatar_component_clause,[],[f284])).
% 117.35/16.97 tff(f288,definition,(
% 117.35/16.97 spl22_4 <=> distinct(int,labels(int,node(int,t2tb(sK20),t2tb(sK18))))),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_4])],[avatar_definition])).
% 117.35/16.97 tff(f290,plain,(
% 117.35/16.97 ~distinct(int,labels(int,node(int,t2tb(sK20),t2tb(sK18)))) | spl22_4),
% 117.35/16.97 inference(avatar_component_clause,[],[f288])).
% 117.35/16.97 tff(f292,definition,(
% 117.35/16.97 spl22_5 <=> same_shape(int,a1,node(a1,t2tb2(sK15),t2tb2(sK16)),node(int,t2tb(sK20),t2tb(sK18)))),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition])).
% 117.35/16.97 tff(f294,plain,(
% 117.35/16.97 ~same_shape(int,a1,node(a1,t2tb2(sK15),t2tb2(sK16)),node(int,t2tb(sK20),t2tb(sK18))) | spl22_5),
% 117.35/16.97 inference(avatar_component_clause,[],[f292])).
% 117.35/16.97 tff(f295,plain,(
% 117.35/16.97 spl22_1 | ~spl22_2 | spl22_3 | ~spl22_4 | ~spl22_5),
% 117.35/16.97 inference(avatar_split_clause,[],[f265,f292,f288,f284,f280,f276])).
% 117.35/16.97 tff(f297,definition,(
% 117.35/16.97 spl22_6 <=> mem(int,t2tb3(sK21),labels(int,node(int,t2tb(sK20),t2tb(sK18))))),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_6])],[avatar_definition])).
% 117.35/16.97 tff(f299,plain,(
% 117.35/16.97 mem(int,t2tb3(sK21),labels(int,node(int,t2tb(sK20),t2tb(sK18)))) | ~spl22_6),
% 117.35/16.97 inference(avatar_component_clause,[],[f297])).
% 117.35/16.97 tff(f300,plain,(
% 117.35/16.97 spl22_6 | spl22_3 | ~spl22_4 | ~spl22_5),
% 117.35/16.97 inference(avatar_split_clause,[],[f264,f292,f288,f284,f297])).
% 117.35/16.97 tff(f307,plain,(
% 117.35/16.97 ( ! [X0 : uni] : (~mem(int,X0,labels(int,t2tb(sK20))) | $less(sK17,tb2t3(X0))) )),
% 117.35/16.97 inference(superposition,[],[f260,f253])).
% 117.35/16.97 tff(f308,plain,(
% 117.35/16.97 ( ! [X0 : uni] : (~mem(int,X0,labels(int,t2tb(sK20))) | ~$less(sK19,tb2t3(X0))) )),
% 117.35/16.97 inference(superposition,[],[f259,f253])).
% 117.35/16.97 tff(f309,plain,(
% 117.35/16.97 ( ! [X0 : uni] : (~mem(int,X0,labels(int,t2tb(sK18))) | $less(sK14,tb2t3(X0))) )),
% 117.35/16.97 inference(superposition,[],[f255,f253])).
% 117.35/16.97 tff(f310,plain,(
% 117.35/16.97 ( ! [X0 : uni] : (~mem(int,X0,labels(int,t2tb(sK18))) | ~$less(sK17,tb2t3(X0))) )),
% 117.35/16.97 inference(superposition,[],[f254,f253])).
% 117.35/16.97 tff(f352,plain,(
% 117.35/16.97 ( ! [X0 : $int] : (~$less(X0,sK14) | ~$less(sK17,X0)) )),
% 117.35/16.97 inference(resolution,[],[f83,f256])).
% 117.35/16.97 tff(f353,plain,(
% 117.35/16.97 ( ! [X0 : $int] : (~$less(X0,sK17) | ~$less(sK19,X0)) )),
% 117.35/16.97 inference(resolution,[],[f83,f261])).
% 117.35/16.97 tff(f360,plain,(
% 117.35/16.97 $less(sK21,sK14) | sK14 = sK21 | spl22_2),
% 117.35/16.97 inference(resolution,[],[f84,f282])).
% 117.35/16.97 tff(f370,plain,(
% 117.35/16.97 ~$less(sK14,sK17) | ~spl22_3),
% 117.35/16.97 inference(resolution,[],[f353,f286])).
% 117.35/16.97 tff(f373,plain,(
% 117.35/16.97 $less(sK17,sK14) | sK14 = sK17 | ~spl22_3),
% 117.35/16.97 inference(resolution,[],[f370,f84])).
% 117.35/16.97 tff(f375,plain,(
% 117.35/16.97 sK14 = sK17 | ~spl22_3),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f373,f256])).
% 117.35/16.97 tff(f379,plain,(
% 117.35/16.97 ~$less(sK19,sK14) | ~spl22_3),
% 117.35/16.97 inference(superposition,[],[f261,f375])).
% 117.35/16.97 tff(f381,plain,(
% 117.35/16.97 $false | ~spl22_3),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f379,f286])).
% 117.35/16.97 tff(f382,plain,(
% 117.35/16.97 ~spl22_3),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f381])).
% 117.35/16.97 tff(f386,definition,(
% 117.35/16.97 spl22_7 <=> sK14 = sK21),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition])).
% 117.35/16.97 tff(f388,plain,(
% 117.35/16.97 sK14 = sK21 | ~spl22_7),
% 117.35/16.97 inference(avatar_component_clause,[],[f386])).
% 117.35/16.97 tff(f390,definition,(
% 117.35/16.97 spl22_8 <=> $less(sK21,sK14)),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition])).
% 117.35/16.97 tff(f392,plain,(
% 117.35/16.97 $less(sK21,sK14) | ~spl22_8),
% 117.35/16.97 inference(avatar_component_clause,[],[f390])).
% 117.35/16.97 tff(f393,plain,(
% 117.35/16.97 spl22_7 | spl22_8 | spl22_2),
% 117.35/16.97 inference(avatar_split_clause,[],[f360,f280,f390,f386])).
% 117.35/16.97 tff(f691,plain,(
% 117.35/16.97 ~$less(sK17,sK21) | ~spl22_8),
% 117.35/16.97 inference(resolution,[],[f392,f352])).
% 117.35/16.97 tff(f1273,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (distinct(X0,labels(X0,node(X0,X1,X2))) | mem(X0,sK7(X0,labels(X0,X1),labels(X0,X2)),labels(X0,X1)) | ~distinct(X0,labels(X0,X2)) | ~distinct(X0,labels(X0,X1))) )),
% 117.35/16.97 inference(superposition,[],[f201,f217])).
% 117.35/16.97 tff(f1283,plain,(
% 117.35/16.97 ( ! [X2 : uni,X0 : ty,X1 : uni] : (distinct(X0,labels(X0,node(X0,X1,X2))) | mem(X0,sK7(X0,labels(X0,X1),labels(X0,X2)),labels(X0,X2)) | ~distinct(X0,labels(X0,X2)) | ~distinct(X0,labels(X0,X1))) )),
% 117.35/16.97 inference(superposition,[],[f202,f217])).
% 117.35/16.97 tff(f1340,plain,(
% 117.35/16.97 ( ! [X2 : ty,X3 : uni,X0 : uni,X1 : ty,X4 : uni] : (same_shape(X1,X2,node(X2,X3,X4),X0) | ~same_shape(X1,X2,X4,node_proj_2(X1,X0)) | ~same_shape(X1,X2,X3,node_proj_1(X1,X0)) | leaf(X1,leaf_proj_1(X1,X0)) = X0) )),
% 117.35/16.97 inference(superposition,[],[f225,f215])).
% 117.35/16.97 tff(f6842,definition,(
% 117.35/16.97 spl22_49 <=> sK17 = sK21),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_49])],[avatar_definition])).
% 117.35/16.97 tff(f6844,plain,(
% 117.35/16.97 sK17 = sK21 | ~spl22_49),
% 117.35/16.97 inference(avatar_component_clause,[],[f6842])).
% 117.35/16.97 tff(f6846,definition,(
% 117.35/16.97 spl22_50 <=> $less(sK21,sK17)),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_50])],[avatar_definition])).
% 117.35/16.97 tff(f6847,plain,(
% 117.35/16.97 ~$less(sK21,sK17) | spl22_50),
% 117.35/16.97 inference(avatar_component_clause,[],[f6846])).
% 117.35/16.97 tff(f6848,plain,(
% 117.35/16.97 $less(sK21,sK17) | ~spl22_50),
% 117.35/16.97 inference(avatar_component_clause,[],[f6846])).
% 117.35/16.97 tff(f6873,plain,(
% 117.35/16.97 ~$less(sK19,sK21) | ~spl22_50),
% 117.35/16.97 inference(resolution,[],[f6848,f353])).
% 117.35/16.97 tff(f12374,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK20))) | ~distinct(int,labels(int,t2tb(sK18))) | ~distinct(int,labels(int,t2tb(sK20))) | spl22_4),
% 117.35/16.97 inference(resolution,[],[f1273,f290])).
% 117.35/16.97 tff(f12377,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK20))) | ~distinct(int,labels(int,t2tb(sK20))) | spl22_4),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12374,f257])).
% 117.35/16.97 tff(f12378,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK20))) | spl22_4),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12377,f262])).
% 117.35/16.97 tff(f12387,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK18))) | ~distinct(int,labels(int,t2tb(sK18))) | ~distinct(int,labels(int,t2tb(sK20))) | spl22_4),
% 117.35/16.97 inference(resolution,[],[f1283,f290])).
% 117.35/16.97 tff(f12390,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK18))) | ~distinct(int,labels(int,t2tb(sK20))) | spl22_4),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12387,f257])).
% 117.35/16.97 tff(f12391,plain,(
% 117.35/16.97 mem(int,sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))),labels(int,t2tb(sK18))) | spl22_4),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12390,f262])).
% 117.35/16.97 tff(f12808,plain,(
% 117.35/16.97 $less(sK17,tb2t3(sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))))) | spl22_4),
% 117.35/16.97 inference(resolution,[],[f12378,f307])).
% 117.35/16.97 tff(f12842,plain,(
% 117.35/16.97 ~$less(sK17,tb2t3(sK7(int,labels(int,t2tb(sK20)),labels(int,t2tb(sK18))))) | spl22_4),
% 117.35/16.97 inference(resolution,[],[f12391,f310])).
% 117.35/16.97 tff(f12877,plain,(
% 117.35/16.97 $false | spl22_4),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12842,f12808])).
% 117.35/16.97 tff(f12878,plain,(
% 117.35/16.97 spl22_4),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f12877])).
% 117.35/16.97 tff(f12884,plain,(
% 117.35/16.97 mem(int,t2tb3(sK21),labels(int,t2tb(sK18))) | mem(int,t2tb3(sK21),labels(int,t2tb(sK20))) | ~spl22_6),
% 117.35/16.97 inference(resolution,[],[f299,f221])).
% 117.35/16.97 tff(f12903,definition,(
% 117.35/16.97 spl22_69 <=> mem(int,t2tb3(sK21),labels(int,t2tb(sK20)))),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_69])],[avatar_definition])).
% 117.35/16.97 tff(f12905,plain,(
% 117.35/16.97 mem(int,t2tb3(sK21),labels(int,t2tb(sK20))) | ~spl22_69),
% 117.35/16.97 inference(avatar_component_clause,[],[f12903])).
% 117.35/16.97 tff(f12907,definition,(
% 117.35/16.97 spl22_70 <=> mem(int,t2tb3(sK21),labels(int,t2tb(sK18)))),
% 117.35/16.97 introduced(definition,[new_symbols(definition,[spl22_70])],[avatar_definition])).
% 117.35/16.97 tff(f12909,plain,(
% 117.35/16.97 mem(int,t2tb3(sK21),labels(int,t2tb(sK18))) | ~spl22_70),
% 117.35/16.97 inference(avatar_component_clause,[],[f12907])).
% 117.35/16.97 tff(f12910,plain,(
% 117.35/16.97 spl22_69 | spl22_70 | ~spl22_6),
% 117.35/16.97 inference(avatar_split_clause,[],[f12884,f297,f12907,f12903])).
% 117.35/16.97 tff(f12912,plain,(
% 117.35/16.97 ~$less(sK17,sK21) | ~spl22_70),
% 117.35/16.97 inference(resolution,[],[f12909,f254])).
% 117.35/16.97 tff(f12914,plain,(
% 117.35/16.97 $less(sK14,tb2t3(t2tb3(sK21))) | ~spl22_70),
% 117.35/16.97 inference(resolution,[],[f12909,f309])).
% 117.35/16.97 tff(f12930,plain,(
% 117.35/16.97 $less(sK14,sK21) | ~spl22_70),
% 117.35/16.97 inference(forward_demodulation,[],[f12914,f252])).
% 117.35/16.97 tff(f12935,plain,(
% 117.35/16.97 $false | (spl22_2 | ~spl22_70)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12930,f282])).
% 117.35/16.97 tff(f12936,plain,(
% 117.35/16.97 spl22_2 | ~spl22_70),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f12935])).
% 117.35/16.97 tff(f12939,plain,(
% 117.35/16.97 ~$less(sK19,tb2t3(t2tb3(sK21))) | ~spl22_69),
% 117.35/16.97 inference(resolution,[],[f12905,f308])).
% 117.35/16.97 tff(f12940,plain,(
% 117.35/16.97 $less(sK17,tb2t3(t2tb3(sK21))) | ~spl22_69),
% 117.35/16.97 inference(resolution,[],[f12905,f307])).
% 117.35/16.97 tff(f12956,plain,(
% 117.35/16.97 $less(sK17,sK21) | ~spl22_69),
% 117.35/16.97 inference(forward_demodulation,[],[f12940,f252])).
% 117.35/16.97 tff(f12957,plain,(
% 117.35/16.97 ~$less(sK19,sK21) | ~spl22_69),
% 117.35/16.97 inference(forward_demodulation,[],[f12939,f252])).
% 117.35/16.97 tff(f12961,plain,(
% 117.35/16.97 $false | (~spl22_8 | ~spl22_69)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12956,f691])).
% 117.35/16.97 tff(f12962,plain,(
% 117.35/16.97 ~spl22_8 | ~spl22_69),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f12961])).
% 117.35/16.97 tff(f12969,plain,(
% 117.35/16.97 ~same_shape(int,a1,t2tb2(sK16),node_proj_2(int,node(int,t2tb(sK20),t2tb(sK18)))) | ~same_shape(int,a1,t2tb2(sK15),node_proj_1(int,node(int,t2tb(sK20),t2tb(sK18)))) | node(int,t2tb(sK20),t2tb(sK18)) = leaf(int,leaf_proj_1(int,node(int,t2tb(sK20),t2tb(sK18)))) | spl22_5),
% 117.35/16.97 inference(resolution,[],[f294,f1340])).
% 117.35/16.97 tff(f12972,plain,(
% 117.35/16.97 ~same_shape(int,a1,t2tb2(sK16),node_proj_2(int,node(int,t2tb(sK20),t2tb(sK18)))) | ~same_shape(int,a1,t2tb2(sK15),node_proj_1(int,node(int,t2tb(sK20),t2tb(sK18)))) | spl22_5),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12969,f208])).
% 117.35/16.97 tff(f12975,plain,(
% 117.35/16.97 ~same_shape(int,a1,t2tb2(sK16),t2tb(sK18)) | ~same_shape(int,a1,t2tb2(sK15),node_proj_1(int,node(int,t2tb(sK20),t2tb(sK18)))) | spl22_5),
% 117.35/16.97 inference(forward_demodulation,[],[f12972,f214])).
% 117.35/16.97 tff(f12979,plain,(
% 117.35/16.97 ~same_shape(int,a1,t2tb2(sK15),node_proj_1(int,node(int,t2tb(sK20),t2tb(sK18)))) | spl22_5),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12975,f258])).
% 117.35/16.97 tff(f12981,plain,(
% 117.35/16.97 ~same_shape(int,a1,t2tb2(sK15),t2tb(sK20)) | spl22_5),
% 117.35/16.97 inference(forward_demodulation,[],[f12979,f212])).
% 117.35/16.97 tff(f12984,plain,(
% 117.35/16.97 $false | spl22_5),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12981,f263])).
% 117.35/16.97 tff(f12985,plain,(
% 117.35/16.97 spl22_5),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f12984])).
% 117.35/16.97 tff(f12991,plain,(
% 117.35/16.97 $less(sK17,sK14) | (~spl22_7 | ~spl22_69)),
% 117.35/16.97 inference(forward_demodulation,[],[f12956,f388])).
% 117.35/16.97 tff(f13036,plain,(
% 117.35/16.97 $false | (~spl22_7 | ~spl22_69)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12991,f256])).
% 117.35/16.97 tff(f13037,plain,(
% 117.35/16.97 ~spl22_7 | ~spl22_69),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f13036])).
% 117.35/16.97 tff(f13085,plain,(
% 117.35/16.97 $false | (~spl22_1 | ~spl22_50)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f6873,f278])).
% 117.35/16.97 tff(f13086,plain,(
% 117.35/16.97 ~spl22_1 | ~spl22_50),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f13085])).
% 117.35/16.97 tff(f13141,plain,(
% 117.35/16.97 $less(sK21,sK17) | sK17 = sK21 | ~spl22_70),
% 117.35/16.97 inference(resolution,[],[f12912,f84])).
% 117.35/16.97 tff(f13143,plain,(
% 117.35/16.97 sK17 = sK21 | (spl22_50 | ~spl22_70)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f13141,f6847])).
% 117.35/16.97 tff(f13242,plain,(
% 117.35/16.97 spl22_49 | spl22_50 | ~spl22_70),
% 117.35/16.97 inference(avatar_split_clause,[],[f13143,f12907,f6846,f6842])).
% 117.35/16.97 tff(f13266,plain,(
% 117.35/16.97 $less(sK19,sK17) | (~spl22_1 | ~spl22_49)),
% 117.35/16.97 inference(superposition,[],[f278,f6844])).
% 117.35/16.97 tff(f13294,plain,(
% 117.35/16.97 $false | (~spl22_1 | ~spl22_49)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f13266,f261])).
% 117.35/16.97 tff(f13295,plain,(
% 117.35/16.97 ~spl22_1 | ~spl22_49),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f13294])).
% 117.35/16.97 tff(f13298,plain,(
% 117.35/16.97 $false | (~spl22_1 | ~spl22_69)),
% 117.35/16.97 inference(forward_subsumption_resolution,[],[f12957,f278])).
% 117.35/16.97 tff(f13299,plain,(
% 117.35/16.97 ~spl22_1 | ~spl22_69),
% 117.35/16.97 inference(avatar_contradiction_clause,[],[f13298])).
% 117.35/16.97 cnf(s1, plain, spl22_1 | ~spl22_2 | spl22_3 | ~spl22_4 | ~spl22_5, inference(sat_conversion,[],[f295])).
% 117.35/16.97 cnf(s2, plain, spl22_3 | ~spl22_4 | ~spl22_5 | spl22_6, inference(sat_conversion,[],[f300])).
% 117.35/16.97 cnf(s3, plain, ~spl22_3, inference(sat_conversion,[],[f382])).
% 117.35/16.97 cnf(s4, plain, spl22_2 | spl22_7 | spl22_8, inference(sat_conversion,[],[f393])).
% 117.35/16.97 cnf(s113, plain, spl22_4, inference(sat_conversion,[],[f12878])).
% 117.35/16.97 cnf(s114, plain, ~spl22_6 | spl22_69 | spl22_70, inference(sat_conversion,[],[f12910])).
% 117.35/16.97 cnf(s116, plain, spl22_2 | ~spl22_70, inference(sat_conversion,[],[f12936])).
% 117.35/16.97 cnf(s118, plain, ~spl22_8 | ~spl22_69, inference(sat_conversion,[],[f12962])).
% 117.35/16.97 cnf(s121, plain, spl22_5, inference(sat_conversion,[],[f12985])).
% 117.35/16.97 cnf(s123, plain, ~spl22_7 | ~spl22_69, inference(sat_conversion,[],[f13037])).
% 117.35/16.97 cnf(s131, plain, ~spl22_1 | ~spl22_50, inference(sat_conversion,[],[f13086])).
% 117.35/16.97 cnf(s132, plain, spl22_49 | spl22_50 | ~spl22_70, inference(sat_conversion,[],[f13242])).
% 117.35/16.97 cnf(s134, plain, ~spl22_1 | ~spl22_49, inference(sat_conversion,[],[f13295])).
% 117.35/16.97 cnf(s136, plain, ~spl22_1 | ~spl22_69, inference(sat_conversion,[],[f13299])).
% 117.35/16.97 cnf(s139, plain, spl22_6, inference(rat,[],[s2,s121,s113,s3])).
% 117.35/16.97 cnf(s140, plain, spl22_1 | ~spl22_2, inference(rat,[],[s1,s121,s113,s3])).
% 117.35/16.97 cnf(s141, plain, spl22_2, inference(rat,[],[s4,s118,s123,s114,s116,s139])).
% 117.35/16.97 cnf(s144, plain, spl22_1, inference(rat,[],[s140,s141])).
% 117.35/16.97 cnf(s146, plain, ~spl22_69, inference(rat,[],[s136,s144])).
% 117.35/16.97 cnf(s147, plain, ~spl22_49, inference(rat,[],[s134,s144])).
% 117.35/16.97 cnf(s148, plain, ~spl22_50, inference(rat,[],[s131,s144])).
% 117.35/16.97 cnf(s151, plain, spl22_70, inference(rat,[],[s114,s139,s146])).
% 117.35/16.97 cnf(s152, plain, $false, inference(rat,[],[s132,s151,s148,s147])).
% 117.35/16.97 tff(f13300,plain,(
% 117.35/16.97 $false),
% 117.35/16.97 inference(avatar_sat_refutation,[],[s152])).
% 117.35/16.97 % SZS output end Proof for theBenchmark
% 117.35/16.97 % (2415743)------------------------------
% 117.35/16.97 % (2415743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 117.35/16.97 % (2415743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 117.35/16.97 % (2415743)CaDiCaL version: 2.1.3
% 117.35/16.97 % (2415743)Termination reason: Refutation
% 117.35/16.97 % (2415743)Time elapsed: 0.693 s
% 117.35/16.97 % (2415743)Peak memory usage: 19 MB
% 117.35/16.97 % (2415743)Instructions burned: 669 (million)
% 117.35/16.97 % (2415628)Success in time 16.647 s
% 117.35/16.97 % Vampire exiting
%------------------------------------------------------------------------------