%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR131^1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:47:05 AM UTC 2026
% Result : Theorem 0.10s 0.28s
% Output : Refutation 0.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR131^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n003.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 17:57:29 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.28 % (2843129)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.10/0.28 % (2843139)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=3517470973: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.10/0.28 % (2843142)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.10/0.28 % (2843142)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.10/0.28 % (2843142)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=1319558974:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.10/0.28 % (2843141)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=370567994:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.10/0.28 % (2843137)lrs+10_16_si=on:nwc=1.5:random_seed=2558664131:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.10/0.28 % (2843138)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=2219055723:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.10/0.28 % (2843136)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=2227909209:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.10/0.28 % (2843140)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=2715219727:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.10/0.28 % (2843138)Refutation not found, incomplete strategy
% 0.10/0.28 % (2843138)------------------------------
% 0.10/0.28 % (2843138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.28 % (2843138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.28 % (2843138)CaDiCaL version: 2.1.3
% 0.10/0.28 % (2843138)Termination reason: Refutation not found, incomplete strategy
% 0.10/0.28 % (2843138)Time elapsed: 0.003 s
% 0.10/0.28 % (2843138)Peak memory usage: 12 MB
% 0.10/0.28 % (2843136)Refutation not found, incomplete strategy
% 0.10/0.28 % (2843136)------------------------------
% 0.10/0.28 % (2843136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.28 % (2843138)Instructions burned: 4 (million)
% 0.10/0.28 % (2843136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.28 % (2843136)CaDiCaL version: 2.1.3
% 0.10/0.28 % (2843136)Termination reason: Refutation not found, incomplete strategy
% 0.10/0.28 % (2843136)Time elapsed: 0.003 s
% 0.10/0.28 % (2843136)Peak memory usage: 12 MB
% 0.10/0.28 % (2843136)Instructions burned: 4 (million)
% 0.10/0.28 % (2843138)------------------------------
% 0.10/0.28 % (2843138)------------------------------
% 0.10/0.28 % (2843136)------------------------------
% 0.10/0.28 % (2843136)------------------------------
% 0.10/0.28 % (2843140)Refutation not found, incomplete strategy
% 0.10/0.28 % (2843140)------------------------------
% 0.10/0.28 % (2843140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.28 % (2843140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.28 % (2843140)CaDiCaL version: 2.1.3
% 0.10/0.28 % (2843140)Termination reason: Refutation not found, incomplete strategy
% 0.10/0.28 % (2843140)Time elapsed: 0.003 s
% 0.10/0.28 % (2843140)Peak memory usage: 11 MB
% 0.10/0.28 % (2843140)Instructions burned: 4 (million)
% 0.10/0.28 % (2843140)------------------------------
% 0.10/0.28 % (2843140)------------------------------
% 0.10/0.28 % (2843139) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2843129-2843139"...
% 0.10/0.28 % (2843137)Instruction limit reached!
% 0.10/0.28 % (2843137)------------------------------
% 0.10/0.28 % (2843137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.28 % (2843137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.28 % (2843137)CaDiCaL version: 2.1.3
% 0.10/0.28 % (2843137)Termination reason: Instruction limit
% 0.10/0.28 % (2843137)Termination phase: Saturation
% 0.10/0.28 % (2843137)Time elapsed: 0.013 s
% 0.10/0.28 % (2843137)Peak memory usage: 12 MB
% 0.10/0.28 % (2843137)Instructions burned: 18 (million)
% 0.10/0.28 % (2843139)...printing done.
% 0.10/0.28 % (2843139)Refutation found. Thanks to Tanya!
% 0.10/0.28 % SZS status Theorem for theBenchmark
% 0.10/0.28 % SZS output start Proof for theBenchmark
% 0.10/0.28 thf(type_def_5, type, num: $tType).
% 0.10/0.28 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.10/0.28 thf(func_def_0, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 0.10/0.28 thf(func_def_7, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 0.10/0.28 thf(func_def_8, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 0.10/0.28 thf(func_def_10, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 0.10/0.28 thf(func_def_12, type, vNOT: ($o > $o)).
% 0.10/0.28 thf(func_def_15, type, vAND: ($o > $o > $o)).
% 0.10/0.28 thf(func_def_16, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.10/0.28 thf(func_def_17, type, db0: !>[X0: $tType]:(X0)).
% 0.10/0.28 thf(func_def_18, type, db1: !>[X0: $tType]:(X0)).
% 0.10/0.28 thf(func_def_19, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.10/0.28 thf(func_def_21, type, sK1: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_22, type, sK2: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_23, type, sK3: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_24, type, sK4: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_25, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.10/0.28 thf(func_def_26, type, sK5: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_27, type, sK6: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_28, type, sK7: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_29, type, sK8: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_30, type, sK9: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_31, type, sK10: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_32, type, sK11: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_33, type, sK12: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_34, type, sK13: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_35, type, sK14: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_36, type, sK15: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_37, type, sK16: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_38, type, sK17: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_39, type, sK18: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_40, type, sK19: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(func_def_41, type, sK20: (($i > $i > $o) > $i)).
% 0.10/0.28 thf(f1,axiom,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.10/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax)).
% 0.10/0.28 thf(f5,axiom,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))),
% 0.10/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_004)).
% 0.10/0.28 thf(f10,axiom,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 0.10/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_009)).
% 0.10/0.28 thf(f11,conjecture,(
% 0.10/0.28 ? [X0 : ($i > $i > $o),X2 : $i,X1 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X4 : $i,X3 : $i] : (X1 @ X3 @ X4)) & (X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i) & (~ ! [X3 : $i,X4 : $i] : (X0 @ X3 @ X4)))),
% 0.10/0.28 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 0.10/0.28 thf(f12,negated_conjecture,(
% 0.10/0.28 ~ ? [X0 : ($i > $i > $o),X2 : $i,X1 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X4 : $i,X3 : $i] : (X1 @ X3 @ X4)) & (X1 @ X2 @ lBill_THFTYPE_i) & (X0 @ X2 @ lAnna_THFTYPE_i) & (~ ! [X3 : $i,X4 : $i] : (X0 @ X3 @ X4)))),
% 0.10/0.28 inference(negated_conjecture,[status(cth)],[f11])).
% 0.10/0.28 thf(f19,plain,(
% 0.10/0.28 ~ ? [X0 : ($i > $i > $o),X1 : $i,X2 : ($i > $i > $o)] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ ! [X3 : $i,X4 : $i] : (X2 @ X4 @ X3)) & (X2 @ X1 @ lBill_THFTYPE_i) & (X0 @ X1 @ lAnna_THFTYPE_i) & (~ ! [X5 : $i,X6 : $i] : (X0 @ X5 @ X6)))),
% 0.10/0.28 inference(rectify,[],[f12])).
% 0.10/0.28 thf(f20,plain,(
% 0.10/0.28 ~ ? [X1 : $i,X0 : ($i > $i > $o),X2 : ($i > $i > $o)] : ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y0 @ Y1))))))))))),
% 0.10/0.28 inference(fool_elimination,[],[f19])).
% 0.10/0.28 thf(f29,plain,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))),
% 0.10/0.28 inference(rectify,[],[f5])).
% 0.10/0.28 thf(f30,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.10/0.28 inference(fool_elimination,[],[f29])).
% 0.10/0.28 thf(f31,plain,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))),
% 0.10/0.28 inference(rectify,[],[f10])).
% 0.10/0.28 thf(f32,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.10/0.28 inference(fool_elimination,[],[f31])).
% 0.10/0.28 thf(f33,plain,(
% 0.10/0.28 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))),
% 0.10/0.28 inference(rectify,[],[f1])).
% 0.10/0.28 thf(f34,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.10/0.28 inference(fool_elimination,[],[f33])).
% 0.10/0.28 thf(f35,plain,(
% 0.10/0.28 ! [X1 : $i,X2 : ($i > $i > $o),X0 : ($i > $i > $o)] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X0 @ Y1 @ Y0)))))) & (X0 @ X1 @ lAnna_THFTYPE_i)) & (X2 @ X1 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y0 @ Y1))))))))))),
% 0.10/0.28 inference(ennf_transformation,[],[f20])).
% 0.10/0.28 thf(f36,plain,(
% 0.10/0.28 ! [X0 : $i,X1 : ($i > $i > $o),X2 : ($i > $i > $o)] : ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y0 @ Y1))))))))))),
% 0.10/0.28 inference(rectify,[],[f35])).
% 0.10/0.28 thf(f37,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.10/0.28 inference(cnf_transformation,[],[f30])).
% 0.10/0.28 thf(f39,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.10/0.28 inference(cnf_transformation,[],[f34])).
% 0.10/0.28 thf(f42,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.10/0.28 inference(cnf_transformation,[],[f32])).
% 0.10/0.28 thf(f46,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X1 @ Y0 @ Y1))))))))))) )),
% 0.10/0.28 inference(cnf_transformation,[],[f36])).
% 0.10/0.28 thf(f49,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(beta-eta_normalization,[],[f46])).
% 0.10/0.28 thf(f56,definition,(
% 0.10/0.28 spl0_2 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 0.10/0.28 thf(f58,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)))) = $true) | ~spl0_2),
% 0.10/0.28 inference(avatar_component_clause,[],[f56])).
% 0.10/0.28 thf(f59,plain,(
% 0.10/0.28 spl0_2),
% 0.10/0.28 inference(avatar_split_clause,[],[f42,f56])).
% 0.10/0.28 thf(f61,definition,(
% 0.10/0.28 spl0_3 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition])).
% 0.10/0.28 thf(f63,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) = $true) | ~spl0_3),
% 0.10/0.28 inference(avatar_component_clause,[],[f61])).
% 0.10/0.28 thf(f64,plain,(
% 0.10/0.28 spl0_3),
% 0.10/0.28 inference(avatar_split_clause,[],[f39,f61])).
% 0.10/0.28 thf(f86,definition,(
% 0.10/0.28 spl0_8 <=> (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))) = $true)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition])).
% 0.10/0.28 thf(f88,plain,(
% 0.10/0.28 (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))) = $true) | ~spl0_8),
% 0.10/0.28 inference(avatar_component_clause,[],[f86])).
% 0.10/0.28 thf(f89,plain,(
% 0.10/0.28 spl0_8),
% 0.10/0.28 inference(avatar_split_clause,[],[f37,f86])).
% 0.10/0.28 thf(f100,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ $true) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))))) | ($false = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))))) )),
% 0.10/0.28 inference(fool_paramodulation,[],[f49])).
% 0.10/0.28 thf(f108,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = (((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))))) )),
% 0.10/0.28 inference(fool_paramodulation,[],[f49])).
% 0.10/0.28 thf(f123,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($false = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))) @ (sK3 @ X2)))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ $true) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(sigma_proxy_clausification,[],[f100])).
% 0.10/0.28 thf(f124,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($false = ((!! @ $i @ (^[Y0 : $i]: (X2 @ Y0 @ (sK3 @ X2)))))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ $true) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(beta-eta_normalization,[],[f123])).
% 0.10/0.28 thf(f125,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ $true) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))))) | ($false = (((^[Y0 : $i]: (X2 @ Y0 @ (sK3 @ X2))) @ (sK4 @ X2))))) )),
% 0.10/0.28 inference(sigma_proxy_clausification,[],[f124])).
% 0.10/0.28 thf(f126,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((((~ $true) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))))) | (((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false)) )),
% 0.10/0.28 inference(beta-eta_normalization,[],[f125])).
% 0.10/0.28 thf(f127,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : ((((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((($false & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(boolean_simplification,[],[f126])).
% 0.10/0.28 thf(f128,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : ((((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (($false & (X1 @ X0 @ lBill_THFTYPE_i)) & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(boolean_simplification,[],[f127])).
% 0.10/0.28 thf(f129,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X1 : ($i > $i > $o)] : ((((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($false & (~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))))))) )),
% 0.10/0.28 inference(boolean_simplification,[],[f128])).
% 0.10/0.28 thf(f130,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o)] : ((((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))) )),
% 0.10/0.28 inference(boolean_simplification,[],[f129])).
% 0.10/0.28 thf(f144,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i))))) )),
% 0.10/0.28 inference(and_proxy_clausification,[],[f108])).
% 0.10/0.28 thf(f145,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)) & (X1 @ X0 @ lBill_THFTYPE_i)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))))))) )),
% 0.10/0.28 inference(not_proxy_clausification,[],[f144])).
% 0.10/0.28 thf(f146,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : (($false = (((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))) & (X2 @ X0 @ lAnna_THFTYPE_i)))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false)) )),
% 0.10/0.28 inference(and_proxy_clausification,[],[f145])).
% 0.10/0.28 thf(f147,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : ((((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($false = ((~ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i)))) )),
% 0.10/0.28 inference(and_proxy_clausification,[],[f146])).
% 0.10/0.28 thf(f148,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X0 : $i,X1 : ($i > $i > $o)] : ((((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (X1 @ Y0)))))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))))))) )),
% 0.10/0.28 inference(not_proxy_clausification,[],[f147])).
% 0.10/0.28 thf(f149,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o)] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0))))))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($true = (((^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))) @ X3)))) )),
% 0.10/0.28 inference(pi_proxy_clausification,[],[f148])).
% 0.10/0.28 thf(f150,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (X1 @ Y0))) @ X3))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (X2 @ Y1 @ Y0)))) @ X4)))) )),
% 0.10/0.28 inference(pi_proxy_clausification,[],[f149])).
% 0.10/0.28 thf(f151,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X4 : $i] : (($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($true = ((!! @ $i @ (X1 @ X3)))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((!! @ $i @ (^[Y0 : $i]: (X2 @ Y0 @ X4)))))) )),
% 0.10/0.28 inference(beta-eta_normalization,[],[f150])).
% 0.10/0.28 thf(f152,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X4 : $i,X5 : $i] : (($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((X1 @ X3 @ X5))) | ($true = ((!! @ $i @ (^[Y0 : $i]: (X2 @ Y0 @ X4))))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)))) )),
% 0.10/0.28 inference(pi_proxy_clausification,[],[f151])).
% 0.10/0.28 thf(f153,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X4 : $i,X5 : $i] : (($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ($true = (((^[Y0 : $i]: (X2 @ Y0 @ X4)) @ X6))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((X1 @ X3 @ X5)))) )),
% 0.10/0.28 inference(pi_proxy_clausification,[],[f152])).
% 0.10/0.28 thf(f154,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X4 : $i,X5 : $i] : (($true = ((X1 @ X3 @ X5))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | ($true = ((X2 @ X6 @ X4))) | ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false)) )),
% 0.10/0.28 inference(beta-eta_normalization,[],[f153])).
% 0.10/0.28 thf(f165,definition,(
% 0.10/0.28 spl0_12 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition])).
% 0.10/0.28 thf(f167,plain,(
% 0.10/0.28 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | spl0_12),
% 0.10/0.28 inference(avatar_component_clause,[],[f165])).
% 0.10/0.28 thf(f170,definition,(
% 0.10/0.28 spl0_13 <=> ! [X2 : ($i > $i > $o)] : (((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition])).
% 0.10/0.28 thf(f171,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o)] : ((((X2 @ (sK4 @ X2) @ (sK3 @ X2))) = $false)) ) | ~spl0_13),
% 0.10/0.28 inference(avatar_component_clause,[],[f170])).
% 0.10/0.28 thf(f172,plain,(
% 0.10/0.28 ~spl0_12 | spl0_13),
% 0.10/0.28 inference(avatar_split_clause,[],[f130,f170,f165])).
% 0.10/0.28 thf(f174,definition,(
% 0.10/0.28 spl0_14 <=> ! [X2 : ($i > $i > $o),X3 : $i,X4 : $i,X0 : $i,X6 : $i,X5 : $i,X1 : ($i > $i > $o)] : (($true = ((X1 @ X3 @ X5))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | ($true = ((X2 @ X6 @ X4))))),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition])).
% 0.10/0.28 thf(f175,plain,(
% 0.10/0.28 ( ! [X2 : ($i > $i > $o),X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X4 : $i,X5 : $i] : (($true = ((X2 @ X6 @ X4))) | ($true = ((X1 @ X3 @ X5))) | ($false = ((X2 @ X0 @ lAnna_THFTYPE_i))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false)) ) | ~spl0_14),
% 0.10/0.28 inference(avatar_component_clause,[],[f174])).
% 0.10/0.28 thf(f177,definition,(
% 0.10/0.28 spl0_15 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true)))),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition])).
% 0.10/0.28 thf(f180,plain,(
% 0.10/0.28 spl0_14 | ~spl0_15),
% 0.10/0.28 inference(avatar_split_clause,[],[f154,f177,f174])).
% 0.10/0.28 thf(f181,plain,(
% 0.10/0.28 (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $true))) | ~spl0_3),
% 0.10/0.28 inference(fool_paramodulation,[],[f63])).
% 0.10/0.28 thf(f184,definition,(
% 0.10/0.28 spl0_16 <=> (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition])).
% 0.10/0.28 thf(f188,plain,(
% 0.10/0.28 spl0_16 | spl0_15 | ~spl0_3),
% 0.10/0.28 inference(avatar_split_clause,[],[f181,f61,f177,f184])).
% 0.10/0.28 thf(f206,plain,(
% 0.10/0.28 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | ~spl0_2),
% 0.10/0.28 inference(fool_paramodulation,[],[f58])).
% 0.10/0.28 thf(f208,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl0_2),
% 0.10/0.28 inference(boolean_simplification,[],[f206])).
% 0.10/0.28 thf(f241,definition,(
% 0.10/0.28 spl0_20 <=> (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition])).
% 0.10/0.28 thf(f243,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lMary_THFTYPE_i)) = $false) | ~spl0_20),
% 0.10/0.28 inference(avatar_component_clause,[],[f241])).
% 0.10/0.28 thf(f244,plain,(
% 0.10/0.28 spl0_12 | spl0_20 | ~spl0_2),
% 0.10/0.28 inference(avatar_split_clause,[],[f208,f56,f241,f165])).
% 0.10/0.28 thf(f262,plain,(
% 0.10/0.28 ($false = (((^[Y0 : $i]: ((^[Y1 : $i]: ($true)))) @ (sK4 @ (^[Y0 : $i]: ((^[Y1 : $i]: ($true))))) @ (sK3 @ (^[Y0 : $i]: ((^[Y1 : $i]: ($true)))))))) | ~spl0_13),
% 0.10/0.28 inference(primitive_instantiation,[],[f171])).
% 0.10/0.28 thf(f270,plain,(
% 0.10/0.28 ($true = $false) | ~spl0_13),
% 0.10/0.28 inference(beta-eta_normalization,[],[f262])).
% 0.10/0.28 thf(f271,plain,(
% 0.10/0.28 $false | ~spl0_13),
% 0.10/0.28 inference(trivial_inequality_removal,[],[f270])).
% 0.10/0.28 thf(f272,plain,(
% 0.10/0.28 ~spl0_13),
% 0.10/0.28 inference(avatar_contradiction_clause,[],[f271])).
% 0.10/0.28 thf(f290,plain,(
% 0.10/0.28 ( ! [X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X7 : ($i > $i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (X7 @ Y0 @ Y1))))) @ X0 @ lAnna_THFTYPE_i))) | ($true = (((^[Y0 : $i]: ((^[Y1 : $i]: (~ (X7 @ Y0 @ Y1))))) @ X6 @ X4))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((X1 @ X3 @ X5)))) ) | ~spl0_14),
% 0.10/0.28 inference(primitive_instantiation,[],[f175])).
% 0.10/0.28 thf(f309,plain,(
% 0.10/0.28 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : $i] : (($false = ((X0 @ X3 @ lAnna_THFTYPE_i))) | ($false = ((X0 @ X3 @ lBill_THFTYPE_i))) | ($true != $true) | ($true = ((X0 @ X1 @ X2)))) ) | ~spl0_14),
% 0.10/0.28 inference(equality_factoring,[],[f175])).
% 0.10/0.28 thf(f316,plain,(
% 0.10/0.28 ( ! [X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X7 : ($i > $i > $o),X4 : $i,X5 : $i] : (($false = ((~ (X7 @ X0 @ lAnna_THFTYPE_i)))) | ($true = ((~ (X7 @ X6 @ X4)))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((X1 @ X3 @ X5)))) ) | ~spl0_14),
% 0.10/0.28 inference(beta-eta_normalization,[],[f290])).
% 0.10/0.28 thf(f317,plain,(
% 0.10/0.28 ( ! [X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X7 : ($i > $i > $o),X4 : $i,X5 : $i] : ((((X1 @ X0 @ lBill_THFTYPE_i)) = $false) | ($true = ((X7 @ X0 @ lAnna_THFTYPE_i))) | ($true = ((X1 @ X3 @ X5))) | ($true = ((~ (X7 @ X6 @ X4))))) ) | ~spl0_14),
% 0.10/0.28 inference(not_proxy_clausification,[],[f316])).
% 0.10/0.28 thf(f318,plain,(
% 0.10/0.28 ( ! [X3 : $i,X0 : $i,X1 : ($i > $i > $o),X6 : $i,X7 : ($i > $i > $o),X4 : $i,X5 : $i] : (($true = ((X7 @ X0 @ lAnna_THFTYPE_i))) | ($true = ((X1 @ X3 @ X5))) | ($false = ((X7 @ X6 @ X4))) | (((X1 @ X0 @ lBill_THFTYPE_i)) = $false)) ) | ~spl0_14),
% 0.10/0.28 inference(not_proxy_clausification,[],[f317])).
% 0.10/0.28 thf(f335,plain,(
% 0.10/0.28 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true = ((X0 @ X1 @ X2))) | ($false = ((X0 @ X3 @ lAnna_THFTYPE_i))) | ($false = ((X0 @ X3 @ lBill_THFTYPE_i)))) ) | ~spl0_14),
% 0.10/0.28 inference(trivial_inequality_removal,[],[f309])).
% 0.10/0.28 thf(f719,definition,(
% 0.10/0.28 (((parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i)) != $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (parent_THFTYPE_IiioI @ lMary_THFTYPE_i @ lAnna_THFTYPE_i))) != $true) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.10/0.28 introduced(theory,[theory_tautology_sat_conflict])).
% 0.10/0.28 thf(f924,plain,(
% 0.10/0.28 ( ! [X0 : $i] : (($false = ((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))) | ($true = $false) | (((likes_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i)) = $false)) ) | (~spl0_14 | ~spl0_20)),
% 0.10/0.28 inference(superposition,[],[f243,f335])).
% 0.10/0.28 thf(f949,plain,(
% 0.10/0.28 ( ! [X0 : $i] : (($false = ((likes_THFTYPE_IiioI @ X0 @ lBill_THFTYPE_i))) | (((likes_THFTYPE_IiioI @ X0 @ lAnna_THFTYPE_i)) = $false)) ) | (~spl0_14 | ~spl0_20)),
% 0.10/0.28 inference(trivial_inequality_removal,[],[f924])).
% 0.10/0.28 thf(f1008,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (~spl0_8 | ~spl0_14 | ~spl0_20)),
% 0.10/0.28 inference(superposition,[],[f88,f949])).
% 0.10/0.28 thf(f1042,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | (~spl0_8 | spl0_12 | ~spl0_14 | ~spl0_20)),
% 0.10/0.28 inference(forward_subsumption_resolution,[],[f1008,f167])).
% 0.10/0.28 thf(f1050,definition,(
% 0.10/0.28 spl0_42 <=> (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition])).
% 0.10/0.28 thf(f1052,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lAnna_THFTYPE_i)) = $false) | ~spl0_42),
% 0.10/0.28 inference(avatar_component_clause,[],[f1050])).
% 0.10/0.28 thf(f1053,plain,(
% 0.10/0.28 spl0_42 | ~spl0_8 | spl0_12 | ~spl0_14 | ~spl0_20),
% 0.10/0.28 inference(avatar_split_clause,[],[f1042,f241,f174,f165,f86,f1050])).
% 0.10/0.28 thf(f1133,definition,(
% 0.10/0.28 spl0_45 <=> ! [X4 : $i,X5 : $i] : ($false = ((likes_THFTYPE_IiioI @ X4 @ X5)))),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition])).
% 0.10/0.28 thf(f1134,plain,(
% 0.10/0.28 ( ! [X4 : $i,X5 : $i] : (($false = ((likes_THFTYPE_IiioI @ X4 @ X5)))) ) | ~spl0_45),
% 0.10/0.28 inference(avatar_component_clause,[],[f1133])).
% 0.10/0.28 thf(f1138,definition,(
% 0.10/0.28 spl0_46 <=> ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : ((((X0 @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ($true = ((X0 @ X1 @ X2))))),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition])).
% 0.10/0.28 thf(f1139,plain,(
% 0.10/0.28 ( ! [X2 : $i,X0 : ($i > $i > $o),X1 : $i] : (($true = ((X0 @ X1 @ X2))) | (((X0 @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false)) ) | ~spl0_46),
% 0.10/0.28 inference(avatar_component_clause,[],[f1138])).
% 0.10/0.28 thf(f1189,plain,(
% 0.10/0.28 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : $i,X4 : $i] : (($true = $false) | ($true = ((X0 @ X1 @ X2))) | ($false = ((likes_THFTYPE_IiioI @ X3 @ X4))) | (((X0 @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false)) ) | (~spl0_14 | ~spl0_42)),
% 0.10/0.28 inference(superposition,[],[f1052,f318])).
% 0.10/0.28 thf(f1213,plain,(
% 0.10/0.28 ( ! [X2 : $i,X3 : $i,X0 : ($i > $i > $o),X1 : $i,X4 : $i] : (($true = ((X0 @ X1 @ X2))) | (((X0 @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ($false = ((likes_THFTYPE_IiioI @ X3 @ X4)))) ) | (~spl0_14 | ~spl0_42)),
% 0.10/0.28 inference(trivial_inequality_removal,[],[f1189])).
% 0.10/0.28 thf(f1220,plain,(
% 0.10/0.28 spl0_46 | spl0_45 | ~spl0_14 | ~spl0_42),
% 0.10/0.28 inference(avatar_split_clause,[],[f1213,f1050,f174,f1133,f1138])).
% 0.10/0.28 thf(f1260,plain,(
% 0.10/0.28 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (~spl0_8 | ~spl0_45)),
% 0.10/0.28 inference(superposition,[],[f88,f1134])).
% 0.10/0.28 thf(f1305,plain,(
% 0.10/0.28 $false | (~spl0_8 | spl0_12 | ~spl0_45)),
% 0.10/0.28 inference(forward_subsumption_resolution,[],[f1260,f167])).
% 0.10/0.28 thf(f1306,plain,(
% 0.10/0.28 ~spl0_8 | spl0_12 | ~spl0_45),
% 0.10/0.28 inference(avatar_contradiction_clause,[],[f1305])).
% 0.10/0.28 thf(f1349,plain,(
% 0.10/0.28 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (~ $true)))) | (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (~spl0_2 | ~spl0_46)),
% 0.10/0.28 inference(superposition,[],[f58,f1139])).
% 0.10/0.28 thf(f1372,plain,(
% 0.10/0.28 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (~spl0_2 | ~spl0_46)),
% 0.10/0.28 inference(boolean_simplification,[],[f1349])).
% 0.10/0.28 thf(f1398,definition,(
% 0.10/0.28 spl0_53 <=> (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 0.10/0.28 introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition])).
% 0.10/0.28 thf(f1413,plain,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | (~spl0_2 | spl0_12 | ~spl0_46)),
% 0.10/0.28 inference(forward_subsumption_resolution,[],[f1372,f167])).
% 0.10/0.28 thf(f1418,plain,(
% 0.10/0.28 spl0_53 | ~spl0_2 | spl0_12 | ~spl0_46),
% 0.10/0.28 inference(avatar_split_clause,[],[f1413,f1138,f165,f56,f1398])).
% 0.10/0.28 thf(f1420,definition,(
% 0.10/0.28 (((likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i)) != $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lBob_THFTYPE_i @ lBill_THFTYPE_i))) != $true) | ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false)))),
% 0.10/0.28 introduced(theory,[theory_tautology_sat_conflict])).
% 0.10/0.28 cnf(s2, plain, spl0_2, inference(sat_conversion,[],[f59])).
% 0.10/0.28 cnf(s3, plain, spl0_3, inference(sat_conversion,[],[f64])).
% 0.10/0.28 cnf(s8, plain, spl0_8, inference(sat_conversion,[],[f89])).
% 0.10/0.28 cnf(s12, plain, ~spl0_12 | spl0_13, inference(sat_conversion,[],[f172])).
% 0.10/0.28 cnf(s13, plain, spl0_14 | ~spl0_15, inference(sat_conversion,[],[f180])).
% 0.10/0.28 cnf(s15, plain, ~spl0_3 | spl0_15 | spl0_16, inference(sat_conversion,[],[f188])).
% 0.10/0.28 cnf(s21, plain, ~spl0_2 | spl0_12 | spl0_20, inference(sat_conversion,[],[f244])).
% 0.10/0.28 cnf(s23, plain, ~spl0_13, inference(sat_conversion,[],[f272])).
% 0.10/0.28 cnf(s35, plain, ~spl0_3 | spl0_12 | ~spl0_16, inference(sat_conversion,[],[f719])).
% 0.10/0.28 cnf(s46, plain, ~spl0_8 | spl0_12 | ~spl0_14 | ~spl0_20 | spl0_42, inference(sat_conversion,[],[f1053])).
% 0.10/0.28 cnf(s63, plain, ~spl0_14 | ~spl0_42 | spl0_45 | spl0_46, inference(sat_conversion,[],[f1220])).
% 0.10/0.28 cnf(s70, plain, ~spl0_8 | spl0_12 | ~spl0_45, inference(sat_conversion,[],[f1306])).
% 0.10/0.28 cnf(s90, plain, ~spl0_2 | spl0_12 | ~spl0_46 | spl0_53, inference(sat_conversion,[],[f1418])).
% 0.10/0.28 cnf(s92, plain, ~spl0_8 | spl0_12 | ~spl0_53, inference(sat_conversion,[],[f1420])).
% 0.10/0.28 cnf(s94, plain, ~spl0_12, inference(rat,[],[s12,s23])).
% 0.10/0.28 cnf(s97, plain, ~spl0_53, inference(rat,[],[s92,s94,s8])).
% 0.10/0.28 cnf(s98, plain, ~spl0_45, inference(rat,[],[s70,s94,s8])).
% 0.10/0.28 cnf(s99, plain, ~spl0_16, inference(rat,[],[s35,s94,s3])).
% 0.10/0.28 cnf(s100, plain, spl0_15, inference(rat,[],[s15,s99,s3])).
% 0.10/0.28 cnf(s101, plain, spl0_14, inference(rat,[],[s13,s100])).
% 0.10/0.28 cnf(s108, plain, ~spl0_46, inference(rat,[],[s90,s97,s94,s2])).
% 0.10/0.28 cnf(s110, plain, spl0_20, inference(rat,[],[s21,s94,s2])).
% 0.10/0.28 cnf(s112, plain, ~spl0_42, inference(rat,[],[s63,s101,s98,s108])).
% 0.10/0.28 cnf(s113, plain, $false, inference(rat,[],[s46,s101,s8,s94,s112,s110])).
% 0.10/0.28 thf(f1421,plain,(
% 0.10/0.28 $false),
% 0.10/0.28 inference(avatar_sat_refutation,[],[s113])).
% 0.10/0.28 % SZS output end Proof for theBenchmark
% 0.10/0.28 % (2843139)------------------------------
% 0.10/0.28 % (2843139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.10/0.28 % (2843139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.10/0.28 % (2843139)CaDiCaL version: 2.1.3
% 0.10/0.28 % (2843139)Termination reason: Refutation
% 0.10/0.28 % (2843139)Time elapsed: 0.026 s
% 0.10/0.28 % (2843139)Peak memory usage: 13 MB
% 0.10/0.28 % (2843139)Instructions burned: 73 (million)
% 0.10/0.28 % (2843129)Success in time 0.05 s
% 0.10/0.28 % Vampire exiting
%------------------------------------------------------------------------------