%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV063^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:37:34 AM UTC 2026
% Result : Theorem 0.58s 0.41s
% Output : Refutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEV063^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 % Computer : n015.cluster.edu
% 0.10/0.26 % Model : x86_64 x86_64
% 0.10/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.26 % Memory : 8046.5625MB
% 0.10/0.26 % OS : Linux 6.8.0-71-generic
% 0.10/0.26 % CPULimit : 300
% 0.10/0.26 % WCLimit : 300
% 0.10/0.26 % DateTime : Tue Sep 29 15:09:18 UTC 2026
% 0.10/0.26 % CPUTime :
% 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.30 Running higher-order theorem proving
% 0.25/0.32 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.58/0.41 % (3640727)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.58/0.41 % (3640736)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=3114758936:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.58/0.41 % (3640738)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.58/0.41 % (3640738)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.58/0.41 % (3640737)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=4077365662:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.58/0.41 % (3640732)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=305811430:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.58/0.41 % (3640733)lrs+10_16_si=on:nwc=1.5:random_seed=475591428:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.58/0.41 % (3640734)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3146700926:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.58/0.41 % (3640736)Instruction limit reached!
% 0.58/0.41 % (3640736)------------------------------
% 0.58/0.41 % (3640736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640736)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640736)Termination reason: Instruction limit
% 0.58/0.41 % (3640736)Termination phase: Saturation
% 0.58/0.41 % (3640736)Time elapsed: 0.013 s
% 0.58/0.41 % (3640736)Peak memory usage: 12 MB
% 0.58/0.41 % (3640736)Instructions burned: 26 (million)
% 0.58/0.41 % (3640735)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=3775766735: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.58/0.41 % (3640738)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=2737497777:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.58/0.41 % (3640734)Instruction limit reached!
% 0.58/0.41 % (3640734)------------------------------
% 0.58/0.41 % (3640734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640734)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640734)Termination reason: Instruction limit
% 0.58/0.41 % (3640734)Termination phase: Saturation
% 0.58/0.41 % (3640734)Time elapsed: 0.006 s
% 0.58/0.41 % (3640734)Peak memory usage: 12 MB
% 0.58/0.41 % (3640734)Instructions burned: 5 (million)
% 0.58/0.41 % (3640733)Instruction limit reached!
% 0.58/0.41 % (3640733)------------------------------
% 0.58/0.41 % (3640733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640733)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640733)Termination reason: Instruction limit
% 0.58/0.41 % (3640733)Termination phase: Saturation
% 0.58/0.41 % (3640733)Time elapsed: 0.017 s
% 0.58/0.41 % (3640733)Peak memory usage: 12 MB
% 0.58/0.41 % (3640733)Instructions burned: 19 (million)
% 0.58/0.41 % (3640746)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3376382258:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.58/0.41 % (3640746)Instruction limit reached!
% 0.58/0.41 % (3640746)------------------------------
% 0.58/0.41 % (3640746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640746)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640746)Termination reason: Instruction limit
% 0.58/0.41 % (3640746)Termination phase: Saturation
% 0.58/0.41 % (3640746)Time elapsed: 0.002 s
% 0.58/0.41 % (3640746)Peak memory usage: 12 MB
% 0.58/0.41 % (3640746)Instructions burned: 3 (million)
% 0.58/0.41 % (3640750)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=1586280253:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.58/0.41 % (3640747)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=3399844044:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.58/0.41 % (3640732) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3640727-3640732"...
% 0.58/0.41 % (3640748)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.58/0.41 % (3640750)Instruction limit reached!
% 0.58/0.41 % (3640750)------------------------------
% 0.58/0.41 % (3640750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640750)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640750)Termination reason: Instruction limit
% 0.58/0.41 % (3640750)Termination phase: Saturation
% 0.58/0.41 % (3640750)Time elapsed: 0.006 s
% 0.58/0.41 % (3640750)Peak memory usage: 12 MB
% 0.58/0.41 % (3640750)Instructions burned: 12 (million)
% 0.58/0.41 % (3640747)Instruction limit reached!
% 0.58/0.41 % (3640747)------------------------------
% 0.58/0.41 % (3640747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640747)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640747)Termination reason: Instruction limit
% 0.58/0.41 % (3640747)Termination phase: Saturation
% 0.58/0.41 % (3640747)Time elapsed: 0.005 s
% 0.58/0.41 % (3640747)Peak memory usage: 12 MB
% 0.58/0.41 % (3640747)Instructions burned: 5 (million)
% 0.58/0.41 % (3640748)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=741248816:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.58/0.41 % (3640732)...printing done.
% 0.58/0.41 % (3640732)Refutation found. Thanks to Tanya!
% 0.58/0.41 % SZS status Theorem for theBenchmark
% 0.58/0.41 % SZS output start Proof for theBenchmark
% 0.58/0.41 thf(type_def_5, type, a: $tType).
% 0.58/0.41 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 0.58/0.41 thf(func_def_3, type, sK0: a).
% 0.58/0.41 thf(func_def_4, type, sK1: a).
% 0.58/0.41 thf(func_def_5, type, sK2: a).
% 0.58/0.41 thf(func_def_6, type, sK3: (a > a > $o)).
% 0.58/0.41 thf(func_def_7, type, sK4: (a > a > $o)).
% 0.58/0.41 thf(func_def_8, type, sK5: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_9, type, sK6: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_10, type, sK7: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_11, type, sK8: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_12, type, sK9: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_13, type, sK10: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_14, type, sK11: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_15, type, sK12: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_16, type, sK13: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_17, type, sK14: ((a > a > $o) > a)).
% 0.58/0.41 thf(func_def_18, type, vNOT: ($o > $o)).
% 0.58/0.41 thf(func_def_19, type, db0: !>[X0: $tType]:(X0)).
% 0.58/0.41 thf(func_def_20, type, db1: !>[X0: $tType]:(X0)).
% 0.58/0.41 thf(func_def_21, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 0.58/0.41 thf(func_def_22, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.58/0.41 thf(f1,conjecture,(
% 0.58/0.41 ! [X0 : (a > a > $o),X3 : a,X2 : a,X1 : a] : ((! [X4 : (a > a > $o)] : ((! [X5 : a,X7 : a,X6 : a] : (((X4 @ X5 @ X6) & (X4 @ X6 @ X7)) => (X4 @ X5 @ X7)) & ! [X5 : a,X6 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6))) => (X4 @ X1 @ X2)) & ! [X4 : (a > a > $o)] : ((! [X6 : a,X5 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6)) & ! [X7 : a,X5 : a,X6 : a] : (((X4 @ X6 @ X7) & (X4 @ X5 @ X6)) => (X4 @ X5 @ X7))) => (X4 @ X2 @ X3))) => ! [X4 : (a > a > $o)] : ((! [X6 : a,X5 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6)) & ! [X5 : a,X6 : a,X7 : a] : (((X4 @ X6 @ X7) & (X4 @ X5 @ X6)) => (X4 @ X5 @ X7))) => (X4 @ X1 @ X3)))),
% 0.58/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM136_pme)).
% 0.58/0.41 thf(f2,negated_conjecture,(
% 0.58/0.41 ~ ! [X0 : (a > a > $o),X3 : a,X2 : a,X1 : a] : ((! [X4 : (a > a > $o)] : ((! [X5 : a,X7 : a,X6 : a] : (((X4 @ X5 @ X6) & (X4 @ X6 @ X7)) => (X4 @ X5 @ X7)) & ! [X5 : a,X6 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6))) => (X4 @ X1 @ X2)) & ! [X4 : (a > a > $o)] : ((! [X6 : a,X5 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6)) & ! [X7 : a,X5 : a,X6 : a] : (((X4 @ X6 @ X7) & (X4 @ X5 @ X6)) => (X4 @ X5 @ X7))) => (X4 @ X2 @ X3))) => ! [X4 : (a > a > $o)] : ((! [X6 : a,X5 : a] : ((X0 @ X5 @ X6) => (X4 @ X5 @ X6)) & ! [X5 : a,X6 : a,X7 : a] : (((X4 @ X6 @ X7) & (X4 @ X5 @ X6)) => (X4 @ X5 @ X7))) => (X4 @ X1 @ X3)))),
% 0.58/0.41 inference(negated_conjecture,[status(cth)],[f1])).
% 0.58/0.41 thf(f3,plain,(
% 0.58/0.41 ~ ! [X0 : (a > a > $o),X1 : a,X2 : a,X3 : a] : ((! [X4 : (a > a > $o)] : ((! [X5 : a,X6 : a,X7 : a] : (((X4 @ X5 @ X7) & (X4 @ X7 @ X6)) => (X4 @ X5 @ X6)) & ! [X8 : a,X9 : a] : ((X0 @ X8 @ X9) => (X4 @ X8 @ X9))) => (X4 @ X3 @ X2)) & ! [X10 : (a > a > $o)] : ((! [X11 : a,X12 : a] : ((X0 @ X12 @ X11) => (X10 @ X12 @ X11)) & ! [X13 : a,X14 : a,X15 : a] : (((X10 @ X15 @ X13) & (X10 @ X14 @ X15)) => (X10 @ X14 @ X13))) => (X10 @ X2 @ X1))) => ! [X16 : (a > a > $o)] : ((! [X17 : a,X18 : a] : ((X0 @ X18 @ X17) => (X16 @ X18 @ X17)) & ! [X19 : a,X20 : a,X21 : a] : (((X16 @ X20 @ X21) & (X16 @ X19 @ X20)) => (X16 @ X19 @ X21))) => (X16 @ X3 @ X1)))),
% 0.58/0.41 inference(rectify,[],[f2])).
% 0.58/0.41 thf(f4,plain,(
% 0.58/0.41 ~ ! [X1 : a,X0 : (a > a > $o),X3 : a,X2 : a] : ((! [X10 : (a > a > $o)] : ((! [X13 : a,X14 : a,X15 : a] : (((((X10 @ X14 @ X15)) = $true) & (((X10 @ X15 @ X13)) = $true)) => (((X10 @ X14 @ X13)) = $true)) & ! [X11 : a,X12 : a] : (($true = ((X0 @ X12 @ X11))) => (((X10 @ X12 @ X11)) = $true))) => (((X10 @ X2 @ X1)) = $true)) & ! [X4 : (a > a > $o)] : ((! [X9 : a,X8 : a] : ((((X0 @ X8 @ X9)) = $true) => (((X4 @ X8 @ X9)) = $true)) & ! [X6 : a,X7 : a,X5 : a] : (((((X4 @ X7 @ X6)) = $true) & (((X4 @ X5 @ X7)) = $true)) => (((X4 @ X5 @ X6)) = $true))) => (((X4 @ X3 @ X2)) = $true))) => ! [X16 : (a > a > $o)] : ((! [X19 : a,X21 : a,X20 : a] : (((((X16 @ X20 @ X21)) = $true) & (((X16 @ X19 @ X20)) = $true)) => (((X16 @ X19 @ X21)) = $true)) & ! [X18 : a,X17 : a] : ((((X0 @ X18 @ X17)) = $true) => (((X16 @ X18 @ X17)) = $true))) => (((X16 @ X3 @ X1)) = $true)))),
% 0.58/0.41 inference(fool_elimination,[],[f3])).
% 0.58/0.41 thf(f5,plain,(
% 0.58/0.41 ? [X1 : a,X0 : (a > a > $o),X3 : a,X2 : a] : (? [X16 : (a > a > $o)] : ((((X16 @ X3 @ X1)) != $true) & (! [X19 : a,X21 : a,X20 : a] : ((((X16 @ X19 @ X21)) = $true) | ((((X16 @ X20 @ X21)) != $true) | (((X16 @ X19 @ X20)) != $true))) & ! [X17 : a,X18 : a] : ((((X16 @ X18 @ X17)) = $true) | (((X0 @ X18 @ X17)) != $true)))) & (! [X10 : (a > a > $o)] : ((((X10 @ X2 @ X1)) = $true) | (? [X13 : a,X14 : a,X15 : a] : ((((X10 @ X14 @ X13)) != $true) & ((((X10 @ X14 @ X15)) = $true) & (((X10 @ X15 @ X13)) = $true))) | ? [X11 : a,X12 : a] : (($true = ((X0 @ X12 @ X11))) & (((X10 @ X12 @ X11)) != $true)))) & ! [X4 : (a > a > $o)] : ((((X4 @ X3 @ X2)) = $true) | (? [X8 : a,X9 : a] : ((((X0 @ X8 @ X9)) = $true) & (((X4 @ X8 @ X9)) != $true)) | ? [X6 : a,X7 : a,X5 : a] : ((((X4 @ X5 @ X6)) != $true) & ((((X4 @ X7 @ X6)) = $true) & (((X4 @ X5 @ X7)) = $true)))))))),
% 0.58/0.41 inference(ennf_transformation,[],[f4])).
% 0.58/0.41 thf(f6,plain,(
% 0.58/0.41 ? [X3 : a,X1 : a,X2 : a,X0 : (a > a > $o)] : (? [X16 : (a > a > $o)] : ((((X16 @ X3 @ X1)) != $true) & ! [X17 : a,X18 : a] : ((((X16 @ X18 @ X17)) = $true) | (((X0 @ X18 @ X17)) != $true)) & ! [X19 : a,X20 : a,X21 : a] : ((((X16 @ X20 @ X21)) != $true) | (((X16 @ X19 @ X20)) != $true) | (((X16 @ X19 @ X21)) = $true))) & ! [X4 : (a > a > $o)] : (? [X5 : a,X7 : a,X6 : a] : ((((X4 @ X7 @ X6)) = $true) & (((X4 @ X5 @ X7)) = $true) & (((X4 @ X5 @ X6)) != $true)) | (((X4 @ X3 @ X2)) = $true) | ? [X8 : a,X9 : a] : ((((X0 @ X8 @ X9)) = $true) & (((X4 @ X8 @ X9)) != $true))) & ! [X10 : (a > a > $o)] : (? [X15 : a,X14 : a,X13 : a] : ((((X10 @ X15 @ X13)) = $true) & (((X10 @ X14 @ X13)) != $true) & (((X10 @ X14 @ X15)) = $true)) | (((X10 @ X2 @ X1)) = $true) | ? [X11 : a,X12 : a] : (($true = ((X0 @ X12 @ X11))) & (((X10 @ X12 @ X11)) != $true))))),
% 0.58/0.41 inference(flattening,[],[f5])).
% 0.58/0.41 thf(f7,plain,(
% 0.58/0.41 ? [X0 : a,X1 : a,X2 : a,X3 : (a > a > $o)] : (? [X4 : (a > a > $o)] : ((((X4 @ X0 @ X1)) != $true) & ! [X5 : a,X6 : a] : ((((X4 @ X6 @ X5)) = $true) | (((X3 @ X6 @ X5)) != $true)) & ! [X7 : a,X8 : a,X9 : a] : ((((X4 @ X8 @ X9)) != $true) | (((X4 @ X7 @ X8)) != $true) | (((X4 @ X7 @ X9)) = $true))) & ! [X10 : (a > a > $o)] : (? [X11 : a,X12 : a,X13 : a] : ((((X10 @ X12 @ X13)) = $true) & ($true = ((X10 @ X11 @ X12))) & (((X10 @ X11 @ X13)) != $true)) | (((X10 @ X0 @ X2)) = $true) | ? [X14 : a,X15 : a] : ((((X3 @ X14 @ X15)) = $true) & (((X10 @ X14 @ X15)) != $true))) & ! [X16 : (a > a > $o)] : (? [X17 : a,X18 : a,X19 : a] : ((((X16 @ X17 @ X19)) = $true) & ($true != ((X16 @ X18 @ X19))) & (((X16 @ X18 @ X17)) = $true)) | ($true = ((X16 @ X2 @ X1))) | ? [X20 : a,X21 : a] : ((((X3 @ X21 @ X20)) = $true) & ($true != ((X16 @ X21 @ X20))))))),
% 0.58/0.41 inference(rectify,[],[f6])).
% 0.58/0.41 thf(f8,plain,(
% 0.58/0.41 ((((sK4 @ sK0 @ sK1)) != $true) & ! [X5 : a,X6 : a] : ((((sK4 @ X6 @ X5)) = $true) | ($true != ((sK3 @ X6 @ X5)))) & ! [X7 : a,X8 : a,X9 : a] : ((((sK4 @ X8 @ X9)) != $true) | (((sK4 @ X7 @ X8)) != $true) | (((sK4 @ X7 @ X9)) = $true))) & ! [X10 : (a > a > $o)] : (((((X10 @ (sK6 @ X10) @ (sK7 @ X10))) = $true) & (((X10 @ (sK5 @ X10) @ (sK6 @ X10))) = $true) & (((X10 @ (sK5 @ X10) @ (sK7 @ X10))) != $true)) | ($true = ((X10 @ sK0 @ sK2))) | ((((sK3 @ (sK8 @ X10) @ (sK9 @ X10))) = $true) & (((X10 @ (sK8 @ X10) @ (sK9 @ X10))) != $true))) & ! [X16 : (a > a > $o)] : ((($true = ((X16 @ (sK10 @ X16) @ (sK12 @ X16)))) & (((X16 @ (sK11 @ X16) @ (sK12 @ X16))) != $true) & (((X16 @ (sK11 @ X16) @ (sK10 @ X16))) = $true)) | (((X16 @ sK2 @ sK1)) = $true) | (($true = ((sK3 @ (sK14 @ X16) @ (sK13 @ X16)))) & (((X16 @ (sK14 @ X16) @ (sK13 @ X16))) != $true)))),
% 0.58/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16),skolemize(X21,sK14 @ X16)],[f7])).
% 0.58/0.41 thf(f9,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : ((((X16 @ (sK14 @ X16) @ (sK13 @ X16))) != $true) | (((X16 @ sK2 @ sK1)) = $true) | (((X16 @ (sK11 @ X16) @ (sK10 @ X16))) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f10,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : (($true = ((sK3 @ (sK14 @ X16) @ (sK13 @ X16)))) | (((X16 @ (sK11 @ X16) @ (sK10 @ X16))) = $true) | (((X16 @ sK2 @ sK1)) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f11,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : ((((X16 @ (sK14 @ X16) @ (sK13 @ X16))) != $true) | (((X16 @ sK2 @ sK1)) = $true) | (((X16 @ (sK11 @ X16) @ (sK12 @ X16))) != $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f12,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : ((((X16 @ (sK11 @ X16) @ (sK12 @ X16))) != $true) | ($true = ((sK3 @ (sK14 @ X16) @ (sK13 @ X16)))) | (((X16 @ sK2 @ sK1)) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f13,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : ((((X16 @ (sK14 @ X16) @ (sK13 @ X16))) != $true) | (((X16 @ sK2 @ sK1)) = $true) | ($true = ((X16 @ (sK10 @ X16) @ (sK12 @ X16))))) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f14,plain,(
% 0.58/0.41 ( ! [X16 : (a > a > $o)] : (($true = ((sK3 @ (sK14 @ X16) @ (sK13 @ X16)))) | ($true = ((X16 @ (sK10 @ X16) @ (sK12 @ X16)))) | (((X16 @ sK2 @ sK1)) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f15,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((X10 @ (sK8 @ X10) @ (sK9 @ X10))) != $true) | ($true = ((X10 @ sK0 @ sK2))) | (((X10 @ (sK5 @ X10) @ (sK7 @ X10))) != $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f16,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((X10 @ (sK5 @ X10) @ (sK7 @ X10))) != $true) | ($true = ((X10 @ sK0 @ sK2))) | (((sK3 @ (sK8 @ X10) @ (sK9 @ X10))) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f17,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((X10 @ (sK8 @ X10) @ (sK9 @ X10))) != $true) | (((X10 @ (sK5 @ X10) @ (sK6 @ X10))) = $true) | ($true = ((X10 @ sK0 @ sK2)))) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f18,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((sK3 @ (sK8 @ X10) @ (sK9 @ X10))) = $true) | (((X10 @ (sK5 @ X10) @ (sK6 @ X10))) = $true) | ($true = ((X10 @ sK0 @ sK2)))) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f19,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((X10 @ (sK8 @ X10) @ (sK9 @ X10))) != $true) | ($true = ((X10 @ sK0 @ sK2))) | (((X10 @ (sK6 @ X10) @ (sK7 @ X10))) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f20,plain,(
% 0.58/0.41 ( ! [X10 : (a > a > $o)] : ((((sK3 @ (sK8 @ X10) @ (sK9 @ X10))) = $true) | (((X10 @ (sK6 @ X10) @ (sK7 @ X10))) = $true) | ($true = ((X10 @ sK0 @ sK2)))) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f21,plain,(
% 0.58/0.41 ( ! [X8 : a,X9 : a,X7 : a] : ((((sK4 @ X8 @ X9)) != $true) | (((sK4 @ X7 @ X8)) != $true) | (((sK4 @ X7 @ X9)) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f22,plain,(
% 0.58/0.41 ( ! [X6 : a,X5 : a] : (($true != ((sK3 @ X6 @ X5))) | (((sK4 @ X6 @ X5)) = $true)) )),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f23,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK1)) != $true)),
% 0.58/0.41 inference(cnf_transformation,[],[f8])).
% 0.58/0.41 thf(f121,definition,(
% 0.58/0.41 spl15_10 <=> ($true = ((sK4 @ sK2 @ sK1)))),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition])).
% 0.58/0.41 thf(f122,plain,(
% 0.58/0.41 ($true != ((sK4 @ sK2 @ sK1))) | spl15_10),
% 0.58/0.41 inference(avatar_component_clause,[],[f121])).
% 0.58/0.41 thf(f123,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | ~spl15_10),
% 0.58/0.41 inference(avatar_component_clause,[],[f121])).
% 0.58/0.41 thf(f125,definition,(
% 0.58/0.41 spl15_11 <=> (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition])).
% 0.58/0.41 thf(f126,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) != $true) | spl15_11),
% 0.58/0.41 inference(avatar_component_clause,[],[f125])).
% 0.58/0.41 thf(f127,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ~spl15_11),
% 0.58/0.41 inference(avatar_component_clause,[],[f125])).
% 0.58/0.41 thf(f132,plain,(
% 0.58/0.41 ( ! [X0 : a] : (($true != ((sK4 @ X0 @ sK2))) | ($true != $true) | ($true = ((sK4 @ X0 @ sK1)))) ) | ~spl15_10),
% 0.58/0.41 inference(constrained_superposition,[],[f21,f123])).
% 0.58/0.41 thf(f133,plain,(
% 0.58/0.41 ( ! [X0 : a] : (($true != ((sK4 @ X0 @ sK2))) | ($true = ((sK4 @ X0 @ sK1)))) ) | ~spl15_10),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f132])).
% 0.58/0.41 thf(f445,definition,(
% 0.58/0.41 spl15_26 <=> (((sK4 @ sK0 @ sK2)) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition])).
% 0.58/0.41 thf(f446,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK2)) != $true) | spl15_26),
% 0.58/0.41 inference(avatar_component_clause,[],[f445])).
% 0.58/0.41 thf(f447,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK2)) = $true) | ~spl15_26),
% 0.58/0.41 inference(avatar_component_clause,[],[f445])).
% 0.58/0.41 thf(f452,definition,(
% 0.58/0.41 spl15_28 <=> (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition])).
% 0.58/0.41 thf(f454,plain,(
% 0.58/0.41 (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ~spl15_28),
% 0.58/0.41 inference(avatar_component_clause,[],[f452])).
% 0.58/0.41 thf(f475,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK1)) = $true) | ($true != $true) | (~spl15_10 | ~spl15_26)),
% 0.58/0.41 inference(constrained_superposition,[],[f133,f447])).
% 0.58/0.41 thf(f477,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK1)) = $true) | (~spl15_10 | ~spl15_26)),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f475])).
% 0.58/0.41 thf(f478,plain,(
% 0.58/0.41 $false | (~spl15_10 | ~spl15_26)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f477,f23])).
% 0.58/0.41 thf(f479,plain,(
% 0.58/0.41 ~spl15_10 | ~spl15_26),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f478])).
% 0.58/0.41 thf(f512,plain,(
% 0.58/0.41 (((sK4 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true != $true) | ~spl15_11),
% 0.58/0.41 inference(constrained_superposition,[],[f22,f127])).
% 0.58/0.41 thf(f513,plain,(
% 0.58/0.41 (((sK4 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ~spl15_11),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f512])).
% 0.58/0.41 thf(f515,plain,(
% 0.58/0.41 ($true != $true) | (((sK4 @ (sK10 @ sK4) @ (sK12 @ sK4))) = $true) | ($true = ((sK4 @ sK2 @ sK1))) | ~spl15_11),
% 0.58/0.41 inference(constrained_superposition,[],[f13,f513])).
% 0.58/0.41 thf(f516,plain,(
% 0.58/0.41 ($true != $true) | (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) != $true) | ($true = ((sK4 @ sK2 @ sK1))) | ~spl15_11),
% 0.58/0.41 inference(constrained_superposition,[],[f11,f513])).
% 0.58/0.41 thf(f517,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | ($true != $true) | (((sK4 @ (sK11 @ sK4) @ (sK10 @ sK4))) = $true) | ~spl15_11),
% 0.58/0.41 inference(constrained_superposition,[],[f9,f513])).
% 0.58/0.41 thf(f519,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (((sK4 @ (sK10 @ sK4) @ (sK12 @ sK4))) = $true) | ~spl15_11),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f515])).
% 0.58/0.41 thf(f520,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) != $true) | ($true = ((sK4 @ sK2 @ sK1))) | ~spl15_11),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f516])).
% 0.58/0.41 thf(f521,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (((sK4 @ (sK11 @ sK4) @ (sK10 @ sK4))) = $true) | ~spl15_11),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f517])).
% 0.58/0.41 thf(f523,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) != $true) | (spl15_10 | ~spl15_11)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f520,f122])).
% 0.58/0.41 thf(f532,definition,(
% 0.58/0.41 spl15_33 <=> (((sK4 @ (sK10 @ sK4) @ (sK12 @ sK4))) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_33])],[avatar_definition])).
% 0.58/0.41 thf(f533,plain,(
% 0.58/0.41 (((sK4 @ (sK10 @ sK4) @ (sK12 @ sK4))) != $true) | spl15_33),
% 0.58/0.41 inference(avatar_component_clause,[],[f532])).
% 0.58/0.41 thf(f534,plain,(
% 0.58/0.41 (((sK4 @ (sK10 @ sK4) @ (sK12 @ sK4))) = $true) | ~spl15_33),
% 0.58/0.41 inference(avatar_component_clause,[],[f532])).
% 0.58/0.41 thf(f535,plain,(
% 0.58/0.41 spl15_10 | spl15_33 | ~spl15_11),
% 0.58/0.41 inference(avatar_split_clause,[],[f519,f125,f532,f121])).
% 0.58/0.41 thf(f537,definition,(
% 0.58/0.41 spl15_34 <=> (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_34])],[avatar_definition])).
% 0.58/0.41 thf(f538,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) = $true) | ~spl15_34),
% 0.58/0.41 inference(avatar_component_clause,[],[f537])).
% 0.58/0.41 thf(f539,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) != $true) | spl15_34),
% 0.58/0.41 inference(avatar_component_clause,[],[f537])).
% 0.58/0.41 thf(f542,definition,(
% 0.58/0.41 spl15_35 <=> (((sK4 @ (sK11 @ sK4) @ (sK10 @ sK4))) = $true)),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_35])],[avatar_definition])).
% 0.58/0.41 thf(f543,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK10 @ sK4))) != $true) | spl15_35),
% 0.58/0.41 inference(avatar_component_clause,[],[f542])).
% 0.58/0.41 thf(f544,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK10 @ sK4))) = $true) | ~spl15_35),
% 0.58/0.41 inference(avatar_component_clause,[],[f542])).
% 0.58/0.41 thf(f545,plain,(
% 0.58/0.41 spl15_35 | spl15_10 | ~spl15_11),
% 0.58/0.41 inference(avatar_split_clause,[],[f521,f125,f121,f542])).
% 0.58/0.41 thf(f579,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ sK0 @ sK2)) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ($true != $true) | (((sK4 @ X0 @ (sK6 @ sK4))) != $true) | (((sK4 @ X0 @ (sK7 @ sK4))) = $true)) )),
% 0.58/0.41 inference(constrained_superposition,[],[f21,f20])).
% 0.58/0.41 thf(f590,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ X0 @ (sK7 @ sK4))) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | (((sK4 @ sK0 @ sK2)) = $true) | (((sK4 @ X0 @ (sK6 @ sK4))) != $true)) )),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f579])).
% 0.58/0.41 thf(f603,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ X0 @ (sK7 @ sK4))) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | (((sK4 @ X0 @ (sK6 @ sK4))) != $true)) ) | spl15_26),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f590,f446])).
% 0.58/0.41 thf(f608,definition,(
% 0.58/0.41 spl15_36 <=> ! [X0 : a] : ((((sK4 @ X0 @ (sK7 @ sK4))) = $true) | (((sK4 @ X0 @ (sK6 @ sK4))) != $true))),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_36])],[avatar_definition])).
% 0.58/0.41 thf(f609,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ X0 @ (sK6 @ sK4))) != $true) | (((sK4 @ X0 @ (sK7 @ sK4))) = $true)) ) | ~spl15_36),
% 0.58/0.41 inference(avatar_component_clause,[],[f608])).
% 0.58/0.41 thf(f610,plain,(
% 0.58/0.41 spl15_28 | spl15_36 | spl15_26),
% 0.58/0.41 inference(avatar_split_clause,[],[f603,f445,f608,f452])).
% 0.58/0.41 thf(f625,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ($true != $true) | (((sK4 @ sK0 @ sK2)) = $true) | ~spl15_36),
% 0.58/0.41 inference(constrained_superposition,[],[f609,f18])).
% 0.58/0.41 thf(f626,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) = $true) | (((sK4 @ sK0 @ sK2)) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ~spl15_36),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f625])).
% 0.58/0.41 thf(f627,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK2)) = $true) | (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ~spl15_36),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f626,f16])).
% 0.58/0.41 thf(f628,plain,(
% 0.58/0.41 (((sK3 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | (spl15_26 | ~spl15_36)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f627,f446])).
% 0.58/0.41 thf(f629,plain,(
% 0.58/0.41 spl15_28 | spl15_26 | ~spl15_36),
% 0.58/0.41 inference(avatar_split_clause,[],[f628,f608,f445,f452])).
% 0.58/0.41 thf(f630,plain,(
% 0.58/0.41 (((sK4 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ($true != $true) | ~spl15_28),
% 0.58/0.41 inference(constrained_superposition,[],[f22,f454])).
% 0.58/0.41 thf(f631,plain,(
% 0.58/0.41 (((sK4 @ (sK8 @ sK4) @ (sK9 @ sK4))) = $true) | ~spl15_28),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f630])).
% 0.58/0.41 thf(f633,plain,(
% 0.58/0.41 ($true = ((sK4 @ (sK6 @ sK4) @ (sK7 @ sK4)))) | ($true != $true) | (((sK4 @ sK0 @ sK2)) = $true) | ~spl15_28),
% 0.58/0.41 inference(constrained_superposition,[],[f19,f631])).
% 0.58/0.41 thf(f634,plain,(
% 0.58/0.41 ($true != $true) | (((sK4 @ sK0 @ sK2)) = $true) | (((sK4 @ (sK5 @ sK4) @ (sK6 @ sK4))) = $true) | ~spl15_28),
% 0.58/0.41 inference(constrained_superposition,[],[f17,f631])).
% 0.58/0.41 thf(f635,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK2)) = $true) | (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) != $true) | ($true != $true) | ~spl15_28),
% 0.58/0.41 inference(constrained_superposition,[],[f15,f631])).
% 0.58/0.41 thf(f636,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) != $true) | (((sK4 @ sK0 @ sK2)) = $true) | ~spl15_28),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f635])).
% 0.58/0.41 thf(f638,plain,(
% 0.58/0.41 (((sK4 @ sK0 @ sK2)) = $true) | ($true = ((sK4 @ (sK6 @ sK4) @ (sK7 @ sK4)))) | ~spl15_28),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f633])).
% 0.58/0.41 thf(f639,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK6 @ sK4))) = $true) | (((sK4 @ sK0 @ sK2)) = $true) | ~spl15_28),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f634])).
% 0.58/0.41 thf(f640,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) != $true) | (spl15_26 | ~spl15_28)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f636,f446])).
% 0.58/0.41 thf(f642,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK6 @ sK4))) = $true) | (spl15_26 | ~spl15_28)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f639,f446])).
% 0.58/0.41 thf(f646,plain,(
% 0.58/0.41 ($true != $true) | (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) = $true) | (spl15_26 | ~spl15_28 | ~spl15_36)),
% 0.58/0.41 inference(constrained_superposition,[],[f609,f642])).
% 0.58/0.41 thf(f647,plain,(
% 0.58/0.41 (((sK4 @ (sK5 @ sK4) @ (sK7 @ sK4))) = $true) | (spl15_26 | ~spl15_28 | ~spl15_36)),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f646])).
% 0.58/0.41 thf(f649,plain,(
% 0.58/0.41 $false | (spl15_26 | ~spl15_28 | ~spl15_36)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f647,f640])).
% 0.58/0.41 thf(f650,plain,(
% 0.58/0.41 spl15_26 | ~spl15_28 | ~spl15_36),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f649])).
% 0.58/0.41 thf(f657,definition,(
% 0.58/0.41 spl15_39 <=> ($true = ((sK4 @ (sK6 @ sK4) @ (sK7 @ sK4))))),
% 0.58/0.41 introduced(definition,[new_symbols(definition,[spl15_39])],[avatar_definition])).
% 0.58/0.41 thf(f659,plain,(
% 0.58/0.41 ($true = ((sK4 @ (sK6 @ sK4) @ (sK7 @ sK4)))) | ~spl15_39),
% 0.58/0.41 inference(avatar_component_clause,[],[f657])).
% 0.58/0.41 thf(f660,plain,(
% 0.58/0.41 spl15_39 | spl15_26 | ~spl15_28),
% 0.58/0.41 inference(avatar_split_clause,[],[f638,f452,f445,f657])).
% 0.58/0.41 thf(f661,plain,(
% 0.58/0.41 ~spl15_34 | spl15_10 | ~spl15_11),
% 0.58/0.41 inference(avatar_split_clause,[],[f523,f125,f121,f537])).
% 0.58/0.41 thf(f664,plain,(
% 0.58/0.41 ( ! [X0 : a] : (($true != ((sK4 @ X0 @ (sK10 @ sK4)))) | ($true = ((sK4 @ X0 @ (sK12 @ sK4)))) | ($true != $true)) ) | ~spl15_33),
% 0.58/0.41 inference(constrained_superposition,[],[f21,f534])).
% 0.58/0.41 thf(f665,plain,(
% 0.58/0.41 ( ! [X0 : a] : (($true != ((sK4 @ X0 @ (sK10 @ sK4)))) | ($true = ((sK4 @ X0 @ (sK12 @ sK4))))) ) | ~spl15_33),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f664])).
% 0.58/0.41 thf(f673,plain,(
% 0.58/0.41 ($true != $true) | (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) = $true) | (~spl15_33 | ~spl15_35)),
% 0.58/0.41 inference(constrained_superposition,[],[f665,f544])).
% 0.58/0.41 thf(f674,plain,(
% 0.58/0.41 (((sK4 @ (sK11 @ sK4) @ (sK12 @ sK4))) = $true) | (~spl15_33 | ~spl15_35)),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f673])).
% 0.58/0.41 thf(f676,plain,(
% 0.58/0.41 $false | (~spl15_33 | spl15_34 | ~spl15_35)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f674,f539])).
% 0.58/0.41 thf(f677,plain,(
% 0.58/0.41 ~spl15_33 | spl15_34 | ~spl15_35),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f676])).
% 0.58/0.41 thf(f680,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true = ((sK4 @ sK2 @ sK1))) | ($true != $true) | spl15_33),
% 0.58/0.41 inference(constrained_superposition,[],[f533,f14])).
% 0.58/0.41 thf(f681,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true = ((sK4 @ sK2 @ sK1))) | spl15_33),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f680])).
% 0.58/0.41 thf(f682,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (spl15_11 | spl15_33)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f681,f126])).
% 0.58/0.41 thf(f683,plain,(
% 0.58/0.41 $false | (spl15_10 | spl15_11 | spl15_33)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f682,f122])).
% 0.58/0.41 thf(f684,plain,(
% 0.58/0.41 spl15_10 | spl15_11 | spl15_33),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f683])).
% 0.58/0.41 thf(f688,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true != $true) | ~spl15_34),
% 0.58/0.41 inference(constrained_superposition,[],[f12,f538])).
% 0.58/0.41 thf(f690,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true = ((sK4 @ sK2 @ sK1))) | ~spl15_34),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f688])).
% 0.58/0.41 thf(f691,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (spl15_11 | ~spl15_34)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f690,f126])).
% 0.58/0.41 thf(f692,plain,(
% 0.58/0.41 $false | (spl15_10 | spl15_11 | ~spl15_34)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f691,f122])).
% 0.58/0.41 thf(f693,plain,(
% 0.58/0.41 spl15_10 | spl15_11 | ~spl15_34),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f692])).
% 0.58/0.41 thf(f694,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | ($true != $true) | spl15_35),
% 0.58/0.41 inference(constrained_superposition,[],[f543,f10])).
% 0.58/0.41 thf(f695,plain,(
% 0.58/0.41 ($true = ((sK4 @ sK2 @ sK1))) | (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | spl15_35),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f694])).
% 0.58/0.41 thf(f696,plain,(
% 0.58/0.41 (((sK3 @ (sK14 @ sK4) @ (sK13 @ sK4))) = $true) | (spl15_10 | spl15_35)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f695,f122])).
% 0.58/0.41 thf(f697,plain,(
% 0.58/0.41 $false | (spl15_10 | spl15_11 | spl15_35)),
% 0.58/0.41 inference(forward_subsumption_resolution,[],[f696,f126])).
% 0.58/0.41 thf(f698,plain,(
% 0.58/0.41 spl15_10 | spl15_11 | spl15_35),
% 0.58/0.41 inference(avatar_contradiction_clause,[],[f697])).
% 0.58/0.41 thf(f711,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ X0 @ (sK6 @ sK4))) != $true) | (((sK4 @ X0 @ (sK7 @ sK4))) = $true) | ($true != $true)) ) | ~spl15_39),
% 0.58/0.41 inference(constrained_superposition,[],[f21,f659])).
% 0.58/0.41 thf(f712,plain,(
% 0.58/0.41 ( ! [X0 : a] : ((((sK4 @ X0 @ (sK6 @ sK4))) != $true) | (((sK4 @ X0 @ (sK7 @ sK4))) = $true)) ) | ~spl15_39),
% 0.58/0.41 inference(trivial_inequality_removal,[],[f711])).
% 0.58/0.41 thf(f713,plain,(
% 0.58/0.41 spl15_36 | ~spl15_39),
% 0.58/0.41 inference(avatar_split_clause,[],[f712,f657,f608])).
% 0.58/0.41 cnf(s22, plain, ~spl15_10 | ~spl15_26, inference(sat_conversion,[],[f479])).
% 0.58/0.41 cnf(s25, plain, spl15_10 | ~spl15_11 | spl15_33, inference(sat_conversion,[],[f535])).
% 0.58/0.41 cnf(s27, plain, spl15_10 | ~spl15_11 | spl15_35, inference(sat_conversion,[],[f545])).
% 0.58/0.41 cnf(s29, plain, spl15_26 | spl15_28 | spl15_36, inference(sat_conversion,[],[f610])).
% 0.58/0.41 cnf(s33, plain, spl15_26 | spl15_28 | ~spl15_36, inference(sat_conversion,[],[f629])).
% 0.58/0.41 cnf(s34, plain, spl15_26 | ~spl15_28 | ~spl15_36, inference(sat_conversion,[],[f650])).
% 0.58/0.41 cnf(s36, plain, spl15_26 | ~spl15_28 | spl15_39, inference(sat_conversion,[],[f660])).
% 0.58/0.41 cnf(s37, plain, spl15_10 | ~spl15_11 | ~spl15_34, inference(sat_conversion,[],[f661])).
% 0.58/0.41 cnf(s38, plain, ~spl15_33 | spl15_34 | ~spl15_35, inference(sat_conversion,[],[f677])).
% 0.58/0.41 cnf(s39, plain, spl15_10 | spl15_11 | spl15_33, inference(sat_conversion,[],[f684])).
% 0.58/0.41 cnf(s40, plain, spl15_10 | spl15_11 | ~spl15_34, inference(sat_conversion,[],[f693])).
% 0.58/0.41 cnf(s41, plain, spl15_10 | spl15_11 | spl15_35, inference(sat_conversion,[],[f698])).
% 0.58/0.41 cnf(s44, plain, spl15_36 | ~spl15_39, inference(sat_conversion,[],[f713])).
% 0.58/0.41 cnf(s45, plain, spl15_11 | spl15_10, inference(rat,[],[s38,s39,s40,s41])).
% 0.58/0.41 cnf(s46, plain, ~spl15_11 | spl15_10, inference(rat,[],[s38,s25,s27,s37])).
% 0.58/0.41 cnf(s47, plain, spl15_10, inference(rat,[],[s46,s45])).
% 0.58/0.41 cnf(s48, plain, ~spl15_26, inference(rat,[],[s22,s47])).
% 0.58/0.41 cnf(s51, plain, ~spl15_28, inference(rat,[],[s44,s34,s36,s48])).
% 0.58/0.41 cnf(s52, plain, spl15_36, inference(rat,[],[s29,s48,s51])).
% 0.58/0.41 cnf(s53, plain, $false, inference(rat,[],[s33,s48,s51,s52])).
% 0.58/0.41 thf(f714,plain,(
% 0.58/0.41 $false),
% 0.58/0.41 inference(avatar_sat_refutation,[],[s53])).
% 0.58/0.41 % SZS output end Proof for theBenchmark
% 0.58/0.41 % (3640732)------------------------------
% 0.58/0.41 % (3640732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.58/0.41 % (3640732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.58/0.41 % (3640732)CaDiCaL version: 2.1.3
% 0.58/0.41 % (3640732)Termination reason: Refutation
% 0.58/0.41 % (3640732)Time elapsed: 0.049 s
% 0.58/0.41 % (3640732)Peak memory usage: 13 MB
% 0.58/0.41 % (3640732)Instructions burned: 50 (million)
% 0.58/0.41 % (3640727)Success in time 0.086 s
% 0.58/0.41 % Vampire exiting
%------------------------------------------------------------------------------