%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PHI008^4 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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:20:21 AM UTC 2026
% Result : Theorem 0.17s 0.30s
% Output : Refutation 0.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI008^4 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/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 13:15:23 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.17/0.30 % (309194)Will run a generic schedule for satisfiability detection.
% 0.17/0.30 % (309199)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1121454562_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.30 % Exception at run slice level
% 0.17/0.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.17/0.30 % (309200)% WARNING: option uhcvi not known.
% 0.17/0.30 % (309200)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2032111126:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.30 % (309201)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=604164539:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.30 % (309202)dis+10_1_sil=32000:sp=arity:random_seed=4210559773:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.30 % (309204)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2223157042:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.30 % (309203)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2830297851:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.30 % (309205)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3548659589:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.30 % (309200)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.17/0.30 % (309203)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.17/0.30 % (309200)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.17/0.30 % (309207)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2068091987:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.17/0.30 % Exception at run slice level
% 0.17/0.30 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.17/0.30 % (309215)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=393265649:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.30 % (309215) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-309194-309215"...
% 0.17/0.30 % (309215)...printing done.
% 0.17/0.30 % (309215)Refutation found. Thanks to Tanya!
% 0.17/0.30 % SZS status Theorem for theBenchmark
% 0.17/0.30 % SZS output start Proof for theBenchmark
% 0.17/0.30 thf(type_def_5, type, qML_mu: $tType).
% 0.17/0.30 thf(type_def_6, type, qML_i: $tType).
% 0.17/0.30 thf(type_def_7, type, sTfun: ($tType * $tType) > $tType).
% 0.17/0.30 thf(func_def_0, type, scott_G: (qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_1, type, scott_NE_QML_mu: (qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_2, type, scott_P: ((qML_mu > qML_i > $o) > qML_i > $o)).
% 0.17/0.30 thf(func_def_3, type, scott_ess_QML_mu: ((qML_mu > qML_i > $o) > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_5, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.17/0.30 thf(func_def_6, type, vIMP: ($o > $o > $o)).
% 0.17/0.30 thf(func_def_7, type, db0: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_8, type, db1: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_9, type, db2: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_10, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 0.17/0.30 thf(func_def_13, type, vAND: ($o > $o > $o)).
% 0.17/0.30 thf(func_def_14, type, db5: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_15, type, vNOT: ($o > $o)).
% 0.17/0.30 thf(func_def_16, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 0.17/0.30 thf(func_def_17, type, sK0: (qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_18, type, sK1: ((qML_mu > qML_i > $o) > (qML_mu > qML_i > $o) > qML_i)).
% 0.17/0.30 thf(func_def_19, type, sK2: ((qML_mu > qML_i > $o) > (qML_mu > qML_i > $o) > qML_mu)).
% 0.17/0.30 thf(func_def_20, type, sK3: qML_i).
% 0.17/0.30 thf(func_def_21, type, sK4: (qML_i > $o)).
% 0.17/0.30 thf(func_def_22, type, sK5: qML_i).
% 0.17/0.30 thf(func_def_23, type, db3: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_24, type, sK6: (qML_mu > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_25, type, sK7: (qML_mu > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_26, type, sK8: (qML_mu > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_27, type, sK9: (qML_mu > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_28, type, db4: !>[X0: $tType]:(X0)).
% 0.17/0.30 thf(func_def_29, type, sK10: (qML_i > (qML_mu > qML_i > qML_mu > qML_i > $o) > qML_mu)).
% 0.17/0.30 thf(func_def_30, type, sK11: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_31, type, sK12: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_32, type, sK13: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_33, type, sK14: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_34, type, sK15: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 0.17/0.30 thf(func_def_35, type, sK16: ((qML_mu > qML_i > $o) > qML_i > qML_mu > qML_i > $o)).
% 0.17/0.30 thf(func_def_36, type, sK17: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_37, type, sK18: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_38, type, sK19: ((qML_mu > qML_i > $o) > qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_39, type, sK20: ((qML_mu > qML_i > $o) > qML_i > qML_i)).
% 0.17/0.30 thf(func_def_40, type, sK21: (qML_i > qML_mu)).
% 0.17/0.30 thf(func_def_41, type, sK22: (qML_i > qML_i)).
% 0.17/0.30 thf(f1,axiom,(
% 0.17/0.30 (scott_G = (^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((scott_P @ X2 @ X1) => (X2 @ X0 @ X1)))))),
% 0.17/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_G__def)).
% 0.17/0.30 thf(f2,axiom,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((scott_P @ X1 @ X0) => ! [X2 : qML_i] : (scott_P @ X1 @ X2))),
% 0.17/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_A4)).
% 0.17/0.30 thf(f3,axiom,(
% 0.17/0.30 ! [X0 : qML_i,X1 : qML_i] : ? [X2 : qML_mu] : (scott_G @ X2 @ X1)),
% 0.17/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_T3)).
% 0.17/0.30 thf(f7,axiom,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (~(scott_P @ X1 @ X0) => (scott_P @ (^[X2 : qML_mu, X3 : qML_i] : (~(X1 @ X2 @ X3))) @ X0))),
% 0.17/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_A1b)).
% 0.17/0.30 thf(f12,conjecture,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_i > $o)] : (! [X2 : qML_i] : (X1 @ X2) | ~(X1 @ X0))),
% 0.17/0.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 0.17/0.30 thf(f13,negated_conjecture,(
% 0.17/0.30 ~ ! [X0 : qML_i,X1 : (qML_i > $o)] : (! [X2 : qML_i] : (X1 @ X2) | ~(X1 @ X0))),
% 0.17/0.30 inference(negated_conjecture,[status(cth)],[f12])).
% 0.17/0.30 thf(f14,plain,(
% 0.17/0.30 (scott_G = (^[X0 : qML_mu, X1 : qML_i] : (! [X2 : (qML_mu > qML_i > $o)] : ((scott_P @ X2 @ X1) => (X2 @ X0 @ X1)))))),
% 0.17/0.30 inference(rectify,[],[f1])).
% 0.17/0.30 thf(f15,plain,(
% 0.17/0.30 (scott_G = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((scott_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))))),
% 0.17/0.30 inference(fool_elimination,[],[f14])).
% 0.17/0.30 thf(f16,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((scott_P @ X1 @ X0) => ! [X2 : qML_i] : (scott_P @ X1 @ X2))),
% 0.17/0.30 inference(rectify,[],[f2])).
% 0.17/0.30 thf(f17,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((scott_P @ X1 @ X0)) = $true) => ! [X2 : qML_i] : (((scott_P @ X1 @ X2)) = $true))),
% 0.17/0.30 inference(fool_elimination,[],[f16])).
% 0.17/0.30 thf(f18,plain,(
% 0.17/0.30 ! [X1 : qML_i] : ? [X2 : qML_mu] : (scott_G @ X2 @ X1)),
% 0.17/0.30 inference(rectify,[],[f3])).
% 0.17/0.30 thf(f19,plain,(
% 0.17/0.30 ! [X1 : qML_i] : ? [X2 : qML_mu] : (((scott_G @ X2 @ X1)) = $true)),
% 0.17/0.30 inference(fool_elimination,[],[f18])).
% 0.17/0.30 thf(f26,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (~(scott_P @ X1 @ X0) => (scott_P @ (^[X2 : qML_mu, X3 : qML_i] : (~(X1 @ X2 @ X3))) @ X0))),
% 0.17/0.30 inference(rectify,[],[f7])).
% 0.17/0.30 thf(f27,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (~ (((scott_P @ X1 @ X0)) = $true) => ($true = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))))),
% 0.17/0.30 inference(fool_elimination,[],[f26])).
% 0.17/0.30 thf(f36,plain,(
% 0.17/0.30 ~ ! [X0 : qML_i,X1 : (qML_i > $o)] : (! [X2 : qML_i] : (X1 @ X2) | ~(X1 @ X0))),
% 0.17/0.30 inference(rectify,[],[f13])).
% 0.17/0.30 thf(f37,plain,(
% 0.17/0.30 ~ ! [X0 : qML_i,X1 : (qML_i > $o)] : (! [X2 : qML_i] : (((X1 @ X2)) = $true) | ~ (((X1 @ X0)) = $true))),
% 0.17/0.30 inference(fool_elimination,[],[f36])).
% 0.17/0.30 thf(f38,plain,(
% 0.17/0.30 ! [X0 : qML_i] : ? [X1 : qML_mu] : (((scott_G @ X1 @ X0)) = $true)),
% 0.17/0.30 inference(rectify,[],[f19])).
% 0.17/0.30 thf(f39,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((scott_P @ X1 @ X0)) != $true) => ($true = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))))),
% 0.17/0.30 inference(flattening,[],[f27])).
% 0.17/0.30 thf(f41,plain,(
% 0.17/0.30 ~ ! [X0 : qML_i,X1 : (qML_i > $o)] : (! [X2 : qML_i] : (((X1 @ X2)) = $true) | (((X1 @ X0)) != $true))),
% 0.17/0.30 inference(flattening,[],[f37])).
% 0.17/0.30 thf(f42,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (! [X2 : qML_i] : (((scott_P @ X1 @ X2)) = $true) | (((scott_P @ X1 @ X0)) != $true))),
% 0.17/0.30 inference(ennf_transformation,[],[f17])).
% 0.17/0.30 thf(f45,plain,(
% 0.17/0.30 ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))) | (((scott_P @ X1 @ X0)) = $true))),
% 0.17/0.30 inference(ennf_transformation,[],[f39])).
% 0.17/0.30 thf(f48,plain,(
% 0.17/0.30 ? [X0 : qML_i,X1 : (qML_i > $o)] : (? [X2 : qML_i] : (((X1 @ X2)) != $true) & (((X1 @ X0)) = $true))),
% 0.17/0.30 inference(ennf_transformation,[],[f41])).
% 0.17/0.30 thf(f49,plain,(
% 0.17/0.30 ! [X0 : qML_i] : ($true = ((scott_G @ (sK0 @ X0) @ X0)))),
% 0.17/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP]),skolemize(X1,sK0 @ X0)],[f38])).
% 0.17/0.30 thf(f51,plain,(
% 0.17/0.30 ($true != ((sK4 @ sK5))) & ($true = ((sK4 @ sK3)))),
% 0.17/0.30 inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5)],[f48])).
% 0.17/0.30 thf(f52,plain,(
% 0.17/0.30 (scott_G = (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((scott_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))))),
% 0.17/0.30 inference(cnf_transformation,[],[f15])).
% 0.17/0.30 thf(f53,plain,(
% 0.17/0.30 ( ! [X2 : qML_i,X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((scott_P @ X1 @ X0)) != $true) | (((scott_P @ X1 @ X2)) = $true)) )),
% 0.17/0.30 inference(cnf_transformation,[],[f42])).
% 0.17/0.30 thf(f54,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = ((scott_G @ (sK0 @ X0) @ X0)))) )),
% 0.17/0.30 inference(cnf_transformation,[],[f49])).
% 0.17/0.30 thf(f59,plain,(
% 0.17/0.30 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X1 @ Y0 @ Y1))))) @ X0))) | (((scott_P @ X1 @ X0)) = $true)) )),
% 0.17/0.30 inference(cnf_transformation,[],[f45])).
% 0.17/0.30 thf(f64,plain,(
% 0.17/0.30 ($true = ((sK4 @ sK3)))),
% 0.17/0.30 inference(cnf_transformation,[],[f51])).
% 0.17/0.30 thf(f65,plain,(
% 0.17/0.30 ($true != ((sK4 @ sK5)))),
% 0.17/0.30 inference(cnf_transformation,[],[f51])).
% 0.17/0.30 thf(f67,definition,(
% 0.17/0.30 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.17/0.30 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.17/0.30 thf(f69,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = (((^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (!! @ (qML_mu > qML_i > $o) @ (^[Y2 : qML_mu > qML_i > $o]: ((scott_P @ Y2 @ Y1) => (Y2 @ Y0 @ Y1))))))) @ (sK0 @ X0) @ X0)))) )),
% 0.17/0.30 inference(definition_unfolding,[],[f54,f52])).
% 0.17/0.30 thf(f107,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = ((!! @ (qML_mu > qML_i > $o) @ (^[Y0 : qML_mu > qML_i > $o]: ((scott_P @ Y0 @ X0) => (Y0 @ (sK0 @ X0) @ X0))))))) )),
% 0.17/0.30 inference(beta-eta_normalization,[],[f69])).
% 0.17/0.30 thf(f108,plain,(
% 0.17/0.30 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = (((^[Y0 : qML_mu > qML_i > $o]: ((scott_P @ Y0 @ X0) => (Y0 @ (sK0 @ X0) @ X0))) @ X1)))) )),
% 0.17/0.30 inference(pi_proxy_clausification,[],[f107])).
% 0.17/0.30 thf(f109,plain,(
% 0.17/0.30 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : (($true = (((scott_P @ X1 @ X0) => (X1 @ (sK0 @ X0) @ X0))))) )),
% 0.17/0.30 inference(beta-eta_normalization,[],[f108])).
% 0.17/0.30 thf(f110,plain,(
% 0.17/0.30 ( ! [X0 : qML_i,X1 : (qML_mu > qML_i > $o)] : ((((scott_P @ X1 @ X0)) = $false) | ($true = ((X1 @ (sK0 @ X0) @ X0)))) )),
% 0.17/0.30 inference(imp_proxy_clausification,[],[f109])).
% 0.17/0.30 thf(f113,plain,(
% 0.17/0.30 ($true != $true) | (((sK4 @ sK5)) = $false)),
% 0.17/0.30 inference(constrained_superposition,[],[f65,f67])).
% 0.17/0.30 thf(f115,plain,(
% 0.17/0.30 (((sK4 @ sK5)) = $false)),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f113])).
% 0.17/0.30 thf(f123,plain,(
% 0.17/0.30 ( ! [X2 : qML_i,X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true != $true) | ($true = ((scott_P @ X0 @ X2))) | ($false = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(constrained_superposition,[],[f53,f67])).
% 0.17/0.30 thf(f124,plain,(
% 0.17/0.30 ( ! [X2 : qML_i,X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true = ((scott_P @ X0 @ X2))) | ($false = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f123])).
% 0.17/0.30 thf(f135,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = $false) | ($false = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (sK4 @ ((^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (Y3)))) @ Y0 @ Y1))))) @ X0))) | (sK5 != X0)) )),
% 0.17/0.30 inference(constrained_superposition,[],[f115,f110])).
% 0.17/0.30 thf(f148,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($false = ((scott_P @ (^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (sK4 @ ((^[Y2 : qML_mu]: ((^[Y3 : qML_i]: (Y3)))) @ Y0 @ Y1))))) @ X0))) | (sK5 != X0)) )),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f135])).
% 0.17/0.30 thf(f149,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : ((sK5 != X0) | ($false = ((scott_P @ (^[Y0 : qML_mu]: (sK4)) @ X0)))) )),
% 0.17/0.30 inference(beta-eta_normalization,[],[f148])).
% 0.17/0.30 thf(f164,plain,(
% 0.17/0.30 ( ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true = $false) | ($true = (((^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X0 @ Y0 @ Y1))))) @ (sK0 @ X1) @ X1))) | ($true = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(constrained_superposition,[],[f110,f59])).
% 0.17/0.30 thf(f165,plain,(
% 0.17/0.30 ( ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true = (((^[Y0 : qML_mu]: ((^[Y1 : qML_i]: (~ (X0 @ Y0 @ Y1))))) @ (sK0 @ X1) @ X1))) | ($true = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f164])).
% 0.17/0.30 thf(f166,plain,(
% 0.17/0.30 ( ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($true = ((~ (X0 @ (sK0 @ X1) @ X1)))) | ($true = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(beta-eta_normalization,[],[f165])).
% 0.17/0.30 thf(f167,plain,(
% 0.17/0.30 ( ! [X0 : (qML_mu > qML_i > $o),X1 : qML_i] : (($false = ((X0 @ (sK0 @ X1) @ X1))) | ($true = ((scott_P @ X0 @ X1)))) )),
% 0.17/0.30 inference(not_proxy_clausification,[],[f166])).
% 0.17/0.30 thf(f171,plain,(
% 0.17/0.30 ($false = ((scott_P @ (^[Y0 : qML_mu]: (sK4)) @ sK5)))),
% 0.17/0.30 inference(equality_resolution,[],[f149])).
% 0.17/0.30 thf(f320,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = $false) | ($false = ((scott_P @ (^[Y0 : qML_mu]: (sK4)) @ X0)))) )),
% 0.17/0.30 inference(constrained_superposition,[],[f171,f124])).
% 0.17/0.30 thf(f336,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($false = ((scott_P @ (^[Y0 : qML_mu]: (sK4)) @ X0)))) )),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f320])).
% 0.17/0.30 thf(f426,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($true = $false) | ($false = (((^[Y0 : qML_mu]: (sK4)) @ (sK0 @ X0) @ X0)))) )),
% 0.17/0.30 inference(constrained_superposition,[],[f336,f167])).
% 0.17/0.30 thf(f436,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($false = (((^[Y0 : qML_mu]: (sK4)) @ (sK0 @ X0) @ X0)))) )),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f426])).
% 0.17/0.30 thf(f437,plain,(
% 0.17/0.30 ( ! [X0 : qML_i] : (($false = ((sK4 @ X0)))) )),
% 0.17/0.30 inference(beta-eta_normalization,[],[f436])).
% 0.17/0.30 thf(f488,plain,(
% 0.17/0.30 ($true = $false)),
% 0.17/0.30 inference(backward_demodulation,[],[f64,f437])).
% 0.17/0.30 thf(f489,plain,(
% 0.17/0.30 $false),
% 0.17/0.30 inference(trivial_inequality_removal,[],[f488])).
% 0.17/0.30 % SZS output end Proof for theBenchmark
% 0.17/0.30 % (309215)------------------------------
% 0.17/0.30 % (309215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.30 % (309215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.30 % (309215)CaDiCaL version: 2.1.3
% 0.17/0.30 % (309215)Termination reason: Refutation
% 0.17/0.30 % (309215)Time elapsed: 0.019 s
% 0.17/0.30 % (309215)Peak memory usage: 12 MB
% 0.17/0.30 % (309215)Instructions burned: 62 (million)
% 0.17/0.30 % (309194)Success in time 0.073 s
% 0.17/0.30 % Vampire exiting
%------------------------------------------------------------------------------