%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR119^2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:13 AM UTC 2026
% Result : Theorem 3.25s 0.87s
% Output : Refutation 3.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR119^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 % Computer : n001.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Tue Sep 29 17:59:06 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.25/0.28 Running first-order model finding
% 0.25/0.28 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.25/0.87 % (1602484)Will run a generic schedule for satisfiability detection.
% 3.25/0.87 % (1602495)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4154405217:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.25/0.87 % (1602489)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3237426351_2999 on theBenchmark for (2999ds/0Mi)
% 3.25/0.87 % (1602490)% WARNING: option uhcvi not known.
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602490)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2435614041:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.25/0.87 % (1602493)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3567027795:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.25/0.87 % (1602494)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2733699655:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.25/0.87 % (1602491)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1918649199:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.25/0.87 % (1602492)dis+10_1_sil=32000:sp=arity:random_seed=1281319624:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.25/0.87 % (1602493)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602490)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602490)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.25/0.87 % (1602502)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2002926401:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602495)Instruction limit reached!
% 3.25/0.87 % (1602495)------------------------------
% 3.25/0.87 % (1602495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602495)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602495)Termination reason: Instruction limit
% 3.25/0.87 % (1602495)Termination phase: Saturation
% 3.25/0.87 % (1602495)Time elapsed: 0.069 s
% 3.25/0.87 % (1602495)Peak memory usage: 12 MB
% 3.25/0.87 % (1602495)Instructions burned: 161 (million)
% 3.25/0.87 % (1602505)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1139402720:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.25/0.87 % (1602506)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=3516380022:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.25/0.87 % (1602506)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602506)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 3.25/0.87 % (1602492)Instruction limit reached!
% 3.25/0.87 % (1602492)------------------------------
% 3.25/0.87 % (1602492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602492)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602492)Termination reason: Instruction limit
% 3.25/0.87 % (1602492)Termination phase: Saturation
% 3.25/0.87 % (1602492)Time elapsed: 0.087 s
% 3.25/0.87 % (1602492)Peak memory usage: 12 MB
% 3.25/0.87 % (1602492)Instructions burned: 104 (million)
% 3.25/0.87 % (1602493)Instruction limit reached!
% 3.25/0.87 % (1602493)------------------------------
% 3.25/0.87 % (1602493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602493)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602493)Termination reason: Instruction limit
% 3.25/0.87 % (1602493)Termination phase: Saturation
% 3.25/0.87 % (1602493)Time elapsed: 0.095 s
% 3.25/0.87 % (1602493)Peak memory usage: 12 MB
% 3.25/0.87 % (1602493)Instructions burned: 116 (million)
% 3.25/0.87 % (1602494)Instruction limit reached!
% 3.25/0.87 % (1602494)------------------------------
% 3.25/0.87 % (1602494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602494)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602494)Termination reason: Instruction limit
% 3.25/0.87 % (1602494)Termination phase: Saturation
% 3.25/0.87 % (1602494)Time elapsed: 0.110 s
% 3.25/0.87 % (1602494)Peak memory usage: 12 MB
% 3.25/0.87 % (1602494)Instructions burned: 131 (million)
% 3.25/0.87 % (1602509)ott-21_1_sil=16000:fs=off:random_seed=659138320:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.25/0.87 % (1602510)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2238404445:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.25/0.87 % (1602511)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=274157203:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602505)Instruction limit reached!
% 3.25/0.87 % (1602505)------------------------------
% 3.25/0.87 % (1602505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602505)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602505)Termination reason: Instruction limit
% 3.25/0.87 % (1602505)Termination phase: Saturation
% 3.25/0.87 % (1602505)Time elapsed: 0.095 s
% 3.25/0.87 % (1602505)Peak memory usage: 13 MB
% 3.25/0.87 % (1602505)Instructions burned: 131 (million)
% 3.25/0.87 % (1602515)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3091103165:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 3.25/0.87 % (1602516)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4024648334:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602519)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=109151254:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 3.25/0.87 % (1602519)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602509)Instruction limit reached!
% 3.25/0.87 % (1602509)------------------------------
% 3.25/0.87 % (1602509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602509)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602509)Termination reason: Instruction limit
% 3.25/0.87 % (1602509)Termination phase: Saturation
% 3.25/0.87 % (1602509)Time elapsed: 0.147 s
% 3.25/0.87 % (1602509)Peak memory usage: 12 MB
% 3.25/0.87 % (1602509)Instructions burned: 181 (million)
% 3.25/0.87 % (1602521)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1437536765:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 3.25/0.87 % (1602521)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602506)Instruction limit reached!
% 3.25/0.87 % (1602506)------------------------------
% 3.25/0.87 % (1602506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602506)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602506)Termination reason: Instruction limit
% 3.25/0.87 % (1602506)Termination phase: Saturation
% 3.25/0.87 % (1602506)Time elapsed: 0.263 s
% 3.25/0.87 % (1602506)Peak memory usage: 13 MB
% 3.25/0.87 % (1602506)Instructions burned: 684 (million)
% 3.25/0.87 % (1602523)fmb+10_1_sil=64000:random_seed=524630481:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 3.25/0.87 % (1602523)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602525)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=921350224:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602527)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3483147700:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 3.25/0.87 % Exception at run slice level
% 3.25/0.87 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 3.25/0.87 % (1602529)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=552143973:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 3.25/0.87 % (1602529)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 3.25/0.87 % (1602515) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1602484-1602515"...
% 3.25/0.87 % (1602490) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1602484-1602490"...
% 3.25/0.87 % (1602515)...printing done.
% 3.25/0.87 % (1602515)Refutation found. Thanks to Tanya!
% 3.25/0.87 % SZS status Theorem for theBenchmark
% 3.25/0.87 % SZS output start Proof for theBenchmark
% 3.25/0.87 thf(type_def_5, type, num: $tType).
% 3.25/0.87 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 3.25/0.87 thf(func_def_2, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_3, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_5, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 3.25/0.87 thf(func_def_6, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 3.25/0.87 thf(func_def_7, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 3.25/0.87 thf(func_def_8, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 3.25/0.87 thf(func_def_9, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 3.25/0.87 thf(func_def_10, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 3.25/0.87 thf(func_def_11, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 3.25/0.87 thf(func_def_12, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_15, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 3.25/0.87 thf(func_def_16, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 3.25/0.87 thf(func_def_17, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 3.25/0.87 thf(func_def_18, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 3.25/0.87 thf(func_def_19, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 3.25/0.87 thf(func_def_20, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 3.25/0.87 thf(func_def_21, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 3.25/0.87 thf(func_def_22, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_26, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 3.25/0.87 thf(func_def_30, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 3.25/0.87 thf(func_def_33, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 3.25/0.87 thf(func_def_39, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.25/0.87 thf(func_def_51, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.25/0.87 thf(func_def_59, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 3.25/0.87 thf(func_def_61, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 3.25/0.87 thf(func_def_65, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_66, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_67, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_68, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 3.25/0.87 thf(func_def_75, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_77, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_78, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_79, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 3.25/0.87 thf(func_def_80, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 3.25/0.87 thf(func_def_81, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_83, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_84, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_85, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 3.25/0.87 thf(func_def_86, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_87, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 3.25/0.87 thf(func_def_89, type, vNOT: ($o > $o)).
% 3.25/0.87 thf(func_def_92, type, vAND: ($o > $o > $o)).
% 3.25/0.87 thf(func_def_93, type, sK0: (($i > $i > $o) > $i)).
% 3.25/0.87 thf(func_def_94, type, sK1: (($i > $i > $o) > $i)).
% 3.25/0.87 thf(func_def_95, type, sK2: (($i > $i > $o) > $i)).
% 3.25/0.87 thf(func_def_97, type, sK4: (($i > $i > $o) > $i)).
% 3.25/0.87 thf(func_def_98, type, sK5: ($i > $i > $i)).
% 3.25/0.87 thf(func_def_100, type, sF7: ($i > $o)).
% 3.25/0.87 thf(func_def_101, type, sF8: ($i > $o)).
% 3.25/0.87 thf(func_def_103, type, db0: !>[X0: $tType]:(X0)).
% 3.25/0.87 thf(func_def_104, type, db1: !>[X0: $tType]:(X0)).
% 3.25/0.87 thf(func_def_105, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 3.25/0.87 thf(func_def_106, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 3.25/0.87 thf(func_def_107, type, db2: !>[X0: $tType]:(X0)).
% 3.25/0.87 thf(func_def_108, type, db3: !>[X0: $tType]:(X0)).
% 3.25/0.87 thf(func_def_109, type, db4: !>[X0: $tType]:(X0)).
% 3.25/0.87 thf(f27,axiom,(
% 3.25/0.87 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 3.25/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax27)).
% 3.25/0.87 thf(f190,conjecture,(
% 3.25/0.87 ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))),
% 3.25/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 3.25/0.87 thf(f191,negated_conjecture,(
% 3.25/0.87 ~ ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))),
% 3.25/0.87 inference(negated_conjecture,[status(cth)],[f190])).
% 3.25/0.87 thf(f244,plain,(
% 3.25/0.87 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 3.25/0.87 inference(rectify,[],[f27])).
% 3.25/0.87 thf(f245,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 3.25/0.87 inference(fool_elimination,[],[f244])).
% 3.25/0.87 thf(f568,plain,(
% 3.25/0.87 ~ ? [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))),
% 3.25/0.87 inference(rectify,[],[f191])).
% 3.25/0.87 thf(f569,plain,(
% 3.25/0.87 ~ ? [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))) = $true)),
% 3.25/0.87 inference(fool_elimination,[],[f568])).
% 3.25/0.87 thf(f620,plain,(
% 3.25/0.87 ! [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))) != $true)),
% 3.25/0.87 inference(ennf_transformation,[],[f569])).
% 3.25/0.87 thf(f663,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 3.25/0.87 inference(cnf_transformation,[],[f245])).
% 3.25/0.87 thf(f828,plain,(
% 3.25/0.87 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))) != $true)) )),
% 3.25/0.87 inference(cnf_transformation,[],[f620])).
% 3.25/0.87 thf(f830,definition,(
% 3.25/0.87 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 3.25/0.87 introduced(theory,[fool_exhaustiveness_axiom])).
% 3.25/0.87 thf(f833,definition,(
% 3.25/0.87 (sF6 = ((lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 3.25/0.87 thf(f834,plain,(
% 3.25/0.87 (((lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i)) = sF6)),
% 3.25/0.87 inference(reorient_equations,[],[f833])).
% 3.25/0.87 thf(f835,definition,(
% 3.25/0.87 ( ! [X0 : $i] : ((((sF7 @ X0)) = ((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i)))) )),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 3.25/0.87 thf(f836,plain,(
% 3.25/0.87 ( ! [X0 : $i] : ((((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i)) = ((sF7 @ X0)))) )),
% 3.25/0.87 inference(reorient_equations,[],[f835])).
% 3.25/0.87 thf(f837,definition,(
% 3.25/0.87 ( ! [X0 : $i] : ((((sF8 @ X0)) = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (sF7 @ X0))))) )),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[sF8])],[function_definition])).
% 3.25/0.87 thf(f838,plain,(
% 3.25/0.87 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ sF6 @ (sF7 @ X0))) = ((sF8 @ X0)))) )),
% 3.25/0.87 inference(reorient_equations,[],[f837])).
% 3.25/0.87 thf(f839,plain,(
% 3.25/0.87 ( ! [X0 : $i] : (($true != ((sF8 @ X0)))) )),
% 3.25/0.87 inference(definition_folding,[],[f828,f838,f836,f834])).
% 3.25/0.87 thf(f852,plain,(
% 3.25/0.87 ( ! [X0 : $i] : ((((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i)) = $true) | ($false = ((sF7 @ X0)))) )),
% 3.25/0.87 inference(iff_proxy_clausification,[],[f836])).
% 3.25/0.87 thf(f853,plain,(
% 3.25/0.87 ( ! [X0 : $i] : ((((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((sF7 @ X0)))) )),
% 3.25/0.87 inference(iff_proxy_clausification,[],[f836])).
% 3.25/0.87 thf(f855,plain,(
% 3.25/0.87 ( ! [X0 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (sF7 @ X0)))) | ($true = ((sF8 @ X0)))) )),
% 3.25/0.87 inference(iff_proxy_clausification,[],[f838])).
% 3.25/0.87 thf(f856,plain,(
% 3.25/0.87 ( ! [X0 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (sF7 @ X0))))) )),
% 3.25/0.87 inference(forward_subsumption_resolution,[],[f855,f839])).
% 3.25/0.87 thf(f860,plain,(
% 3.25/0.87 ( ! [X0 : $i] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $true))) | ($false = ((sF7 @ X0)))) )),
% 3.25/0.87 inference(constrained_superposition,[],[f856,f830])).
% 3.25/0.87 thf(f870,definition,(
% 3.25/0.87 spl9_1 <=> ! [X0 : $i] : ($false = ((sF7 @ X0)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition])).
% 3.25/0.87 thf(f871,plain,(
% 3.25/0.87 ( ! [X0 : $i] : (($false = ((sF7 @ X0)))) ) | ~spl9_1),
% 3.25/0.87 inference(avatar_component_clause,[],[f870])).
% 3.25/0.87 thf(f873,definition,(
% 3.25/0.87 spl9_2 <=> ($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $true)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition])).
% 3.25/0.87 thf(f875,plain,(
% 3.25/0.87 ($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $true))) | ~spl9_2),
% 3.25/0.87 inference(avatar_component_clause,[],[f873])).
% 3.25/0.87 thf(f876,plain,(
% 3.25/0.87 spl9_1 | spl9_2),
% 3.25/0.87 inference(avatar_split_clause,[],[f860,f873,f870])).
% 3.25/0.87 thf(f1797,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & $false)))) | ($true = ((sF7 @ lSue_THFTYPE_i)))),
% 3.25/0.87 inference(constrained_superposition,[],[f663,f853])).
% 3.25/0.87 thf(f1802,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($true & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))))) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 inference(constrained_superposition,[],[f663,f830])).
% 3.25/0.87 thf(f1803,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ((((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))) = $false)),
% 3.25/0.87 inference(constrained_superposition,[],[f663,f830])).
% 3.25/0.87 thf(f1822,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 inference(and_proxy_clausification,[],[f1803])).
% 3.25/0.87 thf(f1823,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 inference(boolean_simplification,[],[f1802])).
% 3.25/0.87 thf(f1828,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($true = ((sF7 @ lSue_THFTYPE_i)))),
% 3.25/0.87 inference(boolean_simplification,[],[f1797])).
% 3.25/0.87 thf(f1834,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $true))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 inference(forward_demodulation,[],[f1822,f834])).
% 3.25/0.87 thf(f1835,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 inference(forward_demodulation,[],[f1823,f834])).
% 3.25/0.87 thf(f1840,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ($true = ((sF7 @ lSue_THFTYPE_i)))),
% 3.25/0.87 inference(forward_demodulation,[],[f1828,f834])).
% 3.25/0.87 thf(f1842,definition,(
% 3.25/0.87 spl9_7 <=> (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition])).
% 3.25/0.87 thf(f1844,plain,(
% 3.25/0.87 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl9_7),
% 3.25/0.87 inference(avatar_component_clause,[],[f1842])).
% 3.25/0.87 thf(f1846,definition,(
% 3.25/0.87 spl9_8 <=> (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition])).
% 3.25/0.87 thf(f1848,plain,(
% 3.25/0.87 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl9_8),
% 3.25/0.87 inference(avatar_component_clause,[],[f1846])).
% 3.25/0.87 thf(f1873,plain,(
% 3.25/0.87 ($true = $false) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl9_2),
% 3.25/0.87 inference(forward_demodulation,[],[f1834,f875])).
% 3.25/0.87 thf(f1874,plain,(
% 3.25/0.87 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl9_2),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f1873])).
% 3.25/0.87 thf(f1876,definition,(
% 3.25/0.87 spl9_15 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_15])],[avatar_definition])).
% 3.25/0.87 thf(f1878,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))) | ~spl9_15),
% 3.25/0.87 inference(avatar_component_clause,[],[f1876])).
% 3.25/0.87 thf(f1879,plain,(
% 3.25/0.87 spl9_8 | spl9_15),
% 3.25/0.87 inference(avatar_split_clause,[],[f1835,f1876,f1846])).
% 3.25/0.87 thf(f1881,definition,(
% 3.25/0.87 spl9_16 <=> ($false = ((sF7 @ lMary_THFTYPE_i)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition])).
% 3.25/0.87 thf(f1883,plain,(
% 3.25/0.87 ($false = ((sF7 @ lMary_THFTYPE_i))) | ~spl9_16),
% 3.25/0.87 inference(avatar_component_clause,[],[f1881])).
% 3.25/0.87 thf(f1890,definition,(
% 3.25/0.87 spl9_18 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_18])],[avatar_definition])).
% 3.25/0.87 thf(f1891,plain,(
% 3.25/0.87 ($true != ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | spl9_18),
% 3.25/0.87 inference(avatar_component_clause,[],[f1890])).
% 3.25/0.87 thf(f1892,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ~spl9_18),
% 3.25/0.87 inference(avatar_component_clause,[],[f1890])).
% 3.25/0.87 thf(f1900,definition,(
% 3.25/0.87 spl9_20 <=> ($false = ((sF7 @ lSue_THFTYPE_i)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_20])],[avatar_definition])).
% 3.25/0.87 thf(f1902,plain,(
% 3.25/0.87 ($false = ((sF7 @ lSue_THFTYPE_i))) | ~spl9_20),
% 3.25/0.87 inference(avatar_component_clause,[],[f1900])).
% 3.25/0.87 thf(f1905,definition,(
% 3.25/0.87 spl9_21 <=> ($true = ((sF7 @ lSue_THFTYPE_i)))),
% 3.25/0.87 introduced(definition,[new_symbols(definition,[spl9_21])],[avatar_definition])).
% 3.25/0.87 thf(f1907,plain,(
% 3.25/0.87 ($true = ((sF7 @ lSue_THFTYPE_i))) | ~spl9_21),
% 3.25/0.87 inference(avatar_component_clause,[],[f1905])).
% 3.25/0.87 thf(f1908,plain,(
% 3.25/0.87 spl9_21 | spl9_18),
% 3.25/0.87 inference(avatar_split_clause,[],[f1840,f1890,f1905])).
% 3.25/0.87 thf(f1909,plain,(
% 3.25/0.87 spl9_8 | spl9_7 | ~spl9_2),
% 3.25/0.87 inference(avatar_split_clause,[],[f1874,f873,f1842,f1846])).
% 3.25/0.87 thf(f1913,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | (~spl9_7 | ~spl9_15)),
% 3.25/0.87 inference(forward_demodulation,[],[f1878,f1844])).
% 3.25/0.87 thf(f1924,plain,(
% 3.25/0.87 ($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ~spl9_1),
% 3.25/0.87 inference(constrained_superposition,[],[f856,f871])).
% 3.25/0.87 thf(f1987,plain,(
% 3.25/0.87 ($true = $false) | (~spl9_1 | ~spl9_18)),
% 3.25/0.87 inference(constrained_superposition,[],[f1892,f1924])).
% 3.25/0.87 thf(f1996,plain,(
% 3.25/0.87 $false | (~spl9_1 | ~spl9_18)),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f1987])).
% 3.25/0.87 thf(f1997,plain,(
% 3.25/0.87 ~spl9_1 | ~spl9_18),
% 3.25/0.87 inference(avatar_contradiction_clause,[],[f1996])).
% 3.25/0.87 thf(f2002,plain,(
% 3.25/0.87 ($true = $false) | (~spl9_1 | ~spl9_21)),
% 3.25/0.87 inference(forward_demodulation,[],[f1907,f871])).
% 3.25/0.87 thf(f2003,plain,(
% 3.25/0.87 $false | (~spl9_1 | ~spl9_21)),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f2002])).
% 3.25/0.87 thf(f2004,plain,(
% 3.25/0.87 ~spl9_1 | ~spl9_21),
% 3.25/0.87 inference(avatar_contradiction_clause,[],[f2003])).
% 3.25/0.87 thf(f2205,plain,(
% 3.25/0.87 ($true = $false) | ($false = ((sF7 @ lMary_THFTYPE_i))) | ~spl9_8),
% 3.25/0.87 inference(constrained_superposition,[],[f852,f1848])).
% 3.25/0.87 thf(f2206,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($false & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))))) | ~spl9_8),
% 3.25/0.87 inference(constrained_superposition,[],[f663,f1848])).
% 3.25/0.87 thf(f2209,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl9_8),
% 3.25/0.87 inference(boolean_simplification,[],[f2206])).
% 3.25/0.87 thf(f2210,plain,(
% 3.25/0.87 ($false = ((sF7 @ lMary_THFTYPE_i))) | ~spl9_8),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f2205])).
% 3.25/0.87 thf(f2213,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ~spl9_8),
% 3.25/0.87 inference(forward_demodulation,[],[f2209,f834])).
% 3.25/0.87 thf(f2218,plain,(
% 3.25/0.87 $false | (~spl9_8 | spl9_18)),
% 3.25/0.87 inference(forward_subsumption_resolution,[],[f2213,f1891])).
% 3.25/0.87 thf(f2219,plain,(
% 3.25/0.87 ~spl9_8 | spl9_18),
% 3.25/0.87 inference(avatar_contradiction_clause,[],[f2218])).
% 3.25/0.87 thf(f2220,plain,(
% 3.25/0.87 spl9_18 | ~spl9_7 | ~spl9_15),
% 3.25/0.87 inference(avatar_split_clause,[],[f1913,f1876,f1842,f1890])).
% 3.25/0.87 thf(f2277,plain,(
% 3.25/0.87 ($true = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $true))) | ($false = ((sF7 @ lSue_THFTYPE_i))) | ~spl9_15),
% 3.25/0.87 inference(constrained_superposition,[],[f1878,f852])).
% 3.25/0.87 thf(f2289,plain,(
% 3.25/0.87 ($true = $false) | ($false = ((sF7 @ lSue_THFTYPE_i))) | (~spl9_2 | ~spl9_15)),
% 3.25/0.87 inference(forward_demodulation,[],[f2277,f875])).
% 3.25/0.87 thf(f2290,plain,(
% 3.25/0.87 ($false = ((sF7 @ lSue_THFTYPE_i))) | (~spl9_2 | ~spl9_15)),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f2289])).
% 3.25/0.87 thf(f2291,plain,(
% 3.25/0.87 spl9_20 | ~spl9_2 | ~spl9_15),
% 3.25/0.87 inference(avatar_split_clause,[],[f2290,f1876,f873,f1900])).
% 3.25/0.87 thf(f2295,plain,(
% 3.25/0.87 ($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ~spl9_20),
% 3.25/0.87 inference(constrained_superposition,[],[f856,f1902])).
% 3.25/0.87 thf(f2332,plain,(
% 3.25/0.87 ($true = $false) | (~spl9_18 | ~spl9_20)),
% 3.25/0.87 inference(constrained_superposition,[],[f1892,f2295])).
% 3.25/0.87 thf(f2334,plain,(
% 3.25/0.87 $false | (~spl9_18 | ~spl9_20)),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f2332])).
% 3.25/0.87 thf(f2335,plain,(
% 3.25/0.87 ~spl9_18 | ~spl9_20),
% 3.25/0.87 inference(avatar_contradiction_clause,[],[f2334])).
% 3.25/0.87 thf(f2344,plain,(
% 3.25/0.87 spl9_16 | ~spl9_8),
% 3.25/0.87 inference(avatar_split_clause,[],[f2210,f1846,f1881])).
% 3.25/0.87 thf(f2367,plain,(
% 3.25/0.87 ($false = ((holdsDuring_THFTYPE_IiooI @ sF6 @ $false))) | ~spl9_16),
% 3.25/0.87 inference(constrained_superposition,[],[f856,f1883])).
% 3.25/0.87 thf(f2378,plain,(
% 3.25/0.87 ($true = $false) | (~spl9_16 | ~spl9_18)),
% 3.25/0.87 inference(constrained_superposition,[],[f1892,f2367])).
% 3.25/0.87 thf(f2380,plain,(
% 3.25/0.87 $false | (~spl9_16 | ~spl9_18)),
% 3.25/0.87 inference(trivial_inequality_removal,[],[f2378])).
% 3.25/0.87 thf(f2381,plain,(
% 3.25/0.87 ~spl9_16 | ~spl9_18),
% 3.25/0.87 inference(avatar_contradiction_clause,[],[f2380])).
% 3.25/0.87 cnf(s1, plain, spl9_1 | spl9_2, inference(sat_conversion,[],[f876])).
% 3.25/0.87 cnf(s8, plain, spl9_8 | spl9_15, inference(sat_conversion,[],[f1879])).
% 3.25/0.87 cnf(s13, plain, spl9_18 | spl9_21, inference(sat_conversion,[],[f1908])).
% 3.25/0.87 cnf(s14, plain, ~spl9_2 | spl9_7 | spl9_8, inference(sat_conversion,[],[f1909])).
% 3.25/0.87 cnf(s19, plain, ~spl9_1 | ~spl9_18, inference(sat_conversion,[],[f1997])).
% 3.25/0.87 cnf(s21, plain, ~spl9_1 | ~spl9_21, inference(sat_conversion,[],[f2004])).
% 3.25/0.87 cnf(s27, plain, ~spl9_8 | spl9_18, inference(sat_conversion,[],[f2219])).
% 3.25/0.87 cnf(s28, plain, ~spl9_7 | ~spl9_15 | spl9_18, inference(sat_conversion,[],[f2220])).
% 3.25/0.87 cnf(s30, plain, ~spl9_2 | ~spl9_15 | spl9_20, inference(sat_conversion,[],[f2291])).
% 3.25/0.87 cnf(s37, plain, ~spl9_18 | ~spl9_20, inference(sat_conversion,[],[f2335])).
% 3.25/0.87 cnf(s39, plain, ~spl9_8 | spl9_16, inference(sat_conversion,[],[f2344])).
% 3.25/0.87 cnf(s46, plain, ~spl9_16 | ~spl9_18, inference(sat_conversion,[],[f2381])).
% 3.25/0.87 cnf(s48, plain, ~spl9_8, inference(rat,[],[s46,s27,s39])).
% 3.25/0.87 cnf(s49, plain, spl9_15, inference(rat,[],[s8,s48])).
% 3.25/0.87 cnf(s50, plain, ~spl9_2, inference(rat,[],[s37,s28,s30,s14,s49,s48])).
% 3.25/0.87 cnf(s51, plain, spl9_1, inference(rat,[],[s1,s50])).
% 3.25/0.87 cnf(s52, plain, ~spl9_21, inference(rat,[],[s21,s51])).
% 3.25/0.87 cnf(s54, plain, ~spl9_18, inference(rat,[],[s19,s51])).
% 3.25/0.87 cnf(s56, plain, $false, inference(rat,[],[s13,s52,s54])).
% 3.25/0.87 thf(f2386,plain,(
% 3.25/0.87 $false),
% 3.25/0.87 inference(avatar_sat_refutation,[],[s56])).
% 3.25/0.87 % SZS output end Proof for theBenchmark
% 3.25/0.87 % (1602515)------------------------------
% 3.25/0.87 % (1602515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.25/0.87 % (1602515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.25/0.87 % (1602515)CaDiCaL version: 2.1.3
% 3.25/0.87 % (1602515)Termination reason: Refutation
% 3.25/0.87 % (1602515)Time elapsed: 0.338 s
% 3.25/0.87 % (1602515)Peak memory usage: 15 MB
% 3.25/0.87 % (1602515)Instructions burned: 413 (million)
% 3.25/0.87 % (1602484)Success in time 0.57 s
% 3.25/0.87 % Vampire exiting
%------------------------------------------------------------------------------