%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR130^1 : 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 : n008.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:16 AM UTC 2026
% Result : Theorem 1.75s 0.49s
% Output : Refutation 1.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR130^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.17 % Computer : n008.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Tue Sep 29 17:56:09 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.06/0.21 Running first-order model finding
% 0.06/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
% 1.75/0.49 % (3506185)Will run a generic schedule for satisfiability detection.
% 1.75/0.49 % (3506193)dis+10_1_sil=32000:sp=arity:random_seed=340281773:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.75/0.49 % (3506191)% WARNING: option uhcvi not known.
% 1.75/0.49 % (3506190)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1735505295_2999 on theBenchmark for (2999ds/0Mi)
% 1.75/0.49 % (3506194)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3721907056:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.75/0.49 % (3506191)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1393402624:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.75/0.49 % (3506192)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2140542573:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.75/0.49 % (3506194)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506191)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.75/0.49 % (3506191)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.75/0.49 % (3506195)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=290245087:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.75/0.49 % (3506196)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1683616253:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.75/0.49 % (3506202)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1980542813:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.75/0.49 % (3506193)Instruction limit reached!
% 1.75/0.49 % (3506193)------------------------------
% 1.75/0.49 % (3506193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506193)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506193)Termination reason: Instruction limit
% 1.75/0.49 % (3506193)Termination phase: Saturation
% 1.75/0.49 % (3506193)Time elapsed: 0.027 s
% 1.75/0.49 % (3506193)Peak memory usage: 12 MB
% 1.75/0.49 % (3506193)Instructions burned: 107 (million)
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506206)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2392631073:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 1.75/0.49 % (3506207)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=3044887669:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 1.75/0.49 % (3506207)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.75/0.49 % (3506207)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 1.75/0.49 % (3506194)Instruction limit reached!
% 1.75/0.49 % (3506194)------------------------------
% 1.75/0.49 % (3506194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506194)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506194)Termination reason: Instruction limit
% 1.75/0.49 % (3506194)Termination phase: Saturation
% 1.75/0.49 % (3506194)Time elapsed: 0.056 s
% 1.75/0.49 % (3506194)Peak memory usage: 12 MB
% 1.75/0.49 % (3506194)Instructions burned: 117 (million)
% 1.75/0.49 % (3506206)Instruction limit reached!
% 1.75/0.49 % (3506206)------------------------------
% 1.75/0.49 % (3506206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506206)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506206)Termination reason: Instruction limit
% 1.75/0.49 % (3506206)Termination phase: Saturation
% 1.75/0.49 % (3506206)Time elapsed: 0.034 s
% 1.75/0.49 % (3506206)Peak memory usage: 12 MB
% 1.75/0.49 % (3506206)Instructions burned: 133 (million)
% 1.75/0.49 % (3506210)ott-21_1_sil=16000:fs=off:random_seed=644589044:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 1.75/0.49 % (3506211)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4294217013:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 1.75/0.49 % (3506195)Instruction limit reached!
% 1.75/0.49 % (3506195)------------------------------
% 1.75/0.49 % (3506195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506195)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506195)Termination reason: Instruction limit
% 1.75/0.49 % (3506195)Termination phase: Saturation
% 1.75/0.49 % (3506195)Time elapsed: 0.064 s
% 1.75/0.49 % (3506195)Peak memory usage: 13 MB
% 1.75/0.49 % (3506195)Instructions burned: 132 (million)
% 1.75/0.49 % (3506196)Instruction limit reached!
% 1.75/0.49 % (3506196)------------------------------
% 1.75/0.49 % (3506196)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506196)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506196)Termination reason: Instruction limit
% 1.75/0.49 % (3506196)Termination phase: Saturation
% 1.75/0.49 % (3506196)Time elapsed: 0.078 s
% 1.75/0.49 % (3506196)Peak memory usage: 13 MB
% 1.75/0.49 % (3506196)Instructions burned: 160 (million)
% 1.75/0.49 % (3506214)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1917064151:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506215)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=303378332:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 1.75/0.49 % (3506217)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3036299053:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506220)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=3950950850: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)
% 1.75/0.49 % (3506220)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.75/0.49 % (3506210)Instruction limit reached!
% 1.75/0.49 % (3506210)------------------------------
% 1.75/0.49 % (3506210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506210)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506210)Termination reason: Instruction limit
% 1.75/0.49 % (3506210)Termination phase: Saturation
% 1.75/0.49 % (3506210)Time elapsed: 0.083 s
% 1.75/0.49 % (3506210)Peak memory usage: 12 MB
% 1.75/0.49 % (3506210)Instructions burned: 182 (million)
% 1.75/0.49 % (3506222)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3461076609:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 1.75/0.49 % (3506222)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 1.75/0.49 % (3506211)Instruction limit reached!
% 1.75/0.49 % (3506211)------------------------------
% 1.75/0.49 % (3506211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506211)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506211)Termination reason: Instruction limit
% 1.75/0.49 % (3506211)Termination phase: Saturation
% 1.75/0.49 % (3506211)Time elapsed: 0.121 s
% 1.75/0.49 % (3506211)Peak memory usage: 14 MB
% 1.75/0.49 % (3506211)Instructions burned: 481 (million)
% 1.75/0.49 % (3506224)fmb+10_1_sil=64000:random_seed=3380739930:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 1.75/0.49 % (3506224)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506226)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3994353930:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506228)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2736017068:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 1.75/0.49 % Exception at run slice level
% 1.75/0.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 1.75/0.49 % (3506215) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3506185-3506215"...
% 1.75/0.49 % (3506215)...printing done.
% 1.75/0.49 % (3506215)Refutation found. Thanks to Tanya!
% 1.75/0.49 % SZS status Theorem for theBenchmark
% 1.75/0.49 % SZS output start Proof for theBenchmark
% 1.75/0.49 thf(type_def_5, type, num: $tType).
% 1.75/0.49 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 1.75/0.49 thf(func_def_0, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 1.75/0.49 thf(func_def_7, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 1.75/0.49 thf(func_def_8, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 1.75/0.49 thf(func_def_10, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 1.75/0.49 thf(func_def_12, type, vNOT: ($o > $o)).
% 1.75/0.49 thf(func_def_15, type, vAND: ($o > $o > $o)).
% 1.75/0.49 thf(func_def_16, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 1.75/0.49 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 1.75/0.49 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 1.75/0.49 thf(func_def_19, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 1.75/0.49 thf(func_def_21, type, sF1: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_22, type, sF2: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_23, type, sF3: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_24, type, sF4: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_25, type, sF5: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_26, type, sF6: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_27, type, sF7: (($i > $i > $o) > $o)).
% 1.75/0.49 thf(func_def_28, type, sK8: (($i > $i > $o) > $i)).
% 1.75/0.49 thf(func_def_29, type, sK9: (($i > $i > $o) > $i)).
% 1.75/0.49 thf(func_def_31, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 1.75/0.49 thf(func_def_32, type, db2: !>[X0: $tType]:(X0)).
% 1.75/0.49 thf(func_def_33, type, db3: !>[X0: $tType]:(X0)).
% 1.75/0.49 thf(func_def_34, type, db4: !>[X0: $tType]:(X0)).
% 1.75/0.49 thf(f1,axiom,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 1.75/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax)).
% 1.75/0.49 thf(f3,axiom,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_002)).
% 1.75/0.49 thf(f5,axiom,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_004)).
% 1.75/0.49 thf(f8,axiom,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 1.75/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_007)).
% 1.75/0.49 thf(f9,conjecture,(
% 1.75/0.49 ? [X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X1 : $i,X2 : $i] : (X0 @ X1 @ X2)) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 1.75/0.49 thf(f10,negated_conjecture,(
% 1.75/0.49 ~ ? [X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X1 : $i,X2 : $i] : (X0 @ X1 @ X2)) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 inference(negated_conjecture,[status(cth)],[f9])).
% 1.75/0.49 thf(f11,plain,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 1.75/0.49 inference(rectify,[],[f1])).
% 1.75/0.49 thf(f12,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(fool_elimination,[],[f11])).
% 1.75/0.49 thf(f15,plain,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 inference(rectify,[],[f3])).
% 1.75/0.49 thf(f16,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(fool_elimination,[],[f15])).
% 1.75/0.49 thf(f19,plain,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 inference(rectify,[],[f5])).
% 1.75/0.49 thf(f20,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(fool_elimination,[],[f19])).
% 1.75/0.49 thf(f25,plain,(
% 1.75/0.49 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 1.75/0.49 inference(rectify,[],[f8])).
% 1.75/0.49 thf(f26,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 1.75/0.49 inference(fool_elimination,[],[f25])).
% 1.75/0.49 thf(f27,plain,(
% 1.75/0.49 ~ ? [X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X1 : $i,X2 : $i] : (X0 @ X1 @ X2)) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 1.75/0.49 inference(rectify,[],[f10])).
% 1.75/0.49 thf(f28,plain,(
% 1.75/0.49 ~ ? [X0 : ($i > $i > $o)] : ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0))))))))))),
% 1.75/0.49 inference(fool_elimination,[],[f27])).
% 1.75/0.49 thf(f29,plain,(
% 1.75/0.49 ! [X0 : ($i > $i > $o)] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0))))))))))),
% 1.75/0.49 inference(ennf_transformation,[],[f28])).
% 1.75/0.49 thf(f30,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(cnf_transformation,[],[f12])).
% 1.75/0.49 thf(f32,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(cnf_transformation,[],[f16])).
% 1.75/0.49 thf(f34,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 1.75/0.49 inference(cnf_transformation,[],[f20])).
% 1.75/0.49 thf(f37,plain,(
% 1.75/0.49 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 1.75/0.49 inference(cnf_transformation,[],[f26])).
% 1.75/0.49 thf(f38,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0))))))))))) )),
% 1.75/0.49 inference(cnf_transformation,[],[f29])).
% 1.75/0.49 thf(f40,definition,(
% 1.75/0.49 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 1.75/0.49 introduced(theory,[fool_exhaustiveness_axiom])).
% 1.75/0.49 thf(f41,definition,(
% 1.75/0.49 (sF0 = ((lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 1.75/0.49 thf(f42,plain,(
% 1.75/0.49 (((lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i)) = sF0)),
% 1.75/0.49 inference(reorient_equations,[],[f41])).
% 1.75/0.49 thf(f43,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF1 @ X0)) = ((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 1.75/0.49 thf(f44,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = ((sF1 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f43])).
% 1.75/0.49 thf(f45,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF2 @ X0)) = ((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 1.75/0.49 thf(f46,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = ((sF2 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f45])).
% 1.75/0.49 thf(f47,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF3 @ X0)) = (((sF1 @ X0) & (sF2 @ X0))))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 1.75/0.49 thf(f48,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (((((sF1 @ X0) & (sF2 @ X0))) = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f47])).
% 1.75/0.49 thf(f49,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF4 @ X0)) = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))))))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 1.75/0.49 thf(f50,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))))) = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f49])).
% 1.75/0.49 thf(f51,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF5 @ X0)) = ((~ (sF4 @ X0))))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 1.75/0.49 thf(f52,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((~ (sF4 @ X0))) = ((sF5 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f51])).
% 1.75/0.49 thf(f53,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF6 @ X0)) = (((sF3 @ X0) & (sF5 @ X0))))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF6])],[function_definition])).
% 1.75/0.49 thf(f54,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (((((sF3 @ X0) & (sF5 @ X0))) = ((sF6 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f53])).
% 1.75/0.49 thf(f55,definition,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((sF7 @ X0)) = ((holdsDuring_THFTYPE_IiooI @ sF0 @ (sF6 @ X0))))) )),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[sF7])],[function_definition])).
% 1.75/0.49 thf(f56,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((holdsDuring_THFTYPE_IiooI @ sF0 @ (sF6 @ X0))) = ((sF7 @ X0)))) )),
% 1.75/0.49 inference(reorient_equations,[],[f55])).
% 1.75/0.49 thf(f57,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true != ((sF7 @ X0)))) )),
% 1.75/0.49 inference(definition_folding,[],[f38,f56,f54,f52,f50,f48,f46,f44,f42])).
% 1.75/0.49 thf(f58,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF1 @ X0))) | (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $true)) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f44])).
% 1.75/0.49 thf(f59,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF1 @ X0))) | (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f44])).
% 1.75/0.49 thf(f61,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF2 @ X0))) | (((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f46])).
% 1.75/0.49 thf(f62,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = (((sF1 @ X0) & (sF2 @ X0)))) | ($false = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f48])).
% 1.75/0.49 thf(f63,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = (((sF1 @ X0) & (sF2 @ X0)))) | ($true = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f48])).
% 1.75/0.49 thf(f64,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF3 @ X0))) | ($false = ((sF2 @ X0))) | ($false = ((sF1 @ X0)))) )),
% 1.75/0.49 inference(and_proxy_clausification,[],[f63])).
% 1.75/0.49 thf(f66,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF3 @ X0))) | ($true = ((sF1 @ X0)))) )),
% 1.75/0.49 inference(and_proxy_clausification,[],[f62])).
% 1.75/0.49 thf(f67,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0))))))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f50])).
% 1.75/0.49 thf(f68,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))))) = $false) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f50])).
% 1.75/0.49 thf(f69,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))) @ (sK8 @ X0)))) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(sigma_proxy_clausification,[],[f68])).
% 1.75/0.49 thf(f70,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((!! @ $i @ (^[Y0 : $i]: (X0 @ Y0 @ (sK8 @ X0)))))) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f69])).
% 1.75/0.49 thf(f71,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = (((^[Y0 : $i]: (X0 @ Y0 @ (sK8 @ X0))) @ (sK9 @ X0)))) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(sigma_proxy_clausification,[],[f70])).
% 1.75/0.49 thf(f72,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((X0 @ (sK9 @ X0) @ (sK8 @ X0)))) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f71])).
% 1.75/0.49 thf(f73,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o),X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))) @ X1))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(pi_proxy_clausification,[],[f67])).
% 1.75/0.49 thf(f74,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o),X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (X0 @ Y0 @ X1))))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f73])).
% 1.75/0.49 thf(f75,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true = (((^[Y0 : $i]: (X0 @ Y0 @ X1)) @ X2))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(pi_proxy_clausification,[],[f74])).
% 1.75/0.49 thf(f76,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true = ((X0 @ X2 @ X1))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f75])).
% 1.75/0.49 thf(f77,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((~ (sF4 @ X0)))) | ($false = ((sF5 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f52])).
% 1.75/0.49 thf(f78,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((~ (sF4 @ X0)))) | ($true = ((sF5 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f52])).
% 1.75/0.49 thf(f79,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF5 @ X0))) | ($true = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(not_proxy_clausification,[],[f78])).
% 1.75/0.49 thf(f80,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF5 @ X0))) | ($false = ((sF4 @ X0)))) )),
% 1.75/0.49 inference(not_proxy_clausification,[],[f77])).
% 1.75/0.49 thf(f81,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = (((sF3 @ X0) & (sF5 @ X0)))) | ($false = ((sF6 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f54])).
% 1.75/0.49 thf(f82,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = (((sF3 @ X0) & (sF5 @ X0)))) | ($true = ((sF6 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f54])).
% 1.75/0.49 thf(f83,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF6 @ X0))) | ($false = ((sF5 @ X0))) | ($false = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(and_proxy_clausification,[],[f82])).
% 1.75/0.49 thf(f84,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF6 @ X0))) | ($true = ((sF5 @ X0)))) )),
% 1.75/0.49 inference(and_proxy_clausification,[],[f81])).
% 1.75/0.49 thf(f85,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF6 @ X0))) | ($true = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(and_proxy_clausification,[],[f81])).
% 1.75/0.49 thf(f87,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ (sF6 @ X0)))) | ($true = ((sF7 @ X0)))) )),
% 1.75/0.49 inference(iff_proxy_clausification,[],[f56])).
% 1.75/0.49 thf(f88,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ (sF6 @ X0))))) )),
% 1.75/0.49 inference(forward_subsumption_resolution,[],[f87,f57])).
% 1.75/0.49 thf(f92,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $true))) | ($false = ((sF6 @ X0)))) )),
% 1.75/0.49 inference(constrained_superposition,[],[f88,f40])).
% 1.75/0.49 thf(f102,definition,(
% 1.75/0.49 spl10_1 <=> ! [X0 : ($i > $i > $o)] : ($false = ((sF6 @ X0)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_1])],[avatar_definition])).
% 1.75/0.49 thf(f103,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF6 @ X0)))) ) | ~spl10_1),
% 1.75/0.49 inference(avatar_component_clause,[],[f102])).
% 1.75/0.49 thf(f105,definition,(
% 1.75/0.49 spl10_2 <=> ($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $true)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_2])],[avatar_definition])).
% 1.75/0.49 thf(f107,plain,(
% 1.75/0.49 ($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $true))) | ~spl10_2),
% 1.75/0.49 inference(avatar_component_clause,[],[f105])).
% 1.75/0.49 thf(f108,plain,(
% 1.75/0.49 spl10_1 | spl10_2),
% 1.75/0.49 inference(avatar_split_clause,[],[f92,f105,f102])).
% 1.75/0.49 thf(f115,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 1.75/0.49 inference(constrained_superposition,[],[f30,f40])).
% 1.75/0.49 thf(f117,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $true))) | (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 1.75/0.49 inference(forward_demodulation,[],[f115,f42])).
% 1.75/0.49 thf(f118,plain,(
% 1.75/0.49 ($true = $false) | (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ~spl10_2),
% 1.75/0.49 inference(forward_demodulation,[],[f117,f107])).
% 1.75/0.49 thf(f119,plain,(
% 1.75/0.49 (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ~spl10_2),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f118])).
% 1.75/0.49 thf(f121,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl10_2),
% 1.75/0.49 inference(constrained_superposition,[],[f30,f119])).
% 1.75/0.49 thf(f123,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ~spl10_2),
% 1.75/0.49 inference(forward_demodulation,[],[f121,f42])).
% 1.75/0.49 thf(f221,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ($true = ((sF5 @ X0)))) )),
% 1.75/0.49 inference(constrained_superposition,[],[f88,f84])).
% 1.75/0.49 thf(f250,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ($true = ((sF3 @ X0)))) )),
% 1.75/0.49 inference(constrained_superposition,[],[f88,f85])).
% 1.75/0.49 thf(f252,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | ($true = ((sF3 @ X0)))) ) | ~spl10_2),
% 1.75/0.49 inference(forward_demodulation,[],[f250,f123])).
% 1.75/0.49 thf(f253,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF3 @ X0)))) ) | ~spl10_2),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f252])).
% 1.75/0.49 thf(f262,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | ($true = ((sF1 @ X0)))) ) | ~spl10_2),
% 1.75/0.49 inference(constrained_superposition,[],[f66,f253])).
% 1.75/0.49 thf(f265,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF1 @ X0)))) ) | ~spl10_2),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f262])).
% 1.75/0.49 thf(f283,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $true)) ) | ~spl10_2),
% 1.75/0.49 inference(constrained_superposition,[],[f58,f265])).
% 1.75/0.49 thf(f284,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $true)) ) | ~spl10_2),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f283])).
% 1.75/0.49 thf(f296,plain,(
% 1.75/0.49 ($true = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ lSue_THFTYPE_i @ lBill_THFTYPE_i))) | ~spl10_2),
% 1.75/0.49 inference(primitive_instantiation,[],[f284])).
% 1.75/0.49 thf(f297,plain,(
% 1.75/0.49 ($true = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (Y0 = Y1))))) @ lSue_THFTYPE_i @ lBill_THFTYPE_i))) | ~spl10_2),
% 1.75/0.49 inference(primitive_instantiation,[],[f284])).
% 1.75/0.49 thf(f440,plain,(
% 1.75/0.49 ($true = ((~ (lSue_THFTYPE_i = lBill_THFTYPE_i)))) | ~spl10_2),
% 1.75/0.49 inference(beta-eta_normalization,[],[f297])).
% 1.75/0.49 thf(f441,plain,(
% 1.75/0.49 ($false = ((lSue_THFTYPE_i = lBill_THFTYPE_i))) | ~spl10_2),
% 1.75/0.49 inference(not_proxy_clausification,[],[f440])).
% 1.75/0.49 thf(f442,plain,(
% 1.75/0.49 (lSue_THFTYPE_i != lBill_THFTYPE_i) | ~spl10_2),
% 1.75/0.49 inference(equality_proxy_clausification,[],[f441])).
% 1.75/0.49 thf(f443,plain,(
% 1.75/0.49 ($true = ((lSue_THFTYPE_i = lBill_THFTYPE_i))) | ~spl10_2),
% 1.75/0.49 inference(beta-eta_normalization,[],[f296])).
% 1.75/0.49 thf(f444,plain,(
% 1.75/0.49 (lSue_THFTYPE_i = lBill_THFTYPE_i) | ~spl10_2),
% 1.75/0.49 inference(equality_proxy_clausification,[],[f443])).
% 1.75/0.49 thf(f456,plain,(
% 1.75/0.49 $false | ~spl10_2),
% 1.75/0.49 inference(forward_subsumption_resolution,[],[f444,f442])).
% 1.75/0.49 thf(f457,plain,(
% 1.75/0.49 ~spl10_2),
% 1.75/0.49 inference(avatar_contradiction_clause,[],[f456])).
% 1.75/0.49 thf(f473,definition,(
% 1.75/0.49 spl10_6 <=> (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_6])],[avatar_definition])).
% 1.75/0.49 thf(f475,plain,(
% 1.75/0.49 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_6),
% 1.75/0.49 inference(avatar_component_clause,[],[f473])).
% 1.75/0.49 thf(f483,definition,(
% 1.75/0.49 spl10_8 <=> (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_8])],[avatar_definition])).
% 1.75/0.49 thf(f485,plain,(
% 1.75/0.49 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_8),
% 1.75/0.49 inference(avatar_component_clause,[],[f483])).
% 1.75/0.49 thf(f515,definition,(
% 1.75/0.49 spl10_14 <=> ! [X0 : ($i > $i > $o)] : ($true = ((sF5 @ X0)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_14])],[avatar_definition])).
% 1.75/0.49 thf(f516,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF5 @ X0)))) ) | ~spl10_14),
% 1.75/0.49 inference(avatar_component_clause,[],[f515])).
% 1.75/0.49 thf(f518,definition,(
% 1.75/0.49 spl10_15 <=> ($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_15])],[avatar_definition])).
% 1.75/0.49 thf(f520,plain,(
% 1.75/0.49 ($false = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ~spl10_15),
% 1.75/0.49 inference(avatar_component_clause,[],[f518])).
% 1.75/0.49 thf(f521,plain,(
% 1.75/0.49 spl10_14 | spl10_15),
% 1.75/0.49 inference(avatar_split_clause,[],[f221,f518,f515])).
% 1.75/0.49 thf(f639,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ ((^[Y2 : $i]: ((^[Y3 : $i]: (Y3)))) @ Y0 @ Y1)))))))) | (lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | (lMary_THFTYPE_i != X2)) )),
% 1.75/0.49 inference(constrained_superposition,[],[f37,f76])).
% 1.75/0.49 thf(f652,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ Y1))))))) | (lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | (lMary_THFTYPE_i != X2)) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f639])).
% 1.75/0.49 thf(f653,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ Y1))))))) | (lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | (lMary_THFTYPE_i != X2)) )),
% 1.75/0.49 inference(boolean_simplification,[],[f652])).
% 1.75/0.49 thf(f754,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ Y1))))))) | (lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | (lMary_THFTYPE_i != X2)) )),
% 1.75/0.49 inference(forward_demodulation,[],[f653,f42])).
% 1.75/0.49 thf(f897,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | ($false = ((sF4 @ X0)))) ) | ~spl10_14),
% 1.75/0.49 inference(constrained_superposition,[],[f80,f516])).
% 1.75/0.49 thf(f898,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF4 @ X0)))) ) | ~spl10_14),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f897])).
% 1.75/0.49 thf(f903,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | ($false = ((sF5 @ X0))) | ($false = ((sF3 @ X0)))) ) | ~spl10_1),
% 1.75/0.49 inference(constrained_superposition,[],[f103,f83])).
% 1.75/0.49 thf(f909,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($false = ((sF5 @ X0))) | ($false = ((sF3 @ X0)))) ) | ~spl10_1),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f903])).
% 1.75/0.49 thf(f932,plain,(
% 1.75/0.49 ( ! [X1 : ($i > $i > $o)] : (($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))) @ (sK9 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))) @ (sK8 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 1.75/0.49 inference(primitive_instantiation,[],[f72])).
% 1.75/0.49 thf(f1012,plain,(
% 1.75/0.49 ( ! [X0 : $o] : (($false = X0) | ($false = X0) | ($true = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) )),
% 1.75/0.49 inference(constrained_superposition,[],[f40,f72])).
% 1.75/0.49 thf(f1026,plain,(
% 1.75/0.49 ( ! [X0 : $o] : (($false = X0) | ($true = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) )),
% 1.75/0.49 inference(duplicate_literal_removal,[],[f1012])).
% 1.75/0.49 thf(f1167,plain,(
% 1.75/0.49 ( ! [X1 : ($i > $i > $o)] : (($false = ((~ (X1 @ (sK9 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))) @ (sK8 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))))))) | ($true = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 1.75/0.49 inference(beta-eta_normalization,[],[f932])).
% 1.75/0.49 thf(f1168,plain,(
% 1.75/0.49 ( ! [X1 : ($i > $i > $o)] : (($true = ((X1 @ (sK9 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))) @ (sK8 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))))))) | ($true = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1))))))))) )),
% 1.75/0.49 inference(not_proxy_clausification,[],[f1167])).
% 1.75/0.49 thf(f1181,plain,(
% 1.75/0.49 ( ! [X0 : $o] : (($true = $false) | ($false = X0)) ) | ~spl10_14),
% 1.75/0.49 inference(forward_demodulation,[],[f1026,f898])).
% 1.75/0.49 thf(f1182,plain,(
% 1.75/0.49 ( ! [X0 : $o] : (($false = X0)) ) | ~spl10_14),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f1181])).
% 1.75/0.49 thf(f1319,plain,(
% 1.75/0.49 ( ! [X1 : ($i > $i > $o)] : (($true = $false) | ($true = ((X1 @ (sK9 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))) @ (sK8 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))))))) ) | ~spl10_14),
% 1.75/0.49 inference(forward_demodulation,[],[f1168,f898])).
% 1.75/0.49 thf(f1320,plain,(
% 1.75/0.49 ( ! [X1 : ($i > $i > $o)] : (($true = ((X1 @ (sK9 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))) @ (sK8 @ (^[Y0 : $i]: ((^[Y1 : $i]: (~ (X1 @ Y0 @ Y1)))))))))) ) | ~spl10_14),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f1319])).
% 1.75/0.49 thf(f1391,plain,(
% 1.75/0.49 ($true = $false) | ~spl10_14),
% 1.75/0.49 inference(forward_demodulation,[],[f1320,f1182])).
% 1.75/0.49 thf(f1392,plain,(
% 1.75/0.49 $false | ~spl10_14),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f1391])).
% 1.75/0.49 thf(f1393,plain,(
% 1.75/0.49 ~spl10_14),
% 1.75/0.49 inference(avatar_contradiction_clause,[],[f1392])).
% 1.75/0.49 thf(f1517,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = $false) | ($true = ((sF4 @ X0))) | ($false = ((sF3 @ X0)))) ) | ~spl10_1),
% 1.75/0.49 inference(constrained_superposition,[],[f79,f909])).
% 1.75/0.49 thf(f1520,plain,(
% 1.75/0.49 ( ! [X0 : ($i > $i > $o)] : (($true = ((sF4 @ X0))) | ($false = ((sF3 @ X0)))) ) | ~spl10_1),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f1517])).
% 1.75/0.49 thf(f1952,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : (($true = $false) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ Y1))))))) | (lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | (lMary_THFTYPE_i != X2)) ) | ~spl10_15),
% 1.75/0.49 inference(forward_demodulation,[],[f754,f520])).
% 1.75/0.49 thf(f1953,plain,(
% 1.75/0.49 ( ! [X2 : $i,X0 : ($i > $i > $i),X1 : $i] : ((lSue_THFTYPE_i != ((X0 @ X1 @ X2))) | ($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ (X0 @ Y0 @ Y1) @ Y1))))))) | (lMary_THFTYPE_i != X2)) ) | ~spl10_15),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f1952])).
% 1.75/0.49 thf(f2290,definition,(
% 1.75/0.49 spl10_37 <=> ($false = ((sF4 @ likes_THFTYPE_IiioI)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_37])],[avatar_definition])).
% 1.75/0.49 thf(f2292,plain,(
% 1.75/0.49 ($false = ((sF4 @ likes_THFTYPE_IiioI))) | ~spl10_37),
% 1.75/0.49 inference(avatar_component_clause,[],[f2290])).
% 1.75/0.49 thf(f2299,plain,(
% 1.75/0.49 ( ! [X0 : $i] : (($false = ((sF4 @ (^[Y0 : $i]: ((^[Y1 : $i]: (likes_THFTYPE_IiioI @ ((^[Y2 : $i]: ((^[Y3 : $i]: (Y2)))) @ Y0 @ Y1) @ Y1))))))) | (lMary_THFTYPE_i != X0)) ) | ~spl10_15),
% 1.75/0.49 inference(equality_resolution,[],[f1953])).
% 1.75/0.49 thf(f2304,plain,(
% 1.75/0.49 ( ! [X0 : $i] : (($false = ((sF4 @ likes_THFTYPE_IiioI))) | (lMary_THFTYPE_i != X0)) ) | ~spl10_15),
% 1.75/0.49 inference(beta-eta_normalization,[],[f2299])).
% 1.75/0.49 thf(f2311,definition,(
% 1.75/0.49 spl10_38 <=> ! [X0 : $i] : (lMary_THFTYPE_i != X0)),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_38])],[avatar_definition])).
% 1.75/0.49 thf(f2312,plain,(
% 1.75/0.49 ( ! [X0 : $i] : ((lMary_THFTYPE_i != X0)) ) | ~spl10_38),
% 1.75/0.49 inference(avatar_component_clause,[],[f2311])).
% 1.75/0.49 thf(f2323,plain,(
% 1.75/0.49 spl10_38 | spl10_37 | ~spl10_15),
% 1.75/0.49 inference(avatar_split_clause,[],[f2304,f518,f2290,f2311])).
% 1.75/0.49 thf(f2350,plain,(
% 1.75/0.49 $false | ~spl10_38),
% 1.75/0.49 inference(equality_resolution,[],[f2312])).
% 1.75/0.49 thf(f2351,plain,(
% 1.75/0.49 ~spl10_38),
% 1.75/0.49 inference(avatar_contradiction_clause,[],[f2350])).
% 1.75/0.49 thf(f2373,plain,(
% 1.75/0.49 ($true = $false) | ($false = ((sF3 @ likes_THFTYPE_IiioI))) | (~spl10_1 | ~spl10_37)),
% 1.75/0.49 inference(constrained_superposition,[],[f1520,f2292])).
% 1.75/0.49 thf(f2377,plain,(
% 1.75/0.49 ($false = ((sF3 @ likes_THFTYPE_IiioI))) | (~spl10_1 | ~spl10_37)),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2373])).
% 1.75/0.49 thf(f2386,plain,(
% 1.75/0.49 ($true = $false) | ($false = ((sF2 @ likes_THFTYPE_IiioI))) | ($false = ((sF1 @ likes_THFTYPE_IiioI))) | (~spl10_1 | ~spl10_37)),
% 1.75/0.49 inference(constrained_superposition,[],[f2377,f64])).
% 1.75/0.49 thf(f2397,plain,(
% 1.75/0.49 ($false = ((sF2 @ likes_THFTYPE_IiioI))) | ($false = ((sF1 @ likes_THFTYPE_IiioI))) | (~spl10_1 | ~spl10_37)),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2386])).
% 1.75/0.49 thf(f2399,definition,(
% 1.75/0.49 spl10_43 <=> ($false = ((sF1 @ likes_THFTYPE_IiioI)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_43])],[avatar_definition])).
% 1.75/0.49 thf(f2401,plain,(
% 1.75/0.49 ($false = ((sF1 @ likes_THFTYPE_IiioI))) | ~spl10_43),
% 1.75/0.49 inference(avatar_component_clause,[],[f2399])).
% 1.75/0.49 thf(f2403,definition,(
% 1.75/0.49 spl10_44 <=> ($false = ((sF2 @ likes_THFTYPE_IiioI)))),
% 1.75/0.49 introduced(definition,[new_symbols(definition,[spl10_44])],[avatar_definition])).
% 1.75/0.49 thf(f2405,plain,(
% 1.75/0.49 ($false = ((sF2 @ likes_THFTYPE_IiioI))) | ~spl10_44),
% 1.75/0.49 inference(avatar_component_clause,[],[f2403])).
% 1.75/0.49 thf(f2407,plain,(
% 1.75/0.49 spl10_43 | spl10_44 | ~spl10_1 | ~spl10_37),
% 1.75/0.49 inference(avatar_split_clause,[],[f2397,f2290,f102,f2403,f2399])).
% 1.75/0.49 thf(f2415,plain,(
% 1.75/0.49 ($true = $false) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_43),
% 1.75/0.49 inference(constrained_superposition,[],[f59,f2401])).
% 1.75/0.49 thf(f2419,plain,(
% 1.75/0.49 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_43),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2415])).
% 1.75/0.49 thf(f2424,plain,(
% 1.75/0.49 spl10_6 | ~spl10_43),
% 1.75/0.49 inference(avatar_split_clause,[],[f2419,f2399,f473])).
% 1.75/0.49 thf(f2450,plain,(
% 1.75/0.49 ($true = $false) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_44),
% 1.75/0.49 inference(constrained_superposition,[],[f61,f2405])).
% 1.75/0.49 thf(f2454,plain,(
% 1.75/0.49 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl10_44),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2450])).
% 1.75/0.49 thf(f2459,plain,(
% 1.75/0.49 spl10_8 | ~spl10_44),
% 1.75/0.49 inference(avatar_split_clause,[],[f2454,f2403,f483])).
% 1.75/0.49 thf(f2465,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl10_8),
% 1.75/0.49 inference(constrained_superposition,[],[f34,f485])).
% 1.75/0.49 thf(f2482,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ~spl10_8),
% 1.75/0.49 inference(forward_demodulation,[],[f2465,f42])).
% 1.75/0.49 thf(f2486,plain,(
% 1.75/0.49 ($true = $false) | (~spl10_8 | ~spl10_15)),
% 1.75/0.49 inference(forward_demodulation,[],[f2482,f520])).
% 1.75/0.49 thf(f2487,plain,(
% 1.75/0.49 $false | (~spl10_8 | ~spl10_15)),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2486])).
% 1.75/0.49 thf(f2488,plain,(
% 1.75/0.49 ~spl10_8 | ~spl10_15),
% 1.75/0.49 inference(avatar_contradiction_clause,[],[f2487])).
% 1.75/0.49 thf(f2506,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl10_6),
% 1.75/0.49 inference(constrained_superposition,[],[f32,f475])).
% 1.75/0.49 thf(f2523,plain,(
% 1.75/0.49 ($true = ((holdsDuring_THFTYPE_IiooI @ sF0 @ $false))) | ~spl10_6),
% 1.75/0.49 inference(forward_demodulation,[],[f2506,f42])).
% 1.75/0.49 thf(f2527,plain,(
% 1.75/0.49 ($true = $false) | (~spl10_6 | ~spl10_15)),
% 1.75/0.49 inference(forward_demodulation,[],[f2523,f520])).
% 1.75/0.49 thf(f2528,plain,(
% 1.75/0.49 $false | (~spl10_6 | ~spl10_15)),
% 1.75/0.49 inference(trivial_inequality_removal,[],[f2527])).
% 1.75/0.49 thf(f2529,plain,(
% 1.75/0.49 ~spl10_6 | ~spl10_15),
% 1.75/0.49 inference(avatar_contradiction_clause,[],[f2528])).
% 1.75/0.49 cnf(s1, plain, spl10_1 | spl10_2, inference(sat_conversion,[],[f108])).
% 1.75/0.49 cnf(s8, plain, ~spl10_2, inference(sat_conversion,[],[f457])).
% 1.75/0.49 cnf(s21, plain, spl10_14 | spl10_15, inference(sat_conversion,[],[f521])).
% 1.75/0.49 cnf(s42, plain, ~spl10_14, inference(sat_conversion,[],[f1393])).
% 1.75/0.49 cnf(s75, plain, ~spl10_15 | spl10_37 | spl10_38, inference(sat_conversion,[],[f2323])).
% 1.75/0.49 cnf(s78, plain, ~spl10_38, inference(sat_conversion,[],[f2351])).
% 1.75/0.49 cnf(s80, plain, ~spl10_1 | ~spl10_37 | spl10_43 | spl10_44, inference(sat_conversion,[],[f2407])).
% 1.75/0.49 cnf(s81, plain, spl10_6 | ~spl10_43, inference(sat_conversion,[],[f2424])).
% 1.75/0.49 cnf(s83, plain, spl10_8 | ~spl10_44, inference(sat_conversion,[],[f2459])).
% 1.75/0.49 cnf(s86, plain, ~spl10_8 | ~spl10_15, inference(sat_conversion,[],[f2488])).
% 1.75/0.49 cnf(s88, plain, ~spl10_6 | ~spl10_15, inference(sat_conversion,[],[f2529])).
% 1.75/0.49 cnf(s91, plain, ~spl10_15 | spl10_37, inference(rat,[],[s75,s78])).
% 1.75/0.49 cnf(s95, plain, spl10_15, inference(rat,[],[s21,s42])).
% 1.75/0.49 cnf(s96, plain, ~spl10_6, inference(rat,[],[s88,s95])).
% 1.75/0.49 cnf(s97, plain, ~spl10_8, inference(rat,[],[s86,s95])).
% 1.75/0.49 cnf(s100, plain, spl10_37, inference(rat,[],[s91,s95])).
% 1.75/0.49 cnf(s106, plain, ~spl10_43, inference(rat,[],[s81,s96])).
% 1.75/0.49 cnf(s107, plain, ~spl10_44, inference(rat,[],[s83,s97])).
% 1.75/0.49 cnf(s109, plain, ~spl10_1, inference(rat,[],[s80,s107,s106,s100])).
% 1.75/0.49 cnf(s112, plain, $false, inference(rat,[],[s1,s8,s109])).
% 1.75/0.49 thf(f2530,plain,(
% 1.75/0.49 $false),
% 1.75/0.49 inference(avatar_sat_refutation,[],[s112])).
% 1.75/0.49 % SZS output end Proof for theBenchmark
% 1.75/0.49 % (3506215)------------------------------
% 1.75/0.49 % (3506215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.75/0.49 % (3506215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.75/0.49 % (3506215)CaDiCaL version: 2.1.3
% 1.75/0.49 % (3506215)Termination reason: Refutation
% 1.75/0.49 % (3506215)Time elapsed: 0.121 s
% 1.75/0.49 % (3506215)Peak memory usage: 14 MB
% 1.75/0.49 % (3506215)Instructions burned: 255 (million)
% 1.75/0.49 % (3506185)Success in time 0.272 s
% 1.75/0.49 % Vampire exiting
%------------------------------------------------------------------------------