%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP053^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : 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:31 AM UTC 2026
% Result : Theorem 64.79s 9.45s
% Output : Refutation 64.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP053^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.22 % Computer : n010.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Tue Sep 29 19:44:19 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.27 Running first-order model finding
% 0.10/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.09/1.13 % (3315815)Will run a generic schedule for satisfiability detection.
% 6.09/1.13 % (3315824)% WARNING: option uhcvi not known.
% 6.09/1.13 % (3315828)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3395212380:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.09/1.13 % (3315824)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1274918853:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.09/1.13 % (3315823)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3316314285_2999 on theBenchmark for (2999ds/0Mi)
% 6.09/1.13 % (3315825)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3272022052:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.09/1.13 % (3315826)dis+10_1_sil=32000:sp=arity:random_seed=3297971644:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.09/1.13 % (3315827)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2973261139:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.09/1.13 % (3315829)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3793445735:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.09/1.13 % (3315824)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.09/1.13 % (3315827)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 6.09/1.13 % Exception at run slice level
% 6.09/1.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.09/1.13 % (3315843)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2293615437:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.09/1.13 % (3315824)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 6.09/1.13 % (3315826)Instruction limit reached!
% 6.09/1.13 % (3315826)------------------------------
% 6.09/1.13 % (3315826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.09/1.13 % (3315826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.09/1.13 % (3315826)CaDiCaL version: 2.1.3
% 6.09/1.13 % (3315826)Termination reason: Instruction limit
% 6.09/1.13 % (3315826)Termination phase: Saturation
% 6.09/1.13 % (3315826)Time elapsed: 0.084 s
% 6.09/1.13 % (3315826)Peak memory usage: 13 MB
% 6.09/1.13 % (3315826)Instructions burned: 103 (million)
% 6.09/1.13 % (3315827)Instruction limit reached!
% 6.09/1.13 % (3315827)------------------------------
% 6.09/1.13 % (3315827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.09/1.13 % (3315827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.09/1.13 % (3315827)CaDiCaL version: 2.1.3
% 6.09/1.13 % (3315827)Termination reason: Instruction limit
% 6.09/1.13 % (3315827)Termination phase: Saturation
% 6.09/1.13 % (3315827)Time elapsed: 0.097 s
% 6.09/1.13 % (3315827)Peak memory usage: 13 MB
% 6.09/1.13 % (3315827)Instructions burned: 116 (million)
% 6.09/1.13 % (3315828)Instruction limit reached!
% 6.09/1.13 % (3315828)------------------------------
% 6.09/1.13 % (3315828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.09/1.13 % (3315828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.09/1.13 % (3315828)CaDiCaL version: 2.1.3
% 6.09/1.13 % (3315828)Termination reason: Instruction limit
% 6.09/1.13 % (3315828)Termination phase: Saturation
% 6.09/1.13 % (3315828)Time elapsed: 0.101 s
% 6.09/1.13 % (3315828)Peak memory usage: 14 MB
% 6.09/1.13 % (3315828)Instructions burned: 132 (million)
% 6.09/1.13 % Exception at run slice level
% 6.09/1.13 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 6.09/1.13 % (3315847)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1119299456:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.09/1.13 % (3315851)ott-21_1_sil=16000:fs=off:random_seed=470839086:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.09/1.13 % (3315850)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=1727042464:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.09/1.13 % (3315852)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3724316348:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.09/1.13 % (3315829)Instruction limit reached!
% 6.09/1.13 % (3315829)------------------------------
% 17.18/2.80 % (3315829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.18/2.80 % (3315829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/2.80 % (3315829)CaDiCaL version: 2.1.3
% 17.18/2.80 % (3315829)Termination reason: Instruction limit
% 17.18/2.80 % (3315829)Termination phase: Saturation
% 17.18/2.80 % (3315829)Time elapsed: 0.138 s
% 17.18/2.80 % (3315829)Peak memory usage: 14 MB
% 17.18/2.80 % (3315829)Instructions burned: 159 (million)
% 17.18/2.80 % (3315847)Instruction limit reached!
% 17.18/2.80 % (3315847)------------------------------
% 17.18/2.80 % (3315847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.18/2.80 % (3315847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/2.80 % (3315847)CaDiCaL version: 2.1.3
% 17.18/2.80 % (3315847)Termination reason: Instruction limit
% 17.18/2.80 % (3315847)Termination phase: Saturation
% 17.18/2.80 % (3315847)Time elapsed: 0.059 s
% 17.18/2.80 % (3315847)Peak memory usage: 13 MB
% 17.18/2.80 % (3315847)Instructions burned: 131 (million)
% 17.18/2.80 % (3315850)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.18/2.80 % (3315862)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2079086630:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 17.18/2.80 % (3315867)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=7266564:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 17.18/2.80 % (3315850)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 17.18/2.80 % Exception at run slice level
% 17.18/2.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.18/2.80 % (3315851)Instruction limit reached!
% 17.18/2.80 % (3315851)------------------------------
% 17.18/2.80 % (3315851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.18/2.80 % (3315851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/2.80 % (3315851)CaDiCaL version: 2.1.3
% 17.18/2.80 % (3315851)Termination reason: Instruction limit
% 17.18/2.80 % (3315851)Termination phase: Saturation
% 17.18/2.80 % (3315851)Time elapsed: 0.142 s
% 17.18/2.80 % (3315851)Peak memory usage: 13 MB
% 17.18/2.80 % (3315851)Instructions burned: 181 (million)
% 17.18/2.80 % (3315878)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2936862944:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 17.18/2.80 % (3315880)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=1087084931:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 17.18/2.80 % (3315880)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.18/2.80 % Exception at run slice level
% 17.18/2.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.18/2.80 % (3315883)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=46540172:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 17.18/2.80 % (3315883)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 17.18/2.80 % (3315852)Instruction limit reached!
% 17.18/2.80 % (3315852)------------------------------
% 17.18/2.80 % (3315852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.18/2.80 % (3315852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.18/2.80 % (3315852)CaDiCaL version: 2.1.3
% 17.18/2.80 % (3315852)Termination reason: Instruction limit
% 17.18/2.80 % (3315852)Termination phase: Saturation
% 17.18/2.80 % (3315852)Time elapsed: 0.289 s
% 17.18/2.80 % (3315852)Peak memory usage: 14 MB
% 17.18/2.80 % (3315852)Instructions burned: 478 (million)
% 17.18/2.80 % (3315887)fmb+10_1_sil=64000:random_seed=2857483422:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 17.18/2.80 % (3315887)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 17.18/2.80 % Exception at run slice level
% 17.18/2.80 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 17.18/2.80 % (3315909)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1044359614:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 17.18/2.80 % (3315867)Instruction limit reached!
% 17.18/2.80 % (3315867)------------------------------
% 17.18/2.80 % (3315867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.36/6.85 % (3315867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.36/6.85 % (3315867)CaDiCaL version: 2.1.3
% 46.36/6.85 % (3315867)Termination reason: Instruction limit
% 46.36/6.85 % (3315867)Termination phase: Saturation
% 46.36/6.85 % (3315867)Time elapsed: 0.334 s
% 46.36/6.85 % (3315867)Peak memory usage: 21 MB
% 46.36/6.85 % (3315867)Instructions burned: 1180 (million)
% 46.36/6.85 % (3315850)Instruction limit reached!
% 46.36/6.85 % (3315850)------------------------------
% 46.36/6.85 % (3315850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.36/6.85 % (3315850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.36/6.85 % (3315850)CaDiCaL version: 2.1.3
% 46.36/6.85 % (3315850)Termination reason: Instruction limit
% 46.36/6.85 % (3315850)Termination phase: Saturation
% 46.36/6.85 % (3315850)Time elapsed: 0.401 s
% 46.36/6.85 % (3315850)Peak memory usage: 15 MB
% 46.36/6.85 % (3315850)Instructions burned: 685 (million)
% 46.36/6.85 % Exception at run slice level
% 46.36/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.36/6.85 % (3315928)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=144234585:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 46.36/6.85 % (3315930)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=354339609:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 46.36/6.85 % (3315929)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2318634063:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 46.36/6.85 % Exception at run slice level
% 46.36/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.36/6.85 % (3315941)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=435643353:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 46.36/6.85 % (3315929)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.36/6.85 % (3315930)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.36/6.85 % Exception at run slice level
% 46.36/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.36/6.85 % (3315930)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 46.36/6.85 % (3315956)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=879212214:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 46.36/6.85 % Exception at run slice level
% 46.36/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.36/6.85 % (3315966)ott-2_1_sil=16000:newcnf=on:random_seed=728681135:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 46.36/6.85 % (3315880)Instruction limit reached!
% 46.36/6.85 % (3315880)------------------------------
% 46.36/6.85 % (3315880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.36/6.85 % (3315880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.36/6.85 % (3315880)CaDiCaL version: 2.1.3
% 46.36/6.85 % (3315880)Termination reason: Instruction limit
% 46.36/6.85 % (3315880)Termination phase: Saturation
% 46.36/6.85 % (3315880)Time elapsed: 0.344 s
% 46.36/6.85 % (3315880)Peak memory usage: 16 MB
% 46.36/6.85 % (3315880)Instructions burned: 692 (million)
% 46.36/6.85 % (3315966)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.36/6.85 % (3315973)ott+10_1_sil=32000:tgt=ground:random_seed=910395849:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 46.36/6.85 % (3315883)Instruction limit reached!
% 46.36/6.85 % (3315883)------------------------------
% 46.36/6.85 % (3315883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.36/6.85 % (3315883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.36/6.85 % (3315883)CaDiCaL version: 2.1.3
% 46.36/6.85 % (3315883)Termination reason: Instruction limit
% 46.36/6.85 % (3315883)Termination phase: Saturation
% 46.36/6.85 % (3315883)Time elapsed: 0.423 s
% 46.36/6.85 % (3315883)Peak memory usage: 19 MB
% 46.36/6.85 % (3315883)Instructions burned: 880 (million)
% 46.36/6.85 % (3316002)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2849097462:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 46.36/6.85 % Exception at run slice level
% 46.36/6.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3315966)Instruction limit reached!
% 64.79/9.45 % (3315966)------------------------------
% 64.79/9.45 % (3315966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3315966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3315966)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3315966)Termination reason: Instruction limit
% 64.79/9.45 % (3315966)Termination phase: Saturation
% 64.79/9.45 % (3315966)Time elapsed: 0.197 s
% 64.79/9.45 % (3315966)Peak memory usage: 16 MB
% 64.79/9.45 % (3315966)Instructions burned: 869 (million)
% 64.79/9.45 % (3316010)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1205423134:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 64.79/9.45 % (3316011)dis+21_1_sil=32000:sas=cadical:random_seed=2646252041:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 64.79/9.45 % (3316010)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 64.79/9.45 % (3315930)Instruction limit reached!
% 64.79/9.45 % (3315930)------------------------------
% 64.79/9.45 % (3315930)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3315930)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3315930)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3315930)Termination reason: Instruction limit
% 64.79/9.45 % (3315930)Termination phase: Saturation
% 64.79/9.45 % (3315930)Time elapsed: 0.745 s
% 64.79/9.45 % (3315930)Peak memory usage: 20 MB
% 64.79/9.45 % (3315930)Instructions burned: 1473 (million)
% 64.79/9.45 % (3316061)ott+11_1_sil=16000:gs=on:random_seed=1801854988:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 64.79/9.45 % (3316061)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 64.79/9.45 % (3316011)Instruction limit reached!
% 64.79/9.45 % (3316011)------------------------------
% 64.79/9.45 % (3316011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316011)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316011)Termination reason: Instruction limit
% 64.79/9.45 % (3316011)Termination phase: Saturation
% 64.79/9.45 % (3316011)Time elapsed: 0.912 s
% 64.79/9.45 % (3316011)Peak memory usage: 29 MB
% 64.79/9.45 % (3316011)Instructions burned: 3775 (million)
% 64.79/9.45 % (3316063)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4074742571:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 64.79/9.45 % Exception at run slice level
% 64.79/9.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3316065)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3318965348:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 64.79/9.45 % (3316061)Instruction limit reached!
% 64.79/9.45 % (3316061)------------------------------
% 64.79/9.45 % (3316061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316061)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316061)Termination reason: Instruction limit
% 64.79/9.45 % (3316061)Termination phase: Saturation
% 64.79/9.45 % (3316061)Time elapsed: 1.081 s
% 64.79/9.45 % (3316061)Peak memory usage: 24 MB
% 64.79/9.45 % (3316061)Instructions burned: 2253 (million)
% 64.79/9.45 % (3316067)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2474710378:i=29340_2975 on theBenchmark for (2975ds/29340Mi)
% 64.79/9.45 % (3316010)Instruction limit reached!
% 64.79/9.45 % (3316010)------------------------------
% 64.79/9.45 % (3316010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316010)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316010)Termination reason: Instruction limit
% 64.79/9.45 % (3316010)Termination phase: Saturation
% 64.79/9.45 % (3316010)Time elapsed: 1.628 s
% 64.79/9.45 % (3316010)Peak memory usage: 29 MB
% 64.79/9.45 % (3316010)Instructions burned: 3512 (million)
% 64.79/9.45 % (3316069)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=796377082:i=5211_2974 on theBenchmark for (2974ds/5211Mi)
% 64.79/9.45 % (3315929)Instruction limit reached!
% 64.79/9.45 % (3315929)------------------------------
% 64.79/9.45 % (3315929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3315929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3315929)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3315929)Termination reason: Instruction limit
% 64.79/9.45 % (3315929)Termination phase: Saturation
% 64.79/9.45 % (3315929)Time elapsed: 2.389 s
% 64.79/9.45 % (3315929)Peak memory usage: 35 MB
% 64.79/9.45 % (3315929)Instructions burned: 5132 (million)
% 64.79/9.45 % (3316071)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1716989042:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi)
% 64.79/9.45 % Exception at run slice level
% 64.79/9.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3316065)Instruction limit reached!
% 64.79/9.45 % (3316065)------------------------------
% 64.79/9.45 % (3316065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316065)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316065)Termination reason: Instruction limit
% 64.79/9.45 % (3316065)Termination phase: Saturation
% 64.79/9.45 % (3316065)Time elapsed: 1.217 s
% 64.79/9.45 % (3316065)Peak memory usage: 29 MB
% 64.79/9.45 % (3316065)Instructions burned: 4594 (million)
% 64.79/9.45 % (3316074)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=811963827:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 64.79/9.45 % (3316073)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=455880061:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 64.79/9.45 % Exception at run slice level
% 64.79/9.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3316077)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=109342355:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 64.79/9.45 % Exception at run slice level
% 64.79/9.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3315973)Instruction limit reached!
% 64.79/9.45 % (3315973)------------------------------
% 64.79/9.45 % (3315973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3315973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3315973)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3315973)Termination reason: Instruction limit
% 64.79/9.45 % (3315973)Termination phase: Saturation
% 64.79/9.45 % (3315973)Time elapsed: 2.416 s
% 64.79/9.45 % (3315973)Peak memory usage: 38 MB
% 64.79/9.45 % (3315973)Instructions burned: 5115 (million)
% 64.79/9.45 % (3316079)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3745273696:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi)
% 64.79/9.45 % (3316080)dis+10_16:1_sil=16000:random_seed=3057925036:i=9155:fsr=off_2968 on theBenchmark for (2968ds/9155Mi)
% 64.79/9.45 % (3316069)Instruction limit reached!
% 64.79/9.45 % (3316069)------------------------------
% 64.79/9.45 % (3316069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316069)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316069)Termination reason: Instruction limit
% 64.79/9.45 % (3316069)Termination phase: Saturation
% 64.79/9.45 % (3316069)Time elapsed: 2.457 s
% 64.79/9.45 % (3316069)Peak memory usage: 44 MB
% 64.79/9.45 % (3316069)Instructions burned: 5211 (million)
% 64.79/9.45 % (3316083)ott-3_8_sil=64000:random_seed=1757096037:i=20139:bs=on_2950 on theBenchmark for (2950ds/20139Mi)
% 64.79/9.45 % (3316077)Instruction limit reached!
% 64.79/9.45 % (3316077)------------------------------
% 64.79/9.45 % (3316077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316077)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316077)Termination reason: Instruction limit
% 64.79/9.45 % (3316077)Termination phase: Saturation
% 64.79/9.45 % (3316077)Time elapsed: 3.474 s
% 64.79/9.45 % (3316077)Peak memory usage: 17 MB
% 64.79/9.45 % (3316077)Instructions burned: 22569 (million)
% 64.79/9.45 % (3316085)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=39142842:fmbsr=2:i=32576_2934 on theBenchmark for (2934ds/32576Mi)
% 64.79/9.45 % Exception at run slice level
% 64.79/9.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 64.79/9.45 % (3316087)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2984258744:i=11404_2934 on theBenchmark for (2934ds/11404Mi)
% 64.79/9.45 % (3316079)Instruction limit reached!
% 64.79/9.45 % (3316079)------------------------------
% 64.79/9.45 % (3316079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316079)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316079)Termination reason: Instruction limit
% 64.79/9.45 % (3316079)Termination phase: Saturation
% 64.79/9.45 % (3316079)Time elapsed: 3.872 s
% 64.79/9.45 % (3316079)Peak memory usage: 68 MB
% 64.79/9.45 % (3316079)Instructions burned: 8174 (million)
% 64.79/9.45 % (3316089)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1539520397:i=14134_2930 on theBenchmark for (2930ds/14134Mi)
% 64.79/9.45 % (3316089)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 64.79/9.45 % (3316080)Instruction limit reached!
% 64.79/9.45 % (3316080)------------------------------
% 64.79/9.45 % (3316080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316080)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316080)Termination reason: Instruction limit
% 64.79/9.45 % (3316080)Termination phase: Saturation
% 64.79/9.45 % (3316080)Time elapsed: 4.152 s
% 64.79/9.45 % (3316080)Peak memory usage: 56 MB
% 64.79/9.45 % (3316080)Instructions burned: 9157 (million)
% 64.79/9.45 % (3316091)dis+33_16_sil=32000:sac=on:random_seed=3438337183:i=15851:nm=0_2927 on theBenchmark for (2927ds/15851Mi)
% 64.79/9.45 % (3316083) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3315815-3316083"...
% 64.79/9.45 % (3316083)...printing done.
% 64.79/9.45 % (3316083)Refutation found. Thanks to Tanya!
% 64.79/9.45 % SZS status Theorem for theBenchmark
% 64.79/9.45 % SZS output start Proof for theBenchmark
% 64.79/9.45 thf(type_def_5, type, product_prod: ($tType * $tType) > $tType).
% 64.79/9.45 thf(type_def_6, type, list: $tType > $tType).
% 64.79/9.45 thf(type_def_7, type, capacity: $tType).
% 64.79/9.45 thf(type_def_8, type, set: $tType > $tType).
% 64.79/9.45 thf(type_def_9, type, nat: $tType).
% 64.79/9.45 thf(type_def_10, type, sTfun: ($tType * $tType) > $tType).
% 64.79/9.45 thf(func_def_0, type, type: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_1, type, size: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_2, type, one: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_3, type, ord: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_4, type, order: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_5, type, group_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_6, type, linorder: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_7, type, preorder: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_8, type, wellorder: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_9, type, semigroup_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_10, type, linordered_idom: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_11, type, comm_monoid_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_12, type, ab_semigroup_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_13, type, linordered_semidom: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_14, type, cancel_semigroup_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_15, type, ordere779506340up_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_16, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_17, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_18, type, ordere236663937imp_le: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_19, type, ordere223160158up_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_20, type, strict2144017051up_add: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_21, type, unique1598680935umeral: !>[X0: $tType]:($o)).
% 64.79/9.45 thf(func_def_22, type, connected: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > nat > $o))).
% 64.79/9.45 thf(func_def_23, type, dist: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > nat > nat > $o))).
% 64.79/9.45 thf(func_def_24, type, isPath: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > list @ product_prod @ nat @ nat > nat > $o))).
% 64.79/9.45 thf(func_def_25, type, isShortestPath: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > list @ product_prod @ nat @ nat > nat > $o))).
% 64.79/9.45 thf(func_def_26, type, isSimplePath: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > list @ product_prod @ nat @ nat > nat > $o))).
% 64.79/9.45 thf(func_def_27, type, min_dist: !>[X0: $tType]:(((product_prod @ nat @ nat > X0) > nat > nat > nat))).
% 64.79/9.45 thf(func_def_28, type, one_one: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_29, type, plus_plus: !>[X0: $tType]:((X0 > X0 > X0))).
% 64.79/9.45 thf(func_def_30, type, nil: !>[X0: $tType]:(list @ X0)).
% 64.79/9.45 thf(func_def_31, type, set2: !>[X0: $tType]:((list @ X0 > set @ X0))).
% 64.79/9.45 thf(func_def_32, type, size_size: !>[X0: $tType]:((X0 > nat))).
% 64.79/9.45 thf(func_def_33, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_34, type, ord_less_eq: !>[X0: $tType]:((X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_35, type, product_Pair: !>[X0: $tType, X1: $tType]:((X0 > X1 > product_prod @ X0 @ X1))).
% 64.79/9.45 thf(func_def_36, type, product_rec_prod: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > product_prod @ X0 @ X1 > X2))).
% 64.79/9.45 thf(func_def_37, type, product_swap: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > product_prod @ X1 @ X0))).
% 64.79/9.45 thf(func_def_38, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 64.79/9.45 thf(func_def_39, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 64.79/9.45 thf(func_def_40, type, c: (product_prod @ nat @ nat > capacity)).
% 64.79/9.45 thf(func_def_41, type, p: list @ product_prod @ nat @ nat).
% 64.79/9.45 thf(func_def_42, type, p1: list @ product_prod @ nat @ nat).
% 64.79/9.45 thf(func_def_43, type, p2: list @ product_prod @ nat @ nat).
% 64.79/9.45 thf(func_def_44, type, p3: list @ product_prod @ nat @ nat).
% 64.79/9.45 thf(func_def_45, type, s: nat).
% 64.79/9.45 thf(func_def_46, type, t: nat).
% 64.79/9.45 thf(func_def_47, type, u: nat).
% 64.79/9.45 thf(func_def_48, type, v: nat).
% 64.79/9.45 thf(func_def_52, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_53, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 64.79/9.45 thf(func_def_54, type, vAND: ($o > $o > $o)).
% 64.79/9.45 thf(func_def_55, type, db0: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_56, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 64.79/9.45 thf(func_def_57, type, db1: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_58, type, db4: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_59, type, db3: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_60, type, db2: !>[X0: $tType]:(X0)).
% 64.79/9.45 thf(func_def_61, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 64.79/9.45 thf(func_def_62, type, vIMP: ($o > $o > $o)).
% 64.79/9.45 thf(func_def_63, type, vOR: ($o > $o > $o)).
% 64.79/9.45 thf(func_def_64, type, vNOT: ($o > $o)).
% 64.79/9.45 thf(func_def_65, type, sP0: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_66, type, sP1: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_67, type, sP2: !>[X0: $tType]:((X0 > X0 > X0 > $o))).
% 64.79/9.45 thf(func_def_68, type, sK3: (nat > nat > nat > nat)).
% 64.79/9.45 thf(func_def_69, type, sK4: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_70, type, sK5: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_71, type, sK6: (nat > nat > list @ product_prod @ nat @ nat)).
% 64.79/9.45 thf(func_def_72, type, sK7: (nat > list @ product_prod @ nat @ nat > nat)).
% 64.79/9.45 thf(func_def_73, type, sK8: (nat > list @ product_prod @ nat @ nat > nat)).
% 64.79/9.45 thf(func_def_74, type, sK9: (nat > nat > nat)).
% 64.79/9.45 thf(func_def_75, type, sK10: ((nat > $o) > nat > nat > nat)).
% 64.79/9.45 thf(func_def_76, type, sK11: (nat > list @ product_prod @ nat @ nat > nat)).
% 64.79/9.45 thf(func_def_77, type, sK12: (nat > list @ product_prod @ nat @ nat > nat)).
% 64.79/9.45 thf(func_def_78, type, sK13: !>[X0: $tType]:((nat > nat > (product_prod @ nat @ nat > X0) > list @ product_prod @ nat @ nat))).
% 64.79/9.45 thf(func_def_79, type, sK14: !>[X0: $tType]:((nat > nat > (product_prod @ nat @ nat > X0) > nat))).
% 64.79/9.45 thf(func_def_80, type, sK15: !>[X0: $tType]:(((nat > $o) > nat > nat > (product_prod @ nat @ nat > X0) > nat))).
% 64.79/9.45 thf(func_def_81, type, sK16: !>[X0: $tType]:((X0 > X0 > X0))).
% 64.79/9.45 thf(func_def_82, type, sK17: !>[X0: $tType]:((nat > nat > nat > (product_prod @ nat @ nat > X0) > nat))).
% 64.79/9.45 thf(func_def_83, type, sK18: (nat > nat > nat)).
% 64.79/9.45 thf(func_def_84, type, sK19: (nat > nat > list @ product_prod @ nat @ nat)).
% 64.79/9.45 thf(func_def_85, type, sK20: ((nat > nat) > nat)).
% 64.79/9.45 thf(func_def_86, type, sK21: ((nat > nat) > nat)).
% 64.79/9.45 thf(func_def_87, type, sK22: !>[X0: $tType, X1: $tType]:(((X1 > $o) > (X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_88, type, sK23: ((nat > $o) > nat)).
% 64.79/9.45 thf(func_def_89, type, sK24: ((nat > $o) > nat)).
% 64.79/9.45 thf(func_def_90, type, sK25: !>[X0: $tType, X1: $tType]:(((X1 > $o) > (X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_91, type, sK26: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_92, type, sK27: ((nat > nat) > nat)).
% 64.79/9.45 thf(func_def_93, type, sK28: ((nat > nat) > nat)).
% 64.79/9.45 thf(func_def_94, type, sK29: !>[X0: $tType]:((nat > nat > (product_prod @ nat @ nat > X0) > list @ product_prod @ nat @ nat))).
% 64.79/9.45 thf(func_def_95, type, sK30: !>[X0: $tType]:((nat > nat > (product_prod @ nat @ nat > X0) > nat))).
% 64.79/9.45 thf(func_def_96, type, sK31: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 64.79/9.45 thf(func_def_97, type, sK32: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 64.79/9.45 thf(func_def_98, type, sK33: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_99, type, sK34: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_100, type, sK35: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X0))).
% 64.79/9.45 thf(func_def_101, type, sK36: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X1))).
% 64.79/9.45 thf(func_def_102, type, sK37: !>[X0: $tType, X1: $tType, X2: $tType]:((product_prod @ X0 @ product_prod @ X1 @ X2 > X2))).
% 64.79/9.45 thf(func_def_103, type, sK38: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ X3 > X0))).
% 64.79/9.45 thf(func_def_104, type, sK39: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ X3 > X1))).
% 64.79/9.45 thf(func_def_105, type, sK40: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ X3 > X2))).
% 64.79/9.45 thf(func_def_106, type, sK41: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ X3 > X3))).
% 64.79/9.45 thf(func_def_107, type, sK42: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ X4 > X0))).
% 64.79/9.45 thf(func_def_108, type, sK43: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ X4 > X1))).
% 64.79/9.45 thf(func_def_109, type, sK44: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ X4 > X2))).
% 64.79/9.45 thf(func_def_110, type, sK45: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ X4 > X3))).
% 64.79/9.45 thf(func_def_111, type, sK46: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ X4 > X4))).
% 64.79/9.45 thf(func_def_112, type, sK47: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X0))).
% 64.79/9.45 thf(func_def_113, type, sK48: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X1))).
% 64.79/9.45 thf(func_def_114, type, sK49: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X2))).
% 64.79/9.45 thf(func_def_115, type, sK50: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X3))).
% 64.79/9.45 thf(func_def_116, type, sK51: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X4))).
% 64.79/9.45 thf(func_def_117, type, sK52: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ X5 > X5))).
% 64.79/9.45 thf(func_def_118, type, sK53: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X0))).
% 64.79/9.45 thf(func_def_119, type, sK54: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X1))).
% 64.79/9.45 thf(func_def_120, type, sK55: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X2))).
% 64.79/9.45 thf(func_def_121, type, sK56: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X3))).
% 64.79/9.45 thf(func_def_122, type, sK57: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X4))).
% 64.79/9.45 thf(func_def_123, type, sK58: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X5))).
% 64.79/9.45 thf(func_def_124, type, sK59: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:((product_prod @ X0 @ product_prod @ X1 @ product_prod @ X2 @ product_prod @ X3 @ product_prod @ X4 @ product_prod @ X5 @ X6 > X6))).
% 64.79/9.45 thf(func_def_125, type, sK60: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X2))).
% 64.79/9.45 thf(func_def_126, type, sK61: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_127, type, sK62: !>[X0: $tType, X1: $tType, X2: $tType]:(((product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_128, type, sK63: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X3))).
% 64.79/9.45 thf(func_def_129, type, sK64: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X2))).
% 64.79/9.45 thf(func_def_130, type, sK65: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_131, type, sK66: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_132, type, sK67: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X4))).
% 64.79/9.45 thf(func_def_133, type, sK68: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X3))).
% 64.79/9.45 thf(func_def_134, type, sK69: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X2))).
% 64.79/9.45 thf(func_def_135, type, sK70: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_136, type, sK71: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_137, type, sK72: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X5))).
% 64.79/9.45 thf(func_def_138, type, sK73: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X4))).
% 64.79/9.45 thf(func_def_139, type, sK74: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X3))).
% 64.79/9.45 thf(func_def_140, type, sK75: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X2))).
% 64.79/9.45 thf(func_def_141, type, sK76: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_142, type, sK77: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_143, type, sK78: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X6))).
% 64.79/9.45 thf(func_def_144, type, sK79: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X5))).
% 64.79/9.45 thf(func_def_145, type, sK80: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X4))).
% 64.79/9.45 thf(func_def_146, type, sK81: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X3))).
% 64.79/9.45 thf(func_def_147, type, sK82: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X2))).
% 64.79/9.45 thf(func_def_148, type, sK83: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_149, type, sK84: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((product_prod @ X6 @ product_prod @ X5 @ product_prod @ X4 @ product_prod @ X3 @ product_prod @ X2 @ product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_150, type, sK85: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X0))).
% 64.79/9.45 thf(func_def_151, type, sK86: !>[X0: $tType, X1: $tType]:((product_prod @ X0 @ X1 > X1))).
% 64.79/9.45 thf(func_def_152, type, sK87: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X1))).
% 64.79/9.45 thf(func_def_153, type, sK88: !>[X0: $tType, X1: $tType]:(((product_prod @ X1 @ X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_154, type, sK89: ((nat > $o) > nat)).
% 64.79/9.45 thf(func_def_155, type, sK90: (nat > (nat > $o) > nat)).
% 64.79/9.45 thf(func_def_156, type, sK91: (nat > nat > nat)).
% 64.79/9.45 thf(func_def_157, type, sK92: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat > X0 > X0))).
% 64.79/9.45 thf(func_def_158, type, sK93: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat))).
% 64.79/9.45 thf(func_def_159, type, sK94: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > nat))).
% 64.79/9.45 thf(func_def_160, type, sK95: !>[X0: $tType]:((((nat > X0 > X0) > nat > nat > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_161, type, sK96: !>[X0: $tType]:((nat > (X0 > nat) > X0 > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_162, type, sK97: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_163, type, sK98: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_164, type, sK99: ((nat > $o) > nat)).
% 64.79/9.45 thf(func_def_165, type, sK100: (nat > (nat > $o) > nat)).
% 64.79/9.45 thf(func_def_166, type, sK101: !>[X0: $tType]:((product_prod @ (nat > X0 > X0) @ product_prod @ nat @ product_prod @ nat @ X0 > nat > X0 > X0))).
% 64.79/9.45 thf(func_def_167, type, sK102: !>[X0: $tType]:((product_prod @ (nat > X0 > X0) @ product_prod @ nat @ product_prod @ nat @ X0 > nat))).
% 64.79/9.45 thf(func_def_168, type, sK103: !>[X0: $tType]:((product_prod @ (nat > X0 > X0) @ product_prod @ nat @ product_prod @ nat @ X0 > nat))).
% 64.79/9.45 thf(func_def_169, type, sK104: !>[X0: $tType]:((product_prod @ (nat > X0 > X0) @ product_prod @ nat @ product_prod @ nat @ X0 > X0))).
% 64.79/9.45 thf(func_def_170, type, sK105: !>[X0: $tType]:(((X0 > nat) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_171, type, sK106: !>[X0: $tType]:((nat > (X0 > nat) > (X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_172, type, sK107: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_173, type, sK108: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_174, type, sK109: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_175, type, sK110: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_176, type, sK111: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 64.79/9.45 thf(func_def_177, type, sK112: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 64.79/9.45 thf(func_def_178, type, sK113: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_179, type, sK114: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_180, type, sK115: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 64.79/9.45 thf(func_def_181, type, sK116: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 64.79/9.45 thf(func_def_182, type, sK117: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_183, type, sK118: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_184, type, sK119: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 64.79/9.45 thf(func_def_185, type, sK120: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_186, type, sK121: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_187, type, sK122: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_188, type, sK123: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_189, type, sK124: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 64.79/9.45 thf(func_def_190, type, sK125: (list @ product_prod @ nat @ nat > nat > nat > list @ product_prod @ nat @ nat)).
% 64.79/9.45 thf(func_def_191, type, sK126: (nat > nat > nat)).
% 64.79/9.45 thf(func_def_192, type, sK127: (nat > nat > list @ product_prod @ nat @ nat)).
% 64.79/9.45 thf(func_def_193, type, sK128: (nat > nat > nat > list @ product_prod @ nat @ nat)).
% 64.79/9.45 thf(f1,axiom,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ one_one @ nat) @ (size_size @ list @ product_prod @ nat @ nat @ p2))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_MIN_H)).
% 64.79/9.45 thf(f3,axiom,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) = ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))))) => (((min_dist @ capacity @ c @ u @ t)) = ((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062min__dist_As_At_A_061_Alength_Ap1_A_L_A_I1_A_L_Alength_Ap2_J_A_092_060Longrightarrow_062_Amin__dist_Au_At_A_061_A1_A_L_Alength_Ap2_092_060close_062)).
% 64.79/9.45 thf(f5,axiom,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) = ((size_size @ list @ product_prod @ nat @ nat @ p)))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_MIN)).
% 64.79/9.45 thf(f11,axiom,(
% 64.79/9.45 ! [X0 : $tType] : (cancel_semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : ((((plus_plus @ X0 @ X1 @ X2)) = ((plus_plus @ X0 @ X3 @ X2))) = (X1 = X3)))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_add__right__cancel)).
% 64.79/9.45 thf(f23,axiom,(
% 64.79/9.45 ! [X0 : $tType] : (ab_semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ X2 @ (plus_plus @ X0 @ X1 @ X3)))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_add_Oleft__commute)).
% 64.79/9.45 thf(f27,axiom,(
% 64.79/9.45 ! [X0 : $tType] : (semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ (plus_plus @ X0 @ X1 @ X2) @ X3)) = ((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3)))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_add_Oassoc)).
% 64.79/9.45 thf(f125,axiom,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ~(ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X0)),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_not__add__less1)).
% 64.79/9.45 thf(f139,axiom,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~(ord_less @ nat @ X0 @ X1) => (ord_less @ nat @ X1 @ X0)))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_linorder__neqE__nat)).
% 64.79/9.45 thf(f179,axiom,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 = X1) => (ord_less_eq @ nat @ X0 @ X1))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_eq__imp__le)).
% 64.79/9.45 thf(f189,axiom,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ? [X2 : nat] : (X1 = ((plus_plus @ nat @ X0 @ X2))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_le__Suc__ex)).
% 64.79/9.45 thf(f193,axiom,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (ord_less_eq @ nat @ X0 @ (plus_plus @ nat @ X0 @ X1))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_le__add1)).
% 64.79/9.45 thf(f283,axiom,(
% 64.79/9.45 cancel_semigroup_add @ nat),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__semigroup__add)).
% 64.79/9.45 thf(f285,axiom,(
% 64.79/9.45 ab_semigroup_add @ nat),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oab__semigroup__add)).
% 64.79/9.45 thf(f287,axiom,(
% 64.79/9.45 semigroup_add @ nat),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Osemigroup__add)).
% 64.79/9.45 thf(f305,conjecture,(
% 64.79/9.45 (((min_dist @ capacity @ c @ u @ t)) = ((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))))),
% 64.79/9.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 64.79/9.45 thf(f306,negated_conjecture,(
% 64.79/9.45 ~ (((min_dist @ capacity @ c @ u @ t)) = ((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))))),
% 64.79/9.45 inference(negated_conjecture,[status(cth)],[f305])).
% 64.79/9.45 thf(f313,plain,(
% 64.79/9.45 ! [X0 : $tType] : (cancel_semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : ((((plus_plus @ X0 @ X1 @ X2)) = ((plus_plus @ X0 @ X3 @ X2))) = (X1 = X3)))),
% 64.79/9.45 inference(rectify,[],[f11])).
% 64.79/9.45 thf(f314,plain,(
% 64.79/9.45 ! [X0 : $tType] : ((cancel_semigroup_add @ X0 = $true) => ! [X1 : X0,X2 : X0,X3 : X0] : ((((plus_plus @ X0 @ X1 @ X2) = (plus_plus @ X0 @ X3 @ X2))) = ((X1 = X3))))),
% 64.79/9.45 inference(fool_elimination,[],[f313])).
% 64.79/9.45 thf(f337,plain,(
% 64.79/9.45 ! [X0 : $tType] : (ab_semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ X2 @ (plus_plus @ X0 @ X1 @ X3)))))),
% 64.79/9.45 inference(rectify,[],[f23])).
% 64.79/9.45 thf(f338,plain,(
% 64.79/9.45 ! [X0 : $tType] : ((ab_semigroup_add @ X0 = $true) => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ X2 @ (plus_plus @ X0 @ X1 @ X3)))))),
% 64.79/9.45 inference(fool_elimination,[],[f337])).
% 64.79/9.45 thf(f345,plain,(
% 64.79/9.45 ! [X0 : $tType] : (semigroup_add @ X0 => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ (plus_plus @ X0 @ X1 @ X2) @ X3)) = ((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3)))))),
% 64.79/9.45 inference(rectify,[],[f27])).
% 64.79/9.45 thf(f346,plain,(
% 64.79/9.45 ! [X0 : $tType] : ((semigroup_add @ X0 = $true) => ! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ (plus_plus @ X0 @ X1 @ X2) @ X3))))),
% 64.79/9.45 inference(fool_elimination,[],[f345])).
% 64.79/9.45 thf(f529,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ~(ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X0)),
% 64.79/9.45 inference(rectify,[],[f125])).
% 64.79/9.45 thf(f530,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ~ (((ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X0)) = $true)),
% 64.79/9.45 inference(fool_elimination,[],[f529])).
% 64.79/9.45 thf(f557,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~(ord_less @ nat @ X0 @ X1) => (ord_less @ nat @ X1 @ X0)))),
% 64.79/9.45 inference(rectify,[],[f139])).
% 64.79/9.45 thf(f558,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 != X1) => (~ (((ord_less @ nat @ X0 @ X1)) = $true) => (((ord_less @ nat @ X1 @ X0)) = $true)))),
% 64.79/9.45 inference(fool_elimination,[],[f557])).
% 64.79/9.45 thf(f621,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 = X1) => (ord_less_eq @ nat @ X0 @ X1))),
% 64.79/9.45 inference(rectify,[],[f179])).
% 64.79/9.45 thf(f622,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 = X1) => (((ord_less_eq @ nat @ X0 @ X1)) = $true))),
% 64.79/9.45 inference(fool_elimination,[],[f621])).
% 64.79/9.45 thf(f640,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((ord_less_eq @ nat @ X0 @ X1) => ? [X2 : nat] : (X1 = ((plus_plus @ nat @ X0 @ X2))))),
% 64.79/9.45 inference(rectify,[],[f189])).
% 64.79/9.45 thf(f641,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) => ? [X2 : nat] : (((plus_plus @ nat @ X0 @ X2)) = X1))),
% 64.79/9.45 inference(fool_elimination,[],[f640])).
% 64.79/9.45 thf(f648,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (ord_less_eq @ nat @ X0 @ (plus_plus @ nat @ X0 @ X1))),
% 64.79/9.45 inference(rectify,[],[f193])).
% 64.79/9.45 thf(f649,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (((ord_less_eq @ nat @ X0 @ (plus_plus @ nat @ X0 @ X1))) = $true)),
% 64.79/9.45 inference(fool_elimination,[],[f648])).
% 64.79/9.45 thf(f817,plain,(
% 64.79/9.45 cancel_semigroup_add @ nat),
% 64.79/9.45 inference(rectify,[],[f283])).
% 64.79/9.45 thf(f818,plain,(
% 64.79/9.45 (cancel_semigroup_add @ nat = $true)),
% 64.79/9.45 inference(fool_elimination,[],[f817])).
% 64.79/9.45 thf(f821,plain,(
% 64.79/9.45 ab_semigroup_add @ nat),
% 64.79/9.45 inference(rectify,[],[f285])).
% 64.79/9.45 thf(f822,plain,(
% 64.79/9.45 (ab_semigroup_add @ nat = $true)),
% 64.79/9.45 inference(fool_elimination,[],[f821])).
% 64.79/9.45 thf(f825,plain,(
% 64.79/9.45 semigroup_add @ nat),
% 64.79/9.45 inference(rectify,[],[f287])).
% 64.79/9.45 thf(f826,plain,(
% 64.79/9.45 (semigroup_add @ nat = $true)),
% 64.79/9.45 inference(fool_elimination,[],[f825])).
% 64.79/9.45 thf(f866,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (((ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X0)) != $true)),
% 64.79/9.45 inference(flattening,[],[f530])).
% 64.79/9.45 thf(f871,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((X0 != X1) => ((((ord_less @ nat @ X0 @ X1)) != $true) => (((ord_less @ nat @ X1 @ X0)) = $true)))),
% 64.79/9.45 inference(flattening,[],[f558])).
% 64.79/9.45 thf(f888,plain,(
% 64.79/9.45 (((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))) != ((min_dist @ capacity @ c @ u @ t)))),
% 64.79/9.45 inference(flattening,[],[f306])).
% 64.79/9.45 thf(f890,plain,(
% 64.79/9.45 (((min_dist @ capacity @ c @ u @ t)) = ((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))) | (((min_dist @ capacity @ c @ s @ t)) != ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))))),
% 64.79/9.45 inference(ennf_transformation,[],[f3])).
% 64.79/9.45 thf(f896,plain,(
% 64.79/9.45 ! [X0 : $tType] : (! [X1 : X0,X2 : X0,X3 : X0] : ((((plus_plus @ X0 @ X1 @ X2) = (plus_plus @ X0 @ X3 @ X2))) = ((X1 = X3))) | (cancel_semigroup_add @ X0 != $true))),
% 64.79/9.45 inference(ennf_transformation,[],[f314])).
% 64.79/9.45 thf(f902,plain,(
% 64.79/9.45 ! [X0 : $tType] : (! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ X2 @ (plus_plus @ X0 @ X1 @ X3)))) | (ab_semigroup_add @ X0 != $true))),
% 64.79/9.45 inference(ennf_transformation,[],[f338])).
% 64.79/9.45 thf(f906,plain,(
% 64.79/9.45 ! [X0 : $tType] : (! [X1 : X0,X2 : X0,X3 : X0] : (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ (plus_plus @ X0 @ X1 @ X2) @ X3))) | (semigroup_add @ X0 != $true))),
% 64.79/9.45 inference(ennf_transformation,[],[f346])).
% 64.79/9.45 thf(f1034,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (((((ord_less @ nat @ X1 @ X0)) = $true) | (((ord_less @ nat @ X0 @ X1)) = $true)) | (X0 = X1))),
% 64.79/9.45 inference(ennf_transformation,[],[f871])).
% 64.79/9.45 thf(f1035,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X1 @ X0)) = $true) | (((ord_less @ nat @ X0 @ X1)) = $true) | (X0 = X1))),
% 64.79/9.45 inference(flattening,[],[f1034])).
% 64.79/9.45 thf(f1085,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) | (X0 != X1))),
% 64.79/9.45 inference(ennf_transformation,[],[f622])).
% 64.79/9.45 thf(f1096,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : (? [X2 : nat] : (((plus_plus @ nat @ X0 @ X2)) = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 64.79/9.45 inference(ennf_transformation,[],[f641])).
% 64.79/9.45 thf(f1246,plain,(
% 64.79/9.45 ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ (sK91 @ X1 @ X0))) = X1) | (((ord_less_eq @ nat @ X0 @ X1)) != $true))),
% 64.79/9.45 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X3,sK3 @ X2 @ X1 @ X0)],[f1096])).
% 64.79/9.45 thf(f1271,plain,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ one_one @ nat) @ (size_size @ list @ product_prod @ nat @ nat @ p2))))),
% 64.79/9.45 inference(cnf_transformation,[],[f1])).
% 64.79/9.45 thf(f1273,plain,(
% 64.79/9.45 (((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))) = ((min_dist @ capacity @ c @ u @ t))) | (((min_dist @ capacity @ c @ s @ t)) != ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))))),
% 64.79/9.45 inference(cnf_transformation,[],[f890])).
% 64.79/9.45 thf(f1275,plain,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) = ((size_size @ list @ product_prod @ nat @ nat @ p)))),
% 64.79/9.45 inference(cnf_transformation,[],[f5])).
% 64.79/9.45 thf(f1281,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : (((((plus_plus @ X0 @ X1 @ X2) = (plus_plus @ X0 @ X3 @ X2))) = ((X1 = X3))) | (cancel_semigroup_add @ X0 != $true)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f896])).
% 64.79/9.45 thf(f1293,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : ((ab_semigroup_add @ X0 != $true) | (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ X2 @ (plus_plus @ X0 @ X1 @ X3))))) )),
% 64.79/9.45 inference(cnf_transformation,[],[f902])).
% 64.79/9.45 thf(f1297,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : ((semigroup_add @ X0 != $true) | (((plus_plus @ X0 @ X1 @ (plus_plus @ X0 @ X2 @ X3))) = ((plus_plus @ X0 @ (plus_plus @ X0 @ X1 @ X2) @ X3)))) )),
% 64.79/9.45 inference(cnf_transformation,[],[f906])).
% 64.79/9.45 thf(f1406,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X0)) != $true)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f866])).
% 64.79/9.45 thf(f1423,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less @ nat @ X1 @ X0)) = $true) | (((ord_less @ nat @ X0 @ X1)) = $true) | (X0 = X1)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f1035])).
% 64.79/9.45 thf(f1468,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) = $true) | (X0 != X1)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f1085])).
% 64.79/9.45 thf(f1481,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ X1)) != $true) | (((plus_plus @ nat @ X0 @ (sK91 @ X1 @ X0))) = X1)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f1246])).
% 64.79/9.45 thf(f1485,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X0 @ (plus_plus @ nat @ X0 @ X1))) = $true)) )),
% 64.79/9.45 inference(cnf_transformation,[],[f649])).
% 64.79/9.45 thf(f1610,plain,(
% 64.79/9.45 (cancel_semigroup_add @ nat = $true)),
% 64.79/9.45 inference(cnf_transformation,[],[f818])).
% 64.79/9.45 thf(f1612,plain,(
% 64.79/9.45 (ab_semigroup_add @ nat = $true)),
% 64.79/9.45 inference(cnf_transformation,[],[f822])).
% 64.79/9.45 thf(f1614,plain,(
% 64.79/9.45 (semigroup_add @ nat = $true)),
% 64.79/9.45 inference(cnf_transformation,[],[f826])).
% 64.79/9.45 thf(f1632,plain,(
% 64.79/9.45 (((plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2))) != ((min_dist @ capacity @ c @ u @ t)))),
% 64.79/9.45 inference(cnf_transformation,[],[f888])).
% 64.79/9.45 thf(f1651,plain,(
% 64.79/9.45 ( ! [X1 : nat] : (($true = ((ord_less_eq @ nat @ X1 @ X1)))) )),
% 64.79/9.45 inference(equality_resolution,[],[f1468])).
% 64.79/9.45 thf(f1825,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : (($true = (((plus_plus @ X0 @ X1 @ X2) = (plus_plus @ X0 @ X3 @ X2)))) | (cancel_semigroup_add @ X0 != $true) | (((X1 = X3)) = $false)) )),
% 64.79/9.45 inference(iff_proxy_clausification,[],[f1281])).
% 64.79/9.45 thf(f1829,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : ((((plus_plus @ X0 @ X1 @ X2)) = ((plus_plus @ X0 @ X3 @ X2))) | (cancel_semigroup_add @ X0 != $true) | (((X1 = X3)) = $false)) )),
% 64.79/9.45 inference(equality_proxy_clausification,[],[f1825])).
% 64.79/9.45 thf(f1830,plain,(
% 64.79/9.45 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0] : ((cancel_semigroup_add @ X0 != $true) | (((plus_plus @ X0 @ X1 @ X2)) = ((plus_plus @ X0 @ X3 @ X2))) | (X1 != X3)) )),
% 64.79/9.45 inference(equality_proxy_clausification,[],[f1829])).
% 64.79/9.45 thf(f1846,plain,(
% 64.79/9.45 (((min_dist @ capacity @ c @ s @ t)) != ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))))),
% 64.79/9.45 inference(forward_subsumption_resolution,[],[f1273,f1632])).
% 64.79/9.45 thf(f1848,plain,(
% 64.79/9.45 (((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ one_one @ nat) @ (size_size @ list @ product_prod @ nat @ nat @ p2))) = ((size_size @ list @ product_prod @ nat @ nat @ p)))),
% 64.79/9.45 inference(forward_demodulation,[],[f1271,f1275])).
% 64.79/9.45 thf(f1849,plain,(
% 64.79/9.45 (((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))) != ((size_size @ list @ product_prod @ nat @ nat @ p)))),
% 64.79/9.45 inference(forward_demodulation,[],[f1846,f1275])).
% 64.79/9.45 thf(f1855,definition,(
% 64.79/9.45 spl129_4 <=> (((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))) = ((size_size @ list @ product_prod @ nat @ nat @ p)))),
% 64.79/9.45 introduced(definition,[new_symbols(definition,[spl129_4])],[avatar_definition])).
% 64.79/9.45 thf(f1857,plain,(
% 64.79/9.45 (((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p2)))) != ((size_size @ list @ product_prod @ nat @ nat @ p))) | spl129_4),
% 64.79/9.45 inference(avatar_component_clause,[],[f1855])).
% 64.79/9.45 thf(f1859,plain,(
% 64.79/9.45 ~spl129_4),
% 64.79/9.45 inference(avatar_split_clause,[],[f1849,f1855])).
% 64.79/9.45 thf(f30233,plain,(
% 64.79/9.45 ( ! [X0 : nat] : (($true != $true) | (((plus_plus @ nat @ X0 @ (sK91 @ X0 @ X0))) = X0)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1481,f1651])).
% 64.79/9.45 thf(f30273,plain,(
% 64.79/9.45 ( ! [X0 : nat] : ((((plus_plus @ nat @ X0 @ (sK91 @ X0 @ X0))) = X0)) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f30233])).
% 64.79/9.45 thf(f32969,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : (($true != $true) | (((plus_plus @ nat @ X0 @ X1)) = ((plus_plus @ nat @ X2 @ X1))) | (X0 != X2)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1830,f1610])).
% 64.79/9.45 thf(f32994,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ X1)) = ((plus_plus @ nat @ X2 @ X1))) | (X0 != X2)) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f32969])).
% 64.79/9.45 thf(f33041,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less @ nat @ (plus_plus @ nat @ X0 @ X1) @ X2)) != $true) | (X0 != X2)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1406,f32994])).
% 64.79/9.45 thf(f33061,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ (sK91 @ X1 @ X1))) = X1) | (X0 != X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f30273,f32994])).
% 64.79/9.45 thf(f35023,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((ord_less_eq @ nat @ X1 @ X0)) = $true) | (X0 != X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1485,f33061])).
% 64.79/9.45 thf(f35129,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : (($true != $true) | (((plus_plus @ nat @ X0 @ (sK91 @ X1 @ X0))) = X1) | (X0 != X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1481,f35023])).
% 64.79/9.45 thf(f35141,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X0 @ (sK91 @ X1 @ X0))) = X1) | (X0 != X1)) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f35129])).
% 64.79/9.45 thf(f38465,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((ord_less @ nat @ X0 @ X2)) != $true) | (X1 != X2) | (X0 != X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f33041,f35141])).
% 64.79/9.45 thf(f38538,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : (($true != $true) | (X1 != X2) | (X0 != X2) | (((ord_less @ nat @ X1 @ X0)) = $true) | (X0 = X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f38465,f1423])).
% 64.79/9.45 thf(f38582,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((X1 != X2) | (X0 != X2) | (((ord_less @ nat @ X1 @ X0)) = $true) | (X0 = X1)) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f38538])).
% 64.79/9.45 thf(f38589,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((X0 = X1) | (X0 != X2) | (X1 != X2)) )),
% 64.79/9.45 inference(forward_subsumption_resolution,[],[f38582,f38465])).
% 64.79/9.45 thf(f40875,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : (($true != $true) | (((plus_plus @ nat @ X1 @ (plus_plus @ nat @ X0 @ X2))) = ((plus_plus @ nat @ X0 @ (plus_plus @ nat @ X1 @ X2))))) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1293,f1612])).
% 64.79/9.45 thf(f40900,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((plus_plus @ nat @ X1 @ (plus_plus @ nat @ X0 @ X2))) = ((plus_plus @ nat @ X0 @ (plus_plus @ nat @ X1 @ X2))))) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f40875])).
% 64.79/9.45 thf(f40941,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : (($true != $true) | (((plus_plus @ nat @ (plus_plus @ nat @ X0 @ X1) @ X2)) = ((plus_plus @ nat @ X0 @ (plus_plus @ nat @ X1 @ X2))))) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1297,f1614])).
% 64.79/9.45 thf(f40966,plain,(
% 64.79/9.45 ( ! [X2 : nat,X0 : nat,X1 : nat] : ((((plus_plus @ nat @ (plus_plus @ nat @ X0 @ X1) @ X2)) = ((plus_plus @ nat @ X0 @ (plus_plus @ nat @ X1 @ X2))))) )),
% 64.79/9.45 inference(trivial_inequality_removal,[],[f40941])).
% 64.79/9.45 thf(f51181,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p)) = ((plus_plus @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ one_one @ nat) @ X0))) | (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) )),
% 64.79/9.45 inference(constrained_superposition,[],[f1848,f38589])).
% 64.79/9.45 thf(f51451,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p)) = ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ X0)))) | (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) )),
% 64.79/9.45 inference(forward_demodulation,[],[f51181,f40966])).
% 64.79/9.45 thf(f51493,definition,(
% 64.79/9.45 spl129_133 <=> ! [X1 : nat] : (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1)),
% 64.79/9.45 introduced(definition,[new_symbols(definition,[spl129_133])],[avatar_definition])).
% 64.79/9.45 thf(f51494,plain,(
% 64.79/9.45 ( ! [X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1)) ) | ~spl129_133),
% 64.79/9.45 inference(avatar_component_clause,[],[f51493])).
% 64.79/9.45 thf(f51531,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p)) = ((plus_plus @ nat @ one_one @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ X0)))) | (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) )),
% 64.79/9.45 inference(forward_demodulation,[],[f51451,f40900])).
% 64.79/9.45 thf(f51535,definition,(
% 64.79/9.45 spl129_136 <=> ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1))),
% 64.79/9.45 introduced(definition,[new_symbols(definition,[spl129_136])],[avatar_definition])).
% 64.79/9.45 thf(f51536,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) ) | ~spl129_136),
% 64.79/9.45 inference(avatar_component_clause,[],[f51535])).
% 64.79/9.45 thf(f51581,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p)) != ((plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ (plus_plus @ nat @ one_one @ nat @ X0)))) | (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) ) | spl129_4),
% 64.79/9.45 inference(constrained_superposition,[],[f1857,f38589])).
% 64.79/9.45 thf(f51604,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p)) != ((plus_plus @ nat @ one_one @ nat @ (plus_plus @ nat @ (size_size @ list @ product_prod @ nat @ nat @ p1) @ X0)))) | (((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) ) | spl129_4),
% 64.79/9.45 inference(forward_demodulation,[],[f51581,f40900])).
% 64.79/9.45 thf(f51608,plain,(
% 64.79/9.45 ( ! [X0 : nat,X1 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p2)) != X1) | (X0 != X1)) ) | spl129_4),
% 64.79/9.45 inference(forward_subsumption_resolution,[],[f51604,f51531])).
% 64.79/9.45 thf(f51612,plain,(
% 64.79/9.45 spl129_136 | spl129_4),
% 64.79/9.45 inference(avatar_split_clause,[],[f51608,f1855,f51535])).
% 64.79/9.45 thf(f51617,plain,(
% 64.79/9.45 ( ! [X0 : nat] : ((((size_size @ list @ product_prod @ nat @ nat @ p2)) != X0)) ) | ~spl129_136),
% 64.79/9.45 inference(equality_resolution,[],[f51536])).
% 64.79/9.45 thf(f51618,plain,(
% 64.79/9.45 spl129_133 | ~spl129_136),
% 64.79/9.45 inference(avatar_split_clause,[],[f51617,f51535,f51493])).
% 64.79/9.45 thf(f51621,plain,(
% 64.79/9.45 $false | ~spl129_133),
% 64.79/9.45 inference(equality_resolution,[],[f51494])).
% 64.79/9.45 thf(f51622,plain,(
% 64.79/9.45 ~spl129_133),
% 64.79/9.45 inference(avatar_contradiction_clause,[],[f51621])).
% 64.79/9.45 cnf(s4, plain, ~spl129_4, inference(sat_conversion,[],[f1859])).
% 64.79/9.45 cnf(s449, plain, spl129_4 | spl129_136, inference(sat_conversion,[],[f51612])).
% 64.79/9.45 cnf(s451, plain, spl129_133 | ~spl129_136, inference(sat_conversion,[],[f51618])).
% 64.79/9.45 cnf(s452, plain, ~spl129_133, inference(sat_conversion,[],[f51622])).
% 64.79/9.45 cnf(s453, plain, ~spl129_136, inference(rat,[],[s451,s452])).
% 64.79/9.45 cnf(s454, plain, spl129_4, inference(rat,[],[s449,s453])).
% 64.79/9.45 cnf(s499, plain, $false, inference(rat,[],[s4,s454])).
% 64.79/9.45 thf(f51623,plain,(
% 64.79/9.45 $false),
% 64.79/9.45 inference(avatar_sat_refutation,[],[s499])).
% 64.79/9.45 % SZS output end Proof for theBenchmark
% 64.79/9.45 % (3316083)------------------------------
% 64.79/9.45 % (3316083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.79/9.45 % (3316083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.79/9.45 % (3316083)CaDiCaL version: 2.1.3
% 64.79/9.45 % (3316083)Termination reason: Refutation
% 64.79/9.45 % (3316083)Time elapsed: 4.149 s
% 64.79/9.45 % (3316083)Peak memory usage: 39 MB
% 64.79/9.45 % (3316083)Instructions burned: 8938 (million)
% 64.79/9.45 % (3315815)Success in time 9.172 s
% 64.79/9.45 % Vampire exiting
%------------------------------------------------------------------------------