%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO016^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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 08:48:43 AM UTC 2026
% Result : Theorem 0.29s 0.30s
% Output : Refutation 0.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO016^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n017.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 16:16:53 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.29/0.29 % (534696)Will run a generic schedule for satisfiability detection.
% 0.29/0.29 % (534704)dis+10_1_sil=32000:sp=arity:random_seed=2634210050:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.29/0.29 % (534704)Refutation not found, incomplete strategy
% 0.29/0.29 % (534704)------------------------------
% 0.29/0.29 % (534704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.29 % (534704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.29 % (534704)CaDiCaL version: 2.1.3
% 0.29/0.29 % (534704)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.29 % (534704)Time elapsed: 0.002 s
% 0.29/0.29 % (534704)Peak memory usage: 12 MB
% 0.29/0.29 % (534704)Instructions burned: 5 (million)
% 0.29/0.29 % (534702)% WARNING: option uhcvi not known.
% 0.29/0.29 % (534704)------------------------------
% 0.29/0.29 % (534704)------------------------------
% 0.29/0.29 % (534703)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3153340199:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.29/0.29 % (534702)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3823523759:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.29/0.29 % (534701)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3493631331_3000 on theBenchmark for (3000ds/0Mi)
% 0.29/0.29 % (534702)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.29/0.29 % (534705)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3358507115:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 0.29/0.29 % (534702)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.29/0.29 % Exception at run slice level% (534706)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3051393817:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.29/0.29
% 0.29/0.29 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.29/0.29 % (534705)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.29/0.29 % (534707)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2181027895:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 0.29/0.29 % (534705)Refutation not found, incomplete strategy
% 0.29/0.29 % (534705)------------------------------
% 0.29/0.29 % (534705)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.29 % (534705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.29 % (534705)CaDiCaL version: 2.1.3
% 0.29/0.29 % (534705)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.29 % (534705)Time elapsed: 0.004 s
% 0.29/0.29 % (534705)Peak memory usage: 12 MB
% 0.29/0.29 % (534705)Instructions burned: 5 (million)
% 0.29/0.29 % (534706)Refutation not found, incomplete strategy
% 0.29/0.29 % (534706)------------------------------
% 0.29/0.29 % (534706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.29 % (534706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.29 % (534706)CaDiCaL version: 2.1.3
% 0.29/0.29 % (534706)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.29 % (534706)Time elapsed: 0.004 s
% 0.29/0.29 % (534706)Peak memory usage: 12 MB
% 0.29/0.30 % (534706)Instructions burned: 5 (million)
% 0.29/0.30 % (534702)Refutation not found, incomplete strategy
% 0.29/0.30 % (534702)------------------------------
% 0.29/0.30 % (534702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534702)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534702)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534702)Time elapsed: 0.005 s
% 0.29/0.30 % (534702)Peak memory usage: 12 MB
% 0.29/0.30 % (534702)Instructions burned: 6 (million)
% 0.29/0.30 % (534705)------------------------------
% 0.29/0.30 % (534705)------------------------------
% 0.29/0.30 % (534706)------------------------------
% 0.29/0.30 % (534706)------------------------------
% 0.29/0.30 % (534702)------------------------------
% 0.29/0.30 % (534702)------------------------------
% 0.29/0.30 % (534703)Refutation not found, incomplete strategy
% 0.29/0.30 % (534703)------------------------------
% 0.29/0.30 % (534703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534703)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534703)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534703)Time elapsed: 0.008 s
% 0.29/0.30 % (534703)Peak memory usage: 12 MB
% 0.29/0.30 % (534703)Instructions burned: 12 (million)
% 0.29/0.30 % (534709)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3786134268:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.29/0.30 % Exception at run slice level
% 0.29/0.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.29/0.30 % (534703)------------------------------
% 0.29/0.30 % (534703)------------------------------
% 0.29/0.30 % (534707)Refutation not found, incomplete strategy
% 0.29/0.30 % (534707)------------------------------
% 0.29/0.30 % (534707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534707)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534707)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534707)Time elapsed: 0.014 s
% 0.29/0.30 % (534707)Peak memory usage: 12 MB
% 0.29/0.30 % (534707)Instructions burned: 16 (million)
% 0.29/0.30 % (534707)------------------------------
% 0.29/0.30 % (534707)------------------------------
% 0.29/0.30 % (534716)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4223370210:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.29/0.30 % (534722)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4089637667:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 0.29/0.30 % (534717)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=414143504:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.29/0.30 % (534719)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=24531479:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 0.29/0.30 % (534717)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.29/0.30 % (534718)ott-21_1_sil=16000:fs=off:random_seed=1815139251:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 0.29/0.30 % (534717)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.29/0.30 % (534716)Refutation not found, incomplete strategy
% 0.29/0.30 % (534716)------------------------------
% 0.29/0.30 % (534716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534716)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534716)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534716)Time elapsed: 0.004 s
% 0.29/0.30 % (534716)Peak memory usage: 12 MB
% 0.29/0.30 % (534716)Instructions burned: 5 (million)
% 0.29/0.30 % (534716)------------------------------
% 0.29/0.30 % (534716)------------------------------
% 0.29/0.30 % (534717)Refutation not found, incomplete strategy
% 0.29/0.30 % (534717)------------------------------
% 0.29/0.30 % (534717)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534717)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534717)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534717)Time elapsed: 0.004 s
% 0.29/0.30 % (534717)Peak memory usage: 12 MB
% 0.29/0.30 % (534717)Instructions burned: 5 (million)
% 0.29/0.30 % (534717)------------------------------
% 0.29/0.30 % (534717)------------------------------
% 0.29/0.30 % (534721)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4263017386:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 0.29/0.30 % Exception at run slice level
% 0.29/0.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.29/0.30 % (534723)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1213649192:i=889:ins=1_2999 on theBenchmark for (2999ds/889Mi)
% 0.29/0.30 % Exception at run slice level
% 0.29/0.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.29/0.30 % (534722) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-534696-534722"...
% 0.29/0.30 % (534719)Refutation not found, incomplete strategy
% 0.29/0.30 % (534719)------------------------------
% 0.29/0.30 % (534719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534719)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534719)Termination reason: Refutation not found, incomplete strategy
% 0.29/0.30 % (534719)Time elapsed: 0.014 s
% 0.29/0.30 % (534719)Peak memory usage: 12 MB
% 0.29/0.30 % (534719)Instructions burned: 22 (million)
% 0.29/0.30 % (534719)------------------------------
% 0.29/0.30 % (534719)------------------------------
% 0.29/0.30 % (534722)...printing done.
% 0.29/0.30 % (534722)Refutation found. Thanks to Tanya!
% 0.29/0.30 % SZS status Theorem for theBenchmark
% 0.29/0.30 % SZS output start Proof for theBenchmark
% 0.29/0.30 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.29/0.30 thf(func_def_0, type, leibeq: ($o > $o > $o)).
% 0.29/0.30 thf(func_def_2, type, h: ($o > $o)).
% 0.29/0.30 thf(func_def_3, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.29/0.30 thf(func_def_4, type, vIMP: ($o > $o > $o)).
% 0.29/0.30 thf(func_def_5, type, db0: !>[X0: $tType]:(X0)).
% 0.29/0.30 thf(func_def_6, type, db2: !>[X0: $tType]:(X0)).
% 0.29/0.30 thf(func_def_7, type, db1: !>[X0: $tType]:(X0)).
% 0.29/0.30 thf(func_def_8, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.29/0.30 thf(func_def_11, type, sF0: $o).
% 0.29/0.30 thf(func_def_12, type, sF1: $o).
% 0.29/0.30 thf(func_def_13, type, sF2: $o).
% 0.29/0.30 thf(func_def_14, type, sF3: $o).
% 0.29/0.30 thf(func_def_15, type, sF4: $o).
% 0.29/0.30 thf(func_def_16, type, vNOT: ($o > $o)).
% 0.29/0.30 thf(func_def_17, type, sK5: ($o > $o)).
% 0.29/0.30 thf(func_def_18, type, sK6: ($o > $o)).
% 0.29/0.30 thf(func_def_20, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.29/0.30 thf(f1,axiom,(
% 0.29/0.30 (leibeq = (^[X0 : $o, X1 : $o] : (! [X2 : ($o > $o)] : ((X2 @ X0) => (X2 @ X1)))))),
% 0.29/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',leibeq)).
% 0.29/0.30 thf(f2,conjecture,(
% 0.29/0.30 (leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))),
% 0.29/0.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 0.29/0.30 thf(f3,negated_conjecture,(
% 0.29/0.30 ~(leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))),
% 0.29/0.30 inference(negated_conjecture,[status(cth)],[f2])).
% 0.29/0.30 thf(f4,plain,(
% 0.29/0.30 (leibeq = (^[X0 : $o, X1 : $o] : (! [X2 : ($o > $o)] : ((X2 @ X0) => (X2 @ X1)))))),
% 0.29/0.30 inference(rectify,[],[f1])).
% 0.29/0.30 thf(f5,plain,(
% 0.29/0.30 (leibeq = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))))),
% 0.29/0.30 inference(fool_elimination,[],[f4])).
% 0.29/0.30 thf(f6,plain,(
% 0.29/0.30 ~(leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))),
% 0.29/0.30 inference(rectify,[],[f3])).
% 0.29/0.30 thf(f7,plain,(
% 0.29/0.30 ~ ($true = ((leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))))),
% 0.29/0.30 inference(fool_elimination,[],[f6])).
% 0.29/0.30 thf(f8,plain,(
% 0.29/0.30 ($true != ((leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))))),
% 0.29/0.30 inference(flattening,[],[f7])).
% 0.29/0.30 thf(f9,plain,(
% 0.29/0.30 (leibeq = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))))),
% 0.29/0.30 inference(cnf_transformation,[],[f5])).
% 0.29/0.30 thf(f10,plain,(
% 0.29/0.30 ($true != ((leibeq @ (h @ (leibeq @ (h @ $true) @ (h @ $false))) @ (h @ $false))))),
% 0.29/0.30 inference(cnf_transformation,[],[f8])).
% 0.29/0.30 thf(f12,definition,(
% 0.29/0.30 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.29/0.30 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.29/0.30 thf(f13,plain,(
% 0.29/0.30 ($true != (((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ (h @ ((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ (h @ $true) @ (h @ $false))) @ (h @ $false))))),
% 0.29/0.30 inference(definition_unfolding,[],[f10,f9,f9])).
% 0.29/0.30 thf(f14,definition,(
% 0.29/0.30 (sF0 = ((h @ $true)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 0.29/0.30 thf(f15,plain,(
% 0.29/0.30 (((h @ $true)) = sF0)),
% 0.29/0.30 inference(reorient_equations,[],[f14])).
% 0.29/0.30 thf(f16,definition,(
% 0.29/0.30 (sF1 = ((h @ $false)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 0.29/0.30 thf(f17,plain,(
% 0.29/0.30 (((h @ $false)) = sF1)),
% 0.29/0.30 inference(reorient_equations,[],[f16])).
% 0.29/0.30 thf(f18,definition,(
% 0.29/0.30 (sF2 = (((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF0 @ sF1)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 0.29/0.30 thf(f19,plain,(
% 0.29/0.30 ((((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF0 @ sF1)) = sF2)),
% 0.29/0.30 inference(reorient_equations,[],[f18])).
% 0.29/0.30 thf(f20,definition,(
% 0.29/0.30 (sF3 = ((h @ sF2)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 0.29/0.30 thf(f21,plain,(
% 0.29/0.30 (((h @ sF2)) = sF3)),
% 0.29/0.30 inference(reorient_equations,[],[f20])).
% 0.29/0.30 thf(f22,definition,(
% 0.29/0.30 (sF4 = (((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF3 @ sF1)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 0.29/0.30 thf(f23,plain,(
% 0.29/0.30 ((((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF3 @ sF1)) = sF4)),
% 0.29/0.30 inference(reorient_equations,[],[f22])).
% 0.29/0.30 thf(f24,plain,(
% 0.29/0.30 ($true != sF4)),
% 0.29/0.30 inference(definition_folding,[],[f13,f23,f17,f21,f19,f17,f15])).
% 0.29/0.30 thf(f25,plain,(
% 0.29/0.30 ($true = ((h @ $true))) | ($false = sF0)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f15])).
% 0.29/0.30 thf(f26,plain,(
% 0.29/0.30 (((h @ $true)) = $false) | ($true = sF0)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f15])).
% 0.29/0.30 thf(f27,plain,(
% 0.29/0.30 ($true = ((h @ $false))) | ($false = sF1)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f17])).
% 0.29/0.30 thf(f28,plain,(
% 0.29/0.30 ($false = ((h @ $false))) | ($true = sF1)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f17])).
% 0.29/0.30 thf(f29,plain,(
% 0.29/0.30 ($true = (((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF0 @ sF1))) | ($false = sF2)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f19])).
% 0.29/0.30 thf(f36,plain,(
% 0.29/0.30 ($true = ((!! @ ($o > $o) @ (^[Y0 : $o > $o]: ((Y0 @ sF0) => (Y0 @ sF1)))))) | ($false = sF2)),
% 0.29/0.30 inference(beta-eta_normalization,[],[f29])).
% 0.29/0.30 thf(f37,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($true = (((^[Y0 : $o > $o]: ((Y0 @ sF0) => (Y0 @ sF1))) @ X1))) | ($false = sF2)) )),
% 0.29/0.30 inference(pi_proxy_clausification,[],[f36])).
% 0.29/0.30 thf(f38,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($true = (((X1 @ sF0) => (X1 @ sF1)))) | ($false = sF2)) )),
% 0.29/0.30 inference(beta-eta_normalization,[],[f37])).
% 0.29/0.30 thf(f39,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($false = ((X1 @ sF0))) | ($false = sF2) | ($true = ((X1 @ sF1)))) )),
% 0.29/0.30 inference(imp_proxy_clausification,[],[f38])).
% 0.29/0.30 thf(f40,plain,(
% 0.29/0.30 ($true = ((h @ sF2))) | ($false = sF3)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f21])).
% 0.29/0.30 thf(f41,plain,(
% 0.29/0.30 ($false = ((h @ sF2))) | ($true = sF3)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f21])).
% 0.29/0.30 thf(f43,plain,(
% 0.29/0.30 ($false = (((^[Y0 : $o]: ((^[Y1 : $o]: (!! @ ($o > $o) @ (^[Y2 : $o > $o]: ((Y2 @ Y0) => (Y2 @ Y1))))))) @ sF3 @ sF1))) | ($true = sF4)),
% 0.29/0.30 inference(iff_proxy_clausification,[],[f23])).
% 0.29/0.30 thf(f44,plain,(
% 0.29/0.30 ($false = ((!! @ ($o > $o) @ (^[Y0 : $o > $o]: ((Y0 @ sF3) => (Y0 @ sF1)))))) | ($true = sF4)),
% 0.29/0.30 inference(beta-eta_normalization,[],[f43])).
% 0.29/0.30 thf(f45,plain,(
% 0.29/0.30 ($false = (((^[Y0 : $o > $o]: ((Y0 @ sF3) => (Y0 @ sF1))) @ sK6))) | ($true = sF4)),
% 0.29/0.30 inference(sigma_proxy_clausification,[],[f44])).
% 0.29/0.30 thf(f46,plain,(
% 0.29/0.30 ($false = (((sK6 @ sF3) => (sK6 @ sF1)))) | ($true = sF4)),
% 0.29/0.30 inference(beta-eta_normalization,[],[f45])).
% 0.29/0.30 thf(f47,plain,(
% 0.29/0.30 ($false = ((sK6 @ sF1))) | ($true = sF4)),
% 0.29/0.30 inference(imp_proxy_clausification,[],[f46])).
% 0.29/0.30 thf(f48,plain,(
% 0.29/0.30 ($true = ((sK6 @ sF3))) | ($true = sF4)),
% 0.29/0.30 inference(imp_proxy_clausification,[],[f46])).
% 0.29/0.30 thf(f54,definition,(
% 0.29/0.30 spl7_1 <=> ($true = sF0)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition])).
% 0.29/0.30 thf(f56,plain,(
% 0.29/0.30 ($true = sF0) | ~spl7_1),
% 0.29/0.30 inference(avatar_component_clause,[],[f54])).
% 0.29/0.30 thf(f58,definition,(
% 0.29/0.30 spl7_2 <=> (((h @ $true)) = $false)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition])).
% 0.29/0.30 thf(f59,plain,(
% 0.29/0.30 (((h @ $true)) != $false) | spl7_2),
% 0.29/0.30 inference(avatar_component_clause,[],[f58])).
% 0.29/0.30 thf(f60,plain,(
% 0.29/0.30 (((h @ $true)) = $false) | ~spl7_2),
% 0.29/0.30 inference(avatar_component_clause,[],[f58])).
% 0.29/0.30 thf(f61,plain,(
% 0.29/0.30 spl7_1 | spl7_2),
% 0.29/0.30 inference(avatar_split_clause,[],[f26,f58,f54])).
% 0.29/0.30 thf(f63,definition,(
% 0.29/0.30 spl7_3 <=> ($false = sF0)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition])).
% 0.29/0.30 thf(f65,plain,(
% 0.29/0.30 ($false = sF0) | ~spl7_3),
% 0.29/0.30 inference(avatar_component_clause,[],[f63])).
% 0.29/0.30 thf(f67,definition,(
% 0.29/0.30 spl7_4 <=> ($true = ((h @ $true)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition])).
% 0.29/0.30 thf(f69,plain,(
% 0.29/0.30 ($true = ((h @ $true))) | ~spl7_4),
% 0.29/0.30 inference(avatar_component_clause,[],[f67])).
% 0.29/0.30 thf(f70,plain,(
% 0.29/0.30 spl7_3 | spl7_4),
% 0.29/0.30 inference(avatar_split_clause,[],[f25,f67,f63])).
% 0.29/0.30 thf(f72,definition,(
% 0.29/0.30 spl7_5 <=> ($true = sF1)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition])).
% 0.29/0.30 thf(f73,plain,(
% 0.29/0.30 ($true != sF1) | spl7_5),
% 0.29/0.30 inference(avatar_component_clause,[],[f72])).
% 0.29/0.30 thf(f74,plain,(
% 0.29/0.30 ($true = sF1) | ~spl7_5),
% 0.29/0.30 inference(avatar_component_clause,[],[f72])).
% 0.29/0.30 thf(f76,definition,(
% 0.29/0.30 spl7_6 <=> ($false = ((h @ $false)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_6])],[avatar_definition])).
% 0.29/0.30 thf(f77,plain,(
% 0.29/0.30 ($false != ((h @ $false))) | spl7_6),
% 0.29/0.30 inference(avatar_component_clause,[],[f76])).
% 0.29/0.30 thf(f78,plain,(
% 0.29/0.30 ($false = ((h @ $false))) | ~spl7_6),
% 0.29/0.30 inference(avatar_component_clause,[],[f76])).
% 0.29/0.30 thf(f79,plain,(
% 0.29/0.30 spl7_5 | spl7_6),
% 0.29/0.30 inference(avatar_split_clause,[],[f28,f76,f72])).
% 0.29/0.30 thf(f81,definition,(
% 0.29/0.30 spl7_7 <=> ($false = sF1)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_7])],[avatar_definition])).
% 0.29/0.30 thf(f83,plain,(
% 0.29/0.30 ($false = sF1) | ~spl7_7),
% 0.29/0.30 inference(avatar_component_clause,[],[f81])).
% 0.29/0.30 thf(f85,definition,(
% 0.29/0.30 spl7_8 <=> ($true = ((h @ $false)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_8])],[avatar_definition])).
% 0.29/0.30 thf(f87,plain,(
% 0.29/0.30 ($true = ((h @ $false))) | ~spl7_8),
% 0.29/0.30 inference(avatar_component_clause,[],[f85])).
% 0.29/0.30 thf(f88,plain,(
% 0.29/0.30 spl7_7 | spl7_8),
% 0.29/0.30 inference(avatar_split_clause,[],[f27,f85,f81])).
% 0.29/0.30 thf(f90,definition,(
% 0.29/0.30 spl7_9 <=> ($true = sF2)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_9])],[avatar_definition])).
% 0.29/0.30 thf(f91,plain,(
% 0.29/0.30 ($true != sF2) | spl7_9),
% 0.29/0.30 inference(avatar_component_clause,[],[f90])).
% 0.29/0.30 thf(f92,plain,(
% 0.29/0.30 ($true = sF2) | ~spl7_9),
% 0.29/0.30 inference(avatar_component_clause,[],[f90])).
% 0.29/0.30 thf(f104,definition,(
% 0.29/0.30 spl7_12 <=> ($false = sF2)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_12])],[avatar_definition])).
% 0.29/0.30 thf(f105,plain,(
% 0.29/0.30 ($false != sF2) | spl7_12),
% 0.29/0.30 inference(avatar_component_clause,[],[f104])).
% 0.29/0.30 thf(f106,plain,(
% 0.29/0.30 ($false = sF2) | ~spl7_12),
% 0.29/0.30 inference(avatar_component_clause,[],[f104])).
% 0.29/0.30 thf(f108,definition,(
% 0.29/0.30 spl7_13 <=> ! [X1 : ($o > $o)] : (($false = ((X1 @ sF0))) | ($true = ((X1 @ sF1))))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_13])],[avatar_definition])).
% 0.29/0.30 thf(f109,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($false = ((X1 @ sF0))) | ($true = ((X1 @ sF1)))) ) | ~spl7_13),
% 0.29/0.30 inference(avatar_component_clause,[],[f108])).
% 0.29/0.30 thf(f110,plain,(
% 0.29/0.30 spl7_12 | spl7_13),
% 0.29/0.30 inference(avatar_split_clause,[],[f39,f108,f104])).
% 0.29/0.30 thf(f112,definition,(
% 0.29/0.30 spl7_14 <=> ($true = sF3)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_14])],[avatar_definition])).
% 0.29/0.30 thf(f114,plain,(
% 0.29/0.30 ($true = sF3) | ~spl7_14),
% 0.29/0.30 inference(avatar_component_clause,[],[f112])).
% 0.29/0.30 thf(f116,definition,(
% 0.29/0.30 spl7_15 <=> ($false = ((h @ sF2)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_15])],[avatar_definition])).
% 0.29/0.30 thf(f118,plain,(
% 0.29/0.30 ($false = ((h @ sF2))) | ~spl7_15),
% 0.29/0.30 inference(avatar_component_clause,[],[f116])).
% 0.29/0.30 thf(f119,plain,(
% 0.29/0.30 spl7_14 | spl7_15),
% 0.29/0.30 inference(avatar_split_clause,[],[f41,f116,f112])).
% 0.29/0.30 thf(f121,definition,(
% 0.29/0.30 spl7_16 <=> ($false = sF3)),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_16])],[avatar_definition])).
% 0.29/0.30 thf(f123,plain,(
% 0.29/0.30 ($false = sF3) | ~spl7_16),
% 0.29/0.30 inference(avatar_component_clause,[],[f121])).
% 0.29/0.30 thf(f125,definition,(
% 0.29/0.30 spl7_17 <=> ($true = ((h @ sF2)))),
% 0.29/0.30 introduced(definition,[new_symbols(definition,[spl7_17])],[avatar_definition])).
% 0.29/0.30 thf(f127,plain,(
% 0.29/0.30 ($true = ((h @ sF2))) | ~spl7_17),
% 0.29/0.30 inference(avatar_component_clause,[],[f125])).
% 0.29/0.30 thf(f128,plain,(
% 0.29/0.30 spl7_16 | spl7_17),
% 0.29/0.30 inference(avatar_split_clause,[],[f40,f125,f121])).
% 0.29/0.30 thf(f129,plain,(
% 0.29/0.30 ($true = ((sK6 @ sF3)))),
% 0.29/0.30 inference(forward_subsumption_resolution,[],[f48,f24])).
% 0.29/0.30 thf(f130,plain,(
% 0.29/0.30 ($false = ((sK6 @ sF1)))),
% 0.29/0.30 inference(forward_subsumption_resolution,[],[f47,f24])).
% 0.29/0.30 thf(f149,plain,(
% 0.29/0.30 ($false = ((sK6 @ $true))) | ($false = sF1)),
% 0.29/0.30 inference(constrained_superposition,[],[f130,f12])).
% 0.29/0.30 thf(f156,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_5 | ~spl7_7)),
% 0.29/0.30 inference(constrained_superposition,[],[f83,f74])).
% 0.29/0.30 thf(f158,plain,(
% 0.29/0.30 ($false = ((sK6 @ $false))) | ~spl7_7),
% 0.29/0.30 inference(constrained_superposition,[],[f130,f83])).
% 0.29/0.30 thf(f161,plain,(
% 0.29/0.30 $false | (~spl7_5 | ~spl7_7)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f156])).
% 0.29/0.30 thf(f162,plain,(
% 0.29/0.30 ~spl7_5 | ~spl7_7),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f161])).
% 0.29/0.30 thf(f171,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_14 | ~spl7_16)),
% 0.29/0.30 inference(constrained_superposition,[],[f123,f114])).
% 0.29/0.30 thf(f173,plain,(
% 0.29/0.30 ($true = ((sK6 @ $false))) | ~spl7_16),
% 0.29/0.30 inference(constrained_superposition,[],[f129,f123])).
% 0.29/0.30 thf(f176,plain,(
% 0.29/0.30 $false | (~spl7_14 | ~spl7_16)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f171])).
% 0.29/0.30 thf(f177,plain,(
% 0.29/0.30 ~spl7_14 | ~spl7_16),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f176])).
% 0.29/0.30 thf(f179,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_7 | ~spl7_16)),
% 0.29/0.30 inference(forward_demodulation,[],[f173,f158])).
% 0.29/0.30 thf(f180,plain,(
% 0.29/0.30 $false | (~spl7_7 | ~spl7_16)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f179])).
% 0.29/0.30 thf(f181,plain,(
% 0.29/0.30 ~spl7_7 | ~spl7_16),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f180])).
% 0.29/0.30 thf(f182,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_6 | ~spl7_8)),
% 0.29/0.30 inference(forward_demodulation,[],[f87,f78])).
% 0.29/0.30 thf(f183,plain,(
% 0.29/0.30 $false | (~spl7_6 | ~spl7_8)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f182])).
% 0.29/0.30 thf(f184,plain,(
% 0.29/0.30 ~spl7_6 | ~spl7_8),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f183])).
% 0.29/0.30 thf(f186,plain,(
% 0.29/0.30 (((h @ $true)) = $false) | (~spl7_9 | ~spl7_15)),
% 0.29/0.30 inference(forward_demodulation,[],[f118,f92])).
% 0.29/0.30 thf(f189,plain,(
% 0.29/0.30 ($true = ((h @ $true))) | (~spl7_9 | ~spl7_17)),
% 0.29/0.30 inference(forward_demodulation,[],[f127,f92])).
% 0.29/0.30 thf(f197,plain,(
% 0.29/0.30 $false | (spl7_2 | ~spl7_9 | ~spl7_15)),
% 0.29/0.30 inference(forward_subsumption_resolution,[],[f186,f59])).
% 0.29/0.30 thf(f198,plain,(
% 0.29/0.30 spl7_2 | ~spl7_9 | ~spl7_15),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f197])).
% 0.29/0.30 thf(f199,plain,(
% 0.29/0.30 spl7_4 | ~spl7_9 | ~spl7_17),
% 0.29/0.30 inference(avatar_split_clause,[],[f189,f125,f90,f67])).
% 0.29/0.30 thf(f211,plain,(
% 0.29/0.30 ($true != $true) | ($false = sF1) | spl7_5),
% 0.29/0.30 inference(constrained_superposition,[],[f73,f12])).
% 0.29/0.30 thf(f212,plain,(
% 0.29/0.30 ($false = sF1) | spl7_5),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f211])).
% 0.29/0.30 thf(f234,plain,(
% 0.29/0.30 ($true = ((h @ $false))) | (~spl7_12 | ~spl7_17)),
% 0.29/0.30 inference(forward_demodulation,[],[f127,f106])).
% 0.29/0.30 thf(f236,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_6 | ~spl7_12 | ~spl7_17)),
% 0.29/0.30 inference(forward_demodulation,[],[f234,f78])).
% 0.29/0.30 thf(f237,plain,(
% 0.29/0.30 $false | (~spl7_6 | ~spl7_12 | ~spl7_17)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f236])).
% 0.29/0.30 thf(f238,plain,(
% 0.29/0.30 ~spl7_6 | ~spl7_12 | ~spl7_17),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f237])).
% 0.29/0.30 thf(f242,plain,(
% 0.29/0.30 ($false = ((h @ $false))) | (~spl7_12 | ~spl7_15)),
% 0.29/0.30 inference(forward_demodulation,[],[f118,f106])).
% 0.29/0.30 thf(f243,plain,(
% 0.29/0.30 ($true = $false) | ($false = ((sK6 @ $true))) | ~spl7_5),
% 0.29/0.30 inference(forward_demodulation,[],[f149,f74])).
% 0.29/0.30 thf(f244,plain,(
% 0.29/0.30 ($false = ((sK6 @ $true))) | ~spl7_5),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f243])).
% 0.29/0.30 thf(f246,plain,(
% 0.29/0.30 $false | (spl7_6 | ~spl7_12 | ~spl7_15)),
% 0.29/0.30 inference(forward_subsumption_resolution,[],[f242,f77])).
% 0.29/0.30 thf(f247,plain,(
% 0.29/0.30 spl7_6 | ~spl7_12 | ~spl7_15),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f246])).
% 0.29/0.30 thf(f248,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($false = ((X1 @ $true))) | ($true = ((X1 @ sF1)))) ) | (~spl7_1 | ~spl7_13)),
% 0.29/0.30 inference(forward_demodulation,[],[f109,f56])).
% 0.29/0.30 thf(f251,plain,(
% 0.29/0.30 ( ! [X0 : $o] : (($false = ((sK6 @ X0))) | ($false = X0)) ) | ~spl7_5),
% 0.29/0.30 inference(constrained_superposition,[],[f244,f12])).
% 0.29/0.30 thf(f257,plain,(
% 0.29/0.30 ($true = $false) | ($false = sF3) | ~spl7_5),
% 0.29/0.30 inference(constrained_superposition,[],[f129,f251])).
% 0.29/0.30 thf(f258,plain,(
% 0.29/0.30 ($false = sF3) | ~spl7_5),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f257])).
% 0.29/0.30 thf(f274,plain,(
% 0.29/0.30 ($true != $true) | ($false = sF2) | spl7_9),
% 0.29/0.30 inference(constrained_superposition,[],[f91,f12])).
% 0.29/0.30 thf(f275,plain,(
% 0.29/0.30 ($false = sF2) | spl7_9),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f274])).
% 0.29/0.30 thf(f276,plain,(
% 0.29/0.30 $false | (spl7_9 | spl7_12)),
% 0.29/0.30 inference(forward_subsumption_resolution,[],[f275,f105])).
% 0.29/0.30 thf(f277,plain,(
% 0.29/0.30 spl7_9 | spl7_12),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f276])).
% 0.29/0.30 thf(f281,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_2 | ~spl7_4)),
% 0.29/0.30 inference(constrained_superposition,[],[f60,f69])).
% 0.29/0.30 thf(f285,plain,(
% 0.29/0.30 $false | (~spl7_2 | ~spl7_4)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f281])).
% 0.29/0.30 thf(f286,plain,(
% 0.29/0.30 ~spl7_2 | ~spl7_4),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f285])).
% 0.29/0.30 thf(f290,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($false = ((X1 @ $false))) | ($true = ((X1 @ sF1)))) ) | (~spl7_3 | ~spl7_13)),
% 0.29/0.30 inference(forward_demodulation,[],[f109,f65])).
% 0.29/0.30 thf(f291,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($true = ((X1 @ $true))) | ($false = ((X1 @ $false)))) ) | (~spl7_3 | ~spl7_5 | ~spl7_13)),
% 0.29/0.30 inference(forward_demodulation,[],[f290,f74])).
% 0.29/0.30 thf(f307,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_3 | ~spl7_5 | ~spl7_13)),
% 0.29/0.30 inference(leibniz_equality_elimination,[],[f291])).
% 0.29/0.30 thf(f436,plain,(
% 0.29/0.30 $false | (~spl7_3 | ~spl7_5 | ~spl7_13)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f307])).
% 0.29/0.30 thf(f437,plain,(
% 0.29/0.30 ~spl7_3 | ~spl7_5 | ~spl7_13),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f436])).
% 0.29/0.30 thf(f462,plain,(
% 0.29/0.30 spl7_16 | ~spl7_5),
% 0.29/0.30 inference(avatar_split_clause,[],[f258,f72,f121])).
% 0.29/0.30 thf(f469,plain,(
% 0.29/0.30 spl7_7 | spl7_5),
% 0.29/0.30 inference(avatar_split_clause,[],[f212,f72,f81])).
% 0.29/0.30 thf(f472,plain,(
% 0.29/0.30 ( ! [X1 : ($o > $o)] : (($false = ((X1 @ $true))) | ($true = ((X1 @ $false)))) ) | (~spl7_1 | ~spl7_7 | ~spl7_13)),
% 0.29/0.30 inference(forward_demodulation,[],[f248,f83])).
% 0.29/0.30 thf(f506,plain,(
% 0.29/0.30 ($true = $false) | (~spl7_1 | ~spl7_7 | ~spl7_13)),
% 0.29/0.30 inference(leibniz_equality_elimination,[],[f472])).
% 0.29/0.30 thf(f676,plain,(
% 0.29/0.30 $false | (~spl7_1 | ~spl7_7 | ~spl7_13)),
% 0.29/0.30 inference(trivial_inequality_removal,[],[f506])).
% 0.29/0.30 thf(f677,plain,(
% 0.29/0.30 ~spl7_1 | ~spl7_7 | ~spl7_13),
% 0.29/0.30 inference(avatar_contradiction_clause,[],[f676])).
% 0.29/0.30 cnf(s1, plain, spl7_1 | spl7_2, inference(sat_conversion,[],[f61])).
% 0.29/0.30 cnf(s2, plain, spl7_3 | spl7_4, inference(sat_conversion,[],[f70])).
% 0.29/0.30 cnf(s3, plain, spl7_5 | spl7_6, inference(sat_conversion,[],[f79])).
% 0.29/0.30 cnf(s4, plain, spl7_7 | spl7_8, inference(sat_conversion,[],[f88])).
% 0.29/0.30 cnf(s7, plain, spl7_12 | spl7_13, inference(sat_conversion,[],[f110])).
% 0.29/0.30 cnf(s8, plain, spl7_14 | spl7_15, inference(sat_conversion,[],[f119])).
% 0.29/0.30 cnf(s9, plain, spl7_16 | spl7_17, inference(sat_conversion,[],[f128])).
% 0.29/0.30 cnf(s12, plain, ~spl7_5 | ~spl7_7, inference(sat_conversion,[],[f162])).
% 0.29/0.30 cnf(s14, plain, ~spl7_14 | ~spl7_16, inference(sat_conversion,[],[f177])).
% 0.29/0.30 cnf(s15, plain, ~spl7_7 | ~spl7_16, inference(sat_conversion,[],[f181])).
% 0.29/0.30 cnf(s16, plain, ~spl7_6 | ~spl7_8, inference(sat_conversion,[],[f184])).
% 0.29/0.30 cnf(s19, plain, spl7_2 | ~spl7_9 | ~spl7_15, inference(sat_conversion,[],[f198])).
% 0.29/0.30 cnf(s20, plain, spl7_4 | ~spl7_9 | ~spl7_17, inference(sat_conversion,[],[f199])).
% 0.29/0.30 cnf(s23, plain, ~spl7_6 | ~spl7_12 | ~spl7_17, inference(sat_conversion,[],[f238])).
% 0.29/0.30 cnf(s25, plain, spl7_6 | ~spl7_12 | ~spl7_15, inference(sat_conversion,[],[f247])).
% 0.29/0.30 cnf(s26, plain, spl7_9 | spl7_12, inference(sat_conversion,[],[f277])).
% 0.29/0.30 cnf(s28, plain, ~spl7_2 | ~spl7_4, inference(sat_conversion,[],[f286])).
% 0.29/0.30 cnf(s30, plain, ~spl7_3 | ~spl7_5 | ~spl7_13, inference(sat_conversion,[],[f437])).
% 0.29/0.30 cnf(s38, plain, ~spl7_5 | spl7_16, inference(sat_conversion,[],[f462])).
% 0.29/0.30 cnf(s42, plain, spl7_5 | spl7_7, inference(sat_conversion,[],[f469])).
% 0.29/0.30 cnf(s46, plain, ~spl7_1 | ~spl7_7 | ~spl7_13, inference(sat_conversion,[],[f677])).
% 0.29/0.30 cnf(s59, plain, spl7_5 | spl7_4, inference(rat,[],[s26,s23,s20,s9,s15,s3,s42])).
% 0.29/0.30 cnf(s60, plain, spl7_4, inference(rat,[],[s25,s16,s8,s7,s4,s14,s30,s12,s38,s59,s2])).
% 0.29/0.30 cnf(s61, plain, ~spl7_2, inference(rat,[],[s28,s60])).
% 0.29/0.30 cnf(s62, plain, spl7_1, inference(rat,[],[s1,s61])).
% 0.29/0.30 cnf(s64, plain, spl7_5, inference(rat,[],[s23,s9,s7,s15,s46,s3,s42,s62])).
% 0.29/0.30 cnf(s65, plain, spl7_16, inference(rat,[],[s38,s64])).
% 0.29/0.30 cnf(s66, plain, ~spl7_7, inference(rat,[],[s12,s64])).
% 0.29/0.30 cnf(s67, plain, ~spl7_14, inference(rat,[],[s14,s65])).
% 0.29/0.30 cnf(s68, plain, spl7_8, inference(rat,[],[s4,s66])).
% 0.29/0.30 cnf(s69, plain, spl7_15, inference(rat,[],[s8,s67])).
% 0.29/0.30 cnf(s70, plain, ~spl7_6, inference(rat,[],[s16,s68])).
% 0.29/0.30 cnf(s71, plain, ~spl7_12, inference(rat,[],[s25,s70,s69])).
% 0.29/0.30 cnf(s72, plain, ~spl7_9, inference(rat,[],[s19,s61,s69])).
% 0.29/0.30 cnf(s74, plain, $false, inference(rat,[],[s26,s71,s72])).
% 0.29/0.30 thf(f710,plain,(
% 0.29/0.30 $false),
% 0.29/0.30 inference(avatar_sat_refutation,[],[s74])).
% 0.29/0.30 % SZS output end Proof for theBenchmark
% 0.29/0.30 % (534722)------------------------------
% 0.29/0.30 % (534722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.29/0.30 % (534722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.29/0.30 % (534722)CaDiCaL version: 2.1.3
% 0.29/0.30 % (534722)Termination reason: Refutation
% 0.29/0.30 % (534722)Time elapsed: 0.018 s
% 0.29/0.30 % (534722)Peak memory usage: 12 MB
% 0.29/0.30 % (534722)Instructions burned: 24 (million)
% 0.29/0.30 % (534696)Success in time 0.065 s
% 0.29/0.30 % Vampire exiting
%------------------------------------------------------------------------------