%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO384^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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:49:50 AM UTC 2026
% Result : Theorem 0.22s 0.27s
% Output : Refutation 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO384^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n008.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:50:39 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.27 % (3413748)Will run a generic schedule for satisfiability detection.
% 0.22/0.27 % (3413753)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2638257761_2999 on theBenchmark for (2999ds/0Mi)
% 0.22/0.27 % Exception at run slice level
% 0.22/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.27 % (3413754)% WARNING: option uhcvi not known.
% 0.22/0.27 % (3413754)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=792366456:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.22/0.27 % (3413757)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=627296742:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.22/0.27 % (3413755)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=549610911:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.22/0.27 % (3413756)dis+10_1_sil=32000:sp=arity:random_seed=1758580113:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.22/0.27 % (3413757)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.27 % (3413754)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.22/0.27 % (3413754)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.22/0.27 % (3413761)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4235893206:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.22/0.27 % Exception at run slice level
% 0.22/0.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.22/0.27 % (3413755) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3413748-3413755"...
% 0.22/0.27 % (3413755)...printing done.
% 0.22/0.27 % (3413755)Refutation found. Thanks to Tanya!
% 0.22/0.27 % SZS status Theorem for theBenchmark
% 0.22/0.27 % SZS output start Proof for theBenchmark
% 0.22/0.27 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.22/0.27 thf(func_def_0, type, cD: ($i > $i > $i > $o)).
% 0.22/0.27 thf(func_def_1, type, cF: ($i > $i > $o)).
% 0.22/0.27 thf(func_def_2, type, cS: ($i > $i > $o)).
% 0.22/0.27 thf(func_def_6, type, sK0: ($i > $i)).
% 0.22/0.27 thf(func_def_7, type, sK1: ($i > $i > $i)).
% 0.22/0.27 thf(func_def_8, type, sK2: ($i > $i > $i)).
% 0.22/0.27 thf(func_def_9, type, sK3: ($i > $i)).
% 0.22/0.27 thf(func_def_11, type, sK5: ($i > $i)).
% 0.22/0.27 thf(func_def_12, type, sK6: ($i > $i)).
% 0.22/0.27 thf(func_def_14, type, sK8: ($i > $i)).
% 0.22/0.27 thf(func_def_16, type, sK10: ($i > $i)).
% 0.22/0.27 thf(func_def_17, type, sK11: ($i > $i)).
% 0.22/0.27 thf(func_def_18, type, sK12: ($i > $i)).
% 0.22/0.27 thf(func_def_19, type, sK13: ($i > $i)).
% 0.22/0.27 thf(func_def_20, type, sK14: ($i > $i)).
% 0.22/0.27 thf(func_def_21, type, sK15: ($i > $i > $i)).
% 0.22/0.27 thf(f1,conjecture,(
% 0.22/0.27 ((! [X2 : $i] : ? [X5 : $i] : ! [X6 : $i,X7 : $i] : ((cD @ X6 @ X7 @ X5) => ! [X1 : $i,X8 : $i] : (((cF @ X7 @ X8) & (cF @ X6 @ X1)) => (cD @ X1 @ X8 @ X2))) & ? [X0 : $i] : ! [X2 : $i] : ? [X3 : $i] : ! [X4 : $i] : ((cS @ X3 @ X4) => (cD @ X4 @ X0 @ X2)) & ! [X0 : $i] : ? [X1 : $i] : (cF @ X0 @ X1)) => ? [X1 : $i] : ! [X2 : $i] : ? [X9 : $i] : ! [X4 : $i] : ((cS @ X9 @ X4) => ! [X8 : $i] : ((cF @ X4 @ X8) => (cD @ X8 @ X1 @ X2)))) => ((! [X2 : $i] : ? [X5 : $i] : ! [X6 : $i,X7 : $i] : ((cD @ X6 @ X7 @ X5) => ! [X1 : $i,X8 : $i] : (((cF @ X7 @ X8) & (cF @ X6 @ X1)) => (cD @ X1 @ X8 @ X2))) & ? [X0 : $i] : ! [X2 : $i] : ? [X3 : $i] : ! [X4 : $i] : ((cS @ X3 @ X4) => (cD @ X4 @ X0 @ X2)) & ! [X0 : $i] : ? [X1 : $i] : (cF @ X0 @ X1)) => ? [X1 : $i] : ! [X2 : $i] : ? [X9 : $i] : ! [X4 : $i] : ((cS @ X9 @ X4) => ! [X8 : $i] : ((cF @ X4 @ X8) => (cD @ X8 @ X1 @ X2))))),
% 0.22/0.27 file('/export/starexec/sandbox/benchmark/theBenchmark.p',cTHM408)).
% 0.22/0.27 thf(f2,negated_conjecture,(
% 0.22/0.27 ~(((! [X2 : $i] : ? [X5 : $i] : ! [X6 : $i,X7 : $i] : ((cD @ X6 @ X7 @ X5) => ! [X1 : $i,X8 : $i] : (((cF @ X7 @ X8) & (cF @ X6 @ X1)) => (cD @ X1 @ X8 @ X2))) & ? [X0 : $i] : ! [X2 : $i] : ? [X3 : $i] : ! [X4 : $i] : ((cS @ X3 @ X4) => (cD @ X4 @ X0 @ X2)) & ! [X0 : $i] : ? [X1 : $i] : (cF @ X0 @ X1)) => ? [X1 : $i] : ! [X2 : $i] : ? [X9 : $i] : ! [X4 : $i] : ((cS @ X9 @ X4) => ! [X8 : $i] : ((cF @ X4 @ X8) => (cD @ X8 @ X1 @ X2)))) => ((! [X2 : $i] : ? [X5 : $i] : ! [X6 : $i,X7 : $i] : ((cD @ X6 @ X7 @ X5) => ! [X1 : $i,X8 : $i] : (((cF @ X7 @ X8) & (cF @ X6 @ X1)) => (cD @ X1 @ X8 @ X2))) & ? [X0 : $i] : ! [X2 : $i] : ? [X3 : $i] : ! [X4 : $i] : ((cS @ X3 @ X4) => (cD @ X4 @ X0 @ X2)) & ! [X0 : $i] : ? [X1 : $i] : (cF @ X0 @ X1)) => ? [X1 : $i] : ! [X2 : $i] : ? [X9 : $i] : ! [X4 : $i] : ((cS @ X9 @ X4) => ! [X8 : $i] : ((cF @ X4 @ X8) => (cD @ X8 @ X1 @ X2)))))),
% 0.22/0.27 inference(negated_conjecture,[status(cth)],[f1])).
% 0.22/0.27 thf(f3,plain,(
% 0.22/0.27 ~(((! [X0 : $i] : ? [X1 : $i] : ! [X2 : $i,X3 : $i] : ((cD @ X2 @ X3 @ X1) => ! [X4 : $i,X5 : $i] : (((cF @ X3 @ X5) & (cF @ X2 @ X4)) => (cD @ X4 @ X5 @ X0))) & ? [X6 : $i] : ! [X7 : $i] : ? [X8 : $i] : ! [X9 : $i] : ((cS @ X8 @ X9) => (cD @ X9 @ X6 @ X7)) & ! [X10 : $i] : ? [X11 : $i] : (cF @ X10 @ X11)) => ? [X12 : $i] : ! [X13 : $i] : ? [X14 : $i] : ! [X15 : $i] : ((cS @ X14 @ X15) => ! [X16 : $i] : ((cF @ X15 @ X16) => (cD @ X16 @ X12 @ X13)))) => ((! [X17 : $i] : ? [X18 : $i] : ! [X19 : $i,X20 : $i] : ((cD @ X19 @ X20 @ X18) => ! [X21 : $i,X22 : $i] : (((cF @ X20 @ X22) & (cF @ X19 @ X21)) => (cD @ X21 @ X22 @ X17))) & ? [X23 : $i] : ! [X24 : $i] : ? [X25 : $i] : ! [X26 : $i] : ((cS @ X25 @ X26) => (cD @ X26 @ X23 @ X24)) & ! [X27 : $i] : ? [X28 : $i] : (cF @ X27 @ X28)) => ? [X29 : $i] : ! [X30 : $i] : ? [X31 : $i] : ! [X32 : $i] : ((cS @ X31 @ X32) => ! [X33 : $i] : ((cF @ X32 @ X33) => (cD @ X33 @ X29 @ X30)))))),
% 0.22/0.27 inference(rectify,[],[f2])).
% 0.22/0.27 thf(f4,plain,(
% 0.22/0.27 ~(((! [X0 : $i] : ? [X1 : $i] : ! [X2 : $i,X3 : $i] : ((((cD @ X2 @ X3 @ X1)) = $true) => ! [X4 : $i,X5 : $i] : (((((cF @ X3 @ X5)) = $true) & (((cF @ X2 @ X4)) = $true)) => (((cD @ X4 @ X5 @ X0)) = $true))) & ? [X6 : $i] : ! [X7 : $i] : ? [X8 : $i] : ! [X9 : $i] : ((((cS @ X8 @ X9)) = $true) => (((cD @ X9 @ X6 @ X7)) = $true)) & ! [X10 : $i] : ? [X11 : $i] : (((cF @ X10 @ X11)) = $true)) => ? [X12 : $i] : ! [X13 : $i] : ? [X14 : $i] : ! [X15 : $i] : ((((cS @ X14 @ X15)) = $true) => ! [X16 : $i] : ((((cF @ X15 @ X16)) = $true) => (((cD @ X16 @ X12 @ X13)) = $true)))) => ((! [X17 : $i] : ? [X18 : $i] : ! [X19 : $i,X20 : $i] : ((((cD @ X19 @ X20 @ X18)) = $true) => ! [X21 : $i,X22 : $i] : (((((cF @ X20 @ X22)) = $true) & (((cF @ X19 @ X21)) = $true)) => (((cD @ X21 @ X22 @ X17)) = $true))) & ? [X23 : $i] : ! [X24 : $i] : ? [X25 : $i] : ! [X26 : $i] : ((((cS @ X25 @ X26)) = $true) => (((cD @ X26 @ X23 @ X24)) = $true)) & ! [X27 : $i] : ? [X28 : $i] : (((cF @ X27 @ X28)) = $true)) => ? [X29 : $i] : ! [X30 : $i] : ? [X31 : $i] : ! [X32 : $i] : ((((cS @ X31 @ X32)) = $true) => ! [X33 : $i] : ((((cF @ X32 @ X33)) = $true) => (((cD @ X33 @ X29 @ X30)) = $true)))))),
% 0.22/0.27 inference(fool_elimination,[],[f3])).
% 0.22/0.27 thf(f5,plain,(
% 0.22/0.27 (! [X29 : $i] : ? [X30 : $i] : ! [X31 : $i] : ? [X32 : $i] : (? [X33 : $i] : ((((cD @ X33 @ X29 @ X30)) != $true) & (((cF @ X32 @ X33)) = $true)) & (((cS @ X31 @ X32)) = $true)) & (! [X17 : $i] : ? [X18 : $i] : ! [X19 : $i,X20 : $i] : (! [X21 : $i,X22 : $i] : ((((cD @ X21 @ X22 @ X17)) = $true) | ((((cF @ X20 @ X22)) != $true) | (((cF @ X19 @ X21)) != $true))) | (((cD @ X19 @ X20 @ X18)) != $true)) & ? [X23 : $i] : ! [X24 : $i] : ? [X25 : $i] : ! [X26 : $i] : ((((cD @ X26 @ X23 @ X24)) = $true) | (((cS @ X25 @ X26)) != $true)) & ! [X27 : $i] : ? [X28 : $i] : (((cF @ X27 @ X28)) = $true))) & (? [X12 : $i] : ! [X13 : $i] : ? [X14 : $i] : ! [X15 : $i] : (! [X16 : $i] : ((((cD @ X16 @ X12 @ X13)) = $true) | (((cF @ X15 @ X16)) != $true)) | (((cS @ X14 @ X15)) != $true)) | (? [X0 : $i] : ! [X1 : $i] : ? [X2 : $i,X3 : $i] : (? [X4 : $i,X5 : $i] : ((((cD @ X4 @ X5 @ X0)) != $true) & ((((cF @ X3 @ X5)) = $true) & (((cF @ X2 @ X4)) = $true))) & (((cD @ X2 @ X3 @ X1)) = $true)) | ! [X6 : $i] : ? [X7 : $i] : ! [X8 : $i] : ? [X9 : $i] : ((((cD @ X9 @ X6 @ X7)) != $true) & (((cS @ X8 @ X9)) = $true)) | ? [X10 : $i] : ! [X11 : $i] : (((cF @ X10 @ X11)) != $true)))),
% 0.22/0.27 inference(ennf_transformation,[],[f4])).
% 0.22/0.27 thf(f6,plain,(
% 0.22/0.27 ! [X29 : $i] : ? [X30 : $i] : ! [X31 : $i] : ? [X32 : $i] : (? [X33 : $i] : ((((cD @ X33 @ X29 @ X30)) != $true) & (((cF @ X32 @ X33)) = $true)) & (((cS @ X31 @ X32)) = $true)) & ! [X17 : $i] : ? [X18 : $i] : ! [X19 : $i,X20 : $i] : (! [X21 : $i,X22 : $i] : ((((cD @ X21 @ X22 @ X17)) = $true) | (((cF @ X20 @ X22)) != $true) | (((cF @ X19 @ X21)) != $true)) | (((cD @ X19 @ X20 @ X18)) != $true)) & ? [X23 : $i] : ! [X24 : $i] : ? [X25 : $i] : ! [X26 : $i] : ((((cD @ X26 @ X23 @ X24)) = $true) | (((cS @ X25 @ X26)) != $true)) & ! [X27 : $i] : ? [X28 : $i] : (((cF @ X27 @ X28)) = $true) & (? [X12 : $i] : ! [X13 : $i] : ? [X14 : $i] : ! [X15 : $i] : (! [X16 : $i] : ((((cD @ X16 @ X12 @ X13)) = $true) | (((cF @ X15 @ X16)) != $true)) | (((cS @ X14 @ X15)) != $true)) | ? [X0 : $i] : ! [X1 : $i] : ? [X2 : $i,X3 : $i] : (? [X4 : $i,X5 : $i] : ((((cD @ X4 @ X5 @ X0)) != $true) & (((cF @ X3 @ X5)) = $true) & (((cF @ X2 @ X4)) = $true)) & (((cD @ X2 @ X3 @ X1)) = $true)) | ! [X6 : $i] : ? [X7 : $i] : ! [X8 : $i] : ? [X9 : $i] : ((((cD @ X9 @ X6 @ X7)) != $true) & (((cS @ X8 @ X9)) = $true)) | ? [X10 : $i] : ! [X11 : $i] : (((cF @ X10 @ X11)) != $true))),
% 0.22/0.27 inference(flattening,[],[f5])).
% 0.22/0.27 thf(f7,plain,(
% 0.22/0.27 ! [X0 : $i] : ? [X1 : $i] : ! [X2 : $i] : ? [X3 : $i] : (? [X4 : $i] : (($true != ((cD @ X4 @ X0 @ X1))) & ($true = ((cF @ X3 @ X4)))) & ($true = ((cS @ X2 @ X3)))) & ! [X5 : $i] : ? [X6 : $i] : ! [X7 : $i,X8 : $i] : (! [X9 : $i,X10 : $i] : (($true = ((cD @ X9 @ X10 @ X5))) | ($true != ((cF @ X8 @ X10))) | ($true != ((cF @ X7 @ X9)))) | ($true != ((cD @ X7 @ X8 @ X6)))) & ? [X11 : $i] : ! [X12 : $i] : ? [X13 : $i] : ! [X14 : $i] : (($true = ((cD @ X14 @ X11 @ X12))) | ($true != ((cS @ X13 @ X14)))) & ! [X15 : $i] : ? [X16 : $i] : (((cF @ X15 @ X16)) = $true) & (? [X17 : $i] : ! [X18 : $i] : ? [X19 : $i] : ! [X20 : $i] : (! [X21 : $i] : (($true = ((cD @ X21 @ X17 @ X18))) | ($true != ((cF @ X20 @ X21)))) | ($true != ((cS @ X19 @ X20)))) | ? [X22 : $i] : ! [X23 : $i] : ? [X24 : $i,X25 : $i] : (? [X26 : $i,X27 : $i] : (($true != ((cD @ X26 @ X27 @ X22))) & ($true = ((cF @ X25 @ X27))) & ($true = ((cF @ X24 @ X26)))) & ($true = ((cD @ X24 @ X25 @ X23)))) | ! [X28 : $i] : ? [X29 : $i] : ! [X30 : $i] : ? [X31 : $i] : (($true != ((cD @ X31 @ X28 @ X29))) & ($true = ((cS @ X30 @ X31)))) | ? [X32 : $i] : ! [X33 : $i] : (((cF @ X32 @ X33)) != $true))),
% 0.22/0.27 inference(rectify,[],[f6])).
% 0.22/0.27 thf(f8,plain,(
% 0.22/0.27 ! [X0 : $i] : ! [X2 : $i] : ((($true != ((cD @ (sK2 @ X2 @ X0) @ X0 @ (sK0 @ X0)))) & ($true = ((cF @ (sK1 @ X2 @ X0) @ (sK2 @ X2 @ X0))))) & ($true = ((cS @ X2 @ (sK1 @ X2 @ X0))))) & ! [X5 : $i] : ! [X7 : $i,X8 : $i] : (! [X9 : $i,X10 : $i] : (($true = ((cD @ X9 @ X10 @ X5))) | ($true != ((cF @ X8 @ X10))) | ($true != ((cF @ X7 @ X9)))) | ($true != ((cD @ X7 @ X8 @ (sK3 @ X5))))) & ! [X12 : $i] : ! [X14 : $i] : (($true = ((cD @ X14 @ sK4 @ X12))) | ($true != ((cS @ (sK5 @ X12) @ X14)))) & ! [X15 : $i] : ($true = ((cF @ X15 @ (sK6 @ X15)))) & (! [X18 : $i] : ! [X20 : $i] : (! [X21 : $i] : (($true = ((cD @ X21 @ sK7 @ X18))) | ($true != ((cF @ X20 @ X21)))) | ($true != ((cS @ (sK8 @ X18) @ X20)))) | ! [X23 : $i] : ((($true != ((cD @ (sK12 @ X23) @ (sK13 @ X23) @ sK9))) & ($true = ((cF @ (sK11 @ X23) @ (sK13 @ X23)))) & ($true = ((cF @ (sK10 @ X23) @ (sK12 @ X23))))) & ($true = ((cD @ (sK10 @ X23) @ (sK11 @ X23) @ X23)))) | ! [X28 : $i] : ! [X30 : $i] : (($true != ((cD @ (sK15 @ X30 @ X28) @ X28 @ (sK14 @ X28)))) & ($true = ((cS @ X30 @ (sK15 @ X30 @ X28))))) | ! [X33 : $i] : ($true != ((cF @ sK16 @ X33))))),
% 0.22/0.27 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP,vAPP,vAPP,sK4,vAPP,vAPP,sK7,vAPP,sK9,vAPP,vAPP,vAPP,vAPP,vAPP,vAPP,sK16]),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X11,sK4),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X17,sK7),skolemize(X31,sK15 @ X30 @ X28),skolemize(X22,sK9),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X31,sK15 @ X30 @ X28),skolemize(X32,sK16)],[f7])).
% 0.22/0.27 thf(f17,plain,(
% 0.22/0.27 ( ! [X15 : $i] : (($true = ((cF @ X15 @ (sK6 @ X15))))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f18,plain,(
% 0.22/0.27 ( ! [X14 : $i,X12 : $i] : (($true != ((cS @ (sK5 @ X12) @ X14))) | ($true = ((cD @ X14 @ sK4 @ X12)))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f19,plain,(
% 0.22/0.27 ( ! [X10 : $i,X8 : $i,X9 : $i,X7 : $i,X5 : $i] : (($true != ((cD @ X7 @ X8 @ (sK3 @ X5)))) | ($true != ((cF @ X8 @ X10))) | ($true != ((cF @ X7 @ X9))) | ($true = ((cD @ X9 @ X10 @ X5)))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f20,plain,(
% 0.22/0.27 ( ! [X2 : $i,X0 : $i] : (($true = ((cS @ X2 @ (sK1 @ X2 @ X0))))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f21,plain,(
% 0.22/0.27 ( ! [X2 : $i,X0 : $i] : (($true = ((cF @ (sK1 @ X2 @ X0) @ (sK2 @ X2 @ X0))))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f22,plain,(
% 0.22/0.27 ( ! [X2 : $i,X0 : $i] : (($true != ((cD @ (sK2 @ X2 @ X0) @ X0 @ (sK0 @ X0))))) )),
% 0.22/0.27 inference(cnf_transformation,[],[f8])).
% 0.22/0.27 thf(f31,plain,(
% 0.22/0.27 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((cD @ (sK1 @ (sK5 @ X0) @ X1) @ sK4 @ X0)))) )),
% 0.22/0.27 inference(constrained_superposition,[],[f18,f20])).
% 0.22/0.27 thf(f32,plain,(
% 0.22/0.27 ( ! [X0 : $i,X1 : $i] : (($true = ((cD @ (sK1 @ (sK5 @ X0) @ X1) @ sK4 @ X0)))) )),
% 0.22/0.27 inference(trivial_inequality_removal,[],[f31])).
% 0.22/0.27 thf(f48,plain,(
% 0.22/0.27 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true != ((cF @ sK4 @ X2))) | ($true != ((cF @ (sK1 @ (sK5 @ (sK3 @ X0)) @ X1) @ X3))) | ($true = ((cD @ X3 @ X2 @ X0)))) )),
% 0.22/0.27 inference(constrained_superposition,[],[f19,f32])).
% 0.22/0.27 thf(f49,plain,(
% 0.22/0.27 ( ! [X2 : $i,X3 : $i,X0 : $i,X1 : $i] : (($true != ((cF @ (sK1 @ (sK5 @ (sK3 @ X0)) @ X1) @ X3))) | ($true != ((cF @ sK4 @ X2))) | ($true = ((cD @ X3 @ X2 @ X0)))) )),
% 0.22/0.27 inference(trivial_inequality_removal,[],[f48])).
% 0.22/0.27 thf(f71,plain,(
% 0.22/0.27 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != $true) | ($true != ((cF @ sK4 @ X2))) | ($true = ((cD @ (sK2 @ (sK5 @ (sK3 @ X0)) @ X1) @ X2 @ X0)))) )),
% 0.22/0.27 inference(constrained_superposition,[],[f49,f21])).
% 0.22/0.27 thf(f72,plain,(
% 0.22/0.27 ( ! [X2 : $i,X0 : $i,X1 : $i] : (($true != ((cF @ sK4 @ X2))) | ($true = ((cD @ (sK2 @ (sK5 @ (sK3 @ X0)) @ X1) @ X2 @ X0)))) )),
% 0.22/0.27 inference(trivial_inequality_removal,[],[f71])).
% 0.22/0.27 thf(f86,plain,(
% 0.22/0.27 ( ! [X0 : $i,X1 : $i] : (($true != $true) | ($true = ((cD @ (sK2 @ (sK5 @ (sK3 @ X0)) @ X1) @ (sK6 @ sK4) @ X0)))) )),
% 0.22/0.27 inference(constrained_superposition,[],[f72,f17])).
% 0.22/0.27 thf(f87,plain,(
% 0.22/0.27 ( ! [X0 : $i,X1 : $i] : (($true = ((cD @ (sK2 @ (sK5 @ (sK3 @ X0)) @ X1) @ (sK6 @ sK4) @ X0)))) )),
% 0.22/0.27 inference(trivial_inequality_removal,[],[f86])).
% 0.22/0.27 thf(f93,plain,(
% 0.22/0.27 ($true != $true)),
% 0.22/0.27 inference(constrained_superposition,[],[f22,f87])).
% 0.22/0.27 thf(f96,plain,(
% 0.22/0.27 $false),
% 0.22/0.27 inference(trivial_inequality_removal,[],[f93])).
% 0.22/0.27 % SZS output end Proof for theBenchmark
% 0.22/0.27 % (3413755)------------------------------
% 0.22/0.27 % (3413755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.27 % (3413755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.27 % (3413755)CaDiCaL version: 2.1.3
% 0.22/0.27 % (3413755)Termination reason: Refutation
% 0.22/0.27 % (3413755)Time elapsed: 0.009 s
% 0.22/0.27 % (3413755)Peak memory usage: 12 MB
% 0.22/0.27 % (3413755)Instructions burned: 13 (million)
% 0.22/0.27 % (3413748)Success in time 0.04 s
% 0.22/0.27 % Vampire exiting
%------------------------------------------------------------------------------