%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR132^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 : n011.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 35.76s 9.71s
% Output : Refutation 35.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR132^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.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 17:55:46 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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.86/0.92 % (437143)Will run a generic schedule for satisfiability detection.
% 3.86/0.92 % (437152)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3321070620:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.86/0.92 % (437152)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.92 % (437149)% WARNING: option uhcvi not known.
% 3.86/0.92 % (437148)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3193712727_2999 on theBenchmark for (2999ds/0Mi)
% 3.86/0.92 % (437149)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4027319110:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.86/0.92 % (437150)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=437370440:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.86/0.92 % (437151)dis+10_1_sil=32000:sp=arity:random_seed=439960934:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.86/0.92 % (437154)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=257256679:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.86/0.92 % (437153)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4159135357:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.86/0.92 % (437149)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.86/0.92 % Exception at run slice level
% 3.86/0.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.92 % (437149)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.86/0.92 % (437152)Instruction limit reached!
% 3.86/0.92 % (437152)------------------------------
% 3.86/0.92 % (437152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.92 % (437152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.92 % (437152)CaDiCaL version: 2.1.3
% 3.86/0.92 % (437152)Termination reason: Instruction limit
% 3.86/0.92 % (437152)Termination phase: Saturation
% 3.86/0.92 % (437152)Time elapsed: 0.026 s
% 3.86/0.92 % (437152)Peak memory usage: 13 MB
% 3.86/0.92 % (437152)Instructions burned: 118 (million)
% 3.86/0.92 % (437162)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=70042162:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.86/0.92 % (437163)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2022990570:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.86/0.92 % Exception at run slice level
% 3.86/0.92 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.86/0.92 % (437151)Instruction limit reached!
% 3.86/0.92 % (437151)------------------------------
% 3.86/0.92 % (437151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.92 % (437151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.92 % (437151)CaDiCaL version: 2.1.3
% 3.86/0.92 % (437151)Termination reason: Instruction limit
% 3.86/0.92 % (437151)Termination phase: Saturation
% 3.86/0.92 % (437151)Time elapsed: 0.043 s
% 3.86/0.92 % (437151)Peak memory usage: 12 MB
% 3.86/0.92 % (437151)Instructions burned: 103 (million)
% 3.86/0.92 % (437153)Instruction limit reached!
% 3.86/0.92 % (437153)------------------------------
% 3.86/0.92 % (437153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.92 % (437153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.92 % (437153)CaDiCaL version: 2.1.3
% 3.86/0.92 % (437153)Termination reason: Instruction limit
% 3.86/0.92 % (437153)Termination phase: Saturation
% 3.86/0.92 % (437153)Time elapsed: 0.057 s
% 3.86/0.92 % (437153)Peak memory usage: 13 MB
% 3.86/0.92 % (437153)Instructions burned: 132 (million)
% 3.86/0.92 % (437166)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=2480031167:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.86/0.92 % (437163)Instruction limit reached!
% 3.86/0.92 % (437163)------------------------------
% 3.86/0.92 % (437163)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.86/0.92 % (437163)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/0.92 % (437163)CaDiCaL version: 2.1.3
% 3.86/0.92 % (437163)Termination reason: Instruction limit
% 3.86/0.92 % (437163)Termination phase: Saturation
% 16.97/2.78 % (437163)Time elapsed: 0.031 s
% 16.97/2.78 % (437163)Peak memory usage: 13 MB
% 16.97/2.78 % (437163)Instructions burned: 131 (million)
% 16.97/2.78 % (437167)ott-21_1_sil=16000:fs=off:random_seed=1133799884:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 16.97/2.78 % (437166)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.97/2.78 % (437154)Instruction limit reached!
% 16.97/2.78 % (437154)------------------------------
% 16.97/2.78 % (437154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.78 % (437154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.78 % (437154)CaDiCaL version: 2.1.3
% 16.97/2.78 % (437154)Termination reason: Instruction limit
% 16.97/2.78 % (437154)Termination phase: Saturation
% 16.97/2.78 % (437154)Time elapsed: 0.070 s
% 16.97/2.78 % (437154)Peak memory usage: 13 MB
% 16.97/2.78 % (437154)Instructions burned: 159 (million)
% 16.97/2.78 % (437170)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4251410122:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 16.97/2.78 % (437166)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 16.97/2.78 % Exception at run slice level
% 16.97/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.97/2.78 % (437168)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3717750820:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 16.97/2.78 % (437175)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3943352856:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 16.97/2.78 % (437172)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1377806798:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 16.97/2.78 % Exception at run slice level
% 16.97/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.97/2.78 % (437178)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=2936078276: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)
% 16.97/2.78 % (437178)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.97/2.78 % (437167)Instruction limit reached!
% 16.97/2.78 % (437167)------------------------------
% 16.97/2.78 % (437167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.78 % (437167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.78 % (437167)CaDiCaL version: 2.1.3
% 16.97/2.78 % (437167)Termination reason: Instruction limit
% 16.97/2.78 % (437167)Termination phase: Saturation
% 16.97/2.78 % (437167)Time elapsed: 0.076 s
% 16.97/2.78 % (437167)Peak memory usage: 13 MB
% 16.97/2.78 % (437167)Instructions burned: 180 (million)
% 16.97/2.78 % (437190)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2760580411:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 16.97/2.78 % (437190)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 16.97/2.78 % (437178)Instruction limit reached!
% 16.97/2.78 % (437178)------------------------------
% 16.97/2.78 % (437178)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.78 % (437178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.78 % (437178)CaDiCaL version: 2.1.3
% 16.97/2.78 % (437178)Termination reason: Instruction limit
% 16.97/2.78 % (437178)Termination phase: Saturation
% 16.97/2.78 % (437178)Time elapsed: 0.159 s
% 16.97/2.78 % (437178)Peak memory usage: 15 MB
% 16.97/2.78 % (437178)Instructions burned: 695 (million)
% 16.97/2.78 % (437248)fmb+10_1_sil=64000:random_seed=4047768874:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 16.97/2.78 % (437248)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 16.97/2.78 % Exception at run slice level
% 16.97/2.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 16.97/2.78 % (437168)Instruction limit reached!
% 16.97/2.78 % (437168)------------------------------
% 16.97/2.78 % (437168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.97/2.78 % (437168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.97/2.78 % (437168)CaDiCaL version: 2.1.3
% 16.97/2.78 % (437168)Termination reason: Instruction limit
% 43.80/6.46 % (437168)Termination phase: Saturation
% 43.80/6.46 % (437168)Time elapsed: 0.212 s
% 43.80/6.46 % (437168)Peak memory usage: 14 MB
% 43.80/6.46 % (437168)Instructions burned: 479 (million)
% 43.80/6.46 % (437254)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2617992691:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 43.80/6.46 % Exception at run slice level
% 43.80/6.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.80/6.46 % (437258)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1082001561:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 43.80/6.46 % (437260)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4066179308:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 43.80/6.46 % (437260)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 43.80/6.46 % Exception at run slice level
% 43.80/6.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.80/6.46 % (437270)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2181834761:i=1472:ins=7:fdi=8:gsp=on_2996 on theBenchmark for (2996ds/1472Mi)
% 43.80/6.46 % (437270)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 43.80/6.46 % (437270)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 43.80/6.46 % (437166)Instruction limit reached!
% 43.80/6.46 % (437166)------------------------------
% 43.80/6.46 % (437166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.80/6.46 % (437166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.80/6.46 % (437166)CaDiCaL version: 2.1.3
% 43.80/6.46 % (437166)Termination reason: Instruction limit
% 43.80/6.46 % (437166)Termination phase: Saturation
% 43.80/6.46 % (437166)Time elapsed: 0.320 s
% 43.80/6.46 % (437166)Peak memory usage: 15 MB
% 43.80/6.46 % (437166)Instructions burned: 684 (million)
% 43.80/6.46 % (437290)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2925910117:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 43.80/6.46 % Exception at run slice level
% 43.80/6.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.80/6.46 % (437304)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=404885426:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 43.80/6.46 % Exception at run slice level
% 43.80/6.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.80/6.46 % (437317)ott-2_1_sil=16000:newcnf=on:random_seed=1120851827:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 43.80/6.46 % (437317)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 43.80/6.46 % (437190)Instruction limit reached!
% 43.80/6.46 % (437190)------------------------------
% 43.80/6.46 % (437190)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.80/6.46 % (437190)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.80/6.46 % (437190)CaDiCaL version: 2.1.3
% 43.80/6.46 % (437190)Termination reason: Instruction limit
% 43.80/6.46 % (437190)Termination phase: Saturation
% 43.80/6.46 % (437190)Time elapsed: 0.391 s
% 43.80/6.46 % (437190)Peak memory usage: 16 MB
% 43.80/6.46 % (437190)Instructions burned: 880 (million)
% 43.80/6.46 % (437350)ott+10_1_sil=32000:tgt=ground:random_seed=761260843:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 43.80/6.46 % (437172)Instruction limit reached!
% 43.80/6.46 % (437172)------------------------------
% 43.80/6.46 % (437172)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.80/6.46 % (437172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.80/6.46 % (437172)CaDiCaL version: 2.1.3
% 43.80/6.46 % (437172)Termination reason: Instruction limit
% 43.80/6.46 % (437172)Termination phase: Saturation
% 43.80/6.46 % (437172)Time elapsed: 0.524 s
% 43.80/6.46 % (437172)Peak memory usage: 16 MB
% 43.80/6.46 % (437172)Instructions burned: 1179 (million)
% 43.80/6.46 % (437352)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3302746025:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 43.80/6.46 % Exception at run slice level
% 43.80/6.46 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 43.80/6.46 % (437354)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2414464780:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 35.76/9.70 % (437354)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.76/9.70 % (437317)Instruction limit reached!
% 35.76/9.70 % (437317)------------------------------
% 35.76/9.70 % (437317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.70 % (437317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.70 % (437317)CaDiCaL version: 2.1.3
% 35.76/9.70 % (437317)Termination reason: Instruction limit
% 35.76/9.70 % (437317)Termination phase: Saturation
% 35.76/9.70 % (437317)Time elapsed: 0.372 s
% 35.76/9.70 % (437317)Peak memory usage: 16 MB
% 35.76/9.70 % (437317)Instructions burned: 871 (million)
% 35.76/9.70 % (437356)dis+21_1_sil=32000:sas=cadical:random_seed=90364212:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 35.76/9.70 % (437270)Instruction limit reached!
% 35.76/9.70 % (437270)------------------------------
% 35.76/9.70 % (437270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.70 % (437270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.70 % (437270)CaDiCaL version: 2.1.3
% 35.76/9.70 % (437270)Termination reason: Instruction limit
% 35.76/9.70 % (437270)Termination phase: Saturation
% 35.76/9.70 % (437270)Time elapsed: 0.666 s
% 35.76/9.70 % (437270)Peak memory usage: 18 MB
% 35.76/9.70 % (437270)Instructions burned: 1473 (million)
% 35.76/9.70 % (437358)ott+11_1_sil=16000:gs=on:random_seed=3409141579:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2989 on theBenchmark for (2989ds/2251Mi)
% 35.76/9.70 % (437358)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.76/9.70 % (437260)Instruction limit reached!
% 35.76/9.70 % (437260)------------------------------
% 35.76/9.70 % (437260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.70 % (437260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.70 % (437260)CaDiCaL version: 2.1.3
% 35.76/9.70 % (437260)Termination reason: Instruction limit
% 35.76/9.70 % (437260)Termination phase: Saturation
% 35.76/9.70 % (437260)Time elapsed: 1.182 s
% 35.76/9.70 % (437260)Peak memory usage: 25 MB
% 35.76/9.70 % (437260)Instructions burned: 5134 (million)
% 35.76/9.70 % (437360)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2748317322:fmbsr=1.6:i=67534_2984 on theBenchmark for (2984ds/67534Mi)
% 35.76/9.70 % Exception at run slice level
% 35.76/9.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.76/9.70 % (437362)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2027631046:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2984 on theBenchmark for (2984ds/4591Mi)
% 35.76/9.70 % (437358)Instruction limit reached!
% 35.76/9.70 % (437358)------------------------------
% 35.76/9.70 % (437358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.70 % (437358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.70 % (437358)CaDiCaL version: 2.1.3
% 35.76/9.70 % (437358)Termination reason: Instruction limit
% 35.76/9.70 % (437358)Termination phase: Saturation
% 35.76/9.70 % (437358)Time elapsed: 1.031 s
% 35.76/9.71 % (437358)Peak memory usage: 21 MB
% 35.76/9.71 % (437358)Instructions burned: 2253 (million)
% 35.76/9.71 % (437364)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=764420658:i=29340_2979 on theBenchmark for (2979ds/29340Mi)
% 35.76/9.71 % (437354)Instruction limit reached!
% 35.76/9.71 % (437354)------------------------------
% 35.76/9.71 % (437354)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437354)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437354)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437354)Termination reason: Instruction limit
% 35.76/9.71 % (437354)Termination phase: Saturation
% 35.76/9.71 % (437354)Time elapsed: 1.559 s
% 35.76/9.71 % (437354)Peak memory usage: 22 MB
% 35.76/9.71 % (437354)Instructions burned: 3514 (million)
% 35.76/9.71 % (437366)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=905769317:i=5211_2977 on theBenchmark for (2977ds/5211Mi)
% 35.76/9.71 % (437356)Instruction limit reached!
% 35.76/9.71 % (437356)------------------------------
% 35.76/9.71 % (437356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437356)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437356)Termination reason: Instruction limit
% 35.76/9.71 % (437356)Termination phase: Saturation
% 35.76/9.71 % (437356)Time elapsed: 1.674 s
% 35.76/9.71 % (437356)Peak memory usage: 24 MB
% 35.76/9.71 % (437356)Instructions burned: 3774 (million)
% 35.76/9.71 % (437368)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2640574975:i=5497:nm=2_2974 on theBenchmark for (2974ds/5497Mi)
% 35.76/9.71 % Exception at run slice level
% 35.76/9.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.76/9.71 % (437362)Instruction limit reached!
% 35.76/9.71 % (437362)------------------------------
% 35.76/9.71 % (437362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437362)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437362)Termination reason: Instruction limit
% 35.76/9.71 % (437362)Termination phase: Saturation
% 35.76/9.71 % (437362)Time elapsed: 1.054 s
% 35.76/9.71 % (437362)Peak memory usage: 23 MB
% 35.76/9.71 % (437362)Instructions burned: 4592 (million)
% 35.76/9.71 % (437370)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=531394815:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 35.76/9.71 % (437371)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=763378052:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 35.76/9.71 % Exception at run slice level
% 35.76/9.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.76/9.71 % Exception at run slice level
% 35.76/9.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.76/9.71 % (437374)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3231196899:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 35.76/9.71 % (437375)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2680758924:i=8173:av=off_2973 on theBenchmark for (2973ds/8173Mi)
% 35.76/9.71 % (437350)Instruction limit reached!
% 35.76/9.71 % (437350)------------------------------
% 35.76/9.71 % (437350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437350)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437350)Termination reason: Instruction limit
% 35.76/9.71 % (437350)Termination phase: Saturation
% 35.76/9.71 % (437350)Time elapsed: 2.183 s
% 35.76/9.71 % (437350)Peak memory usage: 22 MB
% 35.76/9.71 % (437350)Instructions burned: 5116 (million)
% 35.76/9.71 % (437378)dis+10_16:1_sil=16000:random_seed=837159216:i=9155:fsr=off_2972 on theBenchmark for (2972ds/9155Mi)
% 35.76/9.71 % (437366)Instruction limit reached!
% 35.76/9.71 % (437366)------------------------------
% 35.76/9.71 % (437366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437366)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437366)Termination reason: Instruction limit
% 35.76/9.71 % (437366)Termination phase: Saturation
% 35.76/9.71 % (437366)Time elapsed: 2.329 s
% 35.76/9.71 % (437366)Peak memory usage: 30 MB
% 35.76/9.71 % (437366)Instructions burned: 5211 (million)
% 35.76/9.71 % (437380)ott-3_8_sil=64000:random_seed=2418414860:i=20139:bs=on_2953 on theBenchmark for (2953ds/20139Mi)
% 35.76/9.71 % (437375)Instruction limit reached!
% 35.76/9.71 % (437375)------------------------------
% 35.76/9.71 % (437375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437375)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437375)Termination reason: Instruction limit
% 35.76/9.71 % (437375)Termination phase: Saturation
% 35.76/9.71 % (437375)Time elapsed: 3.539 s
% 35.76/9.71 % (437375)Peak memory usage: 28 MB
% 35.76/9.71 % (437375)Instructions burned: 8173 (million)
% 35.76/9.71 % (437383)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2930646111:fmbsr=2:i=32576_2938 on theBenchmark for (2938ds/32576Mi)
% 35.76/9.71 % Exception at run slice level
% 35.76/9.71 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.76/9.71 % (437385)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3111658047:i=11404_2937 on theBenchmark for (2937ds/11404Mi)
% 35.76/9.71 % (437378)Instruction limit reached!
% 35.76/9.71 % (437378)------------------------------
% 35.76/9.71 % (437378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437378)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437378)Termination reason: Instruction limit
% 35.76/9.71 % (437378)Termination phase: Saturation
% 35.76/9.71 % (437378)Time elapsed: 3.838 s
% 35.76/9.71 % (437378)Peak memory usage: 33 MB
% 35.76/9.71 % (437378)Instructions burned: 9156 (million)
% 35.76/9.71 % (437387)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1808610026:i=14134_2933 on theBenchmark for (2933ds/14134Mi)
% 35.76/9.71 % (437387)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.76/9.71 % (437374)Instruction limit reached!
% 35.76/9.71 % (437374)------------------------------
% 35.76/9.71 % (437374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437374)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437374)Termination reason: Instruction limit
% 35.76/9.71 % (437374)Termination phase: Saturation
% 35.76/9.71 % (437374)Time elapsed: 5.129 s
% 35.76/9.71 % (437374)Peak memory usage: 71 MB
% 35.76/9.71 % (437374)Instructions burned: 22567 (million)
% 35.76/9.71 % (437389)dis+33_16_sil=32000:sac=on:random_seed=295202127:i=15851:nm=0_2922 on theBenchmark for (2922ds/15851Mi)
% 35.76/9.71 % (437387) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-437143-437387"...
% 35.76/9.71 % (437387)...printing done.
% 35.76/9.71 % (437387)Refutation found. Thanks to Tanya!
% 35.76/9.71 % SZS status Theorem for theBenchmark
% 35.76/9.71 % SZS output start Proof for theBenchmark
% 35.76/9.71 thf(type_def_5, type, num: $tType).
% 35.76/9.71 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 35.76/9.71 thf(func_def_0, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_2, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 35.76/9.71 thf(func_def_3, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 35.76/9.71 thf(func_def_4, type, disjointDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_5, type, disjointDecomposition_THFTYPE_IioI: ($i > $o)).
% 35.76/9.71 thf(func_def_6, type, disjointRelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_7, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_8, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_10, type, domainSubclass_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_11, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 35.76/9.71 thf(func_def_12, type, domain_THFTYPE_IIIioIiioIiioI: ((($i > $o) > $i > $i > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_13, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_14, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_15, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_16, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_17, type, domain_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_18, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 35.76/9.71 thf(func_def_19, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 35.76/9.71 thf(func_def_21, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 35.76/9.71 thf(func_def_22, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_23, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_24, type, instance_THFTYPE_IIIioIiioIioI: ((($i > $o) > $i > $i > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_25, type, instance_THFTYPE_IIiIiioIoIioI: (($i > ($i > $i > $o) > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_26, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 35.76/9.71 thf(func_def_27, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 35.76/9.71 thf(func_def_28, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_29, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_30, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_31, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_32, type, instrument_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_33, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 35.76/9.71 thf(func_def_38, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 35.76/9.71 thf(func_def_47, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 35.76/9.71 thf(func_def_58, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 35.76/9.71 thf(func_def_60, type, lListOrderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 35.76/9.71 thf(func_def_81, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 35.76/9.71 thf(func_def_83, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 35.76/9.71 thf(func_def_84, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_85, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_86, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_87, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_93, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 35.76/9.71 thf(func_def_94, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_95, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_98, type, property_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_99, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_101, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_102, type, relatedInternalConcept_THFTYPE_IIioIIiioIoI: (($i > $o) > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_103, type, relatedInternalConcept_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_104, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_106, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_107, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_108, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_109, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_110, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 35.76/9.71 thf(func_def_111, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 35.76/9.71 thf(func_def_112, type, subrelation_THFTYPE_IIoooIIiioIoI: (($o > $o > $o) > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_113, type, subrelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 35.76/9.71 thf(func_def_114, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_115, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 35.76/9.71 thf(func_def_116, type, truth_THFTYPE_IoooI: ($o > $o > $o)).
% 35.76/9.71 thf(func_def_118, type, vNOT: ($o > $o)).
% 35.76/9.71 thf(func_def_121, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 35.76/9.71 thf(func_def_122, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 35.76/9.71 thf(func_def_123, type, db0: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(func_def_124, type, db1: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(func_def_125, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 35.76/9.71 thf(func_def_126, type, vAND: ($o > $o > $o)).
% 35.76/9.71 thf(func_def_127, type, sK0: ($i > $i)).
% 35.76/9.71 thf(func_def_128, type, sK1: ($i > $i)).
% 35.76/9.71 thf(func_def_129, type, sK2: ($i > $i > $i)).
% 35.76/9.71 thf(func_def_131, type, sK4: (($i > $i > $o) > $i)).
% 35.76/9.71 thf(func_def_132, type, sK5: ($i > $i > $i)).
% 35.76/9.71 thf(func_def_133, type, sK6: ($i > $i)).
% 35.76/9.71 thf(func_def_134, type, sK7: ($i > $i)).
% 35.76/9.71 thf(func_def_135, type, sK8: ($i > $i > $i)).
% 35.76/9.71 thf(func_def_136, type, db2: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(func_def_138, type, db3: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(func_def_139, type, db4: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(func_def_140, type, db5: !>[X0: $tType]:(X0)).
% 35.76/9.71 thf(f1,axiom,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i))),
% 35.76/9.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax)).
% 35.76/9.71 thf(f29,axiom,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X0 : $i,X1 : $i] : (~ (parent_THFTYPE_IiioI @ X0 @ X1)))),
% 35.76/9.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_028)).
% 35.76/9.71 thf(f35,axiom,(
% 35.76/9.71 ! [X0 : $i,X1 : $o] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 35.76/9.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_034)).
% 35.76/9.71 thf(f81,axiom,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))),
% 35.76/9.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_080)).
% 35.76/9.71 thf(f218,conjecture,(
% 35.76/9.71 ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 = (^[X3 : $i, X4 : $i] : ($true)))) & (~ (X1 = (^[X3 : $i, X4 : $i] : ($true)))) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 35.76/9.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 35.76/9.71 thf(f219,negated_conjecture,(
% 35.76/9.71 ~ ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 = (^[X3 : $i, X4 : $i] : ($true)))) & (~ (X1 = (^[X3 : $i, X4 : $i] : ($true)))) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 35.76/9.71 inference(negated_conjecture,[status(cth)],[f218])).
% 35.76/9.71 thf(f220,plain,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i))),
% 35.76/9.71 inference(rectify,[],[f1])).
% 35.76/9.71 thf(f221,plain,(
% 35.76/9.71 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 35.76/9.71 inference(fool_elimination,[],[f220])).
% 35.76/9.71 thf(f276,plain,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ? [X0 : $i,X1 : $i] : (~ (parent_THFTYPE_IiioI @ X0 @ X1)))),
% 35.76/9.71 inference(rectify,[],[f29])).
% 35.76/9.71 thf(f277,plain,(
% 35.76/9.71 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y1 @ Y0)))))))))),
% 35.76/9.71 inference(fool_elimination,[],[f276])).
% 35.76/9.71 thf(f288,plain,(
% 35.76/9.71 ! [X0 : $i,X1 : $o] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 35.76/9.71 inference(rectify,[],[f35])).
% 35.76/9.71 thf(f289,plain,(
% 35.76/9.71 ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) = $true) => (((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true))),
% 35.76/9.71 inference(fool_elimination,[],[f288])).
% 35.76/9.71 thf(f378,plain,(
% 35.76/9.71 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))),
% 35.76/9.71 inference(rectify,[],[f81])).
% 35.76/9.71 thf(f379,plain,(
% 35.76/9.71 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 35.76/9.71 inference(fool_elimination,[],[f378])).
% 35.76/9.71 thf(f650,plain,(
% 35.76/9.71 ~ ? [X0 : ($i > $i > $o),X1 : ($i > $i > $o),X2 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 = (^[X3 : $i, X4 : $i] : ($true)))) & (~ (X1 = (^[X5 : $i, X6 : $i] : ($true)))) & (X0 @ X2 @ lAnna_THFTYPE_i) & (X1 @ X2 @ lBill_THFTYPE_i))),
% 35.76/9.71 inference(rectify,[],[f219])).
% 35.76/9.71 thf(f651,plain,(
% 35.76/9.71 ~ ? [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)) & (~ (X1 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))))))),
% 35.76/9.71 inference(fool_elimination,[],[f650])).
% 35.76/9.71 thf(f671,plain,(
% 35.76/9.71 ! [X0 : $i,X1 : $o] : ((((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true))),
% 35.76/9.71 inference(ennf_transformation,[],[f289])).
% 35.76/9.71 thf(f722,plain,(
% 35.76/9.71 ! [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)) & (~ (X1 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))))))),
% 35.76/9.71 inference(ennf_transformation,[],[f651])).
% 35.76/9.71 thf(f739,plain,(
% 35.76/9.71 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 35.76/9.71 inference(cnf_transformation,[],[f221])).
% 35.76/9.71 thf(f769,plain,(
% 35.76/9.71 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y1 @ Y0)))))))))),
% 35.76/9.71 inference(cnf_transformation,[],[f277])).
% 35.76/9.71 thf(f775,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $o] : ((((~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1))) = $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true)) )),
% 35.76/9.71 inference(cnf_transformation,[],[f671])).
% 35.76/9.71 thf(f826,plain,(
% 35.76/9.71 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 35.76/9.71 inference(cnf_transformation,[],[f379])).
% 35.76/9.71 thf(f963,plain,(
% 35.76/9.71 ( ! [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)) & (~ (X1 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))))))) )),
% 35.76/9.71 inference(cnf_transformation,[],[f722])).
% 35.76/9.71 thf(f965,definition,(
% 35.76/9.71 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 35.76/9.71 introduced(theory,[fool_exhaustiveness_axiom])).
% 35.76/9.71 thf(f992,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1))) != $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false)) )),
% 35.76/9.71 inference(not_proxy_clausification,[],[f775])).
% 35.76/9.71 thf(f1085,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : $o,X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) & (~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) | ($false = X0)) )),
% 35.76/9.71 inference(constrained_superposition,[],[f963,f965])).
% 35.76/9.71 thf(f1161,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = (((((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) & (~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) )),
% 35.76/9.71 inference(constrained_superposition,[],[f963,f965])).
% 35.76/9.71 thf(f1164,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) | ($false = ((((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) )),
% 35.76/9.71 inference(and_proxy_clausification,[],[f1161])).
% 35.76/9.71 thf(f1165,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($true = ((X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) | ($false = ((((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) )),
% 35.76/9.71 inference(not_proxy_clausification,[],[f1164])).
% 35.76/9.71 thf(f1166,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($false = ((((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) )),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f1165])).
% 35.76/9.71 thf(f1167,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (((~ (X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) = $false) | ($false = (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i))))) )),
% 35.76/9.71 inference(and_proxy_clausification,[],[f1166])).
% 35.76/9.71 thf(f1168,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($true = ((X0 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))))) | ($false = (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i))))) )),
% 35.76/9.71 inference(not_proxy_clausification,[],[f1167])).
% 35.76/9.71 thf(f1169,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ($false = (((X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i))))) )),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f1168])).
% 35.76/9.71 thf(f1170,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i)))) )),
% 35.76/9.71 inference(and_proxy_clausification,[],[f1169])).
% 35.76/9.71 thf(f1323,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : $o,X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 & (X2 @ X1 @ lAnna_THFTYPE_i)) & (~ $true)) & (~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) | ($false = X0)) )),
% 35.76/9.71 inference(boolean_simplification,[],[f1085])).
% 35.76/9.71 thf(f1324,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : $o,X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 & (X2 @ X1 @ lAnna_THFTYPE_i)) & $false) & (~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) | ($false = X0)) )),
% 35.76/9.71 inference(boolean_simplification,[],[f1323])).
% 35.76/9.71 thf(f1325,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($false & (~ (X2 = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))))) | ($false = X0)) )),
% 35.76/9.71 inference(boolean_simplification,[],[f1324])).
% 35.76/9.71 thf(f1326,plain,(
% 35.76/9.71 ( ! [X0 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($false = X0)) )),
% 35.76/9.71 inference(boolean_simplification,[],[f1325])).
% 35.76/9.71 thf(f1501,definition,(
% 35.76/9.71 spl9_1 <=> ! [X0 : $o] : ($false = X0)),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition])).
% 35.76/9.71 thf(f1502,plain,(
% 35.76/9.71 ( ! [X0 : $o] : (($false = X0)) ) | ~spl9_1),
% 35.76/9.71 inference(avatar_component_clause,[],[f1501])).
% 35.76/9.71 thf(f1504,definition,(
% 35.76/9.71 spl9_2 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition])).
% 35.76/9.71 thf(f1506,plain,(
% 35.76/9.71 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl9_2),
% 35.76/9.71 inference(avatar_component_clause,[],[f1504])).
% 35.76/9.71 thf(f1507,plain,(
% 35.76/9.71 spl9_1 | ~spl9_2),
% 35.76/9.71 inference(avatar_split_clause,[],[f1326,f1504,f1501])).
% 35.76/9.71 thf(f1576,definition,(
% 35.76/9.71 spl9_4 <=> ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition])).
% 35.76/9.71 thf(f1577,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) ) | ~spl9_4),
% 35.76/9.71 inference(avatar_component_clause,[],[f1576])).
% 35.76/9.71 thf(f1579,definition,(
% 35.76/9.71 spl9_5 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_5])],[avatar_definition])).
% 35.76/9.71 thf(f1580,plain,(
% 35.76/9.71 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ~spl9_5),
% 35.76/9.71 inference(avatar_component_clause,[],[f1579])).
% 35.76/9.71 thf(f1581,plain,(
% 35.76/9.71 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | spl9_5),
% 35.76/9.71 inference(avatar_component_clause,[],[f1579])).
% 35.76/9.71 thf(f1582,plain,(
% 35.76/9.71 spl9_4 | ~spl9_5),
% 35.76/9.71 inference(avatar_split_clause,[],[f1170,f1579,f1576])).
% 35.76/9.71 thf(f1595,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o),X1 : $i] : (($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ X1 @ lAnna_THFTYPE_i))) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))))) ) | ~spl9_4),
% 35.76/9.71 inference(primitive_instantiation,[],[f1577])).
% 35.76/9.71 thf(f1600,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1))))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) ) | ~spl9_4),
% 35.76/9.71 inference(primitive_instantiation,[],[f1577])).
% 35.76/9.71 thf(f2957,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ($false = ((X1 = lBill_THFTYPE_i))) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) ) | ~spl9_4),
% 35.76/9.71 inference(beta-eta_normalization,[],[f1600])).
% 35.76/9.71 thf(f2958,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | (lBill_THFTYPE_i != X1) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2)) ) | ~spl9_4),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f2957])).
% 35.76/9.71 thf(f2965,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o),X1 : $i] : (($false = ((X1 = lAnna_THFTYPE_i))) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) ) | ~spl9_4),
% 35.76/9.71 inference(beta-eta_normalization,[],[f1595])).
% 35.76/9.71 thf(f2966,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o),X1 : $i] : ((lAnna_THFTYPE_i != X1) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))) ) | ~spl9_4),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f2965])).
% 35.76/9.71 thf(f3004,definition,(
% 35.76/9.71 spl9_6 <=> (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition])).
% 35.76/9.71 thf(f3005,plain,(
% 35.76/9.71 (= != (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | spl9_6),
% 35.76/9.71 inference(avatar_component_clause,[],[f3004])).
% 35.76/9.71 thf(f3006,plain,(
% 35.76/9.71 (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl9_6),
% 35.76/9.71 inference(avatar_component_clause,[],[f3004])).
% 35.76/9.71 thf(f3008,definition,(
% 35.76/9.71 spl9_7 <=> ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X2 @ X1 @ lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | (lBill_THFTYPE_i != X1))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition])).
% 35.76/9.71 thf(f3009,plain,(
% 35.76/9.71 ( ! [X2 : ($i > $i > $o),X1 : $i] : ((lBill_THFTYPE_i != X1) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X2) | ($false = ((X2 @ X1 @ lAnna_THFTYPE_i)))) ) | ~spl9_7),
% 35.76/9.71 inference(avatar_component_clause,[],[f3008])).
% 35.76/9.71 thf(f3010,plain,(
% 35.76/9.71 spl9_6 | spl9_7 | ~spl9_4),
% 35.76/9.71 inference(avatar_split_clause,[],[f2958,f1576,f3008,f3004])).
% 35.76/9.71 thf(f3023,plain,(
% 35.76/9.71 ( ! [X0 : $o] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0)) != X0) | ($false = X0)) ) | spl9_5),
% 35.76/9.71 inference(constrained_superposition,[],[f1581,f965])).
% 35.76/9.71 thf(f3027,plain,(
% 35.76/9.71 ( ! [X0 : $o] : (($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0))) | ($false = X0) | ($false = X0)) ) | spl9_5),
% 35.76/9.71 inference(xor_proxy_clausification,[],[f3023])).
% 35.76/9.71 thf(f3028,plain,(
% 35.76/9.71 ( ! [X0 : $o] : (($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ X0))) | ($false = X0)) ) | spl9_5),
% 35.76/9.71 inference(duplicate_literal_removal,[],[f3027])).
% 35.76/9.71 thf(f4836,definition,(
% 35.76/9.71 spl9_8 <=> ! [X2 : $i,X1 : ($i > $i > $o)] : ((((X1 @ X2 @ lBill_THFTYPE_i)) = $false) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X1) | (lAnna_THFTYPE_i != X2))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition])).
% 35.76/9.71 thf(f4837,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : ($i > $i > $o)] : ((lAnna_THFTYPE_i != X2) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X1) | (((X1 @ X2 @ lBill_THFTYPE_i)) = $false)) ) | ~spl9_8),
% 35.76/9.71 inference(avatar_component_clause,[],[f4836])).
% 35.76/9.71 thf(f4879,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o)] : (($false = ((X0 @ lAnna_THFTYPE_i @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) ) | ~spl9_8),
% 35.76/9.71 inference(equality_resolution,[],[f4837])).
% 35.76/9.71 thf(f4916,plain,(
% 35.76/9.71 ($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ lAnna_THFTYPE_i @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1))))) | ~spl9_8),
% 35.76/9.71 inference(primitive_instantiation,[],[f4879])).
% 35.76/9.71 thf(f5414,plain,(
% 35.76/9.71 ($false = ((lAnna_THFTYPE_i = lBill_THFTYPE_i))) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl9_8),
% 35.76/9.71 inference(beta-eta_normalization,[],[f4916])).
% 35.76/9.71 thf(f5415,plain,(
% 35.76/9.71 (lBill_THFTYPE_i != lAnna_THFTYPE_i) | (= = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl9_8),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f5414])).
% 35.76/9.71 thf(f5459,definition,(
% 35.76/9.71 spl9_10 <=> (lBill_THFTYPE_i = lAnna_THFTYPE_i)),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_10])],[avatar_definition])).
% 35.76/9.71 thf(f5462,plain,(
% 35.76/9.71 spl9_6 | ~spl9_10 | ~spl9_8),
% 35.76/9.71 inference(avatar_split_clause,[],[f5415,f4836,f5459,f3004])).
% 35.76/9.71 thf(f5527,plain,(
% 35.76/9.71 ( ! [X1 : $i] : ((((= @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)))) ) | ~spl9_6),
% 35.76/9.71 inference(argument_congruence,[],[f3006])).
% 35.76/9.71 thf(f5531,plain,(
% 35.76/9.71 ( ! [X1 : $i] : ((((= @ X1)) = (^[Y0 : $i]: ($true)))) ) | ~spl9_6),
% 35.76/9.71 inference(beta-eta_normalization,[],[f5527])).
% 35.76/9.71 thf(f5596,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : ((((X1 = X2)) = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl9_6),
% 35.76/9.71 inference(argument_congruence,[],[f5531])).
% 35.76/9.71 thf(f5597,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (($true = ((X1 = X2))) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl9_6),
% 35.76/9.71 inference(iff_proxy_clausification,[],[f5596])).
% 35.76/9.71 thf(f5601,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : ((X1 = X2) | ($false = (((^[Y0 : $i]: ($true)) @ X2)))) ) | ~spl9_6),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f5597])).
% 35.76/9.71 thf(f29854,plain,(
% 35.76/9.71 ($true = $false) | (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i)) = $false) | spl9_5),
% 35.76/9.71 inference(constrained_superposition,[],[f3028,f739])).
% 35.76/9.71 thf(f29857,plain,(
% 35.76/9.71 (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBen_THFTYPE_i)) = $false) | spl9_5),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f29854])).
% 35.76/9.71 thf(f30010,plain,(
% 35.76/9.71 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl9_5),
% 35.76/9.71 inference(constrained_superposition,[],[f739,f29857])).
% 35.76/9.71 thf(f30028,plain,(
% 35.76/9.71 $false | (spl9_2 | spl9_5)),
% 35.76/9.71 inference(forward_subsumption_resolution,[],[f30010,f1506])).
% 35.76/9.71 thf(f30029,plain,(
% 35.76/9.71 spl9_2 | spl9_5),
% 35.76/9.71 inference(avatar_contradiction_clause,[],[f30028])).
% 35.76/9.71 thf(f30035,plain,(
% 35.76/9.71 ($true = $false) | (~spl9_1 | spl9_5)),
% 35.76/9.71 inference(forward_demodulation,[],[f30010,f1502])).
% 35.76/9.71 thf(f30036,plain,(
% 35.76/9.71 $false | (~spl9_1 | spl9_5)),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f30035])).
% 35.76/9.71 thf(f30037,plain,(
% 35.76/9.71 ~spl9_1 | spl9_5),
% 35.76/9.71 inference(avatar_contradiction_clause,[],[f30036])).
% 35.76/9.71 thf(f30044,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : ((X1 = X2) | ($true = $false)) ) | ~spl9_6),
% 35.76/9.71 inference(beta-eta_normalization,[],[f5601])).
% 35.76/9.71 thf(f30045,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : ((X1 = X2)) ) | ~spl9_6),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f30044])).
% 35.76/9.71 thf(f32529,plain,(
% 35.76/9.71 ( ! [X0 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ X0 @ $true)))) ) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(constrained_superposition,[],[f1580,f30045])).
% 35.76/9.71 thf(f32627,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ X0 @ $true))) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((~ X1)) = $false)) )),
% 35.76/9.71 inference(constrained_superposition,[],[f992,f965])).
% 35.76/9.71 thf(f32647,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $o] : (($true != ((holdsDuring_THFTYPE_IiooI @ X0 @ $true))) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) )),
% 35.76/9.71 inference(not_proxy_clausification,[],[f32627])).
% 35.76/9.71 thf(f32650,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) ) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(forward_subsumption_resolution,[],[f32647,f32529])).
% 35.76/9.71 thf(f32664,plain,(
% 35.76/9.71 ($true = $false) | (((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $true) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(constrained_superposition,[],[f826,f32650])).
% 35.76/9.71 thf(f32688,plain,(
% 35.76/9.71 (((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $true) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f32664])).
% 35.76/9.71 thf(f33031,plain,(
% 35.76/9.71 ( ! [X0 : $i] : (($true = ((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0)))) ) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(constrained_superposition,[],[f32688,f30045])).
% 35.76/9.71 thf(f33815,plain,(
% 35.76/9.71 ( ! [X0 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X0 @ X1)) = $true)) ) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(constrained_superposition,[],[f33031,f30045])).
% 35.76/9.71 thf(f34937,plain,(
% 35.76/9.71 ($true = $false) | ($true = ((?? @ $i @ (^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y1 @ Y0)))))))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(constrained_superposition,[],[f769,f32650])).
% 35.76/9.71 thf(f34959,plain,(
% 35.76/9.71 ($true = $false) | ($true = (((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y1 @ Y0))))) @ sK12))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(sigma_proxy_clausification,[],[f34937])).
% 35.76/9.71 thf(f34960,plain,(
% 35.76/9.71 ($true = (((^[Y0 : $i]: (?? @ $i @ (^[Y1 : $i]: (~ (parent_THFTYPE_IiioI @ Y1 @ Y0))))) @ sK12))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f34959])).
% 35.76/9.71 thf(f34961,plain,(
% 35.76/9.71 ($true = ((?? @ $i @ (^[Y0 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ sK12)))))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(beta-eta_normalization,[],[f34960])).
% 35.76/9.71 thf(f34962,plain,(
% 35.76/9.71 ($true = (((^[Y0 : $i]: (~ (parent_THFTYPE_IiioI @ Y0 @ sK12))) @ sK13))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(sigma_proxy_clausification,[],[f34961])).
% 35.76/9.71 thf(f34963,plain,(
% 35.76/9.71 ($true = ((~ (parent_THFTYPE_IiioI @ sK13 @ sK12)))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(beta-eta_normalization,[],[f34962])).
% 35.76/9.71 thf(f34964,plain,(
% 35.76/9.71 ($false = ((parent_THFTYPE_IiioI @ sK13 @ sK12))) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(not_proxy_clausification,[],[f34963])).
% 35.76/9.71 thf(f34984,plain,(
% 35.76/9.71 ($true = $false) | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(forward_demodulation,[],[f34964,f33815])).
% 35.76/9.71 thf(f34985,plain,(
% 35.76/9.71 $false | (~spl9_5 | ~spl9_6)),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f34984])).
% 35.76/9.71 thf(f34986,plain,(
% 35.76/9.71 ~spl9_5 | ~spl9_6),
% 35.76/9.71 inference(avatar_contradiction_clause,[],[f34985])).
% 35.76/9.71 thf(f35005,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o),X1 : $i] : ((lAnna_THFTYPE_i != X1) | ($false = ((X0 @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) ) | (~spl9_4 | spl9_6)),
% 35.76/9.71 inference(forward_subsumption_resolution,[],[f2966,f3005])).
% 35.76/9.71 thf(f45978,plain,(
% 35.76/9.71 ( ! [X0 : ($i > $i > $o)] : (($false = ((X0 @ lBill_THFTYPE_i @ lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = X0)) ) | ~spl9_7),
% 35.76/9.71 inference(equality_resolution,[],[f3009])).
% 35.76/9.71 thf(f46064,plain,(
% 35.76/9.71 ($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))) @ lBill_THFTYPE_i @ lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl9_7),
% 35.76/9.71 inference(primitive_instantiation,[],[f45978])).
% 35.76/9.71 thf(f47610,plain,(
% 35.76/9.71 ($false = ((~ (lBill_THFTYPE_i = lAnna_THFTYPE_i)))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl9_7),
% 35.76/9.71 inference(beta-eta_normalization,[],[f46064])).
% 35.76/9.71 thf(f47611,plain,(
% 35.76/9.71 ($true = ((lBill_THFTYPE_i = lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl9_7),
% 35.76/9.71 inference(not_proxy_clausification,[],[f47610])).
% 35.76/9.71 thf(f47612,plain,(
% 35.76/9.71 (lBill_THFTYPE_i = lAnna_THFTYPE_i) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl9_7),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f47611])).
% 35.76/9.71 thf(f47904,plain,(
% 35.76/9.71 spl9_8 | ~spl9_4 | spl9_6),
% 35.76/9.71 inference(avatar_split_clause,[],[f35005,f3004,f1576,f4836])).
% 35.76/9.71 thf(f51101,definition,(
% 35.76/9.71 spl9_16 <=> ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))))),
% 35.76/9.71 introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition])).
% 35.76/9.71 thf(f51103,plain,(
% 35.76/9.71 ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = (^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1)))))) | ~spl9_16),
% 35.76/9.71 inference(avatar_component_clause,[],[f51101])).
% 35.76/9.71 thf(f51104,plain,(
% 35.76/9.71 spl9_16 | spl9_10 | ~spl9_7),
% 35.76/9.71 inference(avatar_split_clause,[],[f47612,f3008,f5459,f51101])).
% 35.76/9.71 thf(f51201,plain,(
% 35.76/9.71 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1)) = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))) @ X1)))) ) | ~spl9_16),
% 35.76/9.71 inference(argument_congruence,[],[f51103])).
% 35.76/9.71 thf(f51202,plain,(
% 35.76/9.71 ( ! [X1 : $i] : (((^[Y0 : $i]: ($true)) = (^[Y0 : $i]: (~ (X1 = Y0))))) ) | ~spl9_16),
% 35.76/9.71 inference(beta-eta_normalization,[],[f51201])).
% 35.76/9.71 thf(f51299,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (((((^[Y0 : $i]: ($true)) @ X2)) = (((^[Y0 : $i]: (~ (X1 = Y0))) @ X2)))) ) | ~spl9_16),
% 35.76/9.71 inference(argument_congruence,[],[f51202])).
% 35.76/9.71 thf(f51301,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ($true)) @ X2))) | ($true = (((^[Y0 : $i]: (~ (X1 = Y0))) @ X2)))) ) | ~spl9_16),
% 35.76/9.71 inference(iff_proxy_clausification,[],[f51299])).
% 35.76/9.71 thf(f51302,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (($true = $false) | ($true = ((~ (X1 = X2))))) ) | ~spl9_16),
% 35.76/9.71 inference(beta-eta_normalization,[],[f51301])).
% 35.76/9.71 thf(f51303,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (($true = $false) | ($false = ((X1 = X2)))) ) | ~spl9_16),
% 35.76/9.71 inference(not_proxy_clausification,[],[f51302])).
% 35.76/9.71 thf(f51304,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : (($true = $false) | (X1 != X2)) ) | ~spl9_16),
% 35.76/9.71 inference(equality_proxy_clausification,[],[f51303])).
% 35.76/9.71 thf(f51305,plain,(
% 35.76/9.71 ( ! [X2 : $i,X1 : $i] : ((X1 != X2)) ) | ~spl9_16),
% 35.76/9.71 inference(trivial_inequality_removal,[],[f51304])).
% 35.76/9.71 thf(f51306,plain,(
% 35.76/9.71 $false | ~spl9_16),
% 35.76/9.71 inference(flex-flex_simplification,[],[f51305])).
% 35.76/9.71 thf(f51307,plain,(
% 35.76/9.71 ~spl9_16),
% 35.76/9.71 inference(avatar_contradiction_clause,[],[f51306])).
% 35.76/9.71 cnf(s1, plain, spl9_1 | ~spl9_2, inference(sat_conversion,[],[f1507])).
% 35.76/9.71 cnf(s3, plain, spl9_4 | ~spl9_5, inference(sat_conversion,[],[f1582])).
% 35.76/9.71 cnf(s4, plain, ~spl9_4 | spl9_6 | spl9_7, inference(sat_conversion,[],[f3010])).
% 35.76/9.71 cnf(s6, plain, spl9_6 | ~spl9_8 | ~spl9_10, inference(sat_conversion,[],[f5462])).
% 35.76/9.71 cnf(s11, plain, spl9_2 | spl9_5, inference(sat_conversion,[],[f30029])).
% 35.76/9.71 cnf(s13, plain, ~spl9_1 | spl9_5, inference(sat_conversion,[],[f30037])).
% 35.76/9.71 cnf(s16, plain, ~spl9_5 | ~spl9_6, inference(sat_conversion,[],[f34986])).
% 35.76/9.71 cnf(s18, plain, ~spl9_4 | spl9_6 | spl9_8, inference(sat_conversion,[],[f47904])).
% 35.76/9.71 cnf(s23, plain, ~spl9_7 | spl9_10 | spl9_16, inference(sat_conversion,[],[f51104])).
% 35.76/9.71 cnf(s24, plain, ~spl9_16, inference(sat_conversion,[],[f51307])).
% 35.76/9.71 cnf(s25, plain, ~spl9_7 | spl9_10, inference(rat,[],[s23,s24])).
% 35.76/9.71 cnf(s26, plain, ~spl9_4 | spl9_6, inference(rat,[],[s25,s6,s4,s18])).
% 35.76/9.71 cnf(s27, plain, ~spl9_5, inference(rat,[],[s26,s3,s16])).
% 35.76/9.71 cnf(s28, plain, ~spl9_1, inference(rat,[],[s13,s27])).
% 35.76/9.71 cnf(s29, plain, spl9_2, inference(rat,[],[s11,s27])).
% 35.76/9.71 cnf(s30, plain, $false, inference(rat,[],[s1,s29,s28])).
% 35.76/9.71 thf(f51311,plain,(
% 35.76/9.71 $false),
% 35.76/9.71 inference(avatar_sat_refutation,[],[s30])).
% 35.76/9.71 % SZS output end Proof for theBenchmark
% 35.76/9.71 % (437387)------------------------------
% 35.76/9.71 % (437387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.76/9.71 % (437387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.76/9.71 % (437387)CaDiCaL version: 2.1.3
% 35.76/9.71 % (437387)Termination reason: Refutation
% 35.76/9.71 % (437387)Time elapsed: 2.793 s
% 35.76/9.71 % (437387)Peak memory usage: 29 MB
% 35.76/9.71 % (437387)Instructions burned: 6233 (million)
% 35.76/9.71 % (437143)Success in time 9.486 s
% 35.76/9.71 % Vampire exiting
%------------------------------------------------------------------------------