%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO882^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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:50:30 AM UTC 2026
% Result : Unsatisfiable 2.83s 0.78s
% Output : Refutation 2.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO882^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n018.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 17:26:41 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.34 % (379490)Will run a generic schedule for satisfiability detection.
% 0.22/0.34 % (379496)% WARNING: option uhcvi not known.
% 0.22/0.34 % (379498)dis+10_1_sil=32000:sp=arity:random_seed=4039497841:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.22/0.34 % (379497)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1958067986:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.22/0.34 % (379495)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3735988908_2999 on theBenchmark for (2999ds/0Mi)
% 0.22/0.34 % (379496)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=262581020:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.22/0.34 % (379496)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.34 % (379496)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.22/0.34 % Exception at run slice level
% 0.22/0.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.34 % (379498)Refutation not found, incomplete strategy
% 0.22/0.34 % (379498)------------------------------
% 0.22/0.34 % (379498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.34 % (379498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.34 % (379498)CaDiCaL version: 2.1.3
% 0.22/0.34 % (379498)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.34 % (379498)Time elapsed: 0.002 s
% 0.22/0.34 % (379498)Peak memory usage: 11 MB
% 0.22/0.34 % (379498)Instructions burned: 1 (million)
% 0.22/0.34 % (379496)Refutation not found, incomplete strategy
% 0.22/0.34 % (379496)------------------------------
% 0.22/0.34 % (379496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.34 % (379496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.34 % (379496)CaDiCaL version: 2.1.3
% 0.22/0.34 % (379496)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.34 % (379496)Time elapsed: 0.002 s
% 0.22/0.34 % (379496)Peak memory usage: 12 MB
% 0.22/0.34 % (379496)Instructions burned: 1 (million)
% 0.22/0.34 % (379498)------------------------------
% 0.22/0.34 % (379498)------------------------------
% 0.22/0.34 % (379496)------------------------------
% 0.22/0.34 % (379496)------------------------------
% 0.22/0.34 % (379497)Refutation not found, incomplete strategy
% 0.22/0.34 % (379497)------------------------------
% 0.22/0.34 % (379497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.34 % (379497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.34 % (379497)CaDiCaL version: 2.1.3
% 0.22/0.34 % (379497)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.34 % (379497)Time elapsed: 0.003 s
% 0.22/0.34 % (379497)Peak memory usage: 12 MB
% 0.22/0.34 % (379497)Instructions burned: 2 (million)
% 0.22/0.34 % (379497)------------------------------
% 0.22/0.34 % (379497)------------------------------
% 0.22/0.34 % (379499)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1310073710:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.22/0.34 % (379499)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.34 % (379506)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2142440788:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.22/0.34 % Exception at run slice level
% 0.22/0.34 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.34 % (379499)Refutation not found, incomplete strategy
% 0.22/0.34 % (379499)------------------------------
% 0.22/0.34 % (379499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.34 % (379499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.34 % (379499)CaDiCaL version: 2.1.3
% 0.22/0.34 % (379499)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.34 % (379499)Time elapsed: 0.004 s
% 0.22/0.34 % (379499)Peak memory usage: 12 MB
% 0.22/0.34 % (379499)Instructions burned: 2 (million)
% 0.22/0.34 % (379507)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1239921000:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.34 % (379499)------------------------------
% 0.22/0.34 % (379499)------------------------------
% 0.22/0.34 % (379508)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=623464825:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.22/0.39 % (379509)ott-21_1_sil=16000:fs=off:random_seed=1899838938:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.22/0.39 % (379508)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.39 % (379507)Refutation not found, incomplete strategy
% 0.22/0.39 % (379507)------------------------------
% 0.22/0.39 % (379507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.39 % (379507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.39 % (379507)CaDiCaL version: 2.1.3
% 0.22/0.39 % (379507)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.39 % (379507)Time elapsed: 0.001 s
% 0.22/0.39 % (379507)Peak memory usage: 12 MB
% 0.22/0.39 % (379507)Instructions burned: 1 (million)
% 0.22/0.39 % (379508)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.22/0.39 % (379501)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=883020228:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.22/0.39 % (379507)------------------------------
% 0.22/0.39 % (379507)------------------------------
% 0.22/0.39 % (379500)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3333173189:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.39 % (379508)Refutation not found, incomplete strategy
% 0.22/0.39 % (379508)------------------------------
% 0.22/0.39 % (379508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.39 % (379508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.39 % (379508)CaDiCaL version: 2.1.3
% 0.22/0.39 % (379508)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.39 % (379508)Time elapsed: 0.002 s
% 0.22/0.39 % (379508)Peak memory usage: 13 MB
% 0.22/0.39 % (379508)Instructions burned: 1 (million)
% 0.22/0.39 % (379500)Refutation not found, incomplete strategy
% 0.22/0.39 % (379500)------------------------------
% 0.22/0.39 % (379500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.39 % (379500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.39 % (379500)CaDiCaL version: 2.1.3
% 0.22/0.39 % (379500)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.39 % (379500)Time elapsed: 0.001 s
% 0.22/0.39 % (379500)Peak memory usage: 12 MB
% 0.22/0.39 % (379500)Instructions burned: 1 (million)
% 0.22/0.39 % (379501)Refutation not found, incomplete strategy
% 0.22/0.39 % (379501)------------------------------
% 0.22/0.39 % (379501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.39 % (379501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.39 % (379501)CaDiCaL version: 2.1.3
% 0.22/0.39 % (379501)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.39 % (379501)Time elapsed: 0.001 s
% 0.22/0.39 % (379501)Peak memory usage: 12 MB
% 0.22/0.39 % (379508)------------------------------
% 0.22/0.39 % (379508)------------------------------
% 0.22/0.39 % (379501)Instructions burned: 1 (million)
% 0.22/0.39 % (379500)------------------------------
% 0.22/0.39 % (379500)------------------------------
% 0.22/0.39 % (379501)------------------------------
% 0.22/0.39 % (379501)------------------------------
% 0.22/0.39 % (379512)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4051703688:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.22/0.39 % (379519)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1925199743:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 0.22/0.39 % (379512)Refutation not found, incomplete strategy
% 0.22/0.39 % (379512)------------------------------
% 0.22/0.39 % (379512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.39 % (379512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.39 % (379512)CaDiCaL version: 2.1.3
% 0.22/0.39 % (379512)Termination reason: Refutation not found, incomplete strategy
% 0.22/0.39 % (379512)Time elapsed: 0.003 s
% 0.22/0.39 % (379512)Peak memory usage: 12 MB
% 0.22/0.39 % (379512)Instructions burned: 3 (million)
% 0.22/0.39 % (379512)------------------------------
% 0.22/0.39 % (379512)------------------------------
% 0.22/0.39 % (379519)Refutation not found, incomplete strategy
% 0.22/0.39 % (379519)------------------------------
% 0.22/0.39 % (379519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (379519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (379519)CaDiCaL version: 2.1.3
% 0.89/0.41 % (379519)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.41 % (379519)Time elapsed: 0.001 s
% 0.89/0.41 % (379519)Peak memory usage: 12 MB
% 0.89/0.41 % (379519)Instructions burned: 1 (million)
% 0.89/0.41 % (379520)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2194286743:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 0.89/0.41 % (379519)------------------------------
% 0.89/0.41 % (379519)------------------------------
% 0.89/0.41 % Exception at run slice level
% 0.89/0.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.41 % (379521)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=2075969758:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2999 on theBenchmark for (2999ds/692Mi)
% 0.89/0.41 % (379521)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.89/0.41 % (379516)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3791174283:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.89/0.41 % (379521)Refutation not found, incomplete strategy
% 0.89/0.41 % (379521)------------------------------
% 0.89/0.41 % (379521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (379521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (379521)CaDiCaL version: 2.1.3
% 0.89/0.41 % (379521)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.41 % (379521)Time elapsed: 0.003 s
% 0.89/0.41 % (379521)Peak memory usage: 12 MB
% 0.89/0.41 % (379521)Instructions burned: 3 (million)
% 0.89/0.41 % Exception at run slice level
% 0.89/0.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.41 % (379521)------------------------------
% 0.89/0.41 % (379521)------------------------------
% 0.89/0.41 % (379528)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2253452524:i=9515:nm=5_2999 on theBenchmark for (2999ds/9515Mi)
% 0.89/0.41 % Exception at run slice level
% 0.89/0.41 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.41 % (379531)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1847398197:i=5131_2999 on theBenchmark for (2999ds/5131Mi)
% 0.89/0.41 % (379531)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.89/0.41 % (379522)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3884748105:i=879:kws=inv_precedence:fsr=off_2999 on theBenchmark for (2999ds/879Mi)
% 0.89/0.41 % (379522)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.89/0.41 % (379532)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4037849629:i=1472:ins=7:fdi=8:gsp=on_2999 on theBenchmark for (2999ds/1472Mi)
% 0.89/0.41 % (379532)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.89/0.41 % (379531)Refutation not found, incomplete strategy
% 0.89/0.41 % (379531)------------------------------
% 0.89/0.41 % (379531)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (379531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (379532)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.89/0.41 % (379531)CaDiCaL version: 2.1.3
% 0.89/0.41 % (379531)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.41 % (379531)Time elapsed: 0.001 s
% 0.89/0.41 % (379531)Peak memory usage: 12 MB
% 0.89/0.41 % (379531)Instructions burned: 1 (million)
% 0.89/0.41 % (379531)------------------------------
% 0.89/0.41 % (379531)------------------------------
% 0.89/0.41 % (379522)Refutation not found, incomplete strategy
% 0.89/0.41 % (379522)------------------------------
% 0.89/0.41 % (379522)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.41 % (379522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.41 % (379522)CaDiCaL version: 2.1.3
% 0.89/0.41 % (379526)fmb+10_1_sil=64000:random_seed=1408284234:i=22061:nm=2:gsp=on_2999 on theBenchmark for (2999ds/22061Mi)
% 0.89/0.45 % (379522)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.45 % (379522)Time elapsed: 0.003 s
% 0.89/0.45 % (379522)Peak memory usage: 12 MB
% 0.89/0.45 % (379522)Instructions burned: 3 (million)
% 0.89/0.45 % (379526)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 0.89/0.45 % Exception at run slice level
% 0.89/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.45 % (379522)------------------------------
% 0.89/0.45 % (379522)------------------------------
% 0.89/0.45 % (379529)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=205934527:fmbsr=1.7:i=920_2999 on theBenchmark for (2999ds/920Mi)
% 0.89/0.45 % Exception at run slice level
% 0.89/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.45 % (379534)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3120586555:i=6324_2999 on theBenchmark for (2999ds/6324Mi)
% 0.89/0.45 % Exception at run slice level
% 0.89/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.45 % (379541)ott+10_1_sil=32000:tgt=ground:random_seed=1838361845:i=5114:av=off_2998 on theBenchmark for (2998ds/5114Mi)
% 0.89/0.45 % (379541)Refutation not found, incomplete strategy
% 0.89/0.45 % (379541)------------------------------
% 0.89/0.45 % (379541)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (379541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (379541)CaDiCaL version: 2.1.3
% 0.89/0.45 % (379541)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.45 % (379541)Time elapsed: 0.001 s
% 0.89/0.45 % (379541)Peak memory usage: 11 MB
% 0.89/0.45 % (379541)Instructions burned: 1 (million)
% 0.89/0.45 % (379541)------------------------------
% 0.89/0.45 % (379541)------------------------------
% 0.89/0.45 % (379538)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=369452540:fmbsr=2.30978:i=2174_2998 on theBenchmark for (2998ds/2174Mi)
% 0.89/0.45 % (379509)Instruction limit reached!
% 0.89/0.45 % (379509)------------------------------
% 0.89/0.45 % (379509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (379509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (379509)CaDiCaL version: 2.1.3
% 0.89/0.45 % (379509)Termination reason: Instruction limit
% 0.89/0.45 % (379509)Termination phase: Saturation
% 0.89/0.45 % (379509)Time elapsed: 0.078 s
% 0.89/0.45 % (379509)Peak memory usage: 13 MB
% 0.89/0.45 % (379509)Instructions burned: 181 (million)
% 0.89/0.45 % Exception at run slice level
% 0.89/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.45 % (379545)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2980900948:i=3512:aac=none_2998 on theBenchmark for (2998ds/3512Mi)
% 0.89/0.45 % (379545)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.89/0.45 % (379545)Refutation not found, incomplete strategy
% 0.89/0.45 % (379545)------------------------------
% 0.89/0.45 % (379545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.45 % (379545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.45 % (379545)CaDiCaL version: 2.1.3
% 0.89/0.45 % (379545)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.45 % (379545)Time elapsed: 0.001 s
% 0.89/0.45 % (379545)Peak memory usage: 12 MB
% 0.89/0.45 % (379545)Instructions burned: 1 (million)
% 0.89/0.45 % (379545)------------------------------
% 0.89/0.45 % (379545)------------------------------
% 0.89/0.45 % (379540)ott-2_1_sil=16000:newcnf=on:random_seed=474791081:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2998 on theBenchmark for (2998ds/869Mi)
% 0.89/0.45 % (379543)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=945583074:i=54282_2998 on theBenchmark for (2998ds/54282Mi)
% 0.89/0.45 % Exception at run slice level
% 0.89/0.45 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.45 % (379540)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.89/0.45 % (379547)dis+21_1_sil=32000:sas=cadical:random_seed=3208176643:i=3773:amm=off_2998 on theBenchmark for (2998ds/3773Mi)
% 0.89/0.45 % (379540)Refutation not found, incomplete strategy
% 0.89/0.45 % (379540)------------------------------
% 0.89/0.48 % (379540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.48 % (379547)Refutation not found, incomplete strategy
% 0.89/0.48 % (379547)------------------------------
% 0.89/0.48 % (379547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.48 % (379540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.48 % (379540)CaDiCaL version: 2.1.3
% 0.89/0.48 % (379540)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.48 % (379540)Time elapsed: 0.006 s
% 0.89/0.48 % (379547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.48 % (379540)Peak memory usage: 12 MB
% 0.89/0.48 % (379547)CaDiCaL version: 2.1.3
% 0.89/0.48 % (379540)Instructions burned: 1 (million)
% 0.89/0.48 % (379547)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.48 % (379547)Time elapsed: 0.001 s
% 0.89/0.48 % (379547)Peak memory usage: 12 MB
% 0.89/0.48 % (379547)Instructions burned: 1 (million)
% 0.89/0.48 % (379547)------------------------------
% 0.89/0.48 % (379547)------------------------------
% 0.89/0.48 % (379540)------------------------------
% 0.89/0.48 % (379540)------------------------------
% 0.89/0.48 % (379550)ott+11_1_sil=16000:gs=on:random_seed=292238626:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2998 on theBenchmark for (2998ds/2251Mi)
% 0.89/0.48 % (379550)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.89/0.48 % (379551)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1944522021:fmbsr=1.6:i=67534_2998 on theBenchmark for (2998ds/67534Mi)
% 0.89/0.48 % Exception at run slice level
% 0.89/0.48 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.48 % (379550)Refutation not found, incomplete strategy
% 0.89/0.48 % (379550)------------------------------
% 0.89/0.48 % (379550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.48 % (379550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.48 % (379550)CaDiCaL version: 2.1.3
% 0.89/0.48 % (379550)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.48 % (379550)Time elapsed: 0.001 s
% 0.89/0.48 % (379550)Peak memory usage: 12 MB
% 0.89/0.48 % (379550)Instructions burned: 1 (million)
% 0.89/0.48 % (379550)------------------------------
% 0.89/0.48 % (379550)------------------------------
% 0.89/0.48 % (379552)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3195408822:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2998 on theBenchmark for (2998ds/4591Mi)
% 0.89/0.48 % (379557)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3421156466:i=5211_2998 on theBenchmark for (2998ds/5211Mi)
% 0.89/0.48 % (379556)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3693975471:i=29340_2998 on theBenchmark for (2998ds/29340Mi)
% 0.89/0.48 % (379556)Refutation not found, incomplete strategy
% 0.89/0.48 % (379556)------------------------------
% 0.89/0.48 % (379556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.48 % (379556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.48 % (379556)CaDiCaL version: 2.1.3
% 0.89/0.48 % (379556)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.48 % (379556)Time elapsed: 0.001 s
% 0.89/0.48 % (379556)Peak memory usage: 12 MB
% 0.89/0.48 % (379556)Instructions burned: 1 (million)
% 0.89/0.48 % (379556)------------------------------
% 0.89/0.48 % (379556)------------------------------
% 0.89/0.48 % (379557)Refutation not found, incomplete strategy
% 0.89/0.48 % (379557)------------------------------
% 0.89/0.48 % (379557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.48 % (379557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.48 % (379557)CaDiCaL version: 2.1.3
% 0.89/0.48 % (379557)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.48 % (379557)Time elapsed: 0.003 s
% 0.89/0.48 % (379557)Peak memory usage: 12 MB
% 0.89/0.48 % (379557)Instructions burned: 2 (million)
% 0.89/0.48 % (379557)------------------------------
% 0.89/0.48 % (379557)------------------------------
% 0.89/0.48 % (379561)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=436153895:fmbsr=2:i=46332_2998 on theBenchmark for (2998ds/46332Mi)
% 0.89/0.48 % Exception at run slice level
% 0.89/0.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.52 % (379563)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=844796827:i=14071_2998 on theBenchmark for (2998ds/14071Mi)
% 0.89/0.52 % Exception at run slice level
% 0.89/0.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.52 % (379558)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3935821111:i=5497:nm=2_2998 on theBenchmark for (2998ds/5497Mi)
% 0.89/0.52 % Exception at run slice level
% 0.89/0.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.52 % (379566)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3240042350:i=22565:add=on:rawr=on_2998 on theBenchmark for (2998ds/22565Mi)
% 0.89/0.52 % (379567)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1576877525:i=8173:av=off_2998 on theBenchmark for (2998ds/8173Mi)
% 0.89/0.52 % (379567)Refutation not found, incomplete strategy
% 0.89/0.52 % (379567)------------------------------
% 0.89/0.52 % (379567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.52 % (379567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.52 % (379567)CaDiCaL version: 2.1.3
% 0.89/0.52 % (379567)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.52 % (379567)Time elapsed: 0.001 s
% 0.89/0.52 % (379567)Peak memory usage: 11 MB
% 0.89/0.52 % (379567)Instructions burned: 1 (million)
% 0.89/0.52 % (379567)------------------------------
% 0.89/0.52 % (379567)------------------------------
% 0.89/0.52 % (379566)Refutation not found, incomplete strategy
% 0.89/0.52 % (379566)------------------------------
% 0.89/0.52 % (379566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.52 % (379566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.52 % (379566)CaDiCaL version: 2.1.3
% 0.89/0.52 % (379566)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.52 % (379566)Time elapsed: 0.003 s
% 0.89/0.52 % (379566)Peak memory usage: 12 MB
% 0.89/0.52 % (379566)Instructions burned: 2 (million)
% 0.89/0.52 % (379570)dis+10_16:1_sil=16000:random_seed=130087888:i=9155:fsr=off_2998 on theBenchmark for (2998ds/9155Mi)
% 0.89/0.52 % (379566)------------------------------
% 0.89/0.52 % (379566)------------------------------
% 0.89/0.52 % (379571)ott-3_8_sil=64000:random_seed=4133744272:i=20139:bs=on_2998 on theBenchmark for (2998ds/20139Mi)
% 0.89/0.52 % (379570)Refutation not found, incomplete strategy
% 0.89/0.52 % (379570)------------------------------
% 0.89/0.52 % (379570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.52 % (379570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.52 % (379570)CaDiCaL version: 2.1.3
% 0.89/0.52 % (379570)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.52 % (379570)Time elapsed: 0.001 s
% 0.89/0.52 % (379570)Peak memory usage: 12 MB
% 0.89/0.52 % (379570)Instructions burned: 1 (million)
% 0.89/0.52 % (379571)Refutation not found, incomplete strategy
% 0.89/0.52 % (379571)------------------------------
% 0.89/0.52 % (379571)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.89/0.52 % (379571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.89/0.52 % (379571)CaDiCaL version: 2.1.3
% 0.89/0.52 % (379571)Termination reason: Refutation not found, incomplete strategy
% 0.89/0.52 % (379571)Time elapsed: 0.001 s
% 0.89/0.52 % (379571)Peak memory usage: 12 MB
% 0.89/0.52 % (379570)------------------------------
% 0.89/0.52 % (379570)------------------------------
% 0.89/0.52 % (379571)Instructions burned: 1 (million)
% 0.89/0.52 % (379571)------------------------------
% 0.89/0.52 % (379571)------------------------------
% 0.89/0.52 % (379573)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1219953074:fmbsr=2:i=32576_2998 on theBenchmark for (2998ds/32576Mi)
% 0.89/0.52 % Exception at run slice level
% 0.89/0.52 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.89/0.52 % (379579)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2479086626:i=14134_2998 on theBenchmark for (2998ds/14134Mi)
% 0.89/0.52 % (379580)dis+33_16_sil=32000:sac=on:random_seed=730928078:i=15851:nm=0_2998 on theBenchmark for (2998ds/15851Mi)
% 0.89/0.52 % (379579)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.73/0.55 % (379581)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1734437337:avsq=on:i=17627:add=on:amm=off_2998 on theBenchmark for (2998ds/17627Mi)
% 1.73/0.55 % (379579)Refutation not found, incomplete strategy
% 1.73/0.55 % (379579)------------------------------
% 1.73/0.55 % (379579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.55 % (379579)CaDiCaL version: 2.1.3
% 1.73/0.55 % (379579)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.55 % (379579)Time elapsed: 0.001 s
% 1.73/0.55 % (379579)Peak memory usage: 12 MB
% 1.73/0.55 % (379579)Instructions burned: 1 (million)
% 1.73/0.55 % (379580)Refutation not found, incomplete strategy
% 1.73/0.55 % (379580)------------------------------
% 1.73/0.55 % (379580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.55 % (379580)CaDiCaL version: 2.1.3
% 1.73/0.55 % (379580)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.55 % (379580)Time elapsed: 0.001 s
% 1.73/0.55 % (379580)Peak memory usage: 12 MB
% 1.73/0.55 % (379580)Instructions burned: 1 (million)
% 1.73/0.55 % (379579)------------------------------
% 1.73/0.55 % (379579)------------------------------
% 1.73/0.55 % (379580)------------------------------
% 1.73/0.55 % (379580)------------------------------
% 1.73/0.55 % (379581)Refutation not found, incomplete strategy
% 1.73/0.55 % (379581)------------------------------
% 1.73/0.55 % (379581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.55 % (379581)CaDiCaL version: 2.1.3
% 1.73/0.55 % (379581)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.55 % (379581)Time elapsed: 0.001 s
% 1.73/0.55 % (379581)Peak memory usage: 12 MB
% 1.73/0.55 % (379581)Instructions burned: 1 (million)
% 1.73/0.55 % (379581)------------------------------
% 1.73/0.55 % (379581)------------------------------
% 1.73/0.55 % (379578)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=928822507:i=11404_2998 on theBenchmark for (2998ds/11404Mi)
% 1.73/0.55 % (379578)Refutation not found, incomplete strategy
% 1.73/0.55 % (379578)------------------------------
% 1.73/0.55 % (379578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.55 % (379578)CaDiCaL version: 2.1.3
% 1.73/0.55 % (379578)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.55 % (379578)Time elapsed: 0.001 s
% 1.73/0.55 % (379578)Peak memory usage: 12 MB
% 1.73/0.55 % (379578)Instructions burned: 1 (million)
% 1.73/0.55 % (379578)------------------------------
% 1.73/0.55 % (379578)------------------------------
% 1.73/0.55 % (379588)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=624882029:i=28120:bs=on:fsr=off_2997 on theBenchmark for (2997ds/28120Mi)
% 1.73/0.55 % (379583)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=3978596697:s2a=on:i=53295_2997 on theBenchmark for (2997ds/53295Mi)
% 1.73/0.55 % (379589)fmb+10_1_sil=256000:fmbss=7:random_seed=2129074230:fmbsr=1.6:i=182295_2997 on theBenchmark for (2997ds/182295Mi)
% 1.73/0.55 % Exception at run slice level
% 1.73/0.55 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.55 % (379588)Refutation not found, incomplete strategy
% 1.73/0.55 % (379588)------------------------------
% 1.73/0.55 % (379588)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.55 % (379588)CaDiCaL version: 2.1.3
% 1.73/0.55 % (379588)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.55 % (379588)Time elapsed: 0.001 s
% 1.73/0.55 % (379588)Peak memory usage: 12 MB
% 1.73/0.55 % (379588)Instructions burned: 1 (million)
% 1.73/0.55 % (379588)------------------------------
% 1.73/0.55 % (379588)------------------------------
% 1.73/0.55 % (379583)Refutation not found, incomplete strategy
% 1.73/0.55 % (379583)------------------------------
% 1.73/0.55 % (379583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.55 % (379583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.61 % (379583)CaDiCaL version: 2.1.3
% 1.73/0.61 % (379583)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.61 % (379583)Time elapsed: 0.004 s
% 1.73/0.61 % (379583)Peak memory usage: 13 MB
% 1.73/0.61 % (379583)Instructions burned: 3 (million)
% 1.73/0.61 % (379583)------------------------------
% 1.73/0.61 % (379583)------------------------------
% 1.73/0.61 % (379591)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=298196413:i=44625:gsp=on_2997 on theBenchmark for (2997ds/44625Mi)
% 1.73/0.61 % (379591)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.73/0.61 % (379591)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379587)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1704150932:i=26857:ins=20_2997 on theBenchmark for (2997ds/26857Mi)
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379595)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1417066414:i=160505_2997 on theBenchmark for (2997ds/160505Mi)
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379596)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2064951591:fmbsr=1.3:i=225729_2997 on theBenchmark for (2997ds/225729Mi)
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379599)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=4260590042:rtra=on_2997 on theBenchmark for (2997ds/0Mi)
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379603)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2660956482:i=176048:add=on:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/176048Mi)
% 1.73/0.61 % (379605)dis+10_1_sil=32000:si=on:sp=arity:random_seed=254064353:i=206:fgj=on:rtra=on_2997 on theBenchmark for (2997ds/206Mi)
% 1.73/0.61 % (379597)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=759575382:fmbsr=2:i=185024:ins=7_2997 on theBenchmark for (2997ds/185024Mi)
% 1.73/0.61 % (379603)Refutation not found, incomplete strategy
% 1.73/0.61 % (379603)------------------------------
% 1.73/0.61 % (379603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.61 % (379603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.61 % (379603)CaDiCaL version: 2.1.3
% 1.73/0.61 % (379603)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.61 % (379603)Time elapsed: 0.003 s
% 1.73/0.61 % (379603)Peak memory usage: 12 MB
% 1.73/0.61 % (379603)Instructions burned: 3 (million)
% 1.73/0.61 % (379605)Refutation not found, incomplete strategy
% 1.73/0.61 % (379605)------------------------------
% 1.73/0.61 % (379605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.73/0.61 % (379605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.73/0.61 % (379605)CaDiCaL version: 2.1.3
% 1.73/0.61 % (379605)Termination reason: Refutation not found, incomplete strategy
% 1.73/0.61 % (379605)Time elapsed: 0.001 s
% 1.73/0.61 % (379605)Peak memory usage: 12 MB
% 1.73/0.61 % (379605)Instructions burned: 1 (million)
% 1.73/0.61 % Exception at run slice level
% 1.73/0.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.73/0.61 % (379603)------------------------------
% 1.73/0.61 % (379603)------------------------------
% 1.73/0.61 % (379605)------------------------------
% 1.73/0.61 % (379605)------------------------------
% 1.73/0.61 % (379601)% WARNING: option uhcvi not known.
% 1.73/0.61 % (379607)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3755130431:i=232:rtra=on_2997 on theBenchmark for (2997ds/232Mi)
% 1.73/0.61 % (379607)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.73/0.61 % (379607)Refutation not found, incomplete strategy
% 1.73/0.61 % (379607)------------------------------
% 1.73/0.61 % (379607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.66 % (379607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.66 % (379607)CaDiCaL version: 2.1.3
% 2.60/0.66 % (379607)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.66 % (379607)Time elapsed: 0.002 s
% 2.60/0.66 % (379607)Peak memory usage: 12 MB
% 2.60/0.66 % (379607)Instructions burned: 2 (million)
% 2.60/0.66 % (379607)------------------------------
% 2.60/0.66 % (379607)------------------------------
% 2.60/0.66 % (379601)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=769315014:i=271062:add=off:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/271062Mi)
% 2.60/0.66 % (379601)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.60/0.66 % (379601)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.60/0.66 % (379601)Refutation not found, incomplete strategy
% 2.60/0.66 % (379601)------------------------------
% 2.60/0.66 % (379601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.66 % (379601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.66 % (379601)CaDiCaL version: 2.1.3
% 2.60/0.66 % (379601)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.66 % (379601)Time elapsed: 0.001 s
% 2.60/0.66 % (379601)Peak memory usage: 12 MB
% 2.60/0.66 % (379601)Instructions burned: 1 (million)
% 2.60/0.66 % (379601)------------------------------
% 2.60/0.66 % (379601)------------------------------
% 2.60/0.66 % (379612)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=2294968183:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2997 on theBenchmark for (2997ds/318Mi)
% 2.60/0.66 % (379612)Refutation not found, incomplete strategy
% 2.60/0.66 % (379612)------------------------------
% 2.60/0.66 % (379612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.66 % (379612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.66 % (379612)CaDiCaL version: 2.1.3
% 2.60/0.66 % (379612)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.66 % (379612)Time elapsed: 0.001 s
% 2.60/0.66 % (379612)Peak memory usage: 12 MB
% 2.60/0.66 % (379612)Instructions burned: 1 (million)
% 2.60/0.66 % (379612)------------------------------
% 2.60/0.66 % (379612)------------------------------
% 2.60/0.66 % (379615)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=2034854567:i=262:bd=preordered:rtra=on:fsd=on_2997 on theBenchmark for (2997ds/262Mi)
% 2.60/0.66 % (379615)Refutation not found, incomplete strategy
% 2.60/0.66 % (379615)------------------------------
% 2.60/0.66 % (379615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.66 % (379615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.66 % (379615)CaDiCaL version: 2.1.3
% 2.60/0.66 % (379615)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.66 % (379615)Time elapsed: 0.001 s
% 2.60/0.66 % (379615)Peak memory usage: 12 MB
% 2.60/0.66 % (379615)Instructions burned: 1 (million)
% 2.60/0.66 % (379615)------------------------------
% 2.60/0.66 % (379615)------------------------------
% 2.60/0.66 % (379617)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1862038617:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/1368Mi)
% 2.60/0.66 % (379617)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.60/0.66 % (379617)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.60/0.66 % (379617)Refutation not found, incomplete strategy
% 2.60/0.66 % (379617)------------------------------
% 2.60/0.66 % (379617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.60/0.66 % (379617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.60/0.66 % (379617)CaDiCaL version: 2.1.3
% 2.60/0.66 % (379617)Termination reason: Refutation not found, incomplete strategy
% 2.60/0.66 % (379617)Time elapsed: 0.001 s
% 2.60/0.66 % (379617)Peak memory usage: 12 MB
% 2.60/0.66 % (379617)Instructions burned: 1 (million)
% 2.60/0.66 % (379617)------------------------------
% 2.60/0.66 % (379617)------------------------------
% 2.60/0.66 % (379611)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=1246782247:i=262:rtra=on_2997 on theBenchmark for (2997ds/262Mi)
% 2.60/0.66 % (379613)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=939311454:i=1428:nm=2:rtra=on_2997 on theBenchmark for (2997ds/1428Mi)
% 2.83/0.71 % Exception at run slice level
% 2.83/0.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.71 % (379611)Refutation not found, incomplete strategy
% 2.83/0.71 % (379611)------------------------------
% 2.83/0.71 % (379611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.71 % (379611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.71 % (379611)CaDiCaL version: 2.1.3
% 2.83/0.71 % (379611)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.71 % (379611)Time elapsed: 0.002 s
% 2.83/0.71 % (379611)Peak memory usage: 11 MB
% 2.83/0.71 % (379611)Instructions burned: 1 (million)
% 2.83/0.71 % (379611)------------------------------
% 2.83/0.71 % (379611)------------------------------
% 2.83/0.71 % (379619)ott-21_1_sil=16000:si=on:fs=off:random_seed=435723021:i=360:av=off:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/360Mi)
% 2.83/0.71 % (379621)dis+10_4_sil=64000:si=on:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=773755856:i=954:bd=all:rtra=on_2996 on theBenchmark for (2996ds/954Mi)
% 2.83/0.71 % (379621)Refutation not found, incomplete strategy
% 2.83/0.71 % (379621)------------------------------
% 2.83/0.71 % (379621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.71 % (379621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.71 % (379621)CaDiCaL version: 2.1.3
% 2.83/0.71 % (379621)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.71 % (379621)Time elapsed: 0.003 s
% 2.83/0.71 % (379621)Peak memory usage: 12 MB
% 2.83/0.71 % (379621)Instructions burned: 3 (million)
% 2.83/0.71 % (379621)------------------------------
% 2.83/0.71 % (379621)------------------------------
% 2.83/0.71 % (379623)fmb+10_1_sil=64000:si=on:erd=off:updr=off:random_seed=190166884:fmbsr=1.3:i=1730:ins=25:rtra=on_2996 on theBenchmark for (2996ds/1730Mi)
% 2.83/0.71 % Exception at run slice level
% 2.83/0.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.71 % (379626)ott+10_1_to=lpo:sil=64000:tgt=full:si=on:sp=arity:spb=goal_then_units:random_seed=3629464631:i=2358:rtra=on_2996 on theBenchmark for (2996ds/2358Mi)
% 2.83/0.71 % (379627)fmb+10_1_sil=64000:si=on:erd=off:fmbss=14:random_seed=4075142157:i=1778:ins=1:rtra=on_2996 on theBenchmark for (2996ds/1778Mi)
% 2.83/0.71 % Exception at run slice level
% 2.83/0.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.71 % (379626)Refutation not found, incomplete strategy
% 2.83/0.71 % (379626)------------------------------
% 2.83/0.71 % (379626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.71 % (379626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.71 % (379626)CaDiCaL version: 2.1.3
% 2.83/0.71 % (379626)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.71 % (379626)Time elapsed: 0.004 s
% 2.83/0.71 % (379626)Peak memory usage: 12 MB
% 2.83/0.71 % (379626)Instructions burned: 1 (million)
% 2.83/0.71 % (379626)------------------------------
% 2.83/0.71 % (379626)------------------------------
% 2.83/0.71 % (379630)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:si=on:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=568677448:avsq=on:s2a=on:i=1384:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/1384Mi)
% 2.83/0.71 % (379630)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.83/0.71 % (379630)Refutation not found, incomplete strategy
% 2.83/0.71 % (379630)------------------------------
% 2.83/0.71 % (379630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.71 % (379630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.71 % (379630)CaDiCaL version: 2.1.3
% 2.83/0.71 % (379630)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.71 % (379630)Time elapsed: 0.001 s
% 2.83/0.71 % (379630)Peak memory usage: 12 MB
% 2.83/0.71 % (379630)Instructions burned: 1 (million)
% 2.83/0.71 % (379630)------------------------------
% 2.83/0.71 % (379630)------------------------------
% 2.83/0.71 % (379632)dis-10_1_anc=none:sil=64000:si=on:spb=goal:newcnf=on:cn=on:random_seed=4002801717:i=1758:kws=inv_precedence:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/1758Mi)
% 2.83/0.78 % (379632)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.83/0.78 % (379632)Refutation not found, incomplete strategy
% 2.83/0.78 % (379632)------------------------------
% 2.83/0.78 % (379632)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379632)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379632)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379632)Time elapsed: 0.002 s
% 2.83/0.78 % (379632)Peak memory usage: 12 MB
% 2.83/0.78 % (379632)Instructions burned: 3 (million)
% 2.83/0.78 % (379632)------------------------------
% 2.83/0.78 % (379632)------------------------------
% 2.83/0.78 % (379636)fmb+10_1_sil=16000:sas=cadical:si=on:fmbss=20:random_seed=2607688679:i=19030:nm=5:rtra=on_2996 on theBenchmark for (2996ds/19030Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379635)fmb+10_1_sil=64000:si=on:random_seed=437785678:i=44122:nm=2:rtra=on:gsp=on_2996 on theBenchmark for (2996ds/44122Mi)
% 2.83/0.78 % (379635)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379638)fmb+10_1_sil=64000:sas=cadical:si=on:fmbss=8:random_seed=1465663472:fmbsr=1.7:i=1840:rtra=on_2996 on theBenchmark for (2996ds/1840Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379642)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:si=on:sp=arity:spb=units:lsd=10:nwc=3:random_seed=402668571:i=2944:ins=7:rtra=on:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/2944Mi)
% 2.83/0.78 % (379642)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 2.83/0.78 % (379642)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.83/0.78 % (379644)fmb+10_1_sil=16000:sas=cadical:si=on:bce=on:fmbss=77:random_seed=4134131864:i=12648:rtra=on_2996 on theBenchmark for (2996ds/12648Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379640)dis-4_1_sil=16000:drc=ordering:si=on:sp=const_frequency:sac=on:newcnf=on:random_seed=3905909067:i=10262:rtra=on_2996 on theBenchmark for (2996ds/10262Mi)
% 2.83/0.78 % (379640)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.83/0.78 % (379646)fmb+10_1_fmbas=function:sil=32000:sas=cadical:si=on:fmbss=16:random_seed=1230784454:fmbsr=2.30978:i=4348:rtra=on_2996 on theBenchmark for (2996ds/4348Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379640)Refutation not found, incomplete strategy
% 2.83/0.78 % (379640)------------------------------
% 2.83/0.78 % (379640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379640)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379640)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379640)Time elapsed: 0.002 s
% 2.83/0.78 % (379640)Peak memory usage: 12 MB
% 2.83/0.78 % (379640)Instructions burned: 1 (million)
% 2.83/0.78 % (379640)------------------------------
% 2.83/0.78 % (379640)------------------------------
% 2.83/0.78 % (379650)ott-2_1_sil=16000:si=on:newcnf=on:random_seed=780543913:avsq=on:i=1738:avsqr=1,16:kws=inv_arity_squared:rtra=on_2995 on theBenchmark for (2995ds/1738Mi)
% 2.83/0.78 % (379650)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 2.83/0.78 % (379652)ott+10_1_sil=32000:tgt=ground:si=on:random_seed=1975207513:i=10228:av=off:rtra=on_2995 on theBenchmark for (2995ds/10228Mi)
% 2.83/0.78 % (379650)Refutation not found, incomplete strategy
% 2.83/0.78 % (379650)------------------------------
% 2.83/0.78 % (379650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379650)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379650)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379650)Time elapsed: 0.001 s
% 2.83/0.78 % (379650)Peak memory usage: 12 MB
% 2.83/0.78 % (379650)Instructions burned: 1 (million)
% 2.83/0.78 % (379650)------------------------------
% 2.83/0.78 % (379650)------------------------------
% 2.83/0.78 % (379652)Refutation not found, incomplete strategy
% 2.83/0.78 % (379652)------------------------------
% 2.83/0.78 % (379652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379652)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379652)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379652)Time elapsed: 0.001 s
% 2.83/0.78 % (379652)Peak memory usage: 11 MB
% 2.83/0.78 % (379652)Instructions burned: 1 (million)
% 2.83/0.78 % (379653)fmb+10_1_sil=64000:sas=cadical:si=on:bce=on:rp=on:random_seed=223434294:i=108564:rtra=on_2995 on theBenchmark for (2995ds/108564Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379652)------------------------------
% 2.83/0.78 % (379652)------------------------------
% 2.83/0.78 % (379657)dis-11_1_sil=16000:si=on:sp=reverse_frequency:alpa=true:random_seed=995445911:i=7024:aac=none:rtra=on_2995 on theBenchmark for (2995ds/7024Mi)
% 2.83/0.78 % (379657)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.83/0.78 % (379657)Refutation not found, incomplete strategy
% 2.83/0.78 % (379657)------------------------------
% 2.83/0.78 % (379657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379657)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379657)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379657)Time elapsed: 0.001 s
% 2.83/0.78 % (379657)Peak memory usage: 12 MB
% 2.83/0.78 % (379657)Instructions burned: 1 (million)
% 2.83/0.78 % (379657)------------------------------
% 2.83/0.78 % (379657)------------------------------
% 2.83/0.78 % (379658)dis+21_1_sil=32000:sas=cadical:si=on:random_seed=3630229255:i=7546:rtra=on:amm=off_2995 on theBenchmark for (2995ds/7546Mi)
% 2.83/0.78 % (379658)Refutation not found, incomplete strategy
% 2.83/0.78 % (379658)------------------------------
% 2.83/0.78 % (379658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379658)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379658)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379658)Time elapsed: 0.001 s
% 2.83/0.78 % (379658)Peak memory usage: 12 MB
% 2.83/0.78 % (379658)Instructions burned: 1 (million)
% 2.83/0.78 % (379659)ott+11_1_sil=16000:si=on:gs=on:random_seed=2594093528:s2a=on:i=4502:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:rtra=on:fsd=on_2995 on theBenchmark for (2995ds/4502Mi)
% 2.83/0.78 % (379658)------------------------------
% 2.83/0.78 % (379658)------------------------------
% 2.83/0.78 % (379659)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 2.83/0.78 % (379659)Refutation not found, incomplete strategy
% 2.83/0.78 % (379659)------------------------------
% 2.83/0.78 % (379659)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379659)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379659)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379659)Time elapsed: 0.003 s
% 2.83/0.78 % (379659)Peak memory usage: 12 MB
% 2.83/0.78 % (379659)Instructions burned: 1 (million)
% 2.83/0.78 % (379659)------------------------------
% 2.83/0.78 % (379659)------------------------------
% 2.83/0.78 % (379661)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:si=on:fmbss=7:random_seed=2702143830:fmbsr=1.6:i=135068:rtra=on_2995 on theBenchmark for (2995ds/135068Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379619)Instruction limit reached!
% 2.83/0.78 % (379619)------------------------------
% 2.83/0.78 % (379619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379619)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379619)Termination reason: Instruction limit
% 2.83/0.78 % (379619)Termination phase: Saturation
% 2.83/0.78 % (379619)Time elapsed: 0.156 s
% 2.83/0.78 % (379619)Peak memory usage: 15 MB
% 2.83/0.78 % (379619)Instructions burned: 362 (million)
% 2.83/0.78 % (379668)fmb+10_1_sil=32000:sas=cadical:si=on:bce=on:fmbss=17:random_seed=685779354:i=10994:nm=2:rtra=on_2995 on theBenchmark for (2995ds/10994Mi)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379664)ott-22_32_sil=16000:tgt=full:si=on:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2756340317:avsq=on:i=9182:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:rtra=on:fdi=4_2995 on theBenchmark for (2995ds/9182Mi)
% 2.83/0.78 % (379666)dis+10_64_to=lpo:sil=32000:si=on:spb=intro:urr=on:sac=on:random_seed=777262298:i=58680:rtra=on_2995 on theBenchmark for (2995ds/58680Mi)
% 2.83/0.78 % (379667)dis-10_1_sil=64000:sas=cadical:si=on:cn=on:random_seed=3335762238:i=10422:rtra=on_2995 on theBenchmark for (2995ds/10422Mi)
% 2.83/0.78 % (379666)Refutation not found, incomplete strategy
% 2.83/0.78 % (379666)------------------------------
% 2.83/0.78 % (379666)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379666)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379666)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379666)Time elapsed: 0.004 s
% 2.83/0.78 % (379666)Peak memory usage: 12 MB
% 2.83/0.78 % (379666)Instructions burned: 1 (million)
% 2.83/0.78 % (379666)------------------------------
% 2.83/0.78 % (379666)------------------------------
% 2.83/0.78 % (379670)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:si=on:fmbss=15:random_seed=2775344792:fmbsr=2:i=92664:rtra=on_2995 on theBenchmark for (2995ds/92664Mi)
% 2.83/0.78 % (379667)Refutation not found, incomplete strategy
% 2.83/0.78 % (379667)------------------------------
% 2.83/0.78 % (379667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379667)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379667)Termination reason: Refutation not found, incomplete strategy
% 2.83/0.78 % (379667)Time elapsed: 0.005 s
% 2.83/0.78 % (379667)Peak memory usage: 12 MB
% 2.83/0.78 % (379667)Instructions burned: 2 (million)
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379667)------------------------------
% 2.83/0.78 % (379667)------------------------------
% 2.83/0.78 % (379674)fmb+10_1_sil=128000:tgt=full:sas=cadical:si=on:fmbss=12:random_seed=898759797:i=28142:rtra=on_2994 on theBenchmark for (2994ds/28142Mi)
% 2.83/0.78 % (379532) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-379490-379532"...
% 2.83/0.78 % Exception at run slice level
% 2.83/0.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 2.83/0.78 % (379532)...printing done.
% 2.83/0.78 % (379532)Refutation found. Thanks to Tanya!
% 2.83/0.78 % SZS status Unsatisfiable for theBenchmark
% 2.83/0.78 % SZS output start Proof for theBenchmark
% 2.83/0.78 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 2.83/0.78 thf(func_def_0, type, h: ($i > $i)).
% 2.83/0.78 thf(func_def_1, type, g: ($o > $i)).
% 2.83/0.78 thf(func_def_7, type, sP0: ($i > $o)).
% 2.83/0.78 thf(func_def_8, type, sP1: ($i > $o)).
% 2.83/0.78 thf(func_def_9, type, vNOT: ($o > $o)).
% 2.83/0.78 thf(func_def_10, type, sF2: !>[X0: $tType, X1: $tType]:((X1 > (X1 > $i) > ($i > X0) > X0))).
% 2.83/0.78 thf(func_def_11, type, sF3: !>[X0: $tType]:((X0 > (X0 > $i) > $i))).
% 2.83/0.78 thf(func_def_12, type, sF4: !>[X0: $tType]:(((X0 > $i) > ($i > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_13, type, sF5: !>[X0: $tType]:(($i > ($i > X0) > X0))).
% 2.83/0.78 thf(func_def_14, type, sF6: (($i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_15, type, sF7: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2) > X0 > X1 > X2))).
% 2.83/0.78 thf(func_def_16, type, sF8: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((X2 > X4 > (X0 > X1) > (X4 > (X0 > X1) > X2 > X3) > X3))).
% 2.83/0.78 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 2.83/0.78 thf(func_def_18, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 2.83/0.78 thf(func_def_19, type, sF9: !>[X0: $tType]:((($i > $i) > ($i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_20, type, sF10: !>[X0: $tType]:((($i > X0) > X0))).
% 2.83/0.78 thf(func_def_21, type, sF11: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > (X2 > $i) > X0 > ($i > X1) > X1))).
% 2.83/0.78 thf(func_def_22, type, sF12: !>[X0: $tType, X1: $tType]:(($i > ($i > X0) > (X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_23, type, sF13: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > X1 > (X2 > X3) > X3) > (X2 > X3) > X1 > X3))).
% 2.83/0.78 thf(func_def_24, type, sF14: !>[X0: $tType, X1: $tType]:((((X0 > X1) > X1) > (X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_25, type, sF15: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X0) > ((X1 > X0) > X2 > X3) > X2 > X3))).
% 2.83/0.78 thf(func_def_26, type, sF16: !>[X0: $tType, X1: $tType]:((X0 > $i > ($i > X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_27, type, sF17: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > X1 > X2 > X3) > X2 > X1 > X3))).
% 2.83/0.78 thf(func_def_28, type, sF18: !>[X0: $tType, X1: $tType]:((X1 > (X1 > X0) > (X0 > $i) > $i))).
% 2.83/0.78 thf(func_def_29, type, sF19: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > X1 > X2) > X1 > X2) > (X0 > X1 > X2) > X1 > X2))).
% 2.83/0.78 thf(func_def_30, type, sF20: (($i > $i) > ($i > $i) > ($i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_31, type, sF21: !>[X0: $tType]:(($i > ($i > $i) > ($i > $i) > ($i > X0) > X0))).
% 2.83/0.78 thf(func_def_32, type, sF22: (($i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_33, type, sF23: !>[X0: $tType]:((($i > X0) > (($i > X0) > X0) > X0))).
% 2.83/0.78 thf(func_def_34, type, sF24: ($i > ($i > $i) > ($i > $i) > $i)).
% 2.83/0.78 thf(func_def_35, type, sF25: !>[X0: $tType]:((($i > X0) > X0))).
% 2.83/0.78 thf(func_def_36, type, sF26: !>[X0: $tType, X1: $tType]:((X0 > X1 > (X1 > X0 > $i) > $i))).
% 2.83/0.78 thf(func_def_37, type, sF27: !>[X0: $tType]:((X0 > (X0 > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_38, type, sF28: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ((X0 > X2) > X1) > X1))).
% 2.83/0.78 thf(func_def_39, type, sF29: !>[X0: $tType, X1: $tType]:((X0 > ($i > X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_40, type, sF30: !>[X0: $tType]:(((X0 > $i) > ($i > $i) > X0 > $i))).
% 2.83/0.78 thf(func_def_41, type, sF31: !>[X0: $tType, X1: $tType]:(($i > ($i > X0) > ($i > X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_42, type, sF32: !>[X0: $tType, X1: $tType]:((($i > X0 > X1) > X0 > X1))).
% 2.83/0.78 thf(func_def_43, type, sF33: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (X0 > X2 > X1) > X2 > X1))).
% 2.83/0.78 thf(func_def_44, type, sF34: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > ($i > X2 > X1) > X0 > (X1 > $i) > $i))).
% 2.83/0.78 thf(func_def_45, type, sF35: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2) > (X1 > X0) > X1 > X2))).
% 2.83/0.78 thf(func_def_46, type, sF36: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((X2 > (X1 > X4) > X0 > ((X1 > X4) > X0 > X2 > X3) > X3))).
% 2.83/0.78 thf(func_def_47, type, db1: !>[X0: $tType]:(X0)).
% 2.83/0.78 thf(func_def_49, type, sF38: ($o > $i > $i)).
% 2.83/0.78 thf(func_def_50, type, sF39: !>[X0: $tType, X1: $tType, X2: $tType]:((((X2 > X1) > X0 > $i) > ($i > X2 > X1) > ($i > X0) > $i > $i))).
% 2.83/0.78 thf(func_def_51, type, sF40: !>[X0: $tType, X1: $tType]:(((X1 > (X1 > X0 > $i) > X0 > $i) > ($i > X1) > ($i > X1 > X0 > $i) > ($i > X0) > $i > $i))).
% 2.83/0.78 thf(func_def_52, type, sF41: !>[X0: $tType, X1: $tType, X2: $tType]:((((X2 > X1) > (X0 > $i) > $i) > ($i > X2 > X1) > ($i > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_53, type, sF42: !>[X0: $tType]:((($i > X0 > $i) > X0 > $i))).
% 2.83/0.78 thf(func_def_54, type, sF43: !>[X0: $tType]:((($i > X0) > ($i > $i > X0 > $i) > (($i > X0 > $i) > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_55, type, sF44: !>[X0: $tType]:((($i > $i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_56, type, sF45: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $i) > ($i > X0) > ($i > X1) > $i > $i))).
% 2.83/0.78 thf(func_def_57, type, sF46: !>[X0: $tType]:((($i > X0) > ($i > $i > $i) > (($i > $i) > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_58, type, sF47: ((($i > $i) > $i) > ($i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_59, type, sF48: !>[X0: $tType]:((($i > $i > $i) > ($i > X0) > (X0 > ($i > $i) > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_60, type, sF49: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > X2) > (X0 > X2 > X1 > $i) > ($i > X0) > ($i > X1) > $i > $i))).
% 2.83/0.78 thf(func_def_61, type, sF50: !>[X0: $tType, X1: $tType]:(((X1 > (X1 > X0) > (X0 > $i) > $i) > ($i > X1) > ($i > X1 > X0) > ($i > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_62, type, sF51: !>[X0: $tType]:((($i > $i) > ($i > $i > X0) > (($i > X0) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_63, type, sF52: !>[X0: $tType, X1: $tType]:((($i > $i > X0 > X1) > X0 > X1))).
% 2.83/0.78 thf(func_def_64, type, sF53: !>[X0: $tType, X1: $tType, X2: $tType]:((((X2 > X1) > X0 > $i) > ($i > $i > X2 > X1) > ($i > $i > X0) > $i > $i))).
% 2.83/0.78 thf(func_def_65, type, sF54: !>[X0: $tType]:((($i > $i > X0) > X0))).
% 2.83/0.78 thf(func_def_66, type, sF55: !>[X0: $tType, X1: $tType]:(((X1 > (X1 > X0 > $i) > X0 > $i) > ($i > $i > X1) > ($i > $i > X1 > X0 > $i) > ($i > $i > X0) > $i > $i))).
% 2.83/0.78 thf(func_def_67, type, sF56: !>[X0: $tType, X1: $tType, X2: $tType]:((((X2 > X1) > (X0 > $i) > $i) > ($i > $i > X2 > X1) > ($i > $i > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_68, type, sF57: !>[X0: $tType]:((($i > $i > X0) > ($i > $i > $i > X0 > $i) > (($i > X0 > $i) > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_69, type, sF58: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $i) > ($i > $i > X0) > ($i > $i > X1) > $i > $i))).
% 2.83/0.78 thf(func_def_70, type, sF59: (($i > $i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_71, type, sF60: !>[X0: $tType]:((($i > $i > X0) > ($i > $i > $i > $i) > (($i > $i) > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_72, type, sF61: ((($i > $i) > $i) > ($i > $i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_73, type, sF62: !>[X0: $tType]:((($i > $i > $i > $i) > ($i > $i > X0) > (X0 > ($i > $i) > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_74, type, sF63: (($i > $i) > $i)).
% 2.83/0.78 thf(func_def_75, type, sF64: !>[X0: $tType]:((($i > $i > X0 > $i) > X0 > $i))).
% 2.83/0.78 thf(func_def_76, type, sF65: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > $i > X2) > (X0 > X2 > X1 > $i) > ($i > $i > X0) > ($i > $i > X1) > $i > $i))).
% 2.83/0.78 thf(func_def_77, type, sF66: !>[X0: $tType, X1: $tType]:(((X1 > (X1 > X0) > (X0 > $i) > $i) > ($i > $i > X1) > ($i > $i > X1 > X0) > ($i > $i > X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_78, type, sF67: !>[X0: $tType]:((($i > $i > $i) > ($i > $i > $i > X0) > (($i > X0) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_79, type, sK68: (($i > $i) > $i)).
% 2.83/0.78 thf(func_def_80, type, sF69: !>[X0: $tType]:((($i > $i > X0) > (X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_81, type, sF70: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $i > X1) > (($i > $i > X1) > ($i > $i > X1 > X0) > (X2 > $i > X3) > $i > $i) > (X2 > $i > X3) > ($i > $i > X1 > X0) > $i > $i))).
% 2.83/0.78 thf(func_def_82, type, sF71: !>[X0: $tType, X1: $tType]:(((($i > $i > X0) > X1 > $i) > ($i > $i > X0) > X1 > $i))).
% 2.83/0.78 thf(func_def_83, type, sF72: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X2 > X0) > ((X2 > X0) > (X1 > X3 > X2) > $i > $i) > (X1 > X3 > X2) > $i > $i))).
% 2.83/0.78 thf(func_def_84, type, sF73: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((X2 > X3 > X0) > (X0 > X4 > X3) > ($i > $i > X1) > ((X0 > X4 > X3) > ($i > $i > X1) > (X2 > X3 > X0) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_85, type, sF74: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((($i > $i > X3 > X0) > ((X1 > X4 > X5) > ($i > $i > X3 > X0) > ($i > $i > X2) > $i > $i) > ($i > $i > X2) > (X1 > X4 > X5) > $i > $i))).
% 2.83/0.78 thf(func_def_86, type, sF75: !>[X0: $tType, X1: $tType]:(((($i > $i > X0) > X1) > ($i > $i > X0) > X1))).
% 2.83/0.78 thf(func_def_87, type, sF76: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X1 > $i > X3) > X2 > X0) > (X1 > $i > X3) > X2 > X0))).
% 2.83/0.78 thf(func_def_88, type, sF77: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((($i > X2) > (X0 > X1) > ((X4 > X5) > (X0 > X1) > ($i > X3) > ($i > X2) > $i > $i) > ($i > X3) > (X4 > X5) > $i > $i))).
% 2.83/0.78 thf(func_def_89, type, sF78: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > X1) > (X1 > X2 > $i) > $i > $i) > (X0 > X1) > (X1 > X2 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_90, type, sF79: !>[X0: $tType]:((($i > X0) > (X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_91, type, sF80: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((X2 > X3) > (X1 > X4) > ($i > X0) > ((X1 > X4) > ($i > X0) > (X2 > X3) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_92, type, sF81: !>[X0: $tType, X1: $tType]:(((X0 > $i > X1) > X0 > $i > X1))).
% 2.83/0.78 thf(func_def_93, type, sF82: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2 > $i) > ((X0 > X2 > $i) > X1 > $i) > X1 > $i))).
% 2.83/0.78 thf(func_def_94, type, sF83: !>[X0: $tType, X1: $tType]:(((X0 > X1 > $i) > X0 > X1 > $i))).
% 2.83/0.78 thf(func_def_95, type, sF84: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((($i > X2) > (X1 > X4) > ($i > X3 > X0) > ((X1 > X4) > ($i > X3 > X0) > ($i > X2) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_96, type, sF85: !>[X0: $tType]:((X0 > (X0 > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_97, type, sF86: !>[X0: $tType]:(($o > ($o > X0) > X0))).
% 2.83/0.78 thf(func_def_98, type, sF87: ((($i > $i > $i > $i) > $i > $i) > ($i > $i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_99, type, sF88: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > (X0 > X2) > X1) > X0 > (X0 > X2) > X1))).
% 2.83/0.78 thf(func_def_100, type, sF89: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((($i > X0 > X1) > ((X4 > X5) > ($i > X0 > X1) > (X2 > X3) > $i > $i) > (X2 > X3) > (X4 > X5) > $i > $i))).
% 2.83/0.78 thf(func_def_101, type, sF90: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > X1) > (X1 > X2) > $i > $i) > (X0 > X1) > (X1 > X2) > $i > $i))).
% 2.83/0.78 thf(func_def_102, type, sF91: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X0) > ((X1 > X0) > (X2 > X3) > $i > $i) > (X2 > X3) > $i > $i))).
% 2.83/0.78 thf(func_def_103, type, sF92: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3) > ((X4 > X5) > (X2 > X3) > X0 > X1) > (X4 > X5) > X0 > X1))).
% 2.83/0.78 thf(func_def_104, type, sF93: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > $i > X2) > ((X0 > $i > X2) > X1) > X1))).
% 2.83/0.78 thf(func_def_105, type, sF94: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X1 > X3 > X2) > X0) > (X1 > X3 > X2) > X0))).
% 2.83/0.78 thf(func_def_106, type, sF95: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((X2 > X3 > X0) > (X5 > X6 > X4) > ($i > $i > X1) > ((X5 > X6 > X4) > ($i > $i > X1) > (X2 > X3 > X0) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_107, type, sF96: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((X2 > X3 > X0) > (X0 > X4) > (X1 > X5 > X6) > ((X0 > X4) > (X1 > X5 > X6) > (X2 > X3 > X0) > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_108, type, sF97: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3 > X0) > ((X4 > X5) > (X2 > X3 > X0) > X1 > $i) > (X4 > X5) > X1 > $i))).
% 2.83/0.78 thf(func_def_109, type, sF98: !>[X0: $tType, X1: $tType, X2: $tType]:(((($i > $i > X0) > (X1 > X2) > $i > $i) > ($i > $i > X0) > (X1 > X2) > $i > $i))).
% 2.83/0.78 thf(func_def_110, type, sF99: !>[X0: $tType, X1: $tType]:((((X0 > X1) > $i > $i) > (X0 > X1) > $i > $i))).
% 2.83/0.78 thf(func_def_111, type, sF100: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3) > ((X1 > X4 > X5) > (X2 > X3) > X0 > $i) > (X1 > X4 > X5) > X0 > $i))).
% 2.83/0.78 thf(func_def_112, type, sF101: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType]:(((X1 > X6 > X7) > (X2 > X3 > X0) > ((X4 > X5) > (X1 > X6 > X7) > (X2 > X3 > X0) > $i > $i) > (X4 > X5) > $i > $i))).
% 2.83/0.78 thf(func_def_113, type, sF102: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3 > X0) > ((X4 > X5) > (X2 > X3 > X0) > X1) > (X4 > X5) > X1))).
% 2.83/0.78 thf(func_def_114, type, sF103: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((X1 > ((X4 > X5) > X1 > (X2 > X3) > X0) > (X2 > X3) > (X4 > X5) > X0))).
% 2.83/0.78 thf(func_def_115, type, sF104: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > (X1 > X3) > X2) > (X1 > X3) > X2))).
% 2.83/0.78 thf(func_def_116, type, sF105: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((((X0 > X1) > (X2 > X4) > X3) > (X2 > X4) > (X0 > X1) > X3))).
% 2.83/0.78 thf(func_def_117, type, sF106: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((X6 > X4) > (X7 > X8 > X5) > ((X6 > X4) > (X7 > X8 > X5) > (X2 > X3 > X0) > X1 > $i) > (X2 > X3 > X0) > X1 > $i))).
% 2.83/0.78 thf(func_def_118, type, sF107: !>[X0: $tType]:((X0 > (X0 > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_119, type, sF108: ($o > $i > $i)).
% 2.83/0.78 thf(func_def_120, type, sF109: !>[X0: $tType]:((X0 > $i > X0))).
% 2.83/0.78 thf(func_def_121, type, sF110: !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_122, type, sF111: (($i > $o) > $i > $o)).
% 2.83/0.78 thf(func_def_123, type, sF112: (($i > $i) > ($i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_124, type, sF113: !>[X0: $tType]:((X0 > (X0 > X0) > X0))).
% 2.83/0.78 thf(func_def_125, type, sF114: (($i > $o) > $i > $o)).
% 2.83/0.78 thf(func_def_126, type, sF115: ($o > $o)).
% 2.83/0.78 thf(func_def_127, type, sF116: !>[X0: $tType, X1: $tType]:(((X0 > X1) > ((X0 > X1) > X0) > X0))).
% 2.83/0.78 thf(func_def_128, type, sF117: !>[X0: $tType]:((($i > $i) > ($i > X0) > (X0 > $i > $i) > $i > $i))).
% 2.83/0.78 thf(func_def_129, type, sF118: !>[X0: $tType]:((($i > $i > X0) > X0))).
% 2.83/0.78 thf(func_def_130, type, sF119: (($i > $i > $i) > ($i > $i > $o) > $i > $i)).
% 2.83/0.78 thf(func_def_131, type, sF120: !>[X0: $tType]:((($i > $i > $o) > (($i > $i > $o) > X0) > X0))).
% 2.83/0.78 thf(func_def_132, type, sF121: (($i > $i > $i) > ($o > $i > $i) > ($i > $i > $o) > $i > $i)).
% 2.83/0.78 thf(func_def_133, type, sF122: !>[X0: $tType]:((($i > $i > X0) > (($i > $i > X0) > X0) > X0))).
% 2.83/0.78 thf(func_def_134, type, sF123: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((((X0 > $i > X1) > (X2 > X4) > X3) > (X2 > X4) > (X0 > $i > X1) > X3))).
% 2.83/0.78 thf(func_def_135, type, db2: !>[X0: $tType]:(X0)).
% 2.83/0.78 thf(func_def_136, type, sF124: !>[X0: $tType]:((($i > $i > X0) > ($i > $i > $i > $o) > ($i > $i > X0 > $i) > $o))).
% 2.83/0.78 thf(func_def_137, type, sF125: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $i > X0) > (X0 > X2 > X3 > X1) > ($i > $i > X3) > ($i > $i > X2) > $i > $i > X1))).
% 2.83/0.78 thf(func_def_138, type, sF126: !>[X0: $tType, X1: $tType]:(((X1 > (X0 > $i) > $i) > ($i > $i > X0 > $i) > ($i > $i > X1) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_139, type, sF127: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $i > X1 > X0) > ((X1 > X0) > X3 > X2) > ($i > $i > X3) > X2))).
% 2.83/0.78 thf(func_def_140, type, sF128: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $i > X1 > X0) > ((X1 > X0) > X3 > X2) > ($i > $i > X3) > $i > $i > X2))).
% 2.83/0.78 thf(func_def_141, type, sF129: !>[X0: $tType, X1: $tType]:(((($i > X1 > X0) > X1 > X0) > ($i > $i > X1) > ($i > $i > $i > X1 > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_142, type, sF130: !>[X0: $tType, X1: $tType]:(((($i > X1 > X0) > X1 > X0) > ($i > $i > X1) > ($i > $i > $i > X1 > X0) > X0))).
% 2.83/0.78 thf(func_def_143, type, sF131: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2 > X1) > ($i > $i > X0) > ($i > $i > X2) > $i > $i > X1))).
% 2.83/0.78 thf(func_def_144, type, sF132: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X2 > X1) > ($i > $i > X0) > ($i > $i > X2) > X1))).
% 2.83/0.78 thf(func_def_145, type, sF133: !>[X0: $tType, X1: $tType]:((($i > $i > $i > X1 > X0) > (($i > X1 > X0) > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_146, type, sF134: !>[X0: $tType, X1: $tType]:((($i > $i > $i > X0 > X1) > $i > X0 > X1))).
% 2.83/0.78 thf(func_def_147, type, sF135: !>[X0: $tType, X1: $tType]:(((($i > X0) > X1) > ($i > X0) > X1))).
% 2.83/0.78 thf(func_def_148, type, sF136: !>[X0: $tType, X1: $tType]:((($i > $i > X1 > X0) > ((X1 > X0) > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_149, type, sF137: !>[X0: $tType]:((($i > $i > $i > X0) > (($i > X0) > X0) > X0))).
% 2.83/0.78 thf(func_def_150, type, sF138: !>[X0: $tType]:((($i > $i > $i > X0) > (($i > X0) > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_151, type, sF139: !>[X0: $tType, X1: $tType]:((($i > $i > $i > X1) > (($i > X1) > X0) > X0))).
% 2.83/0.78 thf(func_def_152, type, sF140: ($o > $i > $i)).
% 2.83/0.78 thf(func_def_153, type, sF141: !>[X0: $tType]:((($i > $i > $i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_154, type, sF142: !>[X0: $tType, X1: $tType, X2: $tType]:(((X2 > X0 > X1) > X0 > X2 > X0 > X1))).
% 2.83/0.78 thf(func_def_155, type, sF143: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > $i > X1 > X0 > X1 > X2) > ((X0 > X1 > X2) > X1 > X2) > X1 > X2))).
% 2.83/0.78 thf(func_def_156, type, sF144: !>[X0: $tType, X1: $tType]:((($i > X0 > X1) > X0 > $i > X0 > X1))).
% 2.83/0.78 thf(func_def_157, type, sF145: !>[X0: $tType, X1: $tType]:((($i > $i > X0 > $i > X0 > X1) > (($i > X0 > X1) > X0 > X1) > X0 > X1))).
% 2.83/0.78 thf(func_def_158, type, sF146: !>[X0: $tType]:((($i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_159, type, sF147: (($i > $o) > ($i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_160, type, sF148: (($i > $o) > ($i > $i > $i) > $i > $i > $o)).
% 2.83/0.78 thf(func_def_161, type, sF149: !>[X0: $tType]:(($i > ($i > $i) > ($i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_162, type, sF150: !>[X0: $tType]:((($i > $i > $i) > ($i > $i > X0 > $i > $i) > ((X0 > $i > $i) > $i > $i) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_163, type, sF151: (($i > $i > $i) > $i)).
% 2.83/0.78 thf(func_def_164, type, sF152: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > $i > $i > X1) > ($i > ($i > X1) > X2 > X0) > ($i > $i > $i) > ($i > $i > X2) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_165, type, sF153: !>[X0: $tType, X1: $tType]:(($i > ($i > X1) > (X1 > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_166, type, sF154: (($i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_167, type, sF155: (($i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_168, type, sF156: !>[X0: $tType]:((($i > $i > X0) > (X0 > $i) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_169, type, sF157: !>[X0: $tType]:(((X0 > $i) > ($i > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_170, type, sF158: (($i > $o) > ($i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_171, type, sF159: (($i > $i) > ($i > $i > $i) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_172, type, sF160: (($i > $i > $i) > ($o > $i > $i) > ($i > $i > $o) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_173, type, sF161: !>[X0: $tType, X1: $tType]:(((X1 > X0 > $i) > ($i > $i > X0) > ($i > $i > X1) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_174, type, sF162: !>[X0: $tType]:((($i > $i > $i) > ($i > $i > $i > X0) > (($i > X0) > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_175, type, sF163: !>[X0: $tType, X1: $tType]:(((($i > X0) > X1 > X0) > ($i > $i > X1) > ($i > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_176, type, sF164: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((($i > $i > X1) > ((X4 > X5 > $i) > ($i > $i > X1) > (X2 > $i > X3) > $i > $i > X0) > (X2 > $i > X3) > (X4 > X5 > $i) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_177, type, sF165: !>[X0: $tType, X1: $tType]:((($i > $i > X0) > (X0 > X1) > ((X0 > X1) > ($i > $i > X0) > $i > $i > $i) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_178, type, sF166: !>[X0: $tType, X1: $tType, X2: $tType]:(((($i > X0) > (X1 > X2) > $i > $i > X2) > ($i > X0) > (X1 > X2) > $i > $i > X2))).
% 2.83/0.78 thf(func_def_179, type, sF167: !>[X0: $tType, X1: $tType]:((((X0 > $i > $i) > X1) > (X0 > $i > $i) > X1))).
% 2.83/0.78 thf(func_def_180, type, sF168: !>[X0: $tType, X1: $tType, X2: $tType]:(((($i > X0) > ($i > X1) > $i > $i > X2) > ($i > X0) > ($i > X1) > $i > $i > X2))).
% 2.83/0.78 thf(func_def_181, type, sF169: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X1 > X3) > X2 > X0) > (X1 > X3) > X2 > X0))).
% 2.83/0.78 thf(func_def_182, type, sF170: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((((X2 > X3 > X0) > X3 > X1) > (X2 > X3 > X0) > X3 > X1))).
% 2.83/0.78 thf(func_def_183, type, sF171: !>[X0: $tType, X1: $tType]:((($i > $i > $i > X1) > (($i > X1) > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_184, type, sF172: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > X1 > $i > X3 > X2) > X1 > $i > X3 > X2))).
% 2.83/0.78 thf(func_def_185, type, sF173: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > $i > X2 > X1) > ((X2 > X1) > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_186, type, sF174: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:((($i > $i > X0) > ((X1 > X4 > X5) > ($i > $i > X0) > ($i > $i > X2) > X3) > ($i > $i > X2) > (X1 > X4 > X5) > X3))).
% 2.83/0.78 thf(func_def_187, type, sF175: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((($i > $i > X2) > ($i > $i > X0 > X1) > ((X0 > X1) > X2 > X4) > (($i > $i > X0 > X1) > ((X0 > X1) > X2 > X4) > ($i > $i > X2) > X3) > X3))).
% 2.83/0.78 thf(func_def_188, type, sF176: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $i > X0) > (($i > $i > X0) > (X1 > X3) > X2) > (X1 > X3) > X2))).
% 2.83/0.78 thf(func_def_189, type, sF177: !>[X0: $tType]:(((X0 > $i) > X0 > $i))).
% 2.83/0.78 thf(func_def_190, type, sF178: ($o > $i > $i > $o)).
% 2.83/0.78 thf(func_def_191, type, sF179: !>[X0: $tType]:((($i > $i > X0) > (($i > $i > X0) > $o) > $o))).
% 2.83/0.78 thf(func_def_192, type, sF180: !>[X0: $tType, X1: $tType]:((($i > $i > X1) > (X1 > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_193, type, sF181: !>[X0: $tType, X1: $tType]:((X1 > (X1 > X0) > (X0 > $i) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_194, type, sF182: (($i > $i > $o) > $i)).
% 2.83/0.78 thf(func_def_195, type, sF183: !>[X0: $tType]:((($i > $i > $i) > (($i > $i > $i) > X0) > X0))).
% 2.83/0.78 thf(func_def_196, type, sF184: !>[X0: $tType]:((($i > $i > $i) > ($i > $o) > (($i > $o) > ($i > $i > $i) > X0) > X0))).
% 2.83/0.78 thf(func_def_197, type, sF185: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > $o) > (($i > $o) > (X1 > X3 > X0) > X2) > (X1 > X3 > X0) > X2))).
% 2.83/0.78 thf(func_def_198, type, sF186: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((($i > X0) > (($i > X0) > (X1 > X3) > X2) > (X1 > X3) > X2))).
% 2.83/0.78 thf(func_def_199, type, sF187: (($i > $i > $o) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_200, type, sF188: !>[X0: $tType, X1: $tType, X2: $tType]:(((X2 > X1) > (X0 > X2) > X0 > $i > $i > X1))).
% 2.83/0.78 thf(func_def_201, type, sF189: !>[X0: $tType, X1: $tType]:((((X0 > X1) > $o) > (X0 > X1) > $o))).
% 2.83/0.78 thf(func_def_202, type, sF190: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3) > ((X1 > X4 > X5) > (X2 > X3) > X0) > (X1 > X4 > X5) > X0))).
% 2.83/0.78 thf(func_def_203, type, sF191: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType]:((((X6 > X7) > X4 > X5) > (X2 > X3 > X0) > (($i > $i > X6 > X7) > ((X6 > X7) > X4 > X5) > (X2 > X3 > X0) > X1) > ($i > $i > X6 > X7) > X1))).
% 2.83/0.78 thf(func_def_204, type, sF192: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType]:((($i > $i > X6) > (X2 > X3 > X0) > ((X7 > X4 > X5) > ($i > $i > X6) > (X2 > X3 > X0) > X1) > (X7 > X4 > X5) > X1))).
% 2.83/0.78 thf(func_def_205, type, sF193: !>[X0: $tType, X1: $tType]:(((X0 > $i > $i > X1) > X0 > $i > $i > X1))).
% 2.83/0.78 thf(func_def_206, type, sF194: !>[X0: $tType]:((X0 > $i > $i > X0))).
% 2.83/0.78 thf(func_def_207, type, sF195: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3) > ((X4 > X0 > X5) > (X2 > X3) > X0 > X1) > (X4 > X0 > X5) > X0 > X1))).
% 2.83/0.78 thf(func_def_208, type, sF196: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((((X0 > X1) > (X2 > X4) > $i > $i > X3) > (X2 > X4) > (X0 > X1) > $i > $i > X3))).
% 2.83/0.78 thf(func_def_209, type, sF197: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X2 > X3 > X0) > ((X4 > X5) > (X2 > X3 > X0) > $i > $i > X1) > (X4 > X5) > $i > $i > X1))).
% 2.83/0.78 thf(func_def_210, type, sF198: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType]:(((X2 > $i > X3) > (X5 > X6 > X4) > ($i > $i > X1) > ((X5 > X6 > X4) > ($i > $i > X1) > (X2 > $i > X3) > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_211, type, sF199: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:((((X2 > X4 > X1 > X3) > $i > X0) > (X2 > X4 > X1 > X3) > $i > X0))).
% 2.83/0.78 thf(func_def_212, type, sF200: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType]:(((X5 > X6 > X4) > (X1 > X7 > X8) > ((X5 > X6 > X4) > (X1 > X7 > X8) > (X2 > X3) > $i > $i > X0) > (X2 > X3) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_213, type, sF201: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType]:((((X7 > X4 > X6) > (X8 > X9 > X5) > (X2 > X3 > X0) > X1) > (X7 > X4 > X6) > (X8 > X9 > X5) > (X2 > X3 > X0) > X1))).
% 2.83/0.78 thf(func_def_214, type, sF202: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType, X6: $tType, X7: $tType, X8: $tType, X9: $tType, X10: $tType]:((((X5 > X7 > X2) > ((X9 > X10) > X6 > X8) > (X3 > X4 > X0) > X1) > (X3 > X4 > X0) > (X5 > X7 > X2) > ((X9 > X10) > X6 > X8) > X1))).
% 2.83/0.78 thf(func_def_215, type, sF203: !>[X0: $tType]:(((X0 > $i) > ($i > $i) > X0 > $i > $i > $i))).
% 2.83/0.78 thf(func_def_216, type, sF204: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType, X5: $tType]:(((X0 > X1) > ((X4 > X5) > (X0 > X1) > X2 > X3) > X2 > (X4 > X5) > X3))).
% 2.83/0.78 thf(func_def_217, type, sF205: (($i > $i > $i) > $i)).
% 2.83/0.78 thf(func_def_218, type, sF206: (($i > $i > $i > $i > $i) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_219, type, sF207: (($i > $i > $i > $i) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_220, type, sF208: ((($i > $i > $i) > $i) > ($i > $i > $i) > $i)).
% 2.83/0.78 thf(func_def_221, type, sF209: !>[X0: $tType]:((X0 > (X0 > $i > $i > $i) > $i > $i > $i))).
% 2.83/0.78 thf(func_def_222, type, sF210: (($i > $o) > ($i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_223, type, db3: !>[X0: $tType]:(X0)).
% 2.83/0.78 thf(func_def_224, type, db4: !>[X0: $tType]:(X0)).
% 2.83/0.78 thf(func_def_225, type, sF211: ($o > $o)).
% 2.83/0.78 thf(func_def_226, type, sF212: (($i > $i > $o) > $o)).
% 2.83/0.78 thf(func_def_227, type, sF213: !>[X0: $tType]:((X0 > (X0 > $i > $i > $o) > $i > $i > $o))).
% 2.83/0.78 thf(func_def_228, type, sF214: !>[X0: $tType, X1: $tType]:(((X1 > $i) > (X0 > X1) > X0 > ($i > X0) > X0))).
% 2.83/0.78 thf(func_def_229, type, sF215: (($i > $i > $o) > ($i > $i > $o > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_230, type, sF216: (($i > $o) > ($i > $o > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_231, type, sF217: !>[X0: $tType]:((($i > $o > X0) > $o > X0))).
% 2.83/0.78 thf(func_def_232, type, sF218: !>[X0: $tType, X1: $tType]:(((X0 > $o > X1) > X0 > $o > X1))).
% 2.83/0.78 thf(func_def_233, type, sF219: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > (X1 > X2) > X2) > X0 > (X1 > X2) > X2))).
% 2.83/0.78 thf(func_def_234, type, sF220: ((($i > $i > $o) > $o) > ($i > $i > $o) > $o)).
% 2.83/0.78 thf(func_def_235, type, sF221: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > X0 > X2) > (($i > X0 > X2) > X1) > X1))).
% 2.83/0.78 thf(func_def_236, type, sF222: (($i > $i) > ($i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_237, type, sF223: !>[X0: $tType, X1: $tType, X2: $tType]:(((($i > X0) > (X1 > X2) > X2) > ($i > X0) > (X1 > X2) > X2))).
% 2.83/0.78 thf(func_def_238, type, sF224: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:(((X1 > X2) > (X2 > X0 > X3) > X0 > X1 > X3))).
% 2.83/0.78 thf(func_def_239, type, sF225: !>[X0: $tType, X1: $tType]:((($i > X1) > X0 > $i > X1))).
% 2.83/0.78 thf(func_def_240, type, sF226: ($o > $o)).
% 2.83/0.78 thf(func_def_241, type, sF227: (($o > $o) > $o > $o)).
% 2.83/0.78 thf(func_def_242, type, sF228: (($i > $i > $o) > $i > $i > $o)).
% 2.83/0.78 thf(func_def_243, type, sF229: (($o > $o) > ($i > $i > $o) > $i > $i > $o)).
% 2.83/0.78 thf(func_def_244, type, sF230: !>[X0: $tType, X1: $tType]:((X0 > X1 > (X1 > X0 > $i > $i > $o) > $i > $i > $o))).
% 2.83/0.78 thf(func_def_245, type, sF231: !>[X0: $tType, X1: $tType]:(($i > X1 > (X1 > $i > X0 > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_246, type, sF232: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > X2 > $o) > X0 > X1 > X2 > $o))).
% 2.83/0.78 thf(func_def_247, type, sF233: ($i > $o > $i > $o)).
% 2.83/0.78 thf(func_def_248, type, sF234: !>[X0: $tType]:((($i > $i > $i > X0) > (($i > $i > $i > X0) > $i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_249, type, sF235: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > $i > X2) > ((X0 > $i > X2) > $i > X1) > $i > X1))).
% 2.83/0.78 thf(func_def_250, type, sF236: !>[X0: $tType, X1: $tType]:((X1 > X0 > $i > (X1 > X0 > $i > $o) > $o))).
% 2.83/0.78 thf(func_def_251, type, sF237: !>[X0: $tType, X1: $tType, X2: $tType]:((X2 > X0 > X1 > (X0 > X2 > X1 > $o) > $o))).
% 2.83/0.78 thf(func_def_252, type, sF238: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType, X4: $tType]:(((X2 > (X1 > X4 > X0) > X3) > (X1 > X4 > X0) > X2 > X3))).
% 2.83/0.78 thf(func_def_253, type, sF239: (($i > $i > $o) > $o)).
% 2.83/0.78 thf(func_def_254, type, sF240: ($i > $i > $i > $i)).
% 2.83/0.78 thf(func_def_255, type, sF241: !>[X0: $tType]:(($i > ($i > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_256, type, sF242: !>[X0: $tType, X1: $tType]:((X0 > $i > ($i > X0 > $i > $i > X1) > $i > $i > X1))).
% 2.83/0.78 thf(func_def_257, type, sF243: !>[X0: $tType, X1: $tType]:(((($i > X0 > X1) > X1) > ($i > X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_258, type, sF244: !>[X0: $tType]:(($i > $i > ($i > $i > $i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_259, type, sF245: !>[X0: $tType]:(($i > $i > ($i > $i > X0) > X0))).
% 2.83/0.78 thf(func_def_260, type, sF246: (($i > $i > $i > $i) > $i > $i)).
% 2.83/0.78 thf(func_def_261, type, sF247: ($i > $i > $i)).
% 2.83/0.78 thf(func_def_262, type, sF248: (($i > $i > $i > $i > $i) > $i > $i > $i)).
% 2.83/0.78 thf(func_def_263, type, sF249: !>[X0: $tType]:((X0 > $i > $i > X0))).
% 2.83/0.78 thf(func_def_264, type, sF250: !>[X0: $tType, X1: $tType, X2: $tType, X3: $tType]:((X0 > (X0 > X1 > X3 > X2) > X1 > X3 > X2))).
% 2.83/0.78 thf(func_def_265, type, sF251: !>[X0: $tType, X1: $tType]:((X1 > X0 > $i > X1))).
% 2.83/0.78 thf(func_def_266, type, sF252: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > (X0 > X2 > $i > X1) > X2 > $i > X1))).
% 2.83/0.78 thf(func_def_267, type, sF253: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > $i > X2) > (X0 > X2 > $i > X1) > ($i > $i > X0) > $i > $i > X1))).
% 2.83/0.78 thf(func_def_268, type, sF254: !>[X0: $tType, X1: $tType]:(($i > X1 > (X1 > $i > $i > X0) > $i > X0))).
% 2.83/0.78 thf(func_def_269, type, sF255: !>[X0: $tType, X1: $tType, X2: $tType]:(((X0 > X1 > $i > X2) > X0 > X1 > $i > X2))).
% 2.83/0.78 thf(func_def_270, type, sF256: (($i > $i > $i) > ($i > $i > $o) > ($i > $i > $i) > $i > $i > $o)).
% 2.83/0.78 thf(func_def_271, type, sF257: !>[X0: $tType, X1: $tType]:(($i > X1 > (X1 > $i > X0) > X0))).
% 2.83/0.78 thf(func_def_272, type, sF258: !>[X0: $tType]:((($i > $i > X0 > $o) > ($i > $i > X0) > $i > $i > $o))).
% 2.83/0.78 thf(func_def_273, type, sK259: (($i > $i) > $i)).
% 2.83/0.78 thf(func_def_274, type, sF260: !>[X0: $tType]:(($i > ($i > X0) > (X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_275, type, sF261: !>[X0: $tType, X1: $tType]:((($i > X0 > X1) > X0 > X1))).
% 2.83/0.78 thf(func_def_276, type, sF262: !>[X0: $tType, X1: $tType]:((X1 > (X1 > X0) > (X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_277, type, sF263: !>[X0: $tType, X1: $tType]:((X0 > X1 > (X1 > X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_278, type, sF264: (($i > $i > $i > $o) > $i > $i > $i > $o)).
% 2.83/0.78 thf(func_def_279, type, sF265: !>[X0: $tType]:((($i > X0) > (X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_280, type, sF266: !>[X0: $tType]:(($o > ($o > X0) > (X0 > $i) > $i))).
% 2.83/0.78 thf(func_def_281, type, sF267: !>[X0: $tType, X1: $tType]:((($i > X0) > (X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_282, type, sF268: !>[X0: $tType]:(($i > ($i > X0 > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_283, type, sF269: (($i > $o > $o) > $i > $o > $o)).
% 2.83/0.78 thf(func_def_284, type, sF270: !>[X0: $tType]:((($i > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_285, type, sF271: (($i > $i > $i > $i) > $i > $i > $i > $i)).
% 2.83/0.78 thf(func_def_286, type, sF272: !>[X0: $tType]:((X0 > (X0 > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(func_def_287, type, sF273: (($i > $i > $i > $o) > (($i > $i > $o) > $o) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > $o)).
% 2.83/0.78 thf(func_def_288, type, sF274: !>[X0: $tType, X1: $tType, X2: $tType]:(((($i > $i > X0) > X2) > (X1 > $i > $i > X0) > X1 > X2))).
% 2.83/0.78 thf(func_def_289, type, sF275: !>[X0: $tType, X1: $tType]:((X0 > ($i > $i > $i > $i) > (($i > $i > $i > $i) > X0 > X1) > X1))).
% 2.83/0.78 thf(func_def_290, type, sF276: !>[X0: $tType, X1: $tType]:(((X0 > X1 > $o) > X0 > X1 > $o))).
% 2.83/0.78 thf(func_def_291, type, sF277: !>[X0: $tType, X1: $tType, X2: $tType]:((((X0 > X1) > (X1 > X2) > X2) > (X0 > X1) > (X1 > X2) > X2))).
% 2.83/0.78 thf(func_def_292, type, sF278: !>[X0: $tType]:((($i > X0 > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_293, type, sF279: (($i > $i) > $i)).
% 2.83/0.78 thf(func_def_294, type, sF280: !>[X0: $tType]:((($i > X0 > $o) > X0 > $o))).
% 2.83/0.78 thf(func_def_295, type, sF281: !>[X0: $tType]:((X0 > $i > ($i > X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_296, type, sF282: !>[X0: $tType, X1: $tType]:((($i > X0 > X1) > $i > X0 > X1))).
% 2.83/0.78 thf(func_def_297, type, sF283: !>[X0: $tType, X1: $tType]:((X1 > (X1 > X0) > ($i > X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_298, type, sF284: !>[X0: $tType, X1: $tType, X2: $tType]:((X0 > ($i > X1) > (X0 > X1 > X2) > X2))).
% 2.83/0.78 thf(func_def_299, type, sF285: !>[X0: $tType]:((($i > X0) > $i > ($i > $i > X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_300, type, sF286: !>[X0: $tType, X1: $tType]:((X1 > $i > X0 > (X1 > $i > X0 > $o) > $o))).
% 2.83/0.78 thf(func_def_301, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 2.83/0.78 thf(func_def_302, type, sF287: ($i > ($i > $o) > ($i > $i) > $o)).
% 2.83/0.78 thf(func_def_303, type, sF288: !>[X0: $tType, X1: $tType, X2: $tType]:((($i > X0 > X2) > (X1 > X0) > X1 > X2))).
% 2.83/0.78 thf(func_def_304, type, sF289: !>[X0: $tType]:((($i > $i > $i > X0) > $i > $i > X0))).
% 2.83/0.78 thf(f1,axiom,(
% 2.83/0.78 ! [X0 : ($i > $i)] : ((((h @ (X0 @ a))) != ((h @ (g @ $true)))) | (((h @ (X0 @ b))) != ((h @ (g @ $false)))))),
% 2.83/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1)).
% 2.83/0.78 thf(f2,axiom,(
% 2.83/0.78 (a != b)),
% 2.83/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2)).
% 2.83/0.78 thf(f3,plain,(
% 2.83/0.78 ! [X0 : ($i > $i)] : ((((h @ (X0 @ a))) != ((h @ (g @ $true)))) | (((h @ (X0 @ b))) != ((h @ (g @ $false)))))),
% 2.83/0.78 inference(rectify,[],[f1])).
% 2.83/0.78 thf(f4,plain,(
% 2.83/0.78 ! [X0 : ($i > $i)] : ((((h @ (X0 @ a))) != ((h @ (g @ $true)))) | (((h @ (X0 @ b))) != ((h @ (g @ $false)))))),
% 2.83/0.78 inference(fool_elimination,[],[f3])).
% 2.83/0.78 thf(f5,plain,(
% 2.83/0.78 ( ! [X0 : ($i > $i)] : ((((h @ (X0 @ a))) != ((h @ (g @ $true)))) | (((h @ (X0 @ b))) != ((h @ (g @ $false))))) )),
% 2.83/0.78 inference(cnf_transformation,[],[f4])).
% 2.83/0.78 thf(f6,plain,(
% 2.83/0.78 (b != a)),
% 2.83/0.78 inference(cnf_transformation,[],[f2])).
% 2.83/0.78 thf(f8,definition,(
% 2.83/0.78 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 2.83/0.78 introduced(theory,[fool_exhaustiveness_axiom])).
% 2.83/0.78 thf(f9,definition,(
% 2.83/0.78 ($false = ((sP0 @ (h @ (g @ $true)))))),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction])).
% 2.83/0.78 thf(f10,definition,(
% 2.83/0.78 ($false = ((sP1 @ (h @ (g @ $false)))))),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[sP1])],[inequality_splitting_name_introduction])).
% 2.83/0.78 thf(f11,plain,(
% 2.83/0.78 ( ! [X0 : ($i > $i)] : (($true = ((sP1 @ (h @ (X0 @ b))))) | ($true = ((sP0 @ (h @ (X0 @ a)))))) )),
% 2.83/0.78 inference(inequality_splitting,[],[f5,f10,f9])).
% 2.83/0.78 thf(f35,plain,(
% 2.83/0.78 ( ! [X0 : $o] : (($false = ((sP0 @ (h @ (g @ X0))))) | ($false = X0)) )),
% 2.83/0.78 inference(constrained_superposition,[],[f9,f8])).
% 2.83/0.78 thf(f366,definition,(
% 2.83/0.78 ( ! [X0 : $o] : ((((sF38 @ X0)) = (^[Y0 : $i]: (g @ X0)))) )),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[sF38])],[function_definition])).
% 2.83/0.78 thf(f367,plain,(
% 2.83/0.78 ( ! [X0 : $o] : (((^[Y0 : $i]: (g @ X0)) = ((sF38 @ X0)))) )),
% 2.83/0.78 inference(reorient_equations,[],[f366])).
% 2.83/0.78 thf(f515,plain,(
% 2.83/0.78 ( ! [X0 : $o,X1 : $i] : (((((^[Y0 : $i]: (g @ X0)) @ X1)) = ((sF38 @ X0 @ X1)))) )),
% 2.83/0.78 inference(argument_congruence,[],[f367])).
% 2.83/0.78 thf(f518,plain,(
% 2.83/0.78 ( ! [X0 : $o,X1 : $i] : ((((g @ X0)) = ((sF38 @ X0 @ X1)))) )),
% 2.83/0.78 inference(beta-eta_normalization,[],[f515])).
% 2.83/0.78 thf(f532,plain,(
% 2.83/0.78 ( ! [X2 : ($i > $i),X3 : $i,X0 : $o,X1 : ($i > $o)] : (($true = ((sP1 @ (h @ (g @ X0))))) | ($true = ((sP0 @ (h @ ((^[Y0 : $i]: (sF38 @ (X1 @ Y0) @ (X2 @ Y0))) @ a))))) | (((X1 @ b)) != X0) | (((X2 @ b)) != X3)) )),
% 2.83/0.78 inference(constrained_superposition,[],[f11,f518])).
% 2.83/0.78 thf(f538,plain,(
% 2.83/0.78 ( ! [X2 : ($i > $i),X3 : $i,X0 : $o,X1 : ($i > $o)] : (($true = ((sP1 @ (h @ (g @ X0))))) | ($true = ((sP0 @ (h @ ((^[Y0 : $i]: (sF38 @ (X1 @ Y0) @ (X2 @ Y0))) @ a))))) | ($true = ((X1 @ b))) | (((X2 @ b)) != X3) | ($true = X0)) )),
% 2.83/0.78 inference(xor_proxy_clausification,[],[f532])).
% 2.83/0.78 thf(f541,plain,(
% 2.83/0.78 ( ! [X2 : ($i > $i),X3 : $i,X0 : $o,X1 : ($i > $o)] : (($true = ((sP1 @ (h @ (g @ X0))))) | ($true = ((sP0 @ (h @ (sF38 @ (X1 @ a) @ (X2 @ a)))))) | ($true = ((X1 @ b))) | (((X2 @ b)) != X3) | ($true = X0)) )),
% 2.83/0.78 inference(beta-eta_normalization,[],[f538])).
% 2.83/0.78 thf(f546,plain,(
% 2.83/0.78 ( ! [X2 : ($i > $i),X3 : $i,X0 : $o,X1 : ($i > $o)] : (($true = ((sP0 @ (h @ (g @ (X1 @ a)))))) | ($true = ((sP1 @ (h @ (g @ X0))))) | ($true = ((X1 @ b))) | (((X2 @ b)) != X3) | ($true = X0)) )),
% 2.83/0.78 inference(forward_demodulation,[],[f541,f518])).
% 2.83/0.78 thf(f551,definition,(
% 2.83/0.78 spl37_3 <=> ! [X2 : ($i > $i),X3 : $i] : (((X2 @ b)) != X3)),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition])).
% 2.83/0.78 thf(f552,plain,(
% 2.83/0.78 ( ! [X2 : ($i > $i),X3 : $i] : ((((X2 @ b)) != X3)) ) | ~spl37_3),
% 2.83/0.78 inference(avatar_component_clause,[],[f551])).
% 2.83/0.78 thf(f554,definition,(
% 2.83/0.78 spl37_4 <=> ! [X0 : $o] : (($true = ((sP1 @ (h @ (g @ X0))))) | ($true = X0))),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[spl37_4])],[avatar_definition])).
% 2.83/0.78 thf(f555,plain,(
% 2.83/0.78 ( ! [X0 : $o] : (($true = ((sP1 @ (h @ (g @ X0))))) | ($true = X0)) ) | ~spl37_4),
% 2.83/0.78 inference(avatar_component_clause,[],[f554])).
% 2.83/0.78 thf(f557,definition,(
% 2.83/0.78 spl37_5 <=> ! [X1 : ($i > $o)] : (($true = ((sP0 @ (h @ (g @ (X1 @ a)))))) | ($true = ((X1 @ b))))),
% 2.83/0.78 introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition])).
% 2.83/0.78 thf(f558,plain,(
% 2.83/0.78 ( ! [X1 : ($i > $o)] : (($true = ((sP0 @ (h @ (g @ (X1 @ a)))))) | ($true = ((X1 @ b)))) ) | ~spl37_5),
% 2.83/0.78 inference(avatar_component_clause,[],[f557])).
% 2.83/0.78 thf(f559,plain,(
% 2.83/0.78 spl37_3 | spl37_4 | spl37_5),
% 2.83/0.78 inference(avatar_split_clause,[],[f546,f557,f554,f551])).
% 2.83/0.78 thf(f602,plain,(
% 2.83/0.78 $false | ~spl37_3),
% 2.83/0.78 inference(flex-flex_simplification,[],[f552])).
% 2.83/0.78 thf(f603,plain,(
% 2.83/0.78 ~spl37_3),
% 2.83/0.78 inference(avatar_contradiction_clause,[],[f602])).
% 2.83/0.78 thf(f635,plain,(
% 2.83/0.78 ($false = $true) | ($false = $true) | ~spl37_4),
% 2.83/0.78 inference(constrained_superposition,[],[f555,f10])).
% 2.83/0.78 thf(f640,plain,(
% 2.83/0.78 ($false = $true) | ~spl37_4),
% 2.83/0.78 inference(duplicate_literal_removal,[],[f635])).
% 2.83/0.78 thf(f641,plain,(
% 2.83/0.78 $false | ~spl37_4),
% 2.83/0.78 inference(trivial_inequality_removal,[],[f640])).
% 2.83/0.78 thf(f642,plain,(
% 2.83/0.78 ~spl37_4),
% 2.83/0.78 inference(avatar_contradiction_clause,[],[f641])).
% 2.83/0.78 thf(f2504,plain,(
% 2.83/0.78 ( ! [X0 : ($i > $o)] : (($false = $true) | ($false = ((X0 @ a))) | ($true = ((X0 @ b)))) ) | ~spl37_5),
% 2.83/0.78 inference(constrained_superposition,[],[f35,f558])).
% 2.83/0.78 thf(f2516,plain,(
% 2.83/0.78 ( ! [X0 : ($i > $o)] : (($true = ((X0 @ b))) | ($false = ((X0 @ a)))) ) | ~spl37_5),
% 2.83/0.78 inference(trivial_inequality_removal,[],[f2504])).
% 2.83/0.78 thf(f3411,plain,(
% 2.83/0.78 (b = a) | ~spl37_5),
% 2.83/0.78 inference(leibniz_equality_elimination,[],[f2516])).
% 2.83/0.78 thf(f3814,plain,(
% 2.83/0.78 $false | ~spl37_5),
% 2.83/0.78 inference(forward_subsumption_resolution,[],[f3411,f6])).
% 2.83/0.78 thf(f3815,plain,(
% 2.83/0.78 ~spl37_5),
% 2.83/0.78 inference(avatar_contradiction_clause,[],[f3814])).
% 2.83/0.78 cnf(s3, plain, spl37_3 | spl37_4 | spl37_5, inference(sat_conversion,[],[f559])).
% 2.83/0.78 cnf(s8, plain, ~spl37_3, inference(sat_conversion,[],[f603])).
% 2.83/0.78 cnf(s11, plain, ~spl37_4, inference(sat_conversion,[],[f642])).
% 2.83/0.78 cnf(s110, plain, ~spl37_5, inference(sat_conversion,[],[f3815])).
% 2.83/0.78 cnf(s143, plain, $false, inference(rat,[],[s3,s110,s11,s8])).
% 2.83/0.78 thf(f3850,plain,(
% 2.83/0.78 $false),
% 2.83/0.78 inference(avatar_sat_refutation,[],[s143])).
% 2.83/0.78 % SZS output end Proof for theBenchmark
% 2.83/0.78 % (379532)------------------------------
% 2.83/0.78 % (379532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.83/0.78 % (379532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.83/0.78 % (379532)CaDiCaL version: 2.1.3
% 2.83/0.78 % (379532)Termination reason: Refutation
% 2.83/0.78 % (379532)Time elapsed: 0.435 s
% 2.83/0.78 % (379532)Peak memory usage: 18 MB
% 2.83/0.78 % (379532)Instructions burned: 793 (million)
% 2.83/0.78 % (379490)Success in time 0.54 s
% 2.83/0.78 % Vampire exiting
%------------------------------------------------------------------------------