%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR133^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:06 AM UTC 2026
% Result : Theorem 0.21s 0.30s
% Output : Refutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR133^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n007.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 17:53:41 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running higher-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.30 % (3715401)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.21/0.30 % (3715406)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1060612278:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.21/0.30 % (3715406)Refutation not found, incomplete strategy
% 0.21/0.30 % (3715406)------------------------------
% 0.21/0.30 % (3715406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715406)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715406)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.30 % (3715406)Time elapsed: 0.002 s
% 0.21/0.30 % (3715406)Peak memory usage: 12 MB
% 0.21/0.30 % (3715406)Instructions burned: 4 (million)
% 0.21/0.30 % (3715406)------------------------------
% 0.21/0.30 % (3715406)------------------------------
% 0.21/0.30 % (3715407)lrs+10_16_si=on:nwc=1.5:random_seed=2403581476:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.21/0.30 % (3715410)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2556932938:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.21/0.30 % (3715408)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2201615362:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.21/0.30 % (3715409)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=3105303276:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.21/0.30 % (3715411)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=561126987:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.21/0.30 % (3715410)Refutation not found, incomplete strategy
% 0.21/0.30 % (3715410)------------------------------
% 0.21/0.30 % (3715410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715410)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715410)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.30 % (3715410)Time elapsed: 0.002 s
% 0.21/0.30 % (3715410)Peak memory usage: 11 MB
% 0.21/0.30 % (3715410)Instructions burned: 4 (million)
% 0.21/0.30 % (3715408)Refutation not found, incomplete strategy
% 0.21/0.30 % (3715408)------------------------------
% 0.21/0.30 % (3715408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715408)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715408)Termination reason: Refutation not found, incomplete strategy
% 0.21/0.30 % (3715408)Time elapsed: 0.002 s
% 0.21/0.30 % (3715408)Peak memory usage: 12 MB
% 0.21/0.30 % (3715408)Instructions burned: 4 (million)
% 0.21/0.30 % (3715410)------------------------------
% 0.21/0.30 % (3715410)------------------------------
% 0.21/0.30 % (3715408)------------------------------
% 0.21/0.30 % (3715408)------------------------------
% 0.21/0.30 % (3715412)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.21/0.30 % (3715412)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.21/0.30 % (3715407)Instruction limit reached!
% 0.21/0.30 % (3715407)------------------------------
% 0.21/0.30 % (3715407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715407)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715407)Termination reason: Instruction limit
% 0.21/0.30 % (3715407)Termination phase: Saturation
% 0.21/0.30 % (3715407)Time elapsed: 0.009 s
% 0.21/0.30 % (3715407)Peak memory usage: 12 MB
% 0.21/0.30 % (3715407)Instructions burned: 19 (million)
% 0.21/0.30 % (3715412)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=3694751104:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.21/0.30 % (3715414)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=506807416:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.21/0.30 % (3715414)Instruction limit reached!
% 0.21/0.30 % (3715414)------------------------------
% 0.21/0.30 % (3715414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715414)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715414)Termination reason: Instruction limit
% 0.21/0.30 % (3715414)Termination phase: Saturation
% 0.21/0.30 % (3715414)Time elapsed: 0.002 s
% 0.21/0.30 % (3715414)Peak memory usage: 12 MB
% 0.21/0.30 % (3715414)Instructions burned: 2 (million)
% 0.21/0.30 % (3715409) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3715401-3715409"...
% 0.21/0.30 % (3715421)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.21/0.30 % (3715409)...printing done.
% 0.21/0.30 % (3715420)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3119307856:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.21/0.30 % (3715421)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=4107640462:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.21/0.30 % (3715409)Refutation found. Thanks to Tanya!
% 0.21/0.30 % SZS status Theorem for theBenchmark
% 0.21/0.30 % SZS output start Proof for theBenchmark
% 0.21/0.30 thf(type_def_5, type, num: $tType).
% 0.21/0.30 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.21/0.30 thf(func_def_0, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 0.21/0.30 thf(func_def_7, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 0.21/0.30 thf(func_def_8, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 0.21/0.30 thf(func_def_10, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 0.21/0.30 thf(func_def_12, type, vNOT: ($o > $o)).
% 0.21/0.30 thf(func_def_15, type, vAND: ($o > $o > $o)).
% 0.21/0.30 thf(func_def_16, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.21/0.30 thf(func_def_18, type, db0: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_19, type, db1: !>[X0: $tType]:(X0)).
% 0.21/0.30 thf(func_def_20, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.21/0.30 thf(f1,axiom,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax)).
% 0.21/0.30 thf(f2,axiom,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_001)).
% 0.21/0.30 thf(f7,axiom,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_006)).
% 0.21/0.30 thf(f8,axiom,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_007)).
% 0.21/0.30 thf(f10,axiom,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_009)).
% 0.21/0.30 thf(f11,conjecture,(
% 0.21/0.30 ? [X1 : ($i > $i > $o),X2 : $i,X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X1 = X0)) & (X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i))),
% 0.21/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 0.21/0.30 thf(f12,negated_conjecture,(
% 0.21/0.30 ~ ? [X1 : ($i > $i > $o),X2 : $i,X0 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X1 = X0)) & (X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i))),
% 0.21/0.30 inference(negated_conjecture,[status(cth)],[f11])).
% 0.21/0.30 thf(f15,plain,(
% 0.21/0.30 ~ ? [X0 : ($i > $i > $o),X1 : $i,X2 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (X0 = X2)) & (X0 @ X1 @ lBill_THFTYPE_i) & (X2 @ X1 @ lAnna_THFTYPE_i))),
% 0.21/0.30 inference(rectify,[],[f12])).
% 0.21/0.30 thf(f16,plain,(
% 0.21/0.30 ~ ? [X1 : $i,X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X2 @ X1 @ lAnna_THFTYPE_i) & (X0 @ X1 @ lBill_THFTYPE_i)) & (~ (X0 = X2))))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f15])).
% 0.21/0.30 thf(f17,plain,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))),
% 0.21/0.30 inference(rectify,[],[f2])).
% 0.21/0.30 thf(f18,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f17])).
% 0.21/0.30 thf(f19,plain,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.21/0.30 inference(rectify,[],[f1])).
% 0.21/0.30 thf(f20,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f19])).
% 0.21/0.30 thf(f23,plain,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 0.21/0.30 inference(rectify,[],[f7])).
% 0.21/0.30 thf(f24,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f23])).
% 0.21/0.30 thf(f29,plain,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.21/0.30 inference(rectify,[],[f8])).
% 0.21/0.30 thf(f30,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f29])).
% 0.21/0.30 thf(f31,plain,(
% 0.21/0.30 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 0.21/0.30 inference(rectify,[],[f10])).
% 0.21/0.30 thf(f32,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.21/0.30 inference(fool_elimination,[],[f31])).
% 0.21/0.30 thf(f35,plain,(
% 0.21/0.30 ! [X2 : ($i > $i > $o),X1 : $i,X0 : ($i > $i > $o)] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X2 @ X1 @ lAnna_THFTYPE_i) & (X0 @ X1 @ lBill_THFTYPE_i)) & (~ (X0 = X2))))) != $true)),
% 0.21/0.30 inference(ennf_transformation,[],[f16])).
% 0.21/0.30 thf(f36,plain,(
% 0.21/0.30 ! [X0 : ($i > $i > $o),X1 : $i,X2 : ($i > $i > $o)] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ (X2 = X0))))))),
% 0.21/0.30 inference(rectify,[],[f35])).
% 0.21/0.30 thf(f37,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f20])).
% 0.21/0.30 thf(f42,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f24])).
% 0.21/0.30 thf(f43,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f32])).
% 0.21/0.30 thf(f44,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f30])).
% 0.21/0.30 thf(f46,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ (X2 = X0))))))) )),
% 0.21/0.30 inference(cnf_transformation,[],[f36])).
% 0.21/0.30 thf(f47,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 0.21/0.30 inference(cnf_transformation,[],[f18])).
% 0.21/0.30 thf(f60,definition,(
% 0.21/0.30 spl0_3 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 0.21/0.30 thf(f62,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) = $true) | ~spl0_3),
% 0.21/0.30 inference(avatar_component_clause,[],[f60])).
% 0.21/0.30 thf(f63,plain,(
% 0.21/0.30 spl0_3),
% 0.21/0.30 inference(avatar_split_clause,[],[f47,f60])).
% 0.21/0.30 thf(f70,definition,(
% 0.21/0.30 spl0_5 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition])).
% 0.21/0.30 thf(f72,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true) | ~spl0_5),
% 0.21/0.30 inference(avatar_component_clause,[],[f70])).
% 0.21/0.30 thf(f73,plain,(
% 0.21/0.30 spl0_5),
% 0.21/0.30 inference(avatar_split_clause,[],[f37,f70])).
% 0.21/0.30 thf(f75,definition,(
% 0.21/0.30 spl0_6 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition])).
% 0.21/0.30 thf(f77,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) = $true) | ~spl0_6),
% 0.21/0.30 inference(avatar_component_clause,[],[f75])).
% 0.21/0.30 thf(f78,plain,(
% 0.21/0.30 spl0_6),
% 0.21/0.30 inference(avatar_split_clause,[],[f44,f75])).
% 0.21/0.30 thf(f85,definition,(
% 0.21/0.30 spl0_8 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 0.21/0.30 thf(f87,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true) | ~spl0_8),
% 0.21/0.30 inference(avatar_component_clause,[],[f85])).
% 0.21/0.30 thf(f88,plain,(
% 0.21/0.30 spl0_8),
% 0.21/0.30 inference(avatar_split_clause,[],[f43,f85])).
% 0.21/0.30 thf(f90,definition,(
% 0.21/0.30 spl0_9 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition])).
% 0.21/0.30 thf(f92,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) = $true) | ~spl0_9),
% 0.21/0.30 inference(avatar_component_clause,[],[f90])).
% 0.21/0.30 thf(f93,plain,(
% 0.21/0.30 spl0_9),
% 0.21/0.30 inference(avatar_split_clause,[],[f42,f90])).
% 0.21/0.30 thf(f99,plain,(
% 0.21/0.30 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) = $true) | (((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $false) | ~spl0_3),
% 0.21/0.30 inference(fool_paramodulation,[],[f62])).
% 0.21/0.30 thf(f101,definition,(
% 0.21/0.30 spl0_11 <=> (((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) = $false)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition])).
% 0.21/0.30 thf(f105,definition,(
% 0.21/0.30 spl0_12 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) = $true)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition])).
% 0.21/0.30 thf(f108,plain,(
% 0.21/0.30 spl0_11 | spl0_12 | ~spl0_3),
% 0.21/0.30 inference(avatar_split_clause,[],[f99,f60,f105,f101])).
% 0.21/0.30 thf(f124,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((X2 = X0))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ $true)))))) )),
% 0.21/0.30 inference(fool_paramodulation,[],[f46])).
% 0.21/0.30 thf(f126,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : ((((((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ (X2 = X0)))) = $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true)) )),
% 0.21/0.30 inference(fool_paramodulation,[],[f46])).
% 0.21/0.30 thf(f128,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ $true))))) | (X0 != X2)) )),
% 0.21/0.30 inference(equality_proxy_clausification,[],[f124])).
% 0.21/0.30 thf(f129,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i)) & $false)))) | (X0 != X2)) )),
% 0.21/0.30 inference(boolean_simplification,[],[f128])).
% 0.21/0.30 thf(f130,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (X0 != X2)) )),
% 0.21/0.30 inference(boolean_simplification,[],[f129])).
% 0.21/0.30 thf(f136,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((~ (X2 = X0)))) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | ((((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i))) = $false)) )),
% 0.21/0.30 inference(and_proxy_clausification,[],[f126])).
% 0.21/0.30 thf(f137,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (((((X0 @ X1 @ lAnna_THFTYPE_i) & (X2 @ X1 @ lBill_THFTYPE_i))) = $false) | ($true = ((X2 = X0))) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true)) )),
% 0.21/0.30 inference(not_proxy_clausification,[],[f136])).
% 0.21/0.30 thf(f138,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($true = ((X2 = X0))) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | ($false = ((X0 @ X1 @ lAnna_THFTYPE_i)))) )),
% 0.21/0.30 inference(and_proxy_clausification,[],[f137])).
% 0.21/0.30 thf(f139,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((X0 @ X1 @ lAnna_THFTYPE_i))) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | (X0 = X2)) )),
% 0.21/0.30 inference(equality_proxy_clausification,[],[f138])).
% 0.21/0.30 thf(f142,definition,(
% 0.21/0.30 spl0_15 <=> ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : (X0 != X2)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition])).
% 0.21/0.30 thf(f143,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : ((X0 != X2)) ) | ~spl0_15),
% 0.21/0.30 inference(avatar_component_clause,[],[f142])).
% 0.21/0.30 thf(f145,definition,(
% 0.21/0.30 spl0_16 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition])).
% 0.21/0.30 thf(f147,plain,(
% 0.21/0.30 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl0_16),
% 0.21/0.30 inference(avatar_component_clause,[],[f145])).
% 0.21/0.30 thf(f148,plain,(
% 0.21/0.30 spl0_15 | ~spl0_16),
% 0.21/0.30 inference(avatar_split_clause,[],[f130,f145,f142])).
% 0.21/0.30 thf(f150,definition,(
% 0.21/0.30 spl0_17 <=> ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((X0 @ X1 @ lAnna_THFTYPE_i))) | (X0 = X2) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition])).
% 0.21/0.30 thf(f151,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X0 : ($i > $i > $o),X1 : $i] : (($false = ((X0 @ X1 @ lAnna_THFTYPE_i))) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (X0 = X2)) ) | ~spl0_17),
% 0.21/0.30 inference(avatar_component_clause,[],[f150])).
% 0.21/0.30 thf(f152,plain,(
% 0.21/0.30 ~spl0_12 | spl0_17),
% 0.21/0.30 inference(avatar_split_clause,[],[f139,f150,f105])).
% 0.21/0.30 thf(f153,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) @ X1 @ lAnna_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: (Y0 = Y1)))) = X2) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false)) ) | ~spl0_17),
% 0.21/0.30 inference(primitive_instantiation,[],[f151])).
% 0.21/0.30 thf(f158,plain,(
% 0.21/0.30 ( ! [X0 : ($i > $i > $o)] : ((parent_THFTYPE_IiioI = X0) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ($false = ((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) ) | (~spl0_5 | ~spl0_17)),
% 0.21/0.30 inference(superposition,[],[f72,f151])).
% 0.21/0.30 thf(f166,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X1 : $i] : (($false = ((X1 = lAnna_THFTYPE_i))) | (= = X2) | (((X2 @ X1 @ lBill_THFTYPE_i)) = $false)) ) | ~spl0_17),
% 0.21/0.30 inference(beta-eta_normalization,[],[f153])).
% 0.21/0.30 thf(f167,plain,(
% 0.21/0.30 ( ! [X2 : ($i > $i > $o),X1 : $i] : ((((X2 @ X1 @ lBill_THFTYPE_i)) = $false) | (lAnna_THFTYPE_i != X1) | (= = X2)) ) | ~spl0_17),
% 0.21/0.30 inference(equality_proxy_clausification,[],[f166])).
% 0.21/0.30 thf(f177,definition,(
% 0.21/0.30 spl0_19 <=> ! [X0 : ($i > $i > $o)] : ((parent_THFTYPE_IiioI = X0) | ($false = ((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i))))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition])).
% 0.21/0.30 thf(f178,plain,(
% 0.21/0.30 ( ! [X0 : ($i > $i > $o)] : (($false = ((X0 @ lMary_THFTYPE_i @ lBill_THFTYPE_i))) | (parent_THFTYPE_IiioI = X0)) ) | ~spl0_19),
% 0.21/0.30 inference(avatar_component_clause,[],[f177])).
% 0.21/0.30 thf(f179,plain,(
% 0.21/0.30 spl0_16 | spl0_19 | ~spl0_5 | ~spl0_17),
% 0.21/0.30 inference(avatar_split_clause,[],[f158,f150,f70,f177,f145])).
% 0.21/0.30 thf(f180,plain,(
% 0.21/0.30 $false | ~spl0_15),
% 0.21/0.30 inference(flex-flex_simplification,[],[f143])).
% 0.21/0.30 thf(f181,plain,(
% 0.21/0.30 ~spl0_15),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f180])).
% 0.21/0.30 thf(f183,plain,(
% 0.21/0.30 ( ! [X0 : ($i > $i > $o)] : ((parent_THFTYPE_IiioI = X0) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)) ) | (~spl0_6 | ~spl0_17)),
% 0.21/0.30 inference(superposition,[],[f77,f151])).
% 0.21/0.30 thf(f190,definition,(
% 0.21/0.30 spl0_21 <=> ! [X0 : ($i > $i > $o)] : ((parent_THFTYPE_IiioI = X0) | (((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition])).
% 0.21/0.30 thf(f191,plain,(
% 0.21/0.30 ( ! [X0 : ($i > $i > $o)] : ((((X0 @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (parent_THFTYPE_IiioI = X0)) ) | ~spl0_21),
% 0.21/0.30 inference(avatar_component_clause,[],[f190])).
% 0.21/0.30 thf(f192,plain,(
% 0.21/0.30 spl0_16 | spl0_21 | ~spl0_6 | ~spl0_17),
% 0.21/0.30 inference(avatar_split_clause,[],[f183,f150,f75,f190,f145])).
% 0.21/0.30 thf(f233,plain,(
% 0.21/0.30 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | ~spl0_8),
% 0.21/0.30 inference(fool_paramodulation,[],[f87])).
% 0.21/0.30 thf(f236,plain,(
% 0.21/0.30 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | ~spl0_8),
% 0.21/0.30 inference(boolean_simplification,[],[f233])).
% 0.21/0.30 thf(f237,plain,(
% 0.21/0.30 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | (~spl0_8 | spl0_16)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f236,f147])).
% 0.21/0.30 thf(f239,definition,(
% 0.21/0.30 spl0_27 <=> (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition])).
% 0.21/0.30 thf(f242,plain,(
% 0.21/0.30 spl0_27 | ~spl0_8 | spl0_16),
% 0.21/0.30 inference(avatar_split_clause,[],[f237,f145,f85,f239])).
% 0.21/0.30 thf(f345,plain,(
% 0.21/0.30 (parent_THFTYPE_IiioI = likes_THFTYPE_IiioI) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (~spl0_9 | ~spl0_19)),
% 0.21/0.30 inference(superposition,[],[f92,f178])).
% 0.21/0.30 thf(f372,plain,(
% 0.21/0.30 (parent_THFTYPE_IiioI = likes_THFTYPE_IiioI) | (~spl0_9 | spl0_16 | ~spl0_19)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f345,f147])).
% 0.21/0.30 thf(f374,definition,(
% 0.21/0.30 spl0_34 <=> (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition])).
% 0.21/0.30 thf(f379,definition,(
% 0.21/0.30 spl0_35 <=> (parent_THFTYPE_IiioI = =)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition])).
% 0.21/0.30 thf(f381,plain,(
% 0.21/0.30 (parent_THFTYPE_IiioI = =) | ~spl0_35),
% 0.21/0.30 inference(avatar_component_clause,[],[f379])).
% 0.21/0.30 thf(f384,definition,(
% 0.21/0.30 spl0_36 <=> (parent_THFTYPE_IiioI = likes_THFTYPE_IiioI)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition])).
% 0.21/0.30 thf(f386,plain,(
% 0.21/0.30 (parent_THFTYPE_IiioI = likes_THFTYPE_IiioI) | ~spl0_36),
% 0.21/0.30 inference(avatar_component_clause,[],[f384])).
% 0.21/0.30 thf(f387,plain,(
% 0.21/0.30 spl0_36 | ~spl0_9 | spl0_16 | ~spl0_19),
% 0.21/0.30 inference(avatar_split_clause,[],[f372,f177,f145,f90,f384])).
% 0.21/0.30 thf(f388,plain,(
% 0.21/0.30 ( ! [X1 : $i] : ((((parent_THFTYPE_IiioI @ X1)) = ((likes_THFTYPE_IiioI @ X1)))) ) | ~spl0_36),
% 0.21/0.30 inference(argument_congruence,[],[f386])).
% 0.21/0.30 thf(f389,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((likes_THFTYPE_IiioI @ X1 @ X2)) = ((parent_THFTYPE_IiioI @ X1 @ X2)))) ) | ~spl0_36),
% 0.21/0.30 inference(argument_congruence,[],[f388])).
% 0.21/0.30 thf(f390,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $false) | (((likes_THFTYPE_IiioI @ X1 @ X2)) = $true)) ) | ~spl0_36),
% 0.21/0.30 inference(iff_proxy_clausification,[],[f389])).
% 0.21/0.30 thf(f397,plain,(
% 0.21/0.30 ($true = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (~spl0_6 | ~spl0_36)),
% 0.21/0.30 inference(superposition,[],[f77,f390])).
% 0.21/0.30 thf(f414,plain,(
% 0.21/0.30 ($true = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) | (~spl0_6 | spl0_16 | ~spl0_36)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f397,f147])).
% 0.21/0.30 thf(f419,definition,(
% 0.21/0.30 spl0_37 <=> ($true = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i)))),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition])).
% 0.21/0.30 thf(f422,plain,(
% 0.21/0.30 spl0_37 | ~spl0_6 | spl0_16 | ~spl0_36),
% 0.21/0.30 inference(avatar_split_clause,[],[f414,f384,f145,f75,f419])).
% 0.21/0.30 thf(f526,plain,(
% 0.21/0.30 ((((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl0_21),
% 0.21/0.30 inference(primitive_instantiation,[],[f191])).
% 0.21/0.30 thf(f533,plain,(
% 0.21/0.30 ($false = $true) | (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl0_21),
% 0.21/0.30 inference(beta-eta_normalization,[],[f526])).
% 0.21/0.30 thf(f534,plain,(
% 0.21/0.30 (parent_THFTYPE_IiioI = (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | ~spl0_21),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f533])).
% 0.21/0.30 thf(f547,plain,(
% 0.21/0.30 spl0_34 | ~spl0_21),
% 0.21/0.30 inference(avatar_split_clause,[],[f534,f190,f374])).
% 0.21/0.30 thf(f556,plain,(
% 0.21/0.30 ( ! [X1 : $i] : ((lAnna_THFTYPE_i != X1) | ($false = (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ X1 @ lBill_THFTYPE_i))) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)) ) | ~spl0_17),
% 0.21/0.30 inference(primitive_instantiation,[],[f167])).
% 0.21/0.30 thf(f569,plain,(
% 0.21/0.30 ( ! [X1 : $i] : (($false = $true) | (lAnna_THFTYPE_i != X1) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)) ) | ~spl0_17),
% 0.21/0.30 inference(beta-eta_normalization,[],[f556])).
% 0.21/0.30 thf(f570,plain,(
% 0.21/0.30 ( ! [X1 : $i] : ((lAnna_THFTYPE_i != X1) | ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)) ) | ~spl0_17),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f569])).
% 0.21/0.30 thf(f589,definition,(
% 0.21/0.30 spl0_45 <=> ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) = =)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition])).
% 0.21/0.30 thf(f593,definition,(
% 0.21/0.30 spl0_46 <=> ! [X1 : $i] : (lAnna_THFTYPE_i != X1)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition])).
% 0.21/0.30 thf(f594,plain,(
% 0.21/0.30 ( ! [X1 : $i] : ((lAnna_THFTYPE_i != X1)) ) | ~spl0_46),
% 0.21/0.30 inference(avatar_component_clause,[],[f593])).
% 0.21/0.30 thf(f595,plain,(
% 0.21/0.30 spl0_45 | spl0_46 | ~spl0_17),
% 0.21/0.30 inference(avatar_split_clause,[],[f570,f150,f593,f589])).
% 0.21/0.30 thf(f621,definition,(
% 0.21/0.30 spl0_51 <=> (lMary_THFTYPE_i = lAnna_THFTYPE_i)),
% 0.21/0.30 introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition])).
% 0.21/0.30 thf(f625,plain,(
% 0.21/0.30 ( ! [X1 : $i] : ((((parent_THFTYPE_IiioI @ X1)) = ((= @ X1)))) ) | ~spl0_35),
% 0.21/0.30 inference(argument_congruence,[],[f381])).
% 0.21/0.30 thf(f626,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = ((X1 = X2)))) ) | ~spl0_35),
% 0.21/0.30 inference(argument_congruence,[],[f625])).
% 0.21/0.30 thf(f628,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $false) | ($true = ((X1 = X2)))) ) | ~spl0_35),
% 0.21/0.30 inference(iff_proxy_clausification,[],[f626])).
% 0.21/0.30 thf(f629,plain,(
% 0.21/0.30 ( ! [X2 : $i,X1 : $i] : ((((parent_THFTYPE_IiioI @ X1 @ X2)) = $false) | (X1 = X2)) ) | ~spl0_35),
% 0.21/0.30 inference(equality_proxy_clausification,[],[f628])).
% 0.21/0.30 thf(f635,plain,(
% 0.21/0.30 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (lMary_THFTYPE_i = lAnna_THFTYPE_i) | (~spl0_5 | ~spl0_35)),
% 0.21/0.30 inference(superposition,[],[f72,f629])).
% 0.21/0.30 thf(f659,plain,(
% 0.21/0.30 (lMary_THFTYPE_i = lAnna_THFTYPE_i) | (~spl0_5 | spl0_16 | ~spl0_35)),
% 0.21/0.30 inference(forward_subsumption_resolution,[],[f635,f147])).
% 0.21/0.30 thf(f667,plain,(
% 0.21/0.30 spl0_51 | ~spl0_5 | spl0_16 | ~spl0_35),
% 0.21/0.30 inference(avatar_split_clause,[],[f659,f379,f145,f70,f621])).
% 0.21/0.30 thf(f673,definition,(
% 0.21/0.30 ((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) != =) | (parent_THFTYPE_IiioI != (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) | (parent_THFTYPE_IiioI = =)),
% 0.21/0.30 introduced(theory,[theory_tautology_sat_conflict])).
% 0.21/0.30 thf(f688,plain,(
% 0.21/0.30 (lAnna_THFTYPE_i != lAnna_THFTYPE_i) | ~spl0_46),
% 0.21/0.30 inference(imitation,[],[f594])).
% 0.21/0.30 thf(f691,plain,(
% 0.21/0.30 $false | ~spl0_46),
% 0.21/0.30 inference(trivial_inequality_removal,[],[f688])).
% 0.21/0.30 thf(f692,plain,(
% 0.21/0.30 ~spl0_46),
% 0.21/0.30 inference(avatar_contradiction_clause,[],[f691])).
% 0.21/0.30 thf(f693,definition,(
% 0.21/0.30 (lMary_THFTYPE_i != lAnna_THFTYPE_i) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) != $false) | ($true != ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lAnna_THFTYPE_i))) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)) != $true) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.21/0.30 introduced(theory,[theory_tautology_sat_conflict])).
% 0.21/0.30 thf(f695,definition,(
% 0.21/0.30 (((parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i)) != $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBen_THFTYPE_i))) != $true) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.21/0.30 introduced(theory,[theory_tautology_sat_conflict])).
% 0.21/0.30 cnf(s3, plain, spl0_3, inference(sat_conversion,[],[f63])).
% 0.21/0.30 cnf(s5, plain, spl0_5, inference(sat_conversion,[],[f73])).
% 0.21/0.30 cnf(s6, plain, spl0_6, inference(sat_conversion,[],[f78])).
% 0.21/0.30 cnf(s8, plain, spl0_8, inference(sat_conversion,[],[f88])).
% 0.21/0.30 cnf(s9, plain, spl0_9, inference(sat_conversion,[],[f93])).
% 0.21/0.30 cnf(s11, plain, ~spl0_3 | spl0_11 | spl0_12, inference(sat_conversion,[],[f108])).
% 0.21/0.30 cnf(s14, plain, spl0_15 | ~spl0_16, inference(sat_conversion,[],[f148])).
% 0.21/0.30 cnf(s15, plain, ~spl0_12 | spl0_17, inference(sat_conversion,[],[f152])).
% 0.21/0.30 cnf(s17, plain, ~spl0_5 | spl0_16 | ~spl0_17 | spl0_19, inference(sat_conversion,[],[f179])).
% 0.21/0.30 cnf(s18, plain, ~spl0_15, inference(sat_conversion,[],[f181])).
% 0.21/0.30 cnf(s20, plain, ~spl0_6 | spl0_16 | ~spl0_17 | spl0_21, inference(sat_conversion,[],[f192])).
% 0.21/0.30 cnf(s26, plain, ~spl0_8 | spl0_16 | spl0_27, inference(sat_conversion,[],[f242])).
% 0.21/0.30 cnf(s32, plain, ~spl0_9 | spl0_16 | ~spl0_19 | spl0_36, inference(sat_conversion,[],[f387])).
% 0.21/0.30 cnf(s33, plain, ~spl0_6 | spl0_16 | ~spl0_36 | spl0_37, inference(sat_conversion,[],[f422])).
% 0.21/0.30 cnf(s45, plain, ~spl0_21 | spl0_34, inference(sat_conversion,[],[f547])).
% 0.21/0.30 cnf(s49, plain, ~spl0_17 | spl0_45 | spl0_46, inference(sat_conversion,[],[f595])).
% 0.21/0.30 cnf(s57, plain, ~spl0_5 | spl0_16 | ~spl0_35 | spl0_51, inference(sat_conversion,[],[f667])).
% 0.21/0.30 cnf(s59, plain, ~spl0_34 | spl0_35 | ~spl0_45, inference(sat_conversion,[],[f673])).
% 0.21/0.30 cnf(s63, plain, ~spl0_46, inference(sat_conversion,[],[f692])).
% 0.21/0.30 cnf(s64, plain, ~spl0_12 | spl0_16 | ~spl0_27 | ~spl0_37 | ~spl0_51, inference(sat_conversion,[],[f693])).
% 0.21/0.30 cnf(s66, plain, ~spl0_3 | ~spl0_11 | spl0_16, inference(sat_conversion,[],[f695])).
% 0.21/0.30 cnf(s67, plain, ~spl0_17 | spl0_45, inference(rat,[],[s49,s63])).
% 0.21/0.30 cnf(s68, plain, ~spl0_16, inference(rat,[],[s14,s18])).
% 0.21/0.30 cnf(s69, plain, spl0_27, inference(rat,[],[s26,s68,s8])).
% 0.21/0.30 cnf(s70, plain, ~spl0_11, inference(rat,[],[s66,s68,s3])).
% 0.21/0.30 cnf(s71, plain, spl0_12, inference(rat,[],[s11,s3,s70])).
% 0.21/0.30 cnf(s72, plain, spl0_17, inference(rat,[],[s15,s71])).
% 0.21/0.30 cnf(s73, plain, spl0_45, inference(rat,[],[s67,s72])).
% 0.21/0.30 cnf(s74, plain, spl0_21, inference(rat,[],[s20,s6,s68,s72])).
% 0.21/0.30 cnf(s75, plain, spl0_19, inference(rat,[],[s17,s5,s68,s72])).
% 0.21/0.30 cnf(s76, plain, spl0_34, inference(rat,[],[s45,s74])).
% 0.21/0.30 cnf(s77, plain, spl0_36, inference(rat,[],[s32,s9,s68,s75])).
% 0.21/0.30 cnf(s78, plain, spl0_35, inference(rat,[],[s59,s73,s76])).
% 0.21/0.30 cnf(s82, plain, spl0_37, inference(rat,[],[s33,s6,s68,s77])).
% 0.21/0.30 cnf(s84, plain, spl0_51, inference(rat,[],[s57,s5,s68,s78])).
% 0.21/0.30 cnf(s87, plain, $false, inference(rat,[],[s64,s71,s69,s68,s84,s82])).
% 0.21/0.30 thf(f696,plain,(
% 0.21/0.30 $false),
% 0.21/0.30 inference(avatar_sat_refutation,[],[s87])).
% 0.21/0.30 % SZS output end Proof for theBenchmark
% 0.21/0.30 % (3715409)------------------------------
% 0.21/0.30 % (3715409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.30 % (3715409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.30 % (3715409)CaDiCaL version: 2.1.3
% 0.21/0.30 % (3715409)Termination reason: Refutation
% 0.21/0.30 % (3715409)Time elapsed: 0.021 s
% 0.21/0.30 % (3715409)Peak memory usage: 13 MB
% 0.21/0.30 % (3715409)Instructions burned: 33 (million)
% 0.21/0.30 % (3715401)Success in time 0.056 s
% 0.21/0.30 % Vampire exiting
%------------------------------------------------------------------------------