%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR133^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 : n003.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:17 AM UTC 2026
% Result : Theorem 4.14s 0.93s
% Output : Refutation 4.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR133^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n003.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 17:57:44 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/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
% 4.14/0.93 % (2843848)Will run a generic schedule for satisfiability detection.
% 4.14/0.93 % (2843855)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=424453560:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.14/0.93 % (2843853)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3174617928_2999 on theBenchmark for (2999ds/0Mi)
% 4.14/0.93 % (2843856)dis+10_1_sil=32000:sp=arity:random_seed=148403979:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.14/0.93 % (2843857)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=809339691:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.14/0.93 % (2843858)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=784412454:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.14/0.93 % (2843857)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843854)% WARNING: option uhcvi not known.
% 4.14/0.93 % (2843859)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=865546386:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.14/0.93 % (2843854)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2546085594:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.14/0.93 % (2843854)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843854)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.14/0.93 % (2843865)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2311974923:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843869)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1876808579:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.14/0.93 % (2843856)Instruction limit reached!
% 4.14/0.93 % (2843856)------------------------------
% 4.14/0.93 % (2843856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843856)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843856)Termination reason: Instruction limit
% 4.14/0.93 % (2843856)Termination phase: Saturation
% 4.14/0.93 % (2843856)Time elapsed: 0.049 s
% 4.14/0.93 % (2843856)Peak memory usage: 12 MB
% 4.14/0.93 % (2843856)Instructions burned: 103 (million)
% 4.14/0.93 % (2843857)Instruction limit reached!
% 4.14/0.93 % (2843857)------------------------------
% 4.14/0.93 % (2843857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843857)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843857)Termination reason: Instruction limit
% 4.14/0.93 % (2843857)Termination phase: Saturation
% 4.14/0.93 % (2843857)Time elapsed: 0.056 s
% 4.14/0.93 % (2843857)Peak memory usage: 12 MB
% 4.14/0.93 % (2843857)Instructions burned: 117 (million)
% 4.14/0.93 % (2843858)Instruction limit reached!
% 4.14/0.93 % (2843858)------------------------------
% 4.14/0.93 % (2843858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843858)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843858)Termination reason: Instruction limit
% 4.14/0.93 % (2843858)Termination phase: Saturation
% 4.14/0.93 % (2843858)Time elapsed: 0.062 s
% 4.14/0.93 % (2843858)Peak memory usage: 12 MB
% 4.14/0.93 % (2843858)Instructions burned: 132 (million)
% 4.14/0.93 % (2843871)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=2768791783:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.14/0.93 % (2843871)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843872)ott-21_1_sil=16000:fs=off:random_seed=2583071642:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.14/0.93 % (2843871)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.14/0.93 % (2843873)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2844440559:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.14/0.93 % (2843859)Instruction limit reached!
% 4.14/0.93 % (2843859)------------------------------
% 4.14/0.93 % (2843859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843859)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843859)Termination reason: Instruction limit
% 4.14/0.93 % (2843859)Termination phase: Saturation
% 4.14/0.93 % (2843859)Time elapsed: 0.089 s
% 4.14/0.93 % (2843859)Peak memory usage: 12 MB
% 4.14/0.93 % (2843859)Instructions burned: 159 (million)
% 4.14/0.93 % (2843869)Instruction limit reached!
% 4.14/0.93 % (2843869)------------------------------
% 4.14/0.93 % (2843869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843869)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843869)Termination reason: Instruction limit
% 4.14/0.93 % (2843869)Termination phase: Saturation
% 4.14/0.93 % (2843869)Time elapsed: 0.065 s
% 4.14/0.93 % (2843869)Peak memory usage: 12 MB
% 4.14/0.93 % (2843869)Instructions burned: 133 (million)
% 4.14/0.93 % (2843877)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1640175902:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843878)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=349085453:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.14/0.93 % (2843880)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=198548405:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843872)Instruction limit reached!
% 4.14/0.93 % (2843872)------------------------------
% 4.14/0.93 % (2843872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843872)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843872)Termination reason: Instruction limit
% 4.14/0.93 % (2843872)Termination phase: Saturation
% 4.14/0.93 % (2843872)Time elapsed: 0.090 s
% 4.14/0.93 % (2843872)Peak memory usage: 12 MB
% 4.14/0.93 % (2843872)Instructions burned: 181 (million)
% 4.14/0.93 % (2843883)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=168029482: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)
% 4.14/0.93 % (2843883)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843884)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1554581835:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 4.14/0.93 % (2843884)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843873)Instruction limit reached!
% 4.14/0.93 % (2843873)------------------------------
% 4.14/0.93 % (2843873)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843873)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843873)Termination reason: Instruction limit
% 4.14/0.93 % (2843873)Termination phase: Saturation
% 4.14/0.93 % (2843873)Time elapsed: 0.219 s
% 4.14/0.93 % (2843873)Peak memory usage: 14 MB
% 4.14/0.93 % (2843873)Instructions burned: 477 (million)
% 4.14/0.93 % (2843910)fmb+10_1_sil=64000:random_seed=3815440360:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 4.14/0.93 % (2843910)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843923)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4205186084:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843935)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2927453613:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843952)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3236438652:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 4.14/0.93 % (2843871)Instruction limit reached!
% 4.14/0.93 % (2843871)------------------------------
% 4.14/0.93 % (2843871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843871)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843871)Termination reason: Instruction limit
% 4.14/0.93 % (2843871)Termination phase: Saturation
% 4.14/0.93 % (2843871)Time elapsed: 0.322 s
% 4.14/0.93 % (2843871)Peak memory usage: 15 MB
% 4.14/0.93 % (2843871)Instructions burned: 687 (million)
% 4.14/0.93 % (2843952)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843959)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2935018273:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 4.14/0.93 % (2843959)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.14/0.93 % (2843959)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.14/0.93 % (2843883)Instruction limit reached!
% 4.14/0.93 % (2843883)------------------------------
% 4.14/0.93 % (2843883)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843883)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843883)Termination reason: Instruction limit
% 4.14/0.93 % (2843883)Termination phase: Saturation
% 4.14/0.93 % (2843883)Time elapsed: 0.322 s
% 4.14/0.93 % (2843883)Peak memory usage: 16 MB
% 4.14/0.93 % (2843883)Instructions burned: 694 (million)
% 4.14/0.93 % (2843987)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1693504857:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2843998)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3331923979:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 4.14/0.93 % Exception at run slice level
% 4.14/0.93 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.14/0.93 % (2844000)ott-2_1_sil=16000:newcnf=on:random_seed=988883745:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 4.14/0.93 % (2844000)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.14/0.93 % (2843884)Instruction limit reached!
% 4.14/0.93 % (2843884)------------------------------
% 4.14/0.93 % (2843884)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843884)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843884)Termination reason: Instruction limit
% 4.14/0.93 % (2843884)Termination phase: Saturation
% 4.14/0.93 % (2843884)Time elapsed: 0.414 s
% 4.14/0.93 % (2843884)Peak memory usage: 16 MB
% 4.14/0.93 % (2843884)Instructions burned: 880 (million)
% 4.14/0.93 % (2844014)ott+10_1_sil=32000:tgt=ground:random_seed=3353703452:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 4.14/0.93 % (2843878)Instruction limit reached!
% 4.14/0.93 % (2843878)------------------------------
% 4.14/0.93 % (2843878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843878)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843878)Termination reason: Instruction limit
% 4.14/0.93 % (2843878)Termination phase: Saturation
% 4.14/0.93 % (2843878)Time elapsed: 0.516 s
% 4.14/0.93 % (2843878)Peak memory usage: 14 MB
% 4.14/0.93 % (2843878)Instructions burned: 1180 (million)
% 4.14/0.93 % (2843854) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2843848-2843854"...
% 4.14/0.93 % (2843854)...printing done.
% 4.14/0.93 % (2843854)Refutation found. Thanks to Tanya!
% 4.14/0.93 % SZS status Theorem for theBenchmark
% 4.14/0.93 % SZS output start Proof for theBenchmark
% 4.14/0.93 thf(type_def_5, type, num: $tType).
% 4.14/0.93 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 4.14/0.93 thf(func_def_2, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 4.14/0.93 thf(func_def_3, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 4.14/0.93 thf(func_def_4, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 4.14/0.93 thf(func_def_6, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 4.14/0.93 thf(func_def_7, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 4.14/0.93 thf(func_def_8, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 4.14/0.93 thf(func_def_9, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 4.14/0.93 thf(func_def_10, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_13, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 4.14/0.93 thf(func_def_18, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 4.14/0.93 thf(func_def_29, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 4.14/0.93 thf(func_def_31, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 4.14/0.93 thf(func_def_32, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_33, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_34, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_38, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_39, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_41, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_42, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_43, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_44, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 4.14/0.93 thf(func_def_45, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_46, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 4.14/0.93 thf(func_def_48, type, vNOT: ($o > $o)).
% 4.14/0.93 thf(func_def_51, type, vAND: ($o > $o > $o)).
% 4.14/0.93 thf(func_def_52, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.14/0.93 thf(func_def_53, type, sK0: ($i > $i)).
% 4.14/0.93 thf(func_def_54, type, db0: !>[X0: $tType]:(X0)).
% 4.14/0.93 thf(func_def_55, type, db1: !>[X0: $tType]:(X0)).
% 4.14/0.93 thf(func_def_56, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.14/0.93 thf(func_def_58, type, db2: !>[X0: $tType]:(X0)).
% 4.14/0.93 thf(f10,axiom,(
% 4.14/0.93 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))),
% 4.14/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_009)).
% 4.14/0.93 thf(f20,axiom,(
% 4.14/0.93 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)))),
% 4.14/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_019)).
% 4.14/0.93 thf(f80,conjecture,(
% 4.14/0.93 ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X1 = X0)) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 4.14/0.93 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 4.14/0.93 thf(f81,negated_conjecture,(
% 4.14/0.93 ~ ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X1 = X0)) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 4.14/0.93 inference(negated_conjecture,[status(cth)],[f80])).
% 4.14/0.93 thf(f100,plain,(
% 4.14/0.93 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))),
% 4.14/0.93 inference(rectify,[],[f10])).
% 4.14/0.93 thf(f101,plain,(
% 4.14/0.93 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 4.14/0.93 inference(fool_elimination,[],[f100])).
% 4.14/0.93 thf(f118,plain,(
% 4.14/0.93 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)))),
% 4.14/0.93 inference(rectify,[],[f20])).
% 4.14/0.93 thf(f119,plain,(
% 4.14/0.93 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)))) = $true)),
% 4.14/0.93 inference(fool_elimination,[],[f118])).
% 4.14/0.93 thf(f238,plain,(
% 4.14/0.93 ~ ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X1 = X0)) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 4.14/0.93 inference(rectify,[],[f81])).
% 4.14/0.93 thf(f239,plain,(
% 4.14/0.93 ~ ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i)) & (~ (X0 = X1))))))),
% 4.14/0.93 inference(fool_elimination,[],[f238])).
% 4.14/0.93 thf(f266,plain,(
% 4.14/0.93 ! [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i)) & (~ (X0 = X1))))))),
% 4.14/0.93 inference(ennf_transformation,[],[f239])).
% 4.14/0.93 thf(f278,plain,(
% 4.14/0.93 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 4.14/0.93 inference(cnf_transformation,[],[f101])).
% 4.14/0.93 thf(f288,plain,(
% 4.14/0.93 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)))) = $true)),
% 4.14/0.93 inference(cnf_transformation,[],[f119])).
% 4.14/0.93 thf(f349,plain,(
% 4.14/0.93 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i)) & (~ (X0 = X1))))))) )),
% 4.14/0.93 inference(cnf_transformation,[],[f266])).
% 4.14/0.93 thf(f351,definition,(
% 4.14/0.93 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 4.14/0.93 introduced(theory,[fool_exhaustiveness_axiom])).
% 4.14/0.93 thf(f366,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ $true))))) | ($false = ((X2 = X0)))) )),
% 4.14/0.93 inference(constrained_superposition,[],[f349,f351])).
% 4.14/0.93 thf(f367,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & $true)))) | ($false = ((~ (X2 = X0))))) )),
% 4.14/0.93 inference(constrained_superposition,[],[f349,f351])).
% 4.14/0.93 thf(f384,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & $true)))) | ($true = ((X2 = X0)))) )),
% 4.14/0.93 inference(not_proxy_clausification,[],[f367])).
% 4.14/0.93 thf(f385,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & $true)))) | (X0 = X2)) )),
% 4.14/0.93 inference(equality_proxy_clausification,[],[f384])).
% 4.14/0.93 thf(f386,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i))))) | (X0 = X2)) )),
% 4.14/0.93 inference(boolean_simplification,[],[f385])).
% 4.14/0.93 thf(f387,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ $true))))) | (X0 != X2)) )),
% 4.14/0.93 inference(equality_proxy_clausification,[],[f366])).
% 4.14/0.93 thf(f388,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & $false)))) | (X0 != X2)) )),
% 4.14/0.93 inference(boolean_simplification,[],[f387])).
% 4.14/0.93 thf(f389,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (X0 != X2)) )),
% 4.14/0.93 inference(boolean_simplification,[],[f388])).
% 4.14/0.93 thf(f399,definition,(
% 4.14/0.93 spl1_3 <=> ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : (X0 != X2)),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition])).
% 4.14/0.93 thf(f400,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : ((X0 != X2)) ) | ~spl1_3),
% 4.14/0.93 inference(avatar_component_clause,[],[f399])).
% 4.14/0.93 thf(f402,definition,(
% 4.14/0.93 spl1_4 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition])).
% 4.14/0.93 thf(f405,plain,(
% 4.14/0.93 spl1_3 | ~spl1_4),
% 4.14/0.93 inference(avatar_split_clause,[],[f389,f402,f399])).
% 4.14/0.93 thf(f632,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($true & (X2 @ X1 @ lAnna_THFTYPE_i))))) | (X0 = X2) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i)))) )),
% 4.14/0.93 inference(constrained_superposition,[],[f386,f351])).
% 4.14/0.93 thf(f721,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (X2 @ X1 @ lAnna_THFTYPE_i)))) | (X0 = X2) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i)))) )),
% 4.14/0.93 inference(boolean_simplification,[],[f632])).
% 4.14/0.93 thf(f853,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X0 : $o,X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($false = ((X2 @ X1 @ lBill_THFTYPE_i))) | ($false = X0)) )),
% 4.14/0.93 inference(constrained_superposition,[],[f721,f351])).
% 4.14/0.93 thf(f929,definition,(
% 4.14/0.93 spl1_5 <=> ! [X2 : ($i > $i > $o),X1 : $i] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($false = ((X2 @ X1 @ lBill_THFTYPE_i))))),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition])).
% 4.14/0.93 thf(f930,plain,(
% 4.14/0.93 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) ) | ~spl1_5),
% 4.14/0.93 inference(avatar_component_clause,[],[f929])).
% 4.14/0.93 thf(f932,definition,(
% 4.14/0.93 spl1_6 <=> ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0))) | ($false = X0))),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition])).
% 4.14/0.93 thf(f933,plain,(
% 4.14/0.93 ( ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0))) | ($false = X0)) ) | ~spl1_6),
% 4.14/0.93 inference(avatar_component_clause,[],[f932])).
% 4.14/0.93 thf(f934,plain,(
% 4.14/0.93 spl1_5 | spl1_6),
% 4.14/0.93 inference(avatar_split_clause,[],[f853,f932,f929])).
% 4.14/0.93 thf(f1019,plain,(
% 4.14/0.93 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))))) ) | ~spl1_5),
% 4.14/0.93 inference(primitive_instantiation,[],[f930])).
% 4.14/0.93 thf(f1351,plain,(
% 4.14/0.93 ( ! [X1 : $i] : (($false = ((X1 = lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)) ) | ~spl1_5),
% 4.14/0.93 inference(beta-eta_normalization,[],[f1019])).
% 4.14/0.93 thf(f1362,definition,(
% 4.14/0.93 spl1_9 <=> ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition])).
% 4.14/0.93 thf(f1364,plain,(
% 4.14/0.93 ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =) | ~spl1_9),
% 4.14/0.93 inference(avatar_component_clause,[],[f1362])).
% 4.14/0.93 thf(f1366,definition,(
% 4.14/0.93 spl1_10 <=> ! [X1 : $i] : (lBill_THFTYPE_i != X1)),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_10])],[avatar_definition])).
% 4.14/0.93 thf(f1367,plain,(
% 4.14/0.93 ( ! [X1 : $i] : ((lBill_THFTYPE_i != X1)) ) | ~spl1_10),
% 4.14/0.93 inference(avatar_component_clause,[],[f1366])).
% 4.14/0.93 thf(f6789,plain,(
% 4.14/0.93 $false | ~spl1_3),
% 4.14/0.93 inference(flex-flex_simplification,[],[f400])).
% 4.14/0.93 thf(f6790,plain,(
% 4.14/0.93 ~spl1_3),
% 4.14/0.93 inference(avatar_contradiction_clause,[],[f6789])).
% 4.14/0.93 thf(f10145,plain,(
% 4.14/0.93 ( ! [X1 : $i] : ((lBill_THFTYPE_i != X1) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)) ) | ~spl1_5),
% 4.14/0.93 inference(equality_proxy_clausification,[],[f1351])).
% 4.14/0.93 thf(f10346,plain,(
% 4.14/0.93 spl1_9 | spl1_10 | ~spl1_5),
% 4.14/0.93 inference(avatar_split_clause,[],[f10145,f929,f1366,f1362])).
% 4.14/0.93 thf(f10959,plain,(
% 4.14/0.93 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)) = ((= @ X1)))) ) | ~spl1_9),
% 4.14/0.93 inference(argument_congruence,[],[f1364])).
% 4.14/0.93 thf(f10960,plain,(
% 4.14/0.93 ( ! [X1 : $i] : (((^[Y0 : $i]: ($true)) = ((= @ X1)))) ) | ~spl1_9),
% 4.14/0.93 inference(beta-eta_normalization,[],[f10959])).
% 4.14/0.93 thf(f12328,plain,(
% 4.14/0.93 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 4.14/0.93 inference(constrained_superposition,[],[f288,f351])).
% 4.14/0.93 thf(f12345,plain,(
% 4.14/0.93 ($true != $true) | (((~ (parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i))) = $false) | ~spl1_6),
% 4.14/0.93 inference(constrained_superposition,[],[f933,f288])).
% 4.14/0.93 thf(f12468,plain,(
% 4.14/0.93 ($true != $true) | (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true) | ~spl1_6),
% 4.14/0.93 inference(not_proxy_clausification,[],[f12345])).
% 4.14/0.93 thf(f12469,plain,(
% 4.14/0.93 (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true) | ~spl1_6),
% 4.14/0.93 inference(trivial_inequality_removal,[],[f12468])).
% 4.14/0.93 thf(f12507,plain,(
% 4.14/0.93 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 4.14/0.93 inference(boolean_simplification,[],[f12328])).
% 4.14/0.93 thf(f12509,definition,(
% 4.14/0.93 spl1_683 <=> (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_683])],[avatar_definition])).
% 4.14/0.93 thf(f12511,plain,(
% 4.14/0.93 (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ~spl1_683),
% 4.14/0.93 inference(avatar_component_clause,[],[f12509])).
% 4.14/0.93 thf(f12517,definition,(
% 4.14/0.93 spl1_685 <=> (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true)),
% 4.14/0.93 introduced(definition,[new_symbols(definition,[spl1_685])],[avatar_definition])).
% 4.14/0.93 thf(f12519,plain,(
% 4.14/0.93 (((parent_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $true) | ~spl1_685),
% 4.14/0.93 inference(avatar_component_clause,[],[f12517])).
% 4.14/0.93 thf(f12610,plain,(
% 4.14/0.93 spl1_685 | ~spl1_6),
% 4.14/0.93 inference(avatar_split_clause,[],[f12469,f932,f12517])).
% 4.14/0.93 thf(f12646,plain,(
% 4.14/0.93 spl1_683 | spl1_4),
% 4.14/0.93 inference(avatar_split_clause,[],[f12507,f402,f12509])).
% 4.14/0.93 thf(f12864,plain,(
% 4.14/0.93 ($true = $false) | (~spl1_683 | ~spl1_685)),
% 4.14/0.93 inference(forward_demodulation,[],[f12519,f12511])).
% 4.14/0.93 thf(f12865,plain,(
% 4.14/0.93 $false | (~spl1_683 | ~spl1_685)),
% 4.14/0.93 inference(trivial_inequality_removal,[],[f12864])).
% 4.14/0.93 thf(f12866,plain,(
% 4.14/0.93 ~spl1_683 | ~spl1_685),
% 4.14/0.93 inference(avatar_contradiction_clause,[],[f12865])).
% 4.14/0.93 thf(f12873,plain,(
% 4.14/0.93 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ($true)) @ X2)) = ((X1 = X2)))) ) | ~spl1_9),
% 4.14/0.93 inference(argument_congruence,[],[f10960])).
% 4.14/0.93 thf(f12875,plain,(
% 4.14/0.93 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ($true)) @ X2))) | ($true = ((X1 = X2)))) ) | ~spl1_9),
% 4.14/0.93 inference(iff_proxy_clausification,[],[f12873])).
% 4.14/0.93 thf(f12876,plain,(
% 4.14/0.93 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ($true)) @ X2))) | (X1 = X2)) ) | ~spl1_9),
% 4.14/0.93 inference(equality_proxy_clausification,[],[f12875])).
% 4.14/0.93 thf(f12877,plain,(
% 4.14/0.93 ( ! [X2 : $i,X1 : $i] : (($true = $false) | (X1 = X2)) ) | ~spl1_9),
% 4.14/0.93 inference(beta-eta_normalization,[],[f12876])).
% 4.14/0.93 thf(f12878,plain,(
% 4.14/0.93 ( ! [X2 : $i,X1 : $i] : ((X1 = X2)) ) | ~spl1_9),
% 4.14/0.93 inference(trivial_inequality_removal,[],[f12877])).
% 4.14/0.93 thf(f13182,plain,(
% 4.14/0.93 ( ! [X0 : $i] : (($false = ((parent_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i)))) ) | (~spl1_9 | ~spl1_683)),
% 4.14/0.93 inference(constrained_superposition,[],[f12511,f12878])).
% 4.14/0.93 thf(f14013,plain,(
% 4.14/0.93 $false | ~spl1_10),
% 4.14/0.93 inference(equality_resolution,[],[f1367])).
% 4.14/0.93 thf(f14014,plain,(
% 4.14/0.93 ~spl1_10),
% 4.14/0.93 inference(avatar_contradiction_clause,[],[f14013])).
% 4.14/0.93 thf(f15907,plain,(
% 4.14/0.93 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (~spl1_9 | ~spl1_683)),
% 4.14/0.93 inference(constrained_superposition,[],[f278,f13182])).
% 4.14/0.93 thf(f15964,plain,(
% 4.14/0.93 spl1_4 | ~spl1_9 | ~spl1_683),
% 4.14/0.93 inference(avatar_split_clause,[],[f15907,f12509,f1362,f402])).
% 4.14/0.93 cnf(s2, plain, spl1_3 | ~spl1_4, inference(sat_conversion,[],[f405])).
% 4.14/0.93 cnf(s3, plain, spl1_5 | spl1_6, inference(sat_conversion,[],[f934])).
% 4.14/0.93 cnf(s7, plain, ~spl1_3, inference(sat_conversion,[],[f6790])).
% 4.14/0.93 cnf(s1358, plain, ~spl1_5 | spl1_9 | spl1_10, inference(sat_conversion,[],[f10346])).
% 4.14/0.93 cnf(s1567, plain, ~spl1_6 | spl1_685, inference(sat_conversion,[],[f12610])).
% 4.14/0.93 cnf(s1580, plain, spl1_4 | spl1_683, inference(sat_conversion,[],[f12646])).
% 4.14/0.93 cnf(s1620, plain, ~spl1_683 | ~spl1_685, inference(sat_conversion,[],[f12866])).
% 4.14/0.93 cnf(s1763, plain, ~spl1_10, inference(sat_conversion,[],[f14014])).
% 4.14/0.93 cnf(s1984, plain, spl1_4 | ~spl1_9 | ~spl1_683, inference(sat_conversion,[],[f15964])).
% 4.14/0.93 cnf(s2021, plain, ~spl1_5 | spl1_9, inference(rat,[],[s1358,s1763])).
% 4.14/0.93 cnf(s2025, plain, ~spl1_4, inference(rat,[],[s2,s7])).
% 4.14/0.93 cnf(s2030, plain, spl1_683, inference(rat,[],[s1580,s2025])).
% 4.14/0.93 cnf(s2068, plain, ~spl1_685, inference(rat,[],[s1620,s2030])).
% 4.14/0.93 cnf(s2069, plain, ~spl1_9, inference(rat,[],[s1984,s2025,s2030])).
% 4.14/0.93 cnf(s2251, plain, ~spl1_6, inference(rat,[],[s1567,s2068])).
% 4.14/0.93 cnf(s2258, plain, ~spl1_5, inference(rat,[],[s2021,s2069])).
% 4.14/0.93 cnf(s2261, plain, $false, inference(rat,[],[s3,s2251,s2258])).
% 4.14/0.93 thf(f16070,plain,(
% 4.14/0.93 $false),
% 4.14/0.93 inference(avatar_sat_refutation,[],[s2261])).
% 4.14/0.93 % SZS output end Proof for theBenchmark
% 4.14/0.93 % (2843854)------------------------------
% 4.14/0.93 % (2843854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.14/0.93 % (2843854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.14/0.93 % (2843854)CaDiCaL version: 2.1.3
% 4.14/0.93 % (2843854)Termination reason: Refutation
% 4.14/0.93 % (2843854)Time elapsed: 0.642 s
% 4.14/0.93 % (2843854)Peak memory usage: 18 MB
% 4.14/0.93 % (2843854)Instructions burned: 1279 (million)
% 4.14/0.93 % (2843848)Success in time 0.702 s
% 4.14/0.93 % Vampire exiting
%------------------------------------------------------------------------------