%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR123^2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 07:47:15 AM UTC 2026
% Result : Theorem 3.94s 0.95s
% Output : Refutation 3.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR123^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n020.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:55:50 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.94/0.90 % (1387108)Will run a generic schedule for satisfiability detection.
% 3.94/0.90 % (1387119)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3840981717:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.94/0.90 % (1387114)% WARNING: option uhcvi not known.
% 3.94/0.90 % (1387115)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3553846108:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.94/0.90 % (1387113)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2630569789_2999 on theBenchmark for (2999ds/0Mi)
% 3.94/0.90 % (1387114)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1834346239:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.94/0.90 % (1387116)dis+10_1_sil=32000:sp=arity:random_seed=2097112388:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.94/0.90 % (1387117)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1343018380:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.94/0.90 % (1387118)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1160825266:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.94/0.90 % (1387114)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.90 % (1387117)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.90 % Exception at run slice level
% 3.94/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.90 % (1387114)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.94/0.90 % (1387127)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3576800872:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.94/0.90 % Exception at run slice level
% 3.94/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.90 % (1387119)Instruction limit reached!
% 3.94/0.90 % (1387119)------------------------------
% 3.94/0.90 % (1387119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.90 % (1387119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.90 % (1387119)CaDiCaL version: 2.1.3
% 3.94/0.90 % (1387119)Termination reason: Instruction limit
% 3.94/0.90 % (1387119)Termination phase: Saturation
% 3.94/0.90 % (1387119)Time elapsed: 0.041 s
% 3.94/0.90 % (1387119)Peak memory usage: 13 MB
% 3.94/0.90 % (1387119)Instructions burned: 159 (million)
% 3.94/0.90 % (1387130)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=4009741591:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.94/0.90 % (1387130)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.90 % (1387130)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.94/0.90 % (1387116)Instruction limit reached!
% 3.94/0.90 % (1387116)------------------------------
% 3.94/0.90 % (1387116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.90 % (1387116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.90 % (1387116)CaDiCaL version: 2.1.3
% 3.94/0.90 % (1387116)Termination reason: Instruction limit
% 3.94/0.90 % (1387116)Termination phase: Saturation
% 3.94/0.90 % (1387116)Time elapsed: 0.050 s
% 3.94/0.90 % (1387116)Peak memory usage: 12 MB
% 3.94/0.90 % (1387116)Instructions burned: 104 (million)
% 3.94/0.90 % (1387129)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2465162377:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.94/0.90 % (1387117)Instruction limit reached!
% 3.94/0.90 % (1387117)------------------------------
% 3.94/0.90 % (1387117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.90 % (1387117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.90 % (1387117)CaDiCaL version: 2.1.3
% 3.94/0.90 % (1387117)Termination reason: Instruction limit
% 3.94/0.90 % (1387117)Termination phase: Saturation
% 3.94/0.90 % (1387117)Time elapsed: 0.057 s
% 3.94/0.90 % (1387117)Peak memory usage: 13 MB
% 3.94/0.90 % (1387117)Instructions burned: 117 (million)
% 3.94/0.90 % (1387118)Instruction limit reached!
% 3.94/0.90 % (1387118)------------------------------
% 3.94/0.90 % (1387118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387118)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387118)Termination reason: Instruction limit
% 3.94/0.95 % (1387118)Termination phase: Saturation
% 3.94/0.95 % (1387118)Time elapsed: 0.062 s
% 3.94/0.95 % (1387118)Peak memory usage: 13 MB
% 3.94/0.95 % (1387118)Instructions burned: 131 (million)
% 3.94/0.95 % (1387132)ott-21_1_sil=16000:fs=off:random_seed=1316385102:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.94/0.95 % (1387134)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=677935835:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 3.94/0.95 % (1387135)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3030659349:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387139)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2273476457:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 3.94/0.95 % (1387129)Instruction limit reached!
% 3.94/0.95 % (1387129)------------------------------
% 3.94/0.95 % (1387129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387129)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387129)Termination reason: Instruction limit
% 3.94/0.95 % (1387129)Termination phase: Saturation
% 3.94/0.95 % (1387129)Time elapsed: 0.065 s
% 3.94/0.95 % (1387129)Peak memory usage: 13 MB
% 3.94/0.95 % (1387129)Instructions burned: 131 (million)
% 3.94/0.95 % (1387141)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=469989423:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387132)Instruction limit reached!
% 3.94/0.95 % (1387132)------------------------------
% 3.94/0.95 % (1387132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387132)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387132)Termination reason: Instruction limit
% 3.94/0.95 % (1387132)Termination phase: Saturation
% 3.94/0.95 % (1387132)Time elapsed: 0.091 s
% 3.94/0.95 % (1387132)Peak memory usage: 12 MB
% 3.94/0.95 % (1387132)Instructions burned: 181 (million)
% 3.94/0.95 % (1387143)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=1809697594:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 3.94/0.95 % (1387143)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.95 % (1387145)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3904066647:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 3.94/0.95 % (1387145)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.95 % (1387130)Instruction limit reached!
% 3.94/0.95 % (1387130)------------------------------
% 3.94/0.95 % (1387130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387130)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387130)Termination reason: Instruction limit
% 3.94/0.95 % (1387130)Termination phase: Saturation
% 3.94/0.95 % (1387130)Time elapsed: 0.182 s
% 3.94/0.95 % (1387130)Peak memory usage: 16 MB
% 3.94/0.95 % (1387130)Instructions burned: 685 (million)
% 3.94/0.95 % (1387147)fmb+10_1_sil=64000:random_seed=1858054074:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 3.94/0.95 % (1387147)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387149)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=563936440:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387151)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2740809204:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387153)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=770637833:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 3.94/0.95 % (1387153)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.95 % (1387134)Instruction limit reached!
% 3.94/0.95 % (1387134)------------------------------
% 3.94/0.95 % (1387134)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387134)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387134)Termination reason: Instruction limit
% 3.94/0.95 % (1387134)Termination phase: Saturation
% 3.94/0.95 % (1387134)Time elapsed: 0.216 s
% 3.94/0.95 % (1387134)Peak memory usage: 14 MB
% 3.94/0.95 % (1387134)Instructions burned: 477 (million)
% 3.94/0.95 % (1387155)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=352440812:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 3.94/0.95 % (1387155)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.94/0.95 % (1387155)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.94/0.95 % (1387143)Instruction limit reached!
% 3.94/0.95 % (1387143)------------------------------
% 3.94/0.95 % (1387143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387143)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387143)Termination reason: Instruction limit
% 3.94/0.95 % (1387143)Termination phase: Saturation
% 3.94/0.95 % (1387143)Time elapsed: 0.324 s
% 3.94/0.95 % (1387143)Peak memory usage: 17 MB
% 3.94/0.95 % (1387143)Instructions burned: 692 (million)
% 3.94/0.95 % (1387157)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=428013241:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387159)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=468919812:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387161)ott-2_1_sil=16000:newcnf=on:random_seed=2601501615:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 3.94/0.95 % (1387161)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.94/0.95 % (1387139)Instruction limit reached!
% 3.94/0.95 % (1387139)------------------------------
% 3.94/0.95 % (1387139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387139)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387139)Termination reason: Instruction limit
% 3.94/0.95 % (1387139)Termination phase: Saturation
% 3.94/0.95 % (1387139)Time elapsed: 0.502 s
% 3.94/0.95 % (1387139)Peak memory usage: 17 MB
% 3.94/0.95 % (1387139)Instructions burned: 1180 (million)
% 3.94/0.95 % (1387145)Instruction limit reached!
% 3.94/0.95 % (1387145)------------------------------
% 3.94/0.95 % (1387145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387145)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387145)Termination reason: Instruction limit
% 3.94/0.95 % (1387145)Termination phase: Saturation
% 3.94/0.95 % (1387145)Time elapsed: 0.432 s
% 3.94/0.95 % (1387145)Peak memory usage: 16 MB
% 3.94/0.95 % (1387145)Instructions burned: 880 (million)
% 3.94/0.95 % (1387163)ott+10_1_sil=32000:tgt=ground:random_seed=798850432:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 3.94/0.95 % (1387164)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2775980521:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 3.94/0.95 % Exception at run slice level
% 3.94/0.95 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.94/0.95 % (1387167)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1577014653:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 3.94/0.95 % (1387167)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.94/0.95 % (1387153) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1387108-1387153"...
% 3.94/0.95 % (1387153)...printing done.
% 3.94/0.95 % (1387153)Refutation found. Thanks to Tanya!
% 3.94/0.95 % SZS status Theorem for theBenchmark
% 3.94/0.95 % SZS output start Proof for theBenchmark
% 3.94/0.95 thf(type_def_5, type, num: $tType).
% 3.94/0.95 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.94/0.95 thf(func_def_2, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_3, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_5, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 3.94/0.95 thf(func_def_6, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 3.94/0.95 thf(func_def_7, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 3.94/0.95 thf(func_def_8, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 3.94/0.95 thf(func_def_9, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 3.94/0.95 thf(func_def_10, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 3.94/0.95 thf(func_def_11, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 3.94/0.95 thf(func_def_12, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_15, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 3.94/0.95 thf(func_def_16, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 3.94/0.95 thf(func_def_17, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 3.94/0.95 thf(func_def_18, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 3.94/0.95 thf(func_def_19, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 3.94/0.95 thf(func_def_20, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 3.94/0.95 thf(func_def_21, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 3.94/0.95 thf(func_def_22, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_26, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 3.94/0.95 thf(func_def_31, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 3.94/0.95 thf(func_def_34, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 3.94/0.95 thf(func_def_40, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.94/0.95 thf(func_def_52, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.94/0.95 thf(func_def_60, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 3.94/0.95 thf(func_def_62, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 3.94/0.95 thf(func_def_66, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_67, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_68, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_69, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.94/0.95 thf(func_def_76, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_78, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_79, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_80, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 3.94/0.95 thf(func_def_81, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 3.94/0.95 thf(func_def_82, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_84, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_85, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_86, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 3.94/0.95 thf(func_def_87, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_88, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 3.94/0.95 thf(func_def_90, type, vNOT: ($o > $o)).
% 3.94/0.95 thf(func_def_93, type, vAND: ($o > $o > $o)).
% 3.94/0.95 thf(func_def_94, type, sK0: (($i > $i > $o) > $i)).
% 3.94/0.95 thf(func_def_95, type, sK1: (($i > $i > $o) > $i)).
% 3.94/0.95 thf(func_def_96, type, sK2: (($i > $i > $o) > $i)).
% 3.94/0.95 thf(func_def_98, type, sK4: (($i > $i > $o) > $i)).
% 3.94/0.95 thf(func_def_99, type, sK5: ($i > $i > $i)).
% 3.94/0.95 thf(func_def_100, type, db0: !>[X0: $tType]:(X0)).
% 3.94/0.95 thf(func_def_101, type, db1: !>[X0: $tType]:(X0)).
% 3.94/0.95 thf(func_def_102, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.94/0.95 thf(func_def_104, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.94/0.95 thf(func_def_105, type, db2: !>[X0: $tType]:(X0)).
% 3.94/0.95 thf(func_def_106, type, db3: !>[X0: $tType]:(X0)).
% 3.94/0.95 thf(f22,axiom,(
% 3.94/0.95 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 3.94/0.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_021)).
% 3.94/0.95 thf(f32,axiom,(
% 3.94/0.95 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)))),
% 3.94/0.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_031)).
% 3.94/0.95 thf(f49,axiom,(
% 3.94/0.95 (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)),
% 3.94/0.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_048)).
% 3.94/0.95 thf(f192,conjecture,(
% 3.94/0.95 ? [X0 : ($i > $i > $o),X1 : $i,X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 @ lSue_THFTYPE_i @ X2)) & (X0 @ lSue_THFTYPE_i @ X1))),
% 3.94/0.95 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 3.94/0.95 thf(f193,negated_conjecture,(
% 3.94/0.95 ~ ? [X0 : ($i > $i > $o),X1 : $i,X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 @ lSue_THFTYPE_i @ X2)) & (X0 @ lSue_THFTYPE_i @ X1))),
% 3.94/0.95 inference(negated_conjecture,[status(cth)],[f192])).
% 3.94/0.95 thf(f236,plain,(
% 3.94/0.95 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 3.94/0.95 inference(rectify,[],[f22])).
% 3.94/0.95 thf(f237,plain,(
% 3.94/0.95 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 3.94/0.95 inference(fool_elimination,[],[f236])).
% 3.94/0.95 thf(f256,plain,(
% 3.94/0.95 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)))),
% 3.94/0.95 inference(rectify,[],[f32])).
% 3.94/0.95 thf(f257,plain,(
% 3.94/0.95 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)))) = $true)),
% 3.94/0.95 inference(fool_elimination,[],[f256])).
% 3.94/0.95 thf(f288,plain,(
% 3.94/0.95 (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)),
% 3.94/0.95 inference(rectify,[],[f49])).
% 3.94/0.95 thf(f289,plain,(
% 3.94/0.95 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 3.94/0.95 inference(fool_elimination,[],[f288])).
% 3.94/0.95 thf(f574,plain,(
% 3.94/0.95 ~ ? [X0 : ($i > $i > $o),X1 : $i,X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 @ lSue_THFTYPE_i @ X2)) & (X0 @ lSue_THFTYPE_i @ X1))),
% 3.94/0.95 inference(rectify,[],[f193])).
% 3.94/0.95 thf(f575,plain,(
% 3.94/0.95 ~ ? [X0 : ($i > $i > $o),X1 : $i,X2 : $i] : ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ lSue_THFTYPE_i @ X1) & (~ (X0 @ lSue_THFTYPE_i @ X2))))))),
% 3.94/0.95 inference(fool_elimination,[],[f574])).
% 3.94/0.95 thf(f626,plain,(
% 3.94/0.95 ! [X0 : ($i > $i > $o),X1 : $i,X2 : $i] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ lSue_THFTYPE_i @ X1) & (~ (X0 @ lSue_THFTYPE_i @ X2))))))),
% 3.94/0.95 inference(ennf_transformation,[],[f575])).
% 3.94/0.95 thf(f663,plain,(
% 3.94/0.95 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 3.94/0.95 inference(cnf_transformation,[],[f237])).
% 3.94/0.95 thf(f675,plain,(
% 3.94/0.95 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)))) = $true)),
% 3.94/0.95 inference(cnf_transformation,[],[f257])).
% 3.94/0.95 thf(f693,plain,(
% 3.94/0.95 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 3.94/0.95 inference(cnf_transformation,[],[f289])).
% 3.94/0.95 thf(f836,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ lSue_THFTYPE_i @ X1) & (~ (X0 @ lSue_THFTYPE_i @ X2))))))) )),
% 3.94/0.95 inference(cnf_transformation,[],[f626])).
% 3.94/0.95 thf(f838,definition,(
% 3.94/0.95 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.94/0.95 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.94/0.95 thf(f855,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ lSue_THFTYPE_i @ X2)))))) | ($false = X0)) )),
% 3.94/0.95 inference(constrained_superposition,[],[f836,f838])).
% 3.94/0.95 thf(f859,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ lSue_THFTYPE_i @ X1) & $true)))) | (((~ (X0 @ lSue_THFTYPE_i @ X2))) = $false)) )),
% 3.94/0.95 inference(constrained_superposition,[],[f836,f838])).
% 3.94/0.95 thf(f866,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ lSue_THFTYPE_i @ X1) & $true)))) | (((X0 @ lSue_THFTYPE_i @ X2)) = $true)) )),
% 3.94/0.95 inference(not_proxy_clausification,[],[f859])).
% 3.94/0.95 thf(f867,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 @ lSue_THFTYPE_i @ X1)))) | (((X0 @ lSue_THFTYPE_i @ X2)) = $true)) )),
% 3.94/0.95 inference(boolean_simplification,[],[f866])).
% 3.94/0.95 thf(f873,plain,(
% 3.94/0.95 ( ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 & (~ $true))))) | ($false = X0)) )),
% 3.94/0.95 inference(beta-eta_normalization,[],[f855])).
% 3.94/0.95 thf(f874,plain,(
% 3.94/0.95 ( ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 & $false)))) | ($false = X0)) )),
% 3.94/0.95 inference(boolean_simplification,[],[f873])).
% 3.94/0.95 thf(f875,plain,(
% 3.94/0.95 ( ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($false = X0)) )),
% 3.94/0.95 inference(boolean_simplification,[],[f874])).
% 3.94/0.95 thf(f895,definition,(
% 3.94/0.95 spl6_1 <=> ! [X0 : $o] : ($false = X0)),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_1])],[avatar_definition])).
% 3.94/0.95 thf(f896,plain,(
% 3.94/0.95 ( ! [X0 : $o] : (($false = X0)) ) | ~spl6_1),
% 3.94/0.95 inference(avatar_component_clause,[],[f895])).
% 3.94/0.95 thf(f898,definition,(
% 3.94/0.95 spl6_2 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_2])],[avatar_definition])).
% 3.94/0.95 thf(f900,plain,(
% 3.94/0.95 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl6_2),
% 3.94/0.95 inference(avatar_component_clause,[],[f898])).
% 3.94/0.95 thf(f901,plain,(
% 3.94/0.95 spl6_1 | ~spl6_2),
% 3.94/0.95 inference(avatar_split_clause,[],[f875,f898,f895])).
% 3.94/0.95 thf(f1126,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true != $true) | (((X0 @ lSue_THFTYPE_i @ X2)) = $true) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 @ lSue_THFTYPE_i @ X1))))) )),
% 3.94/0.95 inference(constrained_superposition,[],[f867,f838])).
% 3.94/0.95 thf(f1137,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : ((((X0 @ lSue_THFTYPE_i @ X2)) = $true) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X0 @ lSue_THFTYPE_i @ X1))))) )),
% 3.94/0.95 inference(trivial_inequality_removal,[],[f1126])).
% 3.94/0.95 thf(f1169,plain,(
% 3.94/0.95 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ lSue_THFTYPE_i @ X2))) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ lSue_THFTYPE_i @ X1))))) )),
% 3.94/0.95 inference(primitive_instantiation,[],[f1137])).
% 3.94/0.95 thf(f1484,plain,(
% 3.94/0.95 ( ! [X2 : $i,X1 : $i] : (($true = ((lSue_THFTYPE_i = X2))) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (lSue_THFTYPE_i = X1))))) )),
% 3.94/0.95 inference(beta-eta_normalization,[],[f1169])).
% 3.94/0.95 thf(f1485,plain,(
% 3.94/0.95 ( ! [X2 : $i,X1 : $i] : ((lSue_THFTYPE_i = X2) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (lSue_THFTYPE_i = X1))))) )),
% 3.94/0.95 inference(equality_proxy_clausification,[],[f1484])).
% 3.94/0.95 thf(f1510,definition,(
% 3.94/0.95 spl6_3 <=> ! [X1 : $i] : ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (lSue_THFTYPE_i = X1))))),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_3])],[avatar_definition])).
% 3.94/0.95 thf(f1511,plain,(
% 3.94/0.95 ( ! [X1 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (lSue_THFTYPE_i = X1))))) ) | ~spl6_3),
% 3.94/0.95 inference(avatar_component_clause,[],[f1510])).
% 3.94/0.95 thf(f1513,definition,(
% 3.94/0.95 spl6_4 <=> ! [X2 : $i] : (lSue_THFTYPE_i = X2)),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_4])],[avatar_definition])).
% 3.94/0.95 thf(f1514,plain,(
% 3.94/0.95 ( ! [X2 : $i] : ((lSue_THFTYPE_i = X2)) ) | ~spl6_4),
% 3.94/0.95 inference(avatar_component_clause,[],[f1513])).
% 3.94/0.95 thf(f1515,plain,(
% 3.94/0.95 spl6_3 | spl6_4),
% 3.94/0.95 inference(avatar_split_clause,[],[f1485,f1513,f1510])).
% 3.94/0.95 thf(f1538,plain,(
% 3.94/0.95 ( ! [X0 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((lSue_THFTYPE_i = X0)))) ) | ~spl6_3),
% 3.94/0.95 inference(constrained_superposition,[],[f1511,f838])).
% 3.94/0.95 thf(f1573,plain,(
% 3.94/0.95 ( ! [X0 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (lSue_THFTYPE_i != X0)) ) | ~spl6_3),
% 3.94/0.95 inference(equality_proxy_clausification,[],[f1538])).
% 3.94/0.95 thf(f1597,definition,(
% 3.94/0.95 spl6_5 <=> ! [X0 : $i] : (lSue_THFTYPE_i != X0)),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_5])],[avatar_definition])).
% 3.94/0.95 thf(f1598,plain,(
% 3.94/0.95 ( ! [X0 : $i] : ((lSue_THFTYPE_i != X0)) ) | ~spl6_5),
% 3.94/0.95 inference(avatar_component_clause,[],[f1597])).
% 3.94/0.95 thf(f1600,definition,(
% 3.94/0.95 spl6_6 <=> ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)))),
% 3.94/0.95 introduced(definition,[new_symbols(definition,[spl6_6])],[avatar_definition])).
% 3.94/0.95 thf(f1602,plain,(
% 3.94/0.95 ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ~spl6_6),
% 3.94/0.95 inference(avatar_component_clause,[],[f1600])).
% 3.94/0.95 thf(f1603,plain,(
% 3.94/0.95 spl6_5 | spl6_6 | ~spl6_3),
% 3.94/0.95 inference(avatar_split_clause,[],[f1573,f1510,f1600,f1597])).
% 3.94/0.95 thf(f1626,plain,(
% 3.94/0.95 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) ) | ~spl6_4),
% 3.94/0.95 inference(constrained_superposition,[],[f1514,f1514])).
% 3.94/0.95 thf(f1750,plain,(
% 3.94/0.95 ( ! [X0 : $i] : (($true = ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X0)))) ) | ~spl6_4),
% 3.94/0.95 inference(constrained_superposition,[],[f663,f1626])).
% 3.94/0.95 thf(f1816,plain,(
% 3.94/0.95 ( ! [X0 : $i] : (($true = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0)))) ) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f1750,f1514])).
% 3.94/0.95 thf(f1930,plain,(
% 3.94/0.95 ($true = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lSue_THFTYPE_i))) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f693,f1514])).
% 3.94/0.95 thf(f1942,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($true & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ ((^[Y2 : $i]: ((^[Y3 : $i]: (lSue_THFTYPE_i)))) @ Y0 @ Y1))))) @ lSue_THFTYPE_i @ X2)))))) | (lSue_THFTYPE_i != ((X0 @ lSue_THFTYPE_i @ X1)))) ) | ~spl6_4),
% 3.94/0.95 inference(constrained_superposition,[],[f836,f1930])).
% 3.94/0.95 thf(f1955,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($true & (~ (likes_THFTYPE_IiioI @ (X0 @ lSue_THFTYPE_i @ X2) @ lSue_THFTYPE_i)))))) | (lSue_THFTYPE_i != ((X0 @ lSue_THFTYPE_i @ X1)))) ) | ~spl6_4),
% 3.94/0.95 inference(beta-eta_normalization,[],[f1942])).
% 3.94/0.95 thf(f1956,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ (X0 @ lSue_THFTYPE_i @ X2) @ lSue_THFTYPE_i))))) | (lSue_THFTYPE_i != ((X0 @ lSue_THFTYPE_i @ X1)))) ) | ~spl6_4),
% 3.94/0.95 inference(boolean_simplification,[],[f1955])).
% 3.94/0.95 thf(f1967,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $i)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ (X0 @ lSue_THFTYPE_i @ X2) @ lSue_THFTYPE_i)))))) ) | ~spl6_4),
% 3.94/0.95 inference(forward_subsumption_resolution,[],[f1956,f1514])).
% 3.94/0.95 thf(f1976,plain,(
% 3.94/0.95 ( ! [X2 : $i,X0 : ($i > $i > $i)] : (($true != ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ (~ (likes_THFTYPE_IiioI @ (X0 @ lSue_THFTYPE_i @ X2) @ lSue_THFTYPE_i)))))) ) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f1967,f1514])).
% 3.94/0.95 thf(f1985,plain,(
% 3.94/0.95 ($true != ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lSue_THFTYPE_i))))) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f1976,f1514])).
% 3.94/0.95 thf(f1994,plain,(
% 3.94/0.95 ($true != ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ (~ $true)))) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f1985,f1930])).
% 3.94/0.95 thf(f1995,plain,(
% 3.94/0.95 ($true != ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ $false))) | ~spl6_4),
% 3.94/0.95 inference(boolean_simplification,[],[f1994])).
% 3.94/0.95 thf(f9464,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))))) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f675,f1514])).
% 3.94/0.95 thf(f9465,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ (~ $true)))) | ~spl6_4),
% 3.94/0.95 inference(forward_demodulation,[],[f9464,f1816])).
% 3.94/0.95 thf(f9466,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ lSue_THFTYPE_i @ $false))) | ~spl6_4),
% 3.94/0.95 inference(boolean_simplification,[],[f9465])).
% 3.94/0.95 thf(f9467,plain,(
% 3.94/0.95 $false | ~spl6_4),
% 3.94/0.95 inference(forward_subsumption_resolution,[],[f9466,f1995])).
% 3.94/0.95 thf(f9468,plain,(
% 3.94/0.95 ~spl6_4),
% 3.94/0.95 inference(avatar_contradiction_clause,[],[f9467])).
% 3.94/0.95 thf(f9469,plain,(
% 3.94/0.95 $false | ~spl6_5),
% 3.94/0.95 inference(equality_resolution,[],[f1598])).
% 3.94/0.95 thf(f9470,plain,(
% 3.94/0.95 ~spl6_5),
% 3.94/0.95 inference(avatar_contradiction_clause,[],[f9469])).
% 3.94/0.95 thf(f18239,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $false)),
% 3.94/0.95 inference(constrained_superposition,[],[f675,f838])).
% 3.94/0.95 thf(f18364,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $true)),
% 3.94/0.95 inference(not_proxy_clausification,[],[f18239])).
% 3.94/0.95 thf(f18379,plain,(
% 3.94/0.95 ($true = $false) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $true) | ~spl6_6),
% 3.94/0.95 inference(forward_demodulation,[],[f18364,f1602])).
% 3.94/0.95 thf(f18380,plain,(
% 3.94/0.95 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $true) | ~spl6_6),
% 3.94/0.95 inference(trivial_inequality_removal,[],[f18379])).
% 3.94/0.95 thf(f18410,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | ~spl6_6),
% 3.94/0.95 inference(constrained_superposition,[],[f675,f18380])).
% 3.94/0.95 thf(f18411,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl6_6),
% 3.94/0.95 inference(boolean_simplification,[],[f18410])).
% 3.94/0.95 thf(f18454,plain,(
% 3.94/0.95 $false | (spl6_2 | ~spl6_6)),
% 3.94/0.95 inference(forward_subsumption_resolution,[],[f18411,f900])).
% 3.94/0.95 thf(f18455,plain,(
% 3.94/0.95 spl6_2 | ~spl6_6),
% 3.94/0.95 inference(avatar_contradiction_clause,[],[f18454])).
% 3.94/0.95 thf(f18679,plain,(
% 3.94/0.95 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl6_1),
% 3.94/0.95 inference(constrained_superposition,[],[f675,f896])).
% 3.94/0.95 thf(f19043,plain,(
% 3.94/0.95 ($true = $false) | ~spl6_1),
% 3.94/0.95 inference(forward_demodulation,[],[f18679,f896])).
% 3.94/0.95 thf(f19044,plain,(
% 3.94/0.95 $false | ~spl6_1),
% 3.94/0.95 inference(trivial_inequality_removal,[],[f19043])).
% 3.94/0.95 thf(f19045,plain,(
% 3.94/0.95 ~spl6_1),
% 3.94/0.95 inference(avatar_contradiction_clause,[],[f19044])).
% 3.94/0.95 cnf(s1, plain, spl6_1 | ~spl6_2, inference(sat_conversion,[],[f901])).
% 3.94/0.95 cnf(s2, plain, spl6_3 | spl6_4, inference(sat_conversion,[],[f1515])).
% 3.94/0.95 cnf(s3, plain, ~spl6_3 | spl6_5 | spl6_6, inference(sat_conversion,[],[f1603])).
% 3.94/0.95 cnf(s4, plain, ~spl6_4, inference(sat_conversion,[],[f9468])).
% 3.94/0.95 cnf(s5, plain, ~spl6_5, inference(sat_conversion,[],[f9470])).
% 3.94/0.95 cnf(s7, plain, spl6_2 | ~spl6_6, inference(sat_conversion,[],[f18455])).
% 3.94/0.95 cnf(s165, plain, ~spl6_1, inference(sat_conversion,[],[f19045])).
% 3.94/0.95 cnf(s168, plain, ~spl6_3 | spl6_6, inference(rat,[],[s3,s5])).
% 3.94/0.95 cnf(s169, plain, spl6_3, inference(rat,[],[s2,s4])).
% 3.94/0.95 cnf(s170, plain, spl6_6, inference(rat,[],[s168,s169])).
% 3.94/0.95 cnf(s171, plain, spl6_2, inference(rat,[],[s7,s170])).
% 3.94/0.95 cnf(s172, plain, $false, inference(rat,[],[s1,s171,s165])).
% 3.94/0.95 thf(f19056,plain,(
% 3.94/0.95 $false),
% 3.94/0.95 inference(avatar_sat_refutation,[],[s172])).
% 3.94/0.95 % SZS output end Proof for theBenchmark
% 3.94/0.95 % (1387153)------------------------------
% 3.94/0.95 % (1387153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.94/0.95 % (1387153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.94/0.95 % (1387153)CaDiCaL version: 2.1.3
% 3.94/0.95 % (1387153)Termination reason: Refutation
% 3.94/0.95 % (1387153)Time elapsed: 0.403 s
% 3.94/0.95 % (1387153)Peak memory usage: 18 MB
% 3.94/0.95 % (1387153)Instructions burned: 1685 (million)
% 3.94/0.95 % (1387108)Success in time 0.722 s
% 3.94/0.95 % Vampire exiting
%------------------------------------------------------------------------------