%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN036^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:41:48 AM UTC 2026
% Result : Theorem 0.48s 0.38s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYN036^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.28 % Computer : n002.cluster.edu
% 0.21/0.28 % Model : x86_64 x86_64
% 0.21/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.28 % Memory : 8046.5625MB
% 0.21/0.28 % OS : Linux 6.8.0-71-generic
% 0.21/0.28 % CPULimit : 300
% 0.21/0.28 % WCLimit : 300
% 0.21/0.28 % DateTime : Tue Sep 29 16:15:53 UTC 2026
% 0.21/0.28 % CPUTime :
% 0.21/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.21/0.32 Running first-order model finding
% 0.21/0.32 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.48/0.38 % (1481465)Will run a generic schedule for satisfiability detection.
% 0.48/0.38 % (1481472)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1801919236:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 0.48/0.38 % (1481471)% WARNING: option uhcvi not known.
% 0.48/0.38 % (1481470)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3466884379_3000 on theBenchmark for (3000ds/0Mi)
% 0.48/0.38 % (1481471)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3800052666:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 0.48/0.38 % (1481473)dis+10_1_sil=32000:sp=arity:random_seed=228550771:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 0.48/0.38 % (1481474)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1417491590:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 0.48/0.38 % (1481475)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=17994281:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 0.48/0.38 % (1481476)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=212887559:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 0.48/0.38 % (1481471)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.48/0.38 % (1481474)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 0.48/0.38 % Exception at run slice level
% 0.48/0.38 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.48/0.38 % (1481471)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 0.48/0.38 % (1481472) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1481465-1481472"...
% 0.48/0.38 % (1481472)...printing done.
% 0.48/0.38 % (1481472)Refutation found. Thanks to Tanya!
% 0.48/0.38 % SZS status Theorem for theBenchmark
% 0.48/0.38 % SZS output start Proof for theBenchmark
% 0.48/0.38 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 0.48/0.38 thf(func_def_0, type, cQ: ($i > $o)).
% 0.48/0.38 thf(func_def_1, type, cP: ($i > $o)).
% 0.48/0.38 thf(func_def_5, type, sP0: $o).
% 0.48/0.38 thf(func_def_8, type, sK3: ($i > $i)).
% 0.48/0.38 thf(func_def_17, type, sK12: ($i > $i)).
% 0.48/0.38 thf(func_def_20, type, sK15: ($i > $i)).
% 0.48/0.38 thf(func_def_29, type, sK24: ($i > $i)).
% 0.48/0.38 thf(f1,conjecture,(
% 0.48/0.38 (? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X0 : $i] : (cQ @ X0) <=> ! [X1 : $i] : (cP @ X1))) <=> (? [X0 : $i] : ! [X1 : $i] : ((cQ @ X0) <=> (cQ @ X1)) <=> (? [X0 : $i] : (cP @ X0) <=> ! [X1 : $i] : (cQ @ X1)))),
% 0.48/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cX2129)).
% 0.48/0.38 thf(f2,negated_conjecture,(
% 0.48/0.38 ~((? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X0 : $i] : (cQ @ X0) <=> ! [X1 : $i] : (cP @ X1))) <=> (? [X0 : $i] : ! [X1 : $i] : ((cQ @ X0) <=> (cQ @ X1)) <=> (? [X0 : $i] : (cP @ X0) <=> ! [X1 : $i] : (cQ @ X1))))),
% 0.48/0.38 inference(negated_conjecture,[status(cth)],[f1])).
% 0.48/0.38 thf(f3,plain,(
% 0.48/0.38 ~((? [X0 : $i] : ! [X1 : $i] : ((cP @ X0) <=> (cP @ X1)) <=> (? [X2 : $i] : (cQ @ X2) <=> ! [X3 : $i] : (cP @ X3))) <=> (? [X4 : $i] : ! [X5 : $i] : ((cQ @ X4) <=> (cQ @ X5)) <=> (? [X6 : $i] : (cP @ X6) <=> ! [X7 : $i] : (cQ @ X7))))),
% 0.48/0.38 inference(rectify,[],[f2])).
% 0.48/0.38 thf(f4,plain,(
% 0.48/0.38 ~((? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) <=> (? [X2 : $i] : (((cQ @ X2)) = $true) <=> ! [X3 : $i] : (((cP @ X3)) = $true))) <=> (? [X4 : $i] : ! [X5 : $i] : (((cQ @ X4)) = ((cQ @ X5))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : (((cQ @ X7)) = $true))))),
% 0.48/0.38 inference(fool_elimination,[],[f3])).
% 0.48/0.38 thf(f5,plain,(
% 0.48/0.38 (? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) <=> (? [X2 : $i] : (((cQ @ X2)) = $true) <=> ! [X3 : $i] : (((cP @ X3)) = $true))) <~> (? [X4 : $i] : ! [X5 : $i] : (((cQ @ X4)) = ((cQ @ X5))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : (((cQ @ X7)) = $true)))),
% 0.48/0.38 inference(ennf_transformation,[],[f4])).
% 0.48/0.38 thf(f6,definition,(
% 0.48/0.38 ($true = sP0) <=> (? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) <=> (? [X2 : $i] : (((cQ @ X2)) = $true) <=> ! [X3 : $i] : (((cP @ X3)) = $true)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[=])],[predicate_definition_introduction])).
% 0.48/0.38 thf(f7,plain,(
% 0.48/0.38 ($true = sP0) <~> (? [X4 : $i] : ! [X5 : $i] : (((cQ @ X4)) = ((cQ @ X5))) <=> (? [X6 : $i] : (((cP @ X6)) = $true) <=> ! [X7 : $i] : (((cQ @ X7)) = $true)))),
% 0.48/0.38 inference(definition_folding,[],[f5,f6])).
% 0.48/0.38 thf(f8,plain,(
% 0.48/0.38 (($true = sP0) | ((((? [X3 : $i] : (((cP @ X3)) != $true) | ! [X2 : $i] : (((cQ @ X2)) != $true)) & (! [X3 : $i] : (((cP @ X3)) = $true) | ? [X2 : $i] : (((cQ @ X2)) = $true))) | ! [X0 : $i] : ? [X1 : $i] : (((cP @ X0)) != ((cP @ X1)))) & (((? [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : (((cP @ X3)) != $true)) & (! [X3 : $i] : (((cP @ X3)) = $true) | ! [X2 : $i] : (((cQ @ X2)) != $true))) | ? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1)))))) & (((? [X0 : $i] : ! [X1 : $i] : (((cP @ X0)) = ((cP @ X1))) | ((? [X3 : $i] : (((cP @ X3)) != $true) | ! [X2 : $i] : (((cQ @ X2)) != $true)) & (! [X3 : $i] : (((cP @ X3)) = $true) | ? [X2 : $i] : (((cQ @ X2)) = $true)))) & (((? [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : (((cP @ X3)) != $true)) & (! [X3 : $i] : (((cP @ X3)) = $true) | ! [X2 : $i] : (((cQ @ X2)) != $true))) | ! [X0 : $i] : ? [X1 : $i] : (((cP @ X0)) != ((cP @ X1))))) | ($true != sP0))),
% 0.48/0.38 inference(nnf_transformation,[],[f6])).
% 0.48/0.38 thf(f9,plain,(
% 0.48/0.38 (($true = sP0) | ((((? [X0 : $i] : (((cP @ X0)) != $true) | ! [X1 : $i] : (((cQ @ X1)) != $true)) & (! [X2 : $i] : ($true = ((cP @ X2))) | ? [X3 : $i] : ($true = ((cQ @ X3))))) | ! [X4 : $i] : ? [X5 : $i] : (((cP @ X4)) != ((cP @ X5)))) & (((? [X6 : $i] : ($true = ((cQ @ X6))) | ? [X7 : $i] : ($true != ((cP @ X7)))) & (! [X8 : $i] : ($true = ((cP @ X8))) | ! [X9 : $i] : ($true != ((cQ @ X9))))) | ? [X10 : $i] : ! [X11 : $i] : (((cP @ X10)) = ((cP @ X11)))))) & (((? [X12 : $i] : ! [X13 : $i] : (((cP @ X12)) = ((cP @ X13))) | ((? [X14 : $i] : ($true != ((cP @ X14))) | ! [X15 : $i] : ($true != ((cQ @ X15)))) & (! [X16 : $i] : ($true = ((cP @ X16))) | ? [X17 : $i] : ($true = ((cQ @ X17)))))) & (((? [X18 : $i] : ($true = ((cQ @ X18))) | ? [X19 : $i] : ($true != ((cP @ X19)))) & (! [X20 : $i] : ($true = ((cP @ X20))) | ! [X21 : $i] : ($true != ((cQ @ X21))))) | ! [X22 : $i] : ? [X23 : $i] : (((cP @ X22)) != ((cP @ X23))))) | ($true != sP0))),
% 0.48/0.38 inference(rectify,[],[f8])).
% 0.48/0.38 thf(f10,plain,(
% 0.48/0.38 (($true = sP0) | ((((($true != ((cP @ sK1))) | ! [X1 : $i] : (((cQ @ X1)) != $true)) & (! [X2 : $i] : ($true = ((cP @ X2))) | ($true = ((cQ @ sK2))))) | ! [X4 : $i] : (((cP @ X4)) != ((cP @ (sK3 @ X4))))) & (((($true = ((cQ @ sK4))) | ($true != ((cP @ sK5)))) & (! [X8 : $i] : ($true = ((cP @ X8))) | ! [X9 : $i] : ($true != ((cQ @ X9))))) | ! [X11 : $i] : (((cP @ X11)) = ((cP @ sK6)))))) & (((! [X13 : $i] : (((cP @ X13)) = ((cP @ sK7))) | ((($true != ((cP @ sK8))) | ! [X15 : $i] : ($true != ((cQ @ X15)))) & (! [X16 : $i] : ($true = ((cP @ X16))) | ($true = ((cQ @ sK9)))))) & (((($true = ((cQ @ sK10))) | ($true != ((cP @ sK11)))) & (! [X20 : $i] : ($true = ((cP @ X20))) | ! [X21 : $i] : ($true != ((cQ @ X21))))) | ! [X22 : $i] : (((cP @ X22)) != ((cP @ (sK12 @ X22)))))) | ($true != sP0))),
% 0.48/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,vAPP,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,vAPP]),skolemize(X0,sK1),skolemize(X3,sK2),skolemize(X23,sK12 @ X22),skolemize(X6,sK4),skolemize(X7,sK5),skolemize(X10,sK6),skolemize(X12,sK7),skolemize(X14,sK8),skolemize(X17,sK9),skolemize(X18,sK10),skolemize(X19,sK11),skolemize(X23,sK12 @ X22)],[f9])).
% 0.48/0.38 thf(f11,plain,(
% 0.48/0.38 (((((? [X7 : $i] : (((cQ @ X7)) != $true) | ! [X6 : $i] : (((cP @ X6)) != $true)) & (! [X7 : $i] : (((cQ @ X7)) = $true) | ? [X6 : $i] : (((cP @ X6)) = $true))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X4)) != ((cQ @ X5)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : (((cQ @ X7)) != $true)) & (! [X7 : $i] : (((cQ @ X7)) = $true) | ! [X6 : $i] : (((cP @ X6)) != $true))) | ? [X4 : $i] : ! [X5 : $i] : (((cQ @ X4)) = ((cQ @ X5))))) | ($true != sP0)) & (((? [X4 : $i] : ! [X5 : $i] : (((cQ @ X4)) = ((cQ @ X5))) | ((? [X7 : $i] : (((cQ @ X7)) != $true) | ! [X6 : $i] : (((cP @ X6)) != $true)) & (! [X7 : $i] : (((cQ @ X7)) = $true) | ? [X6 : $i] : (((cP @ X6)) = $true)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : (((cQ @ X7)) != $true)) & (! [X7 : $i] : (((cQ @ X7)) = $true) | ! [X6 : $i] : (((cP @ X6)) != $true))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X4)) != ((cQ @ X5))))) | ($true = sP0))),
% 0.48/0.38 inference(nnf_transformation,[],[f7])).
% 0.48/0.38 thf(f12,plain,(
% 0.48/0.38 (((((? [X0 : $i] : (((cQ @ X0)) != $true) | ! [X1 : $i] : (((cP @ X1)) != $true)) & (! [X2 : $i] : (((cQ @ X2)) = $true) | ? [X3 : $i] : (((cP @ X3)) = $true))) | ! [X4 : $i] : ? [X5 : $i] : (((cQ @ X4)) != ((cQ @ X5)))) & (((? [X6 : $i] : (((cP @ X6)) = $true) | ? [X7 : $i] : (((cQ @ X7)) != $true)) & (! [X8 : $i] : ($true = ((cQ @ X8))) | ! [X9 : $i] : ($true != ((cP @ X9))))) | ? [X10 : $i] : ! [X11 : $i] : (((cQ @ X10)) = ((cQ @ X11))))) | ($true != sP0)) & (((? [X12 : $i] : ! [X13 : $i] : (((cQ @ X12)) = ((cQ @ X13))) | ((? [X14 : $i] : ($true != ((cQ @ X14))) | ! [X15 : $i] : ($true != ((cP @ X15)))) & (! [X16 : $i] : ($true = ((cQ @ X16))) | ? [X17 : $i] : ($true = ((cP @ X17)))))) & (((? [X18 : $i] : ($true = ((cP @ X18))) | ? [X19 : $i] : ($true != ((cQ @ X19)))) & (! [X20 : $i] : ($true = ((cQ @ X20))) | ! [X21 : $i] : ($true != ((cP @ X21))))) | ! [X22 : $i] : ? [X23 : $i] : (((cQ @ X22)) != ((cQ @ X23))))) | ($true = sP0))),
% 0.48/0.38 inference(rectify,[],[f11])).
% 0.48/0.38 thf(f13,plain,(
% 0.48/0.38 (((((($true != ((cQ @ sK13))) | ! [X1 : $i] : (((cP @ X1)) != $true)) & (! [X2 : $i] : (((cQ @ X2)) = $true) | ($true = ((cP @ sK14))))) | ! [X4 : $i] : (((cQ @ X4)) != ((cQ @ (sK15 @ X4))))) & (((($true = ((cP @ sK16))) | ($true != ((cQ @ sK17)))) & (! [X8 : $i] : ($true = ((cQ @ X8))) | ! [X9 : $i] : ($true != ((cP @ X9))))) | ! [X11 : $i] : (((cQ @ X11)) = ((cQ @ sK18))))) | ($true != sP0)) & (((! [X13 : $i] : (((cQ @ X13)) = ((cQ @ sK19))) | ((($true != ((cQ @ sK20))) | ! [X15 : $i] : ($true != ((cP @ X15)))) & (! [X16 : $i] : ($true = ((cQ @ X16))) | ($true = ((cP @ sK21)))))) & (((($true = ((cP @ sK22))) | ($true != ((cQ @ sK23)))) & (! [X20 : $i] : ($true = ((cQ @ X20))) | ! [X21 : $i] : ($true != ((cP @ X21))))) | ! [X22 : $i] : (((cQ @ X22)) != ((cQ @ (sK24 @ X22)))))) | ($true = sP0))),
% 0.48/0.38 inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,vAPP,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,vAPP]),skolemize(X0,sK13),skolemize(X3,sK14),skolemize(X23,sK12 @ X22),skolemize(X6,sK16),skolemize(X7,sK17),skolemize(X10,sK18),skolemize(X12,sK19),skolemize(X14,sK20),skolemize(X17,sK21),skolemize(X18,sK22),skolemize(X19,sK23),skolemize(X23,sK12 @ X22)],[f12])).
% 0.48/0.38 thf(f14,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i,X20 : $i] : (($true = ((cP @ X20))) | ($true != ((cQ @ X21))) | (((cP @ X22)) != ((cP @ (sK12 @ X22)))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f15,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cQ @ sK10))) | ($true != ((cP @ sK11))) | (((cP @ X22)) != ((cP @ (sK12 @ X22)))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f16,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cP @ X13)) = ((cP @ sK7))) | ($true = ((cP @ X16))) | ($true = ((cQ @ sK9))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f18,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = sP0) | ($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | (((cP @ X11)) = ((cP @ sK6)))) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f20,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : (($true = sP0) | ($true = ((cP @ X2))) | ($true = ((cQ @ sK2))) | (((cP @ X4)) != ((cP @ (sK3 @ X4))))) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f21,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true = sP0) | ($true != ((cP @ sK1))) | (((cQ @ X1)) != $true) | (((cP @ X4)) != ((cP @ (sK3 @ X4))))) )),
% 0.48/0.38 inference(cnf_transformation,[],[f10])).
% 0.48/0.38 thf(f22,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i,X20 : $i] : (($true = ((cQ @ X20))) | ($true != ((cP @ X21))) | (((cQ @ X22)) != ((cQ @ (sK24 @ X22)))) | ($true = sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f23,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | ($true != ((cQ @ sK23))) | (((cQ @ X22)) != ((cQ @ (sK24 @ X22)))) | ($true = sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f24,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cQ @ X13)) = ((cQ @ sK19))) | ($true = ((cQ @ X16))) | ($true = ((cP @ sK21))) | ($true = sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f26,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | (((cQ @ X11)) = ((cQ @ sK18))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f28,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : ((((cQ @ X2)) = $true) | ($true = ((cP @ sK14))) | (((cQ @ X4)) != ((cQ @ (sK15 @ X4)))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f29,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true != ((cQ @ sK13))) | (((cP @ X1)) != $true) | (((cQ @ X4)) != ((cQ @ (sK15 @ X4)))) | ($true != sP0)) )),
% 0.48/0.38 inference(cnf_transformation,[],[f13])).
% 0.48/0.38 thf(f31,definition,(
% 0.48/0.38 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 0.48/0.38 introduced(theory,[fool_exhaustiveness_axiom])).
% 0.48/0.38 thf(f32,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i,X20 : $i] : (($true = ((cQ @ X20))) | ($true != ((cP @ X21))) | ($true = ((cQ @ X22))) | ($true = sP0) | ($true = ((cQ @ (sK24 @ X22))))) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f22])).
% 0.48/0.38 thf(f35,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | ($true != ((cQ @ sK23))) | (((cQ @ X22)) = $false) | ($true = sP0) | (((cQ @ (sK24 @ X22))) = $false)) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f23])).
% 0.48/0.38 thf(f36,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = ((cQ @ X13))) | ($true = ((cQ @ X16))) | ($true = ((cP @ sK21))) | ($true = sP0) | (((cQ @ sK19)) = $false)) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f24])).
% 0.48/0.38 thf(f37,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cQ @ X13)) = $false) | ($true = ((cQ @ X16))) | ($true = ((cP @ sK21))) | ($true = sP0) | ($true = ((cQ @ sK19)))) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f24])).
% 0.48/0.38 thf(f40,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | ($true = ((cQ @ X11))) | ($true != sP0) | (((cQ @ sK18)) = $false)) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f26])).
% 0.48/0.38 thf(f41,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | (((cQ @ X11)) = $false) | ($true != sP0) | ($true = ((cQ @ sK18)))) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f26])).
% 0.48/0.38 thf(f44,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : ((((cQ @ X2)) = $true) | ($true = ((cP @ sK14))) | (((cQ @ X4)) = $true) | ($true != sP0) | ($true = ((cQ @ (sK15 @ X4))))) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f28])).
% 0.48/0.38 thf(f47,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true != ((cQ @ sK13))) | (((cP @ X1)) != $true) | (((cQ @ X4)) = $false) | ($true != sP0) | (((cQ @ (sK15 @ X4))) = $false)) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f29])).
% 0.48/0.38 thf(f48,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i,X20 : $i] : (($true = ((cP @ X20))) | ($true != ((cQ @ X21))) | ($true = ((cP @ X22))) | ($true != sP0) | ($true = ((cP @ (sK12 @ X22))))) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f14])).
% 0.48/0.38 thf(f51,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cQ @ sK10))) | ($true != ((cP @ sK11))) | (((cP @ X22)) = $false) | ($true != sP0) | (((cP @ (sK12 @ X22))) = $false)) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f15])).
% 0.48/0.38 thf(f52,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = ((cP @ X13))) | ($true = ((cP @ X16))) | ($true = ((cQ @ sK9))) | ($true != sP0) | (((cP @ sK7)) = $false)) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f16])).
% 0.48/0.38 thf(f53,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cP @ X13)) = $false) | ($true = ((cP @ X16))) | ($true = ((cQ @ sK9))) | ($true != sP0) | ($true = ((cP @ sK7)))) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f16])).
% 0.48/0.38 thf(f56,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = sP0) | ($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | ($true = ((cP @ X11))) | (((cP @ sK6)) = $false)) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f18])).
% 0.48/0.38 thf(f57,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = sP0) | ($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | (((cP @ X11)) = $false) | ($true = ((cP @ sK6)))) )),
% 0.48/0.38 inference(iff_proxy_clausification,[],[f18])).
% 0.48/0.38 thf(f60,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : (($true = sP0) | ($true = ((cP @ X2))) | ($true = ((cQ @ sK2))) | ($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f20])).
% 0.48/0.38 thf(f63,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true = sP0) | ($true != ((cP @ sK1))) | (((cQ @ X1)) != $true) | (((cP @ X4)) = $false) | (((cP @ (sK3 @ X4))) = $false)) )),
% 0.48/0.38 inference(xor_proxy_clausification,[],[f21])).
% 0.48/0.38 thf(f65,definition,(
% 0.48/0.38 spl25_1 <=> (((cQ @ sK19)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition])).
% 0.48/0.38 thf(f66,plain,(
% 0.48/0.38 (((cQ @ sK19)) != $false) | spl25_1),
% 0.48/0.38 inference(avatar_component_clause,[],[f65])).
% 0.48/0.38 thf(f67,plain,(
% 0.48/0.38 (((cQ @ sK19)) = $false) | ~spl25_1),
% 0.48/0.38 inference(avatar_component_clause,[],[f65])).
% 0.48/0.38 thf(f69,definition,(
% 0.48/0.38 spl25_2 <=> ($true = sP0)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition])).
% 0.48/0.38 thf(f70,plain,(
% 0.48/0.38 ($true != sP0) | spl25_2),
% 0.48/0.38 inference(avatar_component_clause,[],[f69])).
% 0.48/0.38 thf(f71,plain,(
% 0.48/0.38 ($true = sP0) | ~spl25_2),
% 0.48/0.38 inference(avatar_component_clause,[],[f69])).
% 0.48/0.38 thf(f73,definition,(
% 0.48/0.38 spl25_3 <=> ($true = ((cP @ sK21)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition])).
% 0.48/0.38 thf(f75,plain,(
% 0.48/0.38 ($true = ((cP @ sK21))) | ~spl25_3),
% 0.48/0.38 inference(avatar_component_clause,[],[f73])).
% 0.48/0.38 thf(f77,definition,(
% 0.48/0.38 spl25_4 <=> ! [X16 : $i] : ($true = ((cQ @ X16)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition])).
% 0.48/0.38 thf(f78,plain,(
% 0.48/0.38 ( ! [X16 : $i] : (($true = ((cQ @ X16)))) ) | ~spl25_4),
% 0.48/0.38 inference(avatar_component_clause,[],[f77])).
% 0.48/0.38 thf(f79,plain,(
% 0.48/0.38 spl25_1 | spl25_2 | spl25_3 | spl25_4 | spl25_4),
% 0.48/0.38 inference(avatar_split_clause,[],[f36,f77,f77,f73,f69,f65])).
% 0.48/0.38 thf(f80,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = $false) | (((cQ @ X13)) = $false) | ($true = ((cQ @ X16))) | ($true = ((cP @ sK21))) | ($true = sP0)) ) | ~spl25_1),
% 0.48/0.38 inference(forward_demodulation,[],[f37,f67])).
% 0.48/0.38 thf(f81,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cQ @ X13)) = $false) | ($true = ((cQ @ X16))) | ($true = ((cP @ sK21))) | ($true = sP0)) ) | ~spl25_1),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f80])).
% 0.48/0.38 thf(f83,definition,(
% 0.48/0.38 spl25_5 <=> ! [X13 : $i] : (((cQ @ X13)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition])).
% 0.48/0.38 thf(f84,plain,(
% 0.48/0.38 ( ! [X13 : $i] : ((((cQ @ X13)) = $false)) ) | ~spl25_5),
% 0.48/0.38 inference(avatar_component_clause,[],[f83])).
% 0.48/0.38 thf(f85,plain,(
% 0.48/0.38 spl25_2 | spl25_3 | spl25_4 | spl25_5 | ~spl25_1),
% 0.48/0.38 inference(avatar_split_clause,[],[f81,f65,f83,f77,f73,f69])).
% 0.48/0.38 thf(f86,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | ($true = ((cQ @ X11))) | (((cQ @ sK18)) = $false)) ) | ~spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f40,f71])).
% 0.48/0.38 thf(f88,definition,(
% 0.48/0.38 spl25_6 <=> (((cQ @ sK18)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition])).
% 0.48/0.38 thf(f90,plain,(
% 0.48/0.38 (((cQ @ sK18)) = $false) | ~spl25_6),
% 0.48/0.38 inference(avatar_component_clause,[],[f88])).
% 0.48/0.38 thf(f92,definition,(
% 0.48/0.38 spl25_7 <=> ! [X9 : $i] : ($true != ((cP @ X9)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition])).
% 0.48/0.38 thf(f93,plain,(
% 0.48/0.38 ( ! [X9 : $i] : (($true != ((cP @ X9)))) ) | ~spl25_7),
% 0.48/0.38 inference(avatar_component_clause,[],[f92])).
% 0.48/0.38 thf(f94,plain,(
% 0.48/0.38 spl25_6 | spl25_4 | spl25_7 | spl25_4 | ~spl25_2),
% 0.48/0.38 inference(avatar_split_clause,[],[f86,f69,f77,f92,f77,f88])).
% 0.48/0.38 thf(f95,plain,(
% 0.48/0.38 ($true = $false) | (~spl25_1 | ~spl25_4)),
% 0.48/0.38 inference(constrained_superposition,[],[f78,f67])).
% 0.48/0.38 thf(f99,plain,(
% 0.48/0.38 $false | (~spl25_1 | ~spl25_4)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f95])).
% 0.48/0.38 thf(f100,plain,(
% 0.48/0.38 ~spl25_1 | ~spl25_4),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f99])).
% 0.48/0.38 thf(f102,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : ((((cP @ X1)) != $true) | (((cQ @ X4)) = $false) | ($true != sP0) | (((cQ @ (sK15 @ X4))) = $false)) ) | ~spl25_4),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f47,f78])).
% 0.48/0.38 thf(f103,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : ((((cP @ X1)) != $true) | (((cQ @ X4)) = $false) | (((cQ @ (sK15 @ X4))) = $false)) ) | (~spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f102,f71])).
% 0.48/0.38 thf(f104,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true = $false) | (((cP @ X1)) != $true) | (((cQ @ (sK15 @ X4))) = $false)) ) | (~spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_demodulation,[],[f103,f78])).
% 0.48/0.38 thf(f105,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : ((((cP @ X1)) != $true) | (((cQ @ (sK15 @ X4))) = $false)) ) | (~spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f104])).
% 0.48/0.38 thf(f106,plain,(
% 0.48/0.38 ( ! [X1 : $i] : (($true = $false) | (((cP @ X1)) != $true)) ) | (~spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_demodulation,[],[f105,f78])).
% 0.48/0.38 thf(f107,plain,(
% 0.48/0.38 ( ! [X1 : $i] : ((((cP @ X1)) != $true)) ) | (~spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f106])).
% 0.48/0.38 thf(f108,plain,(
% 0.48/0.38 spl25_7 | ~spl25_2 | ~spl25_4),
% 0.48/0.38 inference(avatar_split_clause,[],[f107,f77,f69,f92])).
% 0.48/0.38 thf(f157,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | (((cQ @ X11)) = $false) | ($true = ((cQ @ sK18)))) ) | ~spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f41,f71])).
% 0.48/0.38 thf(f160,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : ((((cQ @ X2)) = $true) | ($true = ((cP @ sK14))) | (((cQ @ X4)) = $true) | ($true = ((cQ @ (sK15 @ X4))))) ) | ~spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f44,f71])).
% 0.48/0.38 thf(f167,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = $false) | ($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | (((cQ @ X11)) = $false)) ) | (~spl25_2 | ~spl25_6)),
% 0.48/0.38 inference(forward_demodulation,[],[f157,f90])).
% 0.48/0.38 thf(f168,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cQ @ X8))) | ($true != ((cP @ X9))) | (((cQ @ X11)) = $false)) ) | (~spl25_2 | ~spl25_6)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f167])).
% 0.48/0.38 thf(f169,plain,(
% 0.48/0.38 spl25_5 | spl25_7 | spl25_4 | ~spl25_2 | ~spl25_6),
% 0.48/0.38 inference(avatar_split_clause,[],[f168,f88,f69,f77,f92,f83])).
% 0.48/0.38 thf(f171,plain,(
% 0.48/0.38 ($false != $false) | (spl25_1 | ~spl25_5)),
% 0.48/0.38 inference(constrained_superposition,[],[f66,f84])).
% 0.48/0.38 thf(f172,plain,(
% 0.48/0.38 $false | (spl25_1 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f171])).
% 0.48/0.38 thf(f173,plain,(
% 0.48/0.38 spl25_1 | ~spl25_5),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f172])).
% 0.48/0.38 thf(f175,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = $false) | ($true = ((cP @ sK14))) | (((cQ @ X4)) = $true) | ($true = ((cQ @ (sK15 @ X4))))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f160,f84])).
% 0.48/0.38 thf(f176,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = ((cP @ sK14))) | (((cQ @ X4)) = $true) | ($true = ((cQ @ (sK15 @ X4))))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f175])).
% 0.48/0.38 thf(f177,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = $false) | ($true = ((cP @ sK14))) | ($true = ((cQ @ (sK15 @ X4))))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f176,f84])).
% 0.48/0.38 thf(f178,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = ((cP @ sK14))) | ($true = ((cQ @ (sK15 @ X4))))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f177])).
% 0.48/0.38 thf(f179,plain,(
% 0.48/0.38 ($true = $false) | ($true = ((cP @ sK14))) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f178,f84])).
% 0.48/0.38 thf(f180,plain,(
% 0.48/0.38 ($true = ((cP @ sK14))) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f179])).
% 0.48/0.38 thf(f196,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = ((cP @ X13))) | ($true = ((cP @ X16))) | ($true = ((cQ @ sK9))) | (((cP @ sK7)) = $false)) ) | ~spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f52,f71])).
% 0.48/0.38 thf(f197,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = $false) | ($true = ((cP @ X13))) | ($true = ((cP @ X16))) | (((cP @ sK7)) = $false)) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f196,f84])).
% 0.48/0.38 thf(f198,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = ((cP @ X13))) | ($true = ((cP @ X16))) | (((cP @ sK7)) = $false)) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f197])).
% 0.48/0.38 thf(f200,definition,(
% 0.48/0.38 spl25_10 <=> (((cP @ sK7)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition])).
% 0.48/0.38 thf(f202,plain,(
% 0.48/0.38 (((cP @ sK7)) = $false) | ~spl25_10),
% 0.48/0.38 inference(avatar_component_clause,[],[f200])).
% 0.48/0.38 thf(f204,definition,(
% 0.48/0.38 spl25_11 <=> ! [X16 : $i] : ($true = ((cP @ X16)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition])).
% 0.48/0.38 thf(f205,plain,(
% 0.48/0.38 ( ! [X16 : $i] : (($true = ((cP @ X16)))) ) | ~spl25_11),
% 0.48/0.38 inference(avatar_component_clause,[],[f204])).
% 0.48/0.38 thf(f206,plain,(
% 0.48/0.38 spl25_10 | spl25_11 | spl25_11 | ~spl25_2 | ~spl25_5),
% 0.48/0.38 inference(avatar_split_clause,[],[f198,f83,f69,f204,f204,f200])).
% 0.48/0.38 thf(f209,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cP @ X13)) = $false) | ($true = ((cP @ X16))) | ($true = ((cQ @ sK9))) | ($true = ((cP @ sK7)))) ) | ~spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f53,f71])).
% 0.48/0.38 thf(f210,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = $false) | (((cP @ X13)) = $false) | ($true = ((cP @ X16))) | ($true = ((cP @ sK7)))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f209,f84])).
% 0.48/0.38 thf(f211,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cP @ X13)) = $false) | ($true = ((cP @ X16))) | ($true = ((cP @ sK7)))) ) | (~spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f210])).
% 0.48/0.38 thf(f212,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : (($true = $false) | (((cP @ X13)) = $false) | ($true = ((cP @ X16)))) ) | (~spl25_2 | ~spl25_5 | ~spl25_10)),
% 0.48/0.38 inference(forward_demodulation,[],[f211,f202])).
% 0.48/0.38 thf(f213,plain,(
% 0.48/0.38 ( ! [X16 : $i,X13 : $i] : ((((cP @ X13)) = $false) | ($true = ((cP @ X16)))) ) | (~spl25_2 | ~spl25_5 | ~spl25_10)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f212])).
% 0.48/0.38 thf(f215,definition,(
% 0.48/0.38 spl25_12 <=> ! [X13 : $i] : (((cP @ X13)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition])).
% 0.48/0.38 thf(f216,plain,(
% 0.48/0.38 ( ! [X13 : $i] : ((((cP @ X13)) = $false)) ) | ~spl25_12),
% 0.48/0.38 inference(avatar_component_clause,[],[f215])).
% 0.48/0.38 thf(f217,plain,(
% 0.48/0.38 spl25_11 | spl25_12 | ~spl25_2 | ~spl25_5 | ~spl25_10),
% 0.48/0.38 inference(avatar_split_clause,[],[f213,f200,f83,f69,f215,f204])).
% 0.48/0.38 thf(f225,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cQ @ sK10))) | (((cP @ X22)) = $false) | ($true != sP0) | (((cP @ (sK12 @ X22))) = $false)) ) | ~spl25_11),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f51,f205])).
% 0.48/0.38 thf(f226,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cQ @ sK10))) | (((cP @ X22)) = $false) | (((cP @ (sK12 @ X22))) = $false)) ) | (~spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f225,f71])).
% 0.48/0.38 thf(f227,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = $false) | (((cP @ X22)) = $false) | (((cP @ (sK12 @ X22))) = $false)) ) | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(forward_demodulation,[],[f226,f84])).
% 0.48/0.38 thf(f228,plain,(
% 0.48/0.38 ( ! [X22 : $i] : ((((cP @ X22)) = $false) | (((cP @ (sK12 @ X22))) = $false)) ) | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f227])).
% 0.48/0.38 thf(f229,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = $false) | (((cP @ (sK12 @ X22))) = $false)) ) | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(forward_demodulation,[],[f228,f205])).
% 0.48/0.38 thf(f230,plain,(
% 0.48/0.38 ( ! [X22 : $i] : ((((cP @ (sK12 @ X22))) = $false)) ) | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f229])).
% 0.48/0.38 thf(f231,plain,(
% 0.48/0.38 ($true = $false) | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(forward_demodulation,[],[f230,f205])).
% 0.48/0.38 thf(f232,plain,(
% 0.48/0.38 $false | (~spl25_2 | ~spl25_5 | ~spl25_11)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f231])).
% 0.48/0.38 thf(f233,plain,(
% 0.48/0.38 ~spl25_2 | ~spl25_5 | ~spl25_11),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f232])).
% 0.48/0.38 thf(f251,plain,(
% 0.48/0.38 ($true = $false) | (~spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(constrained_superposition,[],[f216,f180])).
% 0.48/0.38 thf(f255,plain,(
% 0.48/0.38 $false | (~spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f251])).
% 0.48/0.38 thf(f256,plain,(
% 0.48/0.38 ~spl25_2 | ~spl25_5 | ~spl25_12),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f255])).
% 0.48/0.38 thf(f258,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true = $false) | ($true != ((cP @ X21))) | ($true = ((cQ @ X22))) | ($true = sP0) | ($true = ((cQ @ (sK24 @ X22))))) ) | ~spl25_5),
% 0.48/0.38 inference(forward_demodulation,[],[f32,f84])).
% 0.48/0.38 thf(f259,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true != ((cP @ X21))) | ($true = ((cQ @ X22))) | ($true = sP0) | ($true = ((cQ @ (sK24 @ X22))))) ) | ~spl25_5),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f258])).
% 0.48/0.38 thf(f284,plain,(
% 0.48/0.38 ( ! [X2 : $i,X4 : $i] : (($true = ((cP @ X2))) | ($true = ((cQ @ sK2))) | ($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) ) | spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f60,f70])).
% 0.48/0.38 thf(f285,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = $false) | ($true = ((cQ @ sK2))) | ($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f284,f216])).
% 0.48/0.38 thf(f286,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = ((cQ @ sK2))) | ($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f285])).
% 0.48/0.38 thf(f287,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = $false) | ($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f286,f84])).
% 0.48/0.38 thf(f288,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = ((cP @ X4))) | ($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f287])).
% 0.48/0.38 thf(f289,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = $false) | ($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f288,f216])).
% 0.48/0.38 thf(f290,plain,(
% 0.48/0.38 ( ! [X4 : $i] : (($true = ((cP @ (sK3 @ X4))))) ) | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f289])).
% 0.48/0.38 thf(f291,plain,(
% 0.48/0.38 ($true = $false) | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f290,f216])).
% 0.48/0.38 thf(f292,plain,(
% 0.48/0.38 $false | (spl25_2 | ~spl25_5 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f291])).
% 0.48/0.38 thf(f293,plain,(
% 0.48/0.38 spl25_2 | ~spl25_5 | ~spl25_12),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f292])).
% 0.48/0.38 thf(f299,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true != ((cP @ X21))) | ($true = ((cQ @ X22))) | ($true = ((cQ @ (sK24 @ X22))))) ) | (spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f259,f70])).
% 0.48/0.38 thf(f309,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true = $false) | ($true != ((cP @ X21))) | ($true = ((cQ @ (sK24 @ X22))))) ) | (spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f299,f84])).
% 0.48/0.38 thf(f310,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true != ((cP @ X21))) | ($true = ((cQ @ (sK24 @ X22))))) ) | (spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f309])).
% 0.48/0.38 thf(f311,plain,(
% 0.48/0.38 ( ! [X21 : $i] : (($true = $false) | ($true != ((cP @ X21)))) ) | (spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(forward_demodulation,[],[f310,f84])).
% 0.48/0.38 thf(f312,plain,(
% 0.48/0.38 ( ! [X21 : $i] : (($true != ((cP @ X21)))) ) | (spl25_2 | ~spl25_5)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f311])).
% 0.48/0.38 thf(f313,plain,(
% 0.48/0.38 spl25_7 | spl25_2 | ~spl25_5),
% 0.48/0.38 inference(avatar_split_clause,[],[f312,f83,f69,f92])).
% 0.48/0.38 thf(f314,plain,(
% 0.48/0.38 ( ! [X0 : $i] : (($true != $true) | (((cP @ X0)) = $false)) ) | ~spl25_7),
% 0.48/0.38 inference(constrained_superposition,[],[f93,f31])).
% 0.48/0.38 thf(f316,plain,(
% 0.48/0.38 ( ! [X0 : $i] : ((((cP @ X0)) = $false)) ) | ~spl25_7),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f314])).
% 0.48/0.38 thf(f317,plain,(
% 0.48/0.38 spl25_12 | ~spl25_7),
% 0.48/0.38 inference(avatar_split_clause,[],[f316,f92,f215])).
% 0.48/0.38 thf(f328,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true != ((cQ @ X21))) | ($true = ((cP @ X22))) | ($true != sP0) | ($true = ((cP @ (sK12 @ X22))))) ) | ~spl25_7),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f48,f93])).
% 0.48/0.38 thf(f336,plain,(
% 0.48/0.38 ( ! [X21 : $i,X22 : $i] : (($true != ((cQ @ X21))) | ($true != sP0) | ($true = ((cP @ (sK12 @ X22))))) ) | ~spl25_7),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f328,f93])).
% 0.48/0.38 thf(f339,plain,(
% 0.48/0.38 ( ! [X21 : $i] : (($true != ((cQ @ X21))) | ($true != sP0)) ) | ~spl25_7),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f336,f93])).
% 0.48/0.38 thf(f341,definition,(
% 0.48/0.38 spl25_13 <=> ! [X21 : $i] : ($true != ((cQ @ X21)))),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition])).
% 0.48/0.38 thf(f342,plain,(
% 0.48/0.38 ( ! [X21 : $i] : (($true != ((cQ @ X21)))) ) | ~spl25_13),
% 0.48/0.38 inference(avatar_component_clause,[],[f341])).
% 0.48/0.38 thf(f343,plain,(
% 0.48/0.38 ~spl25_2 | spl25_13 | ~spl25_7),
% 0.48/0.38 inference(avatar_split_clause,[],[f339,f92,f341,f69])).
% 0.48/0.38 thf(f344,plain,(
% 0.48/0.38 ( ! [X0 : $i] : (($true != $true) | (((cQ @ X0)) = $false)) ) | ~spl25_13),
% 0.48/0.38 inference(constrained_superposition,[],[f342,f31])).
% 0.48/0.38 thf(f346,plain,(
% 0.48/0.38 ( ! [X0 : $i] : ((((cQ @ X0)) = $false)) ) | ~spl25_13),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f344])).
% 0.48/0.38 thf(f353,plain,(
% 0.48/0.38 spl25_5 | ~spl25_13),
% 0.48/0.38 inference(avatar_split_clause,[],[f346,f341,f83])).
% 0.48/0.38 thf(f377,plain,(
% 0.48/0.38 ($true = $false) | (~spl25_3 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f75,f216])).
% 0.48/0.38 thf(f378,plain,(
% 0.48/0.38 $false | (~spl25_3 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f377])).
% 0.48/0.38 thf(f379,plain,(
% 0.48/0.38 ~spl25_3 | ~spl25_12),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f378])).
% 0.48/0.38 thf(f385,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | ($true != ((cQ @ sK23))) | (((cQ @ X22)) = $false) | (((cQ @ (sK24 @ X22))) = $false)) ) | spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f35,f70])).
% 0.48/0.38 thf(f405,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | ($true = ((cP @ X11))) | (((cP @ sK6)) = $false)) ) | spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f56,f70])).
% 0.48/0.38 thf(f406,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | (((cP @ X11)) = $false) | ($true = ((cP @ sK6)))) ) | spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f57,f70])).
% 0.48/0.38 thf(f421,definition,(
% 0.48/0.38 spl25_15 <=> (((cP @ sK6)) = $false)),
% 0.48/0.38 introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition])).
% 0.48/0.38 thf(f423,plain,(
% 0.48/0.38 (((cP @ sK6)) = $false) | ~spl25_15),
% 0.48/0.38 inference(avatar_component_clause,[],[f421])).
% 0.48/0.38 thf(f424,plain,(
% 0.48/0.38 spl25_15 | spl25_11 | spl25_13 | spl25_11 | spl25_2),
% 0.48/0.38 inference(avatar_split_clause,[],[f405,f69,f204,f341,f204,f421])).
% 0.48/0.38 thf(f427,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = $false) | ($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | (((cP @ X11)) = $false)) ) | (spl25_2 | ~spl25_15)),
% 0.48/0.38 inference(forward_demodulation,[],[f406,f423])).
% 0.48/0.38 thf(f428,plain,(
% 0.48/0.38 ( ! [X11 : $i,X8 : $i,X9 : $i] : (($true = ((cP @ X8))) | ($true != ((cQ @ X9))) | (((cP @ X11)) = $false)) ) | (spl25_2 | ~spl25_15)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f427])).
% 0.48/0.38 thf(f429,plain,(
% 0.48/0.38 spl25_12 | spl25_13 | spl25_11 | spl25_2 | ~spl25_15),
% 0.48/0.38 inference(avatar_split_clause,[],[f428,f421,f69,f204,f341,f215])).
% 0.48/0.38 thf(f458,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true != ((cP @ sK1))) | (((cQ @ X1)) != $true) | (((cP @ X4)) = $false) | (((cP @ (sK3 @ X4))) = $false)) ) | spl25_2),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f63,f70])).
% 0.48/0.38 thf(f467,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | (((cQ @ X22)) = $false) | (((cQ @ (sK24 @ X22))) = $false)) ) | (spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f385,f78])).
% 0.48/0.38 thf(f470,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = $false) | ($true = ((cP @ sK22))) | (((cQ @ (sK24 @ X22))) = $false)) ) | (spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_demodulation,[],[f467,f78])).
% 0.48/0.38 thf(f471,plain,(
% 0.48/0.38 ( ! [X22 : $i] : (($true = ((cP @ sK22))) | (((cQ @ (sK24 @ X22))) = $false)) ) | (spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f470])).
% 0.48/0.38 thf(f473,plain,(
% 0.48/0.38 ($true = $false) | ($true = ((cP @ sK22))) | (spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(forward_demodulation,[],[f471,f78])).
% 0.48/0.38 thf(f474,plain,(
% 0.48/0.38 ($true = ((cP @ sK22))) | (spl25_2 | ~spl25_4)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f473])).
% 0.48/0.38 thf(f483,plain,(
% 0.48/0.38 ($true = $false) | (spl25_2 | ~spl25_4 | ~spl25_12)),
% 0.48/0.38 inference(forward_demodulation,[],[f474,f216])).
% 0.48/0.38 thf(f484,plain,(
% 0.48/0.38 $false | (spl25_2 | ~spl25_4 | ~spl25_12)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f483])).
% 0.48/0.38 thf(f485,plain,(
% 0.48/0.38 spl25_2 | ~spl25_4 | ~spl25_12),
% 0.48/0.38 inference(avatar_contradiction_clause,[],[f484])).
% 0.48/0.38 thf(f521,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : ((((cQ @ X1)) != $true) | (((cP @ X4)) = $false) | (((cP @ (sK3 @ X4))) = $false)) ) | (spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(forward_subsumption_resolution,[],[f458,f205])).
% 0.48/0.38 thf(f522,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : (($true = $false) | (((cQ @ X1)) != $true) | (((cP @ (sK3 @ X4))) = $false)) ) | (spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(forward_demodulation,[],[f521,f205])).
% 0.48/0.38 thf(f523,plain,(
% 0.48/0.38 ( ! [X1 : $i,X4 : $i] : ((((cQ @ X1)) != $true) | (((cP @ (sK3 @ X4))) = $false)) ) | (spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f522])).
% 0.48/0.38 thf(f524,plain,(
% 0.48/0.38 ( ! [X1 : $i] : (($true = $false) | (((cQ @ X1)) != $true)) ) | (spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(forward_demodulation,[],[f523,f205])).
% 0.48/0.38 thf(f525,plain,(
% 0.48/0.38 ( ! [X1 : $i] : ((((cQ @ X1)) != $true)) ) | (spl25_2 | ~spl25_11)),
% 0.48/0.38 inference(trivial_inequality_removal,[],[f524])).
% 0.48/0.38 thf(f526,plain,(
% 0.48/0.38 spl25_13 | spl25_2 | ~spl25_11),
% 0.48/0.38 inference(avatar_split_clause,[],[f525,f204,f69,f341])).
% 0.48/0.38 cnf(s37, plain, spl25_4 | spl25_2 | spl25_3 | spl25_1 | spl25_4, inference(sat_conversion,[],[f79])).
% 0.48/0.38 cnf(s38, plain, spl25_1 | spl25_2 | spl25_3 | spl25_4, inference(rat,[],[s37])).
% 0.48/0.38 cnf(s43, plain, ~spl25_1 | spl25_2 | spl25_3 | spl25_4 | spl25_5, inference(sat_conversion,[],[f85])).
% 0.48/0.38 cnf(s48, plain, spl25_4 | ~spl25_2 | spl25_4 | spl25_6 | spl25_7, inference(sat_conversion,[],[f94])).
% 0.48/0.38 cnf(s49, plain, ~spl25_2 | spl25_4 | spl25_6 | spl25_7, inference(rat,[],[s48])).
% 0.48/0.38 cnf(s53, plain, ~spl25_1 | ~spl25_4, inference(sat_conversion,[],[f100])).
% 0.48/0.38 cnf(s56, plain, ~spl25_2 | ~spl25_4 | spl25_7, inference(sat_conversion,[],[f108])).
% 0.48/0.38 cnf(s83, plain, ~spl25_2 | spl25_4 | spl25_5 | ~spl25_6 | spl25_7, inference(sat_conversion,[],[f169])).
% 0.48/0.38 cnf(s86, plain, spl25_1 | ~spl25_5, inference(sat_conversion,[],[f173])).
% 0.48/0.38 cnf(s95, plain, spl25_11 | ~spl25_5 | spl25_10 | ~spl25_2 | spl25_11, inference(sat_conversion,[],[f206])).
% 0.48/0.38 cnf(s96, plain, ~spl25_2 | ~spl25_5 | spl25_10 | spl25_11, inference(rat,[],[s95])).
% 0.48/0.38 cnf(s101, plain, ~spl25_2 | ~spl25_5 | ~spl25_10 | spl25_11 | spl25_12, inference(sat_conversion,[],[f217])).
% 0.48/0.38 cnf(s106, plain, ~spl25_2 | ~spl25_5 | ~spl25_11, inference(sat_conversion,[],[f233])).
% 0.48/0.38 cnf(s115, plain, ~spl25_2 | ~spl25_5 | ~spl25_12, inference(sat_conversion,[],[f256])).
% 0.48/0.38 cnf(s121, plain, spl25_2 | ~spl25_5 | ~spl25_12, inference(sat_conversion,[],[f293])).
% 0.48/0.38 cnf(s127, plain, spl25_2 | ~spl25_5 | spl25_7, inference(sat_conversion,[],[f313])).
% 0.48/0.38 cnf(s132, plain, ~spl25_7 | spl25_12, inference(sat_conversion,[],[f317])).
% 0.48/0.38 cnf(s150, plain, ~spl25_2 | ~spl25_7 | spl25_13, inference(sat_conversion,[],[f343])).
% 0.48/0.38 cnf(s158, plain, spl25_5 | ~spl25_13, inference(sat_conversion,[],[f353])).
% 0.48/0.38 cnf(s171, plain, ~spl25_3 | ~spl25_12, inference(sat_conversion,[],[f379])).
% 0.48/0.38 cnf(s199, plain, spl25_11 | spl25_2 | spl25_11 | spl25_13 | spl25_15, inference(sat_conversion,[],[f424])).
% 0.48/0.38 cnf(s200, plain, spl25_2 | spl25_11 | spl25_13 | spl25_15, inference(rat,[],[s199])).
% 0.48/0.38 cnf(s205, plain, spl25_2 | spl25_11 | spl25_12 | spl25_13 | ~spl25_15, inference(sat_conversion,[],[f429])).
% 0.48/0.38 cnf(s233, plain, spl25_2 | ~spl25_4 | ~spl25_12, inference(sat_conversion,[],[f485])).
% 0.48/0.38 cnf(s281, plain, spl25_2 | ~spl25_11 | spl25_13, inference(sat_conversion,[],[f526])).
% 0.48/0.38 cnf(s282, plain, spl25_2 | spl25_1, inference(rat,[],[s38,s233,s171,s205,s200,s281,s158,s86])).
% 0.48/0.38 cnf(s283, plain, spl25_1, inference(rat,[],[s83,s49,s56,s150,s282,s158,s86])).
% 0.48/0.38 cnf(s284, plain, ~spl25_4, inference(rat,[],[s53,s283])).
% 0.48/0.38 cnf(s285, plain, ~spl25_5 | spl25_2, inference(rat,[],[s132,s121,s127])).
% 0.48/0.38 cnf(s286, plain, spl25_2, inference(rat,[],[s205,s171,s200,s281,s43,s158,s285,s283,s284])).
% 0.48/0.38 cnf(s288, plain, spl25_5, inference(rat,[],[s83,s49,s150,s158,s284,s286])).
% 0.48/0.38 cnf(s289, plain, ~spl25_12, inference(rat,[],[s115,s286,s288])).
% 0.48/0.38 cnf(s290, plain, ~spl25_11, inference(rat,[],[s106,s286,s288])).
% 0.48/0.38 cnf(s291, plain, ~spl25_10, inference(rat,[],[s101,s289,s290,s286,s288])).
% 0.48/0.38 cnf(s292, plain, $false, inference(rat,[],[s96,s290,s286,s291,s288])).
% 0.48/0.38 thf(f527,plain,(
% 0.48/0.38 $false),
% 0.48/0.38 inference(avatar_sat_refutation,[],[s292])).
% 0.48/0.38 % SZS output end Proof for theBenchmark
% 0.48/0.38 % (1481472)------------------------------
% 0.48/0.38 % (1481472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.48/0.38 % (1481472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.48/0.38 % (1481472)CaDiCaL version: 2.1.3
% 0.48/0.38 % (1481472)Termination reason: Refutation
% 0.48/0.38 % (1481472)Time elapsed: 0.021 s
% 0.48/0.38 % (1481472)Peak memory usage: 13 MB
% 0.48/0.38 % (1481472)Instructions burned: 40 (million)
% 0.48/0.38 % (1481465)Success in time 0.043 s
% 0.48/0.38 % Vampire exiting
%------------------------------------------------------------------------------