%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR144^2 : 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 : n018.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:10 AM UTC 2026
% Result : Theorem 0.48s 0.41s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR144^2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n018.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Tue Sep 29 17:59:11 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.20/0.28 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.48/0.40 % (427857)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.48/0.40 % (427867)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=246625963:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.48/0.40 % (427868)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.48/0.40 % (427868)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.48/0.40 % (427863)lrs+10_16_si=on:nwc=1.5:random_seed=2326721548:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.48/0.40 % (427864)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=1158936217:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.48/0.40 % (427866)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=98094695:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.48/0.40 % (427865)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=1258724665: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.48/0.40 % (427868)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=1328965907:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.48/0.40 % (427864)Instruction limit reached!
% 0.48/0.40 % (427864)------------------------------
% 0.48/0.40 % (427864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.40 % (427864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.40 % (427864)CaDiCaL version: 2.1.3
% 0.48/0.40 % (427864)Termination reason: Instruction limit
% 0.48/0.40 % (427864)Termination phase: shuffling
% 0.48/0.40 % (427864)Time elapsed: 0.002 s
% 0.48/0.40 % (427864)Peak memory usage: 10 MB
% 0.48/0.40 % (427864)Instructions burned: 4 (million)
% 0.48/0.40 % (427863)Instruction limit reached!
% 0.48/0.40 % (427863)------------------------------
% 0.48/0.40 % (427863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.40 % (427863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.40 % (427863)CaDiCaL version: 2.1.3
% 0.48/0.40 % (427863)Termination reason: Instruction limit
% 0.48/0.40 % (427863)Termination phase: Preprocessing 2
% 0.48/0.40 % (427863)Time elapsed: 0.009 s
% 0.48/0.40 % (427863)Peak memory usage: 10 MB
% 0.48/0.40 % (427863)Instructions burned: 20 (million)
% 0.48/0.40 % (427862)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=1578425942:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.48/0.40 % (427866)Instruction limit reached!
% 0.48/0.40 % (427866)------------------------------
% 0.48/0.40 % (427866)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.40 % (427866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.40 % (427866)CaDiCaL version: 2.1.3
% 0.48/0.40 % (427866)Termination reason: Instruction limit
% 0.48/0.41 % (427866)Termination phase: Property scanning
% 0.48/0.41 % (427866)Time elapsed: 0.011 s
% 0.48/0.41 % (427866)Peak memory usage: 10 MB
% 0.48/0.41 % (427866)Instructions burned: 25 (million)
% 0.48/0.41 % (427867)Instruction limit reached!
% 0.48/0.41 % (427867)------------------------------
% 0.48/0.41 % (427867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427867)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427867)Termination reason: Instruction limit
% 0.48/0.41 % (427867)Termination phase: Saturation
% 0.48/0.41 % (427867)Time elapsed: 0.020 s
% 0.48/0.41 % (427867)Peak memory usage: 13 MB
% 0.48/0.41 % (427867)Instructions burned: 76 (million)
% 0.48/0.41 % (427878)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.48/0.41 % (427876)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=1882060708:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.48/0.41 % (427875)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=2224644561:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.48/0.41 % (427878)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=2775614070:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.48/0.41 % (427876)Instruction limit reached!
% 0.48/0.41 % (427876)------------------------------
% 0.48/0.41 % (427876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427876)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427876)Termination reason: Instruction limit
% 0.48/0.41 % (427876)Termination phase: shuffling
% 0.48/0.41 % (427876)Time elapsed: 0.003 s
% 0.48/0.41 % (427876)Peak memory usage: 10 MB
% 0.48/0.41 % (427876)Instructions burned: 6 (million)
% 0.48/0.41 % (427875)Instruction limit reached!
% 0.48/0.41 % (427875)------------------------------
% 0.48/0.41 % (427875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427875)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427875)Termination reason: Instruction limit
% 0.48/0.41 % (427875)Termination phase: shuffling
% 0.48/0.41 % (427875)Time elapsed: 0.003 s
% 0.48/0.41 % (427875)Peak memory usage: 10 MB
% 0.48/0.41 % (427875)Instructions burned: 6 (million)
% 0.48/0.41 % (427878)Instruction limit reached!
% 0.48/0.41 % (427878)------------------------------
% 0.48/0.41 % (427878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427878)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427878)Termination reason: Instruction limit
% 0.48/0.41 % (427878)Termination phase: shuffling
% 0.48/0.41 % (427878)Time elapsed: 0.003 s
% 0.48/0.41 % (427878)Peak memory usage: 10 MB
% 0.48/0.41 % (427878)Instructions burned: 7 (million)
% 0.48/0.41 % (427862)Instruction limit reached!
% 0.48/0.41 % (427862)------------------------------
% 0.48/0.41 % (427862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427862)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427862)Termination reason: Instruction limit
% 0.48/0.41 % (427862)Termination phase: Saturation
% 0.48/0.41 % (427862)Time elapsed: 0.025 s
% 0.48/0.41 % (427862)Peak memory usage: 12 MB
% 0.48/0.41 % (427862)Instructions burned: 96 (million)
% 0.48/0.41 % (427886)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.48/0.41 % (427886)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=632463496:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.48/0.41 % (427883)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.48/0.41 % (427883)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.48/0.41 % (427879)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2828825110:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.48/0.41 % (427886)Instruction limit reached!
% 0.48/0.41 % (427886)------------------------------
% 0.48/0.41 % (427886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427886)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427886)Termination reason: Instruction limit
% 0.48/0.41 % (427886)Termination phase: shuffling
% 0.48/0.41 % (427886)Time elapsed: 0.001 s
% 0.48/0.41 % (427886)Peak memory usage: 10 MB
% 0.48/0.41 % (427886)Instructions burned: 3 (million)
% 0.48/0.41 % (427883)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=3195837317:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.48/0.41 % (427884)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=1420015113:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.48/0.41 % (427885)lrs+10_1_si=on:cs=on:random_seed=2180470043:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.48/0.41 % (427879)Instruction limit reached!
% 0.48/0.41 % (427879)------------------------------
% 0.48/0.41 % (427879)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427865) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-427857-427865"...
% 0.48/0.41 % (427879)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427879)Termination reason: Instruction limit
% 0.48/0.41 % (427879)Termination phase: Property scanning
% 0.48/0.41 % (427879)Time elapsed: 0.010 s
% 0.48/0.41 % (427879)Peak memory usage: 10 MB
% 0.48/0.41 % (427879)Instructions burned: 13 (million)
% 0.48/0.41 % (427889)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=1513980545:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.48/0.41 % (427885)Instruction limit reached!
% 0.48/0.41 % (427885)------------------------------
% 0.48/0.41 % (427885)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427885)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427885)Termination reason: Instruction limit
% 0.48/0.41 % (427885)Termination phase: shuffling
% 0.48/0.41 % (427885)Time elapsed: 0.004 s
% 0.48/0.41 % (427885)Peak memory usage: 10 MB
% 0.48/0.41 % (427885)Instructions burned: 10 (million)
% 0.48/0.41 % (427865)...printing done.
% 0.48/0.41 % (427865)Refutation found. Thanks to Tanya!
% 0.48/0.41 % SZS status Theorem for theBenchmark
% 0.48/0.41 % SZS output start Proof for theBenchmark
% 0.48/0.41 thf(type_def_5, type, num: $tType).
% 0.48/0.41 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.48/0.41 thf(func_def_0, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_1, type, attribute_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_2, type, before_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_3, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_5, type, considers_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_6, type, contraryAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_7, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 0.48/0.41 thf(func_def_8, type, desires_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_9, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_11, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.48/0.41 thf(func_def_12, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_13, type, domain_THFTYPE_IIIiioIIiooIoIiioI: ((($i > $i > $o) > ($i > $o > $o) > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_14, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_15, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_16, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_17, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_18, type, domain_THFTYPE_IIioioIiioI: (($i > $o > $i > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_19, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 0.48/0.41 thf(func_def_20, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.48/0.41 thf(func_def_22, type, father_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_23, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_24, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_25, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_26, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_27, type, hasPurposeForAgent_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 0.48/0.41 thf(func_def_28, type, hasPurpose_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_29, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_30, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_31, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_32, type, inScopeOfInterest_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_33, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_34, type, instance_THFTYPE_IIIiioIiioIioI: ((($i > $i > $o) > $i > $i > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_35, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 0.48/0.41 thf(func_def_36, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 0.48/0.41 thf(func_def_37, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_38, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_39, type, instance_THFTYPE_IIioioIioI: (($i > $o > $i > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_40, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_41, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_42, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.48/0.41 thf(func_def_43, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 0.48/0.41 thf(func_def_47, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 0.48/0.41 thf(func_def_54, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 0.48/0.41 thf(func_def_63, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 0.48/0.41 thf(func_def_67, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 0.48/0.41 thf(func_def_93, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 0.48/0.41 thf(func_def_96, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_97, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_98, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_99, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_100, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_101, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_102, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_103, type, mother_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_107, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.48/0.41 thf(func_def_108, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_109, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_110, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 0.48/0.41 thf(func_def_111, type, patient_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_112, type, possesses_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_113, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_114, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.48/0.41 thf(func_def_115, type, relatedInternalConcept_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 0.48/0.41 thf(func_def_116, type, relatedInternalConcept_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 0.48/0.41 thf(func_def_118, type, result_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_120, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_121, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_122, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_123, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 0.48/0.41 thf(func_def_124, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 0.48/0.41 thf(func_def_125, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 0.48/0.41 thf(func_def_126, type, subrelation_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 0.48/0.41 thf(func_def_127, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_128, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_129, type, time_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_130, type, wants_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_131, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_133, type, vNOT: ($o > $o)).
% 0.48/0.41 thf(func_def_136, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.48/0.41 thf(func_def_137, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.48/0.41 thf(func_def_138, type, db0: !>[X0: $tType]:(X0)).
% 0.48/0.41 thf(func_def_139, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.48/0.41 thf(func_def_140, type, vAND: ($o > $o > $o)).
% 0.48/0.41 thf(func_def_141, type, sK0: ($i > $i)).
% 0.48/0.41 thf(func_def_142, type, sK1: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_143, type, sK2: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_144, type, sK3: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_145, type, sK4: ($i > $i)).
% 0.48/0.41 thf(func_def_146, type, sK5: ($i > $i > $i)).
% 0.48/0.41 thf(func_def_147, type, sK6: ($i > $o > $i)).
% 0.48/0.41 thf(func_def_148, type, sK7: ($i > $i)).
% 0.48/0.41 thf(func_def_149, type, sK8: ($o > $i > $i)).
% 0.48/0.41 thf(func_def_150, type, sK9: ($i > $o)).
% 0.48/0.41 thf(func_def_151, type, sK10: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_152, type, sK11: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_153, type, sK12: (($i > $i > $o) > $i)).
% 0.48/0.41 thf(func_def_154, type, sK13: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_155, type, sK14: ($i > $i > $i)).
% 0.48/0.41 thf(func_def_156, type, sK15: ($i > $i)).
% 0.48/0.41 thf(func_def_157, type, sK16: ($i > $i)).
% 0.48/0.41 thf(func_def_159, type, sK18: ($i > $i)).
% 0.48/0.41 thf(func_def_160, type, sK19: ($i > $i)).
% 0.48/0.41 thf(func_def_161, type, sK20: ($i > $i > $o)).
% 0.48/0.41 thf(func_def_162, type, sK21: ($i > $i)).
% 0.48/0.41 thf(func_def_164, type, db1: !>[X0: $tType]:(X0)).
% 0.48/0.41 thf(f30,axiom,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : ((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i) <=> ! [X1 : $i] : (~ (X0 @ X1 @ X1)))),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_029)).
% 0.48/0.41 thf(f59,axiom,(
% 0.48/0.41 ! [X0 : $o,X1 : $i] : ((believes_THFTYPE_IiooI @ X1 @ X0) => ? [X2 : $i] : (holdsDuring_THFTYPE_IiooI @ X2 @ (considers_THFTYPE_IiooI @ X1 @ X0)))),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_058)).
% 0.48/0.41 thf(f90,axiom,(
% 0.48/0.41 ! [X0 : $i] : (~ ? [X1 : $i] : (holdsDuring_THFTYPE_IiooI @ X1 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))))),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_089)).
% 0.48/0.41 thf(f163,axiom,(
% 0.48/0.41 (instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_162)).
% 0.48/0.41 thf(f268,axiom,(
% 0.48/0.41 (instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_267)).
% 0.48/0.41 thf(f324,conjecture,(
% 0.48/0.41 ? [X0 : $i] : (~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))),
% 0.48/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 0.48/0.41 thf(f325,negated_conjecture,(
% 0.48/0.41 ~ ? [X0 : $i] : (~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))),
% 0.48/0.41 inference(negated_conjecture,[status(cth)],[f324])).
% 0.48/0.41 thf(f346,plain,(
% 0.48/0.41 (instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.48/0.41 inference(rectify,[],[f268])).
% 0.48/0.41 thf(f347,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 inference(fool_elimination,[],[f346])).
% 0.48/0.41 thf(f382,plain,(
% 0.48/0.41 ~ ? [X0 : $i] : (~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))),
% 0.48/0.41 inference(rectify,[],[f325])).
% 0.48/0.41 thf(f383,plain,(
% 0.48/0.41 ~ ? [X0 : $i] : (((~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))) = $true)),
% 0.48/0.41 inference(fool_elimination,[],[f382])).
% 0.48/0.41 thf(f450,plain,(
% 0.48/0.41 ! [X0 : $o,X1 : $i] : ((believes_THFTYPE_IiooI @ X1 @ X0) => ? [X2 : $i] : (holdsDuring_THFTYPE_IiooI @ X2 @ (considers_THFTYPE_IiooI @ X1 @ X0)))),
% 0.48/0.41 inference(rectify,[],[f59])).
% 0.48/0.41 thf(f451,plain,(
% 0.48/0.41 ! [X0 : $o,X1 : $i] : ((((believes_THFTYPE_IiooI @ X1 @ X0)) = $true) => ? [X2 : $i] : (((holdsDuring_THFTYPE_IiooI @ X2 @ (considers_THFTYPE_IiooI @ X1 @ X0))) = $true))),
% 0.48/0.41 inference(fool_elimination,[],[f450])).
% 0.48/0.41 thf(f540,plain,(
% 0.48/0.41 (instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)),
% 0.48/0.41 inference(rectify,[],[f163])).
% 0.48/0.41 thf(f541,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 inference(fool_elimination,[],[f540])).
% 0.48/0.41 thf(f632,plain,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : ((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i) <=> ! [X1 : $i] : (~ (X0 @ X1 @ X1)))),
% 0.48/0.41 inference(rectify,[],[f30])).
% 0.48/0.41 thf(f633,plain,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : ((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) <=> ! [X1 : $i] : (((~ (X0 @ X1 @ X1))) = $true))),
% 0.48/0.41 inference(fool_elimination,[],[f632])).
% 0.48/0.41 thf(f894,plain,(
% 0.48/0.41 ! [X0 : $i] : (~ ? [X1 : $i] : (holdsDuring_THFTYPE_IiooI @ X1 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))))),
% 0.48/0.41 inference(rectify,[],[f90])).
% 0.48/0.41 thf(f895,plain,(
% 0.48/0.41 ! [X0 : $i] : (((~ (?? @ $i @ (^[Y0 : $i]: (holdsDuring_THFTYPE_IiooI @ Y0 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))))))) = $true)),
% 0.48/0.41 inference(fool_elimination,[],[f894])).
% 0.48/0.41 thf(f973,plain,(
% 0.48/0.41 ! [X0 : $i] : (((~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))) != $true)),
% 0.48/0.41 inference(ennf_transformation,[],[f383])).
% 0.48/0.41 thf(f989,plain,(
% 0.48/0.41 ! [X0 : $o,X1 : $i] : (? [X2 : $i] : (((holdsDuring_THFTYPE_IiooI @ X2 @ (considers_THFTYPE_IiooI @ X1 @ X0))) = $true) | (((believes_THFTYPE_IiooI @ X1 @ X0)) != $true))),
% 0.48/0.41 inference(ennf_transformation,[],[f451])).
% 0.48/0.41 thf(f1060,plain,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ? [X1 : $i] : (((~ (X0 @ X1 @ X1))) != $true)) & (! [X1 : $i] : (((~ (X0 @ X1 @ X1))) = $true) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 0.48/0.41 inference(nnf_transformation,[],[f633])).
% 0.48/0.41 thf(f1061,plain,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ? [X1 : $i] : (((~ (X0 @ X1 @ X1))) != $true)) & (! [X2 : $i] : (((~ (X0 @ X2 @ X2))) = $true) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 0.48/0.41 inference(rectify,[],[f1060])).
% 0.48/0.41 thf(f1062,plain,(
% 0.48/0.41 ! [X0 : ($i > $i > $o)] : (((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) = $true) | (((~ (X0 @ (sK1 @ X0) @ (sK1 @ X0)))) != $true)) & (! [X2 : $i] : (((~ (X0 @ X2 @ X2))) = $true) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)))),
% 0.48/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X0)],[f1061])).
% 0.48/0.41 thf(f1075,plain,(
% 0.48/0.41 ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (sK6 @ X1 @ X0) @ (considers_THFTYPE_IiooI @ X1 @ X0))) = $true) | (((believes_THFTYPE_IiooI @ X1 @ X0)) != $true))),
% 0.48/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X2,sK0 @ X0)],[f989])).
% 0.48/0.41 thf(f1157,plain,(
% 0.48/0.41 ( ! [X2 : $i,X0 : ($i > $i > $o)] : ((((~ (X0 @ X2 @ X2))) = $true) | (((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true)) )),
% 0.48/0.41 inference(cnf_transformation,[],[f1062])).
% 0.48/0.41 thf(f1167,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 inference(cnf_transformation,[],[f347])).
% 0.48/0.41 thf(f1191,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((~ (?? @ $i @ (^[Y0 : $i]: (holdsDuring_THFTYPE_IiooI @ Y0 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))))))) = $true)) )),
% 0.48/0.41 inference(cnf_transformation,[],[f895])).
% 0.48/0.41 thf(f1204,plain,(
% 0.48/0.41 ( ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (sK6 @ X1 @ X0) @ (considers_THFTYPE_IiooI @ X1 @ X0))) = $true) | (((believes_THFTYPE_IiooI @ X1 @ X0)) != $true)) )),
% 0.48/0.41 inference(cnf_transformation,[],[f1075])).
% 0.48/0.41 thf(f1335,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 inference(cnf_transformation,[],[f541])).
% 0.48/0.41 thf(f1339,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((~ (believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0)))) != $true)) )),
% 0.48/0.41 inference(cnf_transformation,[],[f973])).
% 0.48/0.41 thf(f1478,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((?? @ $i @ (^[Y0 : $i]: (holdsDuring_THFTYPE_IiooI @ Y0 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i)))))) = $false)) )),
% 0.48/0.41 inference(not_proxy_clausification,[],[f1191])).
% 0.48/0.41 thf(f1479,plain,(
% 0.48/0.41 ( ! [X0 : $i,X1 : $i] : (((((^[Y0 : $i]: (holdsDuring_THFTYPE_IiooI @ Y0 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i)))) @ X1)) = $false)) )),
% 0.48/0.41 inference(pi_proxy_clausification,[],[f1478])).
% 0.48/0.41 thf(f1480,plain,(
% 0.48/0.41 ( ! [X0 : $i,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (considers_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i)))) = $false)) )),
% 0.48/0.41 inference(beta-eta_normalization,[],[f1479])).
% 0.48/0.41 thf(f1498,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (husband_THFTYPE_IiioI @ lMax_THFTYPE_i @ X0))) = $true)) )),
% 0.48/0.41 inference(not_proxy_clausification,[],[f1339])).
% 0.48/0.41 thf(f1502,plain,(
% 0.48/0.41 ( ! [X2 : $i,X0 : ($i > $i > $o)] : ((((instance_THFTYPE_IIiioIioI @ X0 @ lIrreflexiveRelation_THFTYPE_i)) != $true) | ($false = ((X0 @ X2 @ X2)))) )),
% 0.48/0.41 inference(not_proxy_clausification,[],[f1157])).
% 0.48/0.41 thf(f1539,definition,(
% 0.48/0.41 spl22_8 <=> (((instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition])).
% 0.48/0.41 thf(f1541,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ husband_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ~spl22_8),
% 0.48/0.41 inference(avatar_component_clause,[],[f1539])).
% 0.48/0.41 thf(f1542,plain,(
% 0.48/0.41 spl22_8),
% 0.48/0.41 inference(avatar_split_clause,[],[f1167,f1539])).
% 0.48/0.41 thf(f1734,definition,(
% 0.48/0.41 spl22_47 <=> (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true)),
% 0.48/0.41 introduced(definition,[new_symbols(definition,[spl22_47])],[avatar_definition])).
% 0.48/0.41 thf(f1736,plain,(
% 0.48/0.41 (((instance_THFTYPE_IIiioIioI @ wife_THFTYPE_IiioI @ lIrreflexiveRelation_THFTYPE_i)) = $true) | ~spl22_47),
% 0.48/0.41 inference(avatar_component_clause,[],[f1734])).
% 0.48/0.41 thf(f1737,plain,(
% 0.48/0.41 spl22_47),
% 0.48/0.41 inference(avatar_split_clause,[],[f1335,f1734])).
% 0.48/0.41 thf(f2799,definition,(
% 0.48/0.41 spl22_260 <=> (((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ $false)) = $true)),
% 0.48/0.41 introduced(definition,[new_symbols(definition,[spl22_260])],[avatar_definition])).
% 0.48/0.41 thf(f2823,plain,(
% 0.48/0.41 ( ! [X0 : $i] : (($true != $true) | (((husband_THFTYPE_IiioI @ X0 @ X0)) = $false)) ) | ~spl22_8),
% 0.48/0.41 inference(superposition,[],[f1502,f1541])).
% 0.48/0.41 thf(f2824,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((husband_THFTYPE_IiioI @ X0 @ X0)) = $false)) ) | ~spl22_8),
% 0.48/0.41 inference(trivial_inequality_removal,[],[f2823])).
% 0.48/0.41 thf(f2831,plain,(
% 0.48/0.41 (((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ $false)) = $true) | ~spl22_8),
% 0.48/0.41 inference(superposition,[],[f1498,f2824])).
% 0.48/0.41 thf(f2835,plain,(
% 0.48/0.41 ( ! [X0 : $i] : (($false = $true) | (((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))) != $true)) )),
% 0.48/0.41 inference(superposition,[],[f1480,f1204])).
% 0.48/0.41 thf(f2837,plain,(
% 0.48/0.41 ( ! [X0 : $i] : ((((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X0 @ lMax_THFTYPE_i))) != $true)) )),
% 0.48/0.41 inference(trivial_inequality_removal,[],[f2835])).
% 0.48/0.41 thf(f2893,definition,(
% 0.48/0.41 spl22_269 <=> ! [X1 : $i] : (((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X1 @ lMax_THFTYPE_i))) != $true)),
% 0.48/0.41 introduced(definition,[new_symbols(definition,[spl22_269])],[avatar_definition])).
% 0.48/0.41 thf(f2894,plain,(
% 0.48/0.41 ( ! [X1 : $i] : ((((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ (wife_THFTYPE_IiioI @ X1 @ lMax_THFTYPE_i))) != $true)) ) | ~spl22_269),
% 0.48/0.41 inference(avatar_component_clause,[],[f2893])).
% 0.48/0.41 thf(f2922,plain,(
% 0.48/0.41 spl22_269),
% 0.48/0.41 inference(avatar_split_clause,[],[f2837,f2893])).
% 0.48/0.41 thf(f3228,plain,(
% 0.48/0.41 ( ! [X0 : $i] : (($true != $true) | ($false = ((wife_THFTYPE_IiioI @ X0 @ X0)))) ) | ~spl22_47),
% 0.48/0.41 inference(superposition,[],[f1502,f1736])).
% 0.48/0.41 thf(f3229,plain,(
% 0.48/0.41 ( ! [X0 : $i] : (($false = ((wife_THFTYPE_IiioI @ X0 @ X0)))) ) | ~spl22_47),
% 0.48/0.41 inference(trivial_inequality_removal,[],[f3228])).
% 0.48/0.41 thf(f3258,plain,(
% 0.48/0.41 (((believes_THFTYPE_IiooI @ lMax_THFTYPE_i @ $false)) != $true) | (~spl22_47 | ~spl22_269)),
% 0.48/0.41 inference(superposition,[],[f2894,f3229])).
% 0.48/0.41 thf(f3272,plain,(
% 0.48/0.41 ~spl22_260 | ~spl22_47 | ~spl22_269),
% 0.48/0.41 inference(avatar_split_clause,[],[f3258,f2893,f1734,f2799])).
% 0.48/0.41 thf(f3273,plain,(
% 0.48/0.41 spl22_260 | ~spl22_8),
% 0.48/0.41 inference(avatar_split_clause,[],[f2831,f1539,f2799])).
% 0.48/0.41 cnf(s8, plain, spl22_8, inference(sat_conversion,[],[f1542])).
% 0.48/0.41 cnf(s47, plain, spl22_47, inference(sat_conversion,[],[f1737])).
% 0.48/0.41 cnf(s277, plain, spl22_269, inference(sat_conversion,[],[f2922])).
% 0.48/0.41 cnf(s327, plain, ~spl22_47 | ~spl22_260 | ~spl22_269, inference(sat_conversion,[],[f3272])).
% 0.48/0.41 cnf(s328, plain, ~spl22_8 | spl22_260, inference(sat_conversion,[],[f3273])).
% 0.48/0.41 cnf(s344, plain, ~spl22_260, inference(rat,[],[s327,s277,s47])).
% 0.48/0.41 cnf(s346, plain, ~spl22_8, inference(rat,[],[s328,s344])).
% 0.48/0.41 cnf(s355, plain, $false, inference(rat,[],[s8,s346])).
% 0.48/0.41 thf(f3278,plain,(
% 0.48/0.41 $false),
% 0.48/0.41 inference(avatar_sat_refutation,[],[s355])).
% 0.48/0.41 % SZS output end Proof for theBenchmark
% 0.48/0.41 % (427865)------------------------------
% 0.48/0.41 % (427865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.41 % (427865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.41 % (427865)CaDiCaL version: 2.1.3
% 0.48/0.41 % (427865)Termination reason: Refutation
% 0.48/0.41 % (427865)Time elapsed: 0.061 s
% 0.48/0.41 % (427865)Peak memory usage: 15 MB
% 0.48/0.41 % (427865)Instructions burned: 112 (million)
% 0.48/0.41 % (427857)Success in time 0.116 s
% 0.48/0.41 % Vampire exiting
%------------------------------------------------------------------------------