%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW328+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Thu Sep 24 03:08:59 PM UTC 2026
% Result : Theorem 254.24s 33.28s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW328+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Mon Sep 21 09:47:34 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.79/1.05 % Drodi V4.1.1
% 254.24/33.28 % Refutation found
% 254.24/33.28 % SZS status Theorem for theBenchmark: Theorem is valid
% 254.24/33.28 % SZS output start CNFRefutation for theBenchmark
% 254.24/33.28 fof(f5205,hypothesis,(
% 254.24/33.28 (! [B_n] :( (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))=> c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,B_x) ))=> (! [B_Z,B_s] :( ( v_P(B_Z,B_s)& hBOOL(hAPP(v_b,B_s)) )=> (! [B_s_H] :( c_Natural_Oevaln(v_c,B_s,B_n,B_s_H)=> v_P(B_Z,B_s_H) ) )) )) )),
% 254.24/33.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 254.24/33.28 fof(f5206,hypothesis,(
% 254.24/33.28 hBOOL(hAPP(v_ba,v_s0)) ),
% 254.24/33.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 254.24/33.28 fof(f5207,hypothesis,(
% 254.24/33.28 c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1) ),
% 254.24/33.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 254.24/33.28 fof(f5210,hypothesis,(
% 254.24/33.28 ( c_Com_Ocom_OWhile(v_ba,v_ca) = c_Com_Ocom_OWhile(v_b,v_c)=> ( (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x) ))=> (! [B_Z] :( v_P(B_Z,v_s1)=> ( v_P(B_Z,v_s2)& ~ hBOOL(hAPP(v_b,v_s2)) ) ) )) ) ),
% 254.24/33.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 254.24/33.28 fof(f5211,conjecture,(
% 254.24/33.28 ( ( v_ba = v_b& v_ca = v_c )=> ( (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x) ))=> (! [B_Z] :( v_P(B_Z,v_s0)=> ( v_P(B_Z,v_s2)& ~ hBOOL(hAPP(v_b,v_s2)) ) ) )) ) ),
% 254.24/33.28 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 254.24/33.28 fof(f5212,negated_conjecture,(
% 254.24/33.28 ~(( ( v_ba = v_b& v_ca = v_c )=> ( (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x) ))=> (! [B_Z] :( v_P(B_Z,v_s0)=> ( v_P(B_Z,v_s2)& ~ hBOOL(hAPP(v_b,v_s2)) ) ) )) ) )),
% 254.24/33.28 inference(negated_conjecture,[status(cth)],[f5211])).
% 254.24/33.28 fof(f19789,plain,(
% 254.24/33.28 ![B_n]: ((?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))&~c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,B_x)))|(![B_Z,B_s]: ((~v_P(B_Z,B_s)|~hBOOL(hAPP(v_b,B_s)))|(![B_s_H]: (~c_Natural_Oevaln(v_c,B_s,B_n,B_s_H)|v_P(B_Z,B_s_H))))))),
% 254.24/33.28 inference(pre_NNF_transformation,[status(thm)],[f5205])).
% 254.24/33.28 fof(f19790,plain,(
% 254.24/33.28 ![B_n]: ((hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(B_n)),v_G))&~c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,sK496_skl(B_n)))|(![B_Z,B_s]: ((~v_P(B_Z,B_s)|~hBOOL(hAPP(v_b,B_s)))|(![B_s_H]: (~c_Natural_Oevaln(v_c,B_s,B_n,B_s_H)|v_P(B_Z,B_s_H))))))),
% 254.24/33.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK496_skl]),skolemize(B_x,sK496_skl(B_n))],[f19789])).
% 254.24/33.28 fof(f19791,plain,(
% 254.24/33.28 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(X0)),v_G))|~v_P(X1,X2)|~hBOOL(hAPP(v_b,X2))|~c_Natural_Oevaln(v_c,X2,X0,X3)|v_P(X1,X3))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19790])).
% 254.24/33.28 fof(f19792,plain,(
% 254.24/33.28 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK496_skl(X0))|~v_P(X1,X2)|~hBOOL(hAPP(v_b,X2))|~c_Natural_Oevaln(v_c,X2,X0,X3)|v_P(X1,X3))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19790])).
% 254.24/33.28 fof(f19793,plain,(
% 254.24/33.28 hBOOL(hAPP(v_ba,v_s0))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f5206])).
% 254.24/33.28 fof(f19794,plain,(
% 254.24/33.28 c_Natural_Oevaln(v_ca,v_s0,v_na,v_s1)),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f5207])).
% 254.24/33.28 fof(f19802,plain,(
% 254.24/33.28 ~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_b,v_c)|((?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))&~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x)))|(![B_Z]: (~v_P(B_Z,v_s1)|(v_P(B_Z,v_s2)&~hBOOL(hAPP(v_b,v_s2))))))),
% 254.24/33.28 inference(pre_NNF_transformation,[status(thm)],[f5210])).
% 254.24/33.28 fof(f19803,definition,(
% 254.24/33.28 ![B_Z]: (sP42_prd(B_Z)<=>(v_P(B_Z,v_s2)&~hBOOL(hAPP(v_b,v_s2))))),
% 254.24/33.28 introduced(definition,[new_symbols(definition,[sP42_prd])],[])).
% 254.24/33.28 fof(f19804,plain,(
% 254.24/33.28 ~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_b,v_c)|((?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))&~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x)))|(![B_Z]: (~v_P(B_Z,v_s1)|sP42_prd(B_Z))))),
% 254.24/33.28 inference(formula_renaming,[status(thm)],[f19802,f19803])).
% 254.24/33.28 fof(f19805,plain,(
% 254.24/33.28 ~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_b,v_c)|((hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))&~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl))|(![B_Z]: (~v_P(B_Z,v_s1)|sP42_prd(B_Z))))),
% 254.24/33.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK498_skl]),skolemize(B_x,sK498_skl)],[f19804])).
% 254.24/33.28 fof(f19806,plain,(
% 254.24/33.28 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_b,v_c)|hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))|~v_P(X0,v_s1)|sP42_prd(X0))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19805])).
% 254.24/33.28 fof(f19807,plain,(
% 254.24/33.28 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_b,v_c)|~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl)|~v_P(X0,v_s1)|sP42_prd(X0))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19805])).
% 254.24/33.28 fof(f19808,plain,(
% 254.24/33.28 ((v_ba=v_b&v_ca=v_c)&((![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))|c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x)))&(?[B_Z]: (v_P(B_Z,v_s0)&(~v_P(B_Z,v_s2)|hBOOL(hAPP(v_b,v_s2)))))))),
% 254.24/33.28 inference(pre_NNF_transformation,[status(thm)],[f5212])).
% 254.24/33.28 fof(f19809,plain,(
% 254.24/33.28 (v_ba=v_b&v_ca=v_c)&((![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))|c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,B_x)))&(v_P(sK499_skl,v_s0)&(~v_P(sK499_skl,v_s2)|hBOOL(hAPP(v_b,v_s2)))))),
% 254.24/33.28 inference(skolemize,[status(esa),new_symbols(skolem,[sK499_skl]),skolemize(B_Z,sK499_skl)],[f19808])).
% 254.24/33.28 fof(f19810,plain,(
% 254.24/33.28 v_ba=v_b),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19809])).
% 254.24/33.28 fof(f19811,plain,(
% 254.24/33.28 v_ca=v_c),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19809])).
% 254.24/33.28 fof(f19812,plain,(
% 254.24/33.28 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))|c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,X0))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19809])).
% 254.24/33.28 fof(f19813,plain,(
% 254.24/33.28 v_P(sK499_skl,v_s0)),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19809])).
% 254.24/33.28 fof(f19814,plain,(
% 254.24/33.28 ~v_P(sK499_skl,v_s2)|hBOOL(hAPP(v_b,v_s2))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f19809])).
% 254.24/33.28 fof(f20089,plain,(
% 254.24/33.28 ![B_Z]: ((~sP42_prd(B_Z)|(v_P(B_Z,v_s2)&~hBOOL(hAPP(v_b,v_s2))))&(sP42_prd(B_Z)|(~v_P(B_Z,v_s2)|hBOOL(hAPP(v_b,v_s2)))))),
% 254.24/33.28 inference(NNF_transformation,[status(thm)],[f19803])).
% 254.24/33.28 fof(f20090,plain,(
% 254.24/33.28 (![B_Z]: (~sP42_prd(B_Z)|(v_P(B_Z,v_s2)&~hBOOL(hAPP(v_b,v_s2)))))&(![B_Z]: (sP42_prd(B_Z)|(~v_P(B_Z,v_s2)|hBOOL(hAPP(v_b,v_s2)))))),
% 254.24/33.28 inference(miniscoping,[status(thm)],[f20089])).
% 254.24/33.28 fof(f20091,plain,(
% 254.24/33.28 ![X0]: (~sP42_prd(X0)|v_P(X0,v_s2))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f20090])).
% 254.24/33.28 fof(f20092,plain,(
% 254.24/33.28 ![X0]: (~sP42_prd(X0)|~hBOOL(hAPP(v_b,v_s2)))),
% 254.24/33.28 inference(cnf_transformation,[status(thm)],[f20090])).
% 254.24/33.28 fof(f23776,plain,(
% 254.24/33.28 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_ba,v_c)|~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl)|~v_P(X0,v_s1)|sP42_prd(X0))),
% 254.24/33.28 inference(backward_demodulation,[status(thm)],[f19810,f19807])).
% 254.24/33.28 fof(f23777,plain,(
% 254.24/33.28 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_ba,v_c)|hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))|~v_P(X0,v_s1)|sP42_prd(X0))),
% 254.24/33.28 inference(backward_demodulation,[status(thm)],[f19810,f19806])).
% 254.24/33.28 fof(f23780,plain,(
% 254.24/33.28 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK496_skl(X0))|~v_P(X1,X2)|~hBOOL(hAPP(v_ba,X2))|~c_Natural_Oevaln(v_c,X2,X0,X3)|v_P(X1,X3))),
% 254.24/33.28 inference(backward_demodulation,[status(thm)],[f19810,f19792])).
% 254.24/33.28 fof(f23781,plain,(
% 254.24/33.28 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(X0)),v_G))|~v_P(X1,X2)|~hBOOL(hAPP(v_ba,X2))|~c_Natural_Oevaln(v_c,X2,X0,X3)|v_P(X1,X3))),
% 254.24/33.28 inference(backward_demodulation,[status(thm)],[f19810,f19791])).
% 254.24/33.28 fof(f23782,plain,(
% 254.24/33.28 ~v_P(sK499_skl,v_s2)|hBOOL(hAPP(v_ba,v_s2))),
% 254.24/33.28 inference(forward_demodulation,[status(thm)],[f19810,f19814])).
% 254.24/33.28 fof(f23861,plain,(
% 254.24/33.28 ![X0]: (~sP42_prd(X0)|~hBOOL(hAPP(v_ba,v_s2)))),
% 254.24/33.28 inference(forward_demodulation,[status(thm)],[f19810,f20092])).
% 254.24/33.28 fof(f24761,plain,(
% 254.24/33.28 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_ba,v_ca)|~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl)|~v_P(X0,v_s1)|sP42_prd(X0))),
% 122.63/33.65 inference(forward_demodulation,[status(thm)],[f19811,f23776])).
% 122.63/33.65 fof(f24762,plain,(
% 122.63/33.65 ![X0]: (~c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl)|~v_P(X0,v_s1)|sP42_prd(X0))),
% 122.63/33.65 inference(trivial_equality_resolution,[status(thm)],[f24761])).
% 122.63/33.65 fof(f24763,plain,(
% 122.63/33.65 ![X0]: (~c_Com_Ocom_OWhile(v_ba,v_ca)=c_Com_Ocom_OWhile(v_ba,v_ca)|hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))|~v_P(X0,v_s1)|sP42_prd(X0))),
% 122.63/33.65 inference(forward_demodulation,[status(thm)],[f19811,f23777])).
% 122.63/33.65 fof(f24764,plain,(
% 122.63/33.65 ![X0]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))|~v_P(X0,v_s1)|sP42_prd(X0))),
% 122.63/33.65 inference(trivial_equality_resolution,[status(thm)],[f24763])).
% 122.63/33.65 fof(f24767,plain,(
% 122.63/33.65 ![X0,X1,X2,X3]: (~c_Hoare__Mirabelle_Otriple__valid(t_a,X0,sK496_skl(X0))|~v_P(X1,X2)|~hBOOL(hAPP(v_ba,X2))|~c_Natural_Oevaln(v_ca,X2,X0,X3)|v_P(X1,X3))),
% 122.63/33.65 inference(forward_demodulation,[status(thm)],[f19811,f23780])).
% 122.63/33.65 fof(f24768,plain,(
% 122.63/33.65 ![X0,X1,X2,X3]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(X0)),v_G))|~v_P(X1,X2)|~hBOOL(hAPP(v_ba,X2))|~c_Natural_Oevaln(v_ca,X2,X0,X3)|v_P(X1,X3))),
% 122.63/33.65 inference(forward_demodulation,[status(thm)],[f19811,f23781])).
% 122.63/33.65 fof(f25100,plain,(
% 122.63/33.65 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(X0)),v_G))|~v_P(X1,v_s0)|~c_Natural_Oevaln(v_ca,v_s0,X0,X2)|v_P(X1,X2))),
% 122.63/33.65 inference(resolution,[status(thm)],[f24768,f19793])).
% 122.63/33.65 fof(f25111,plain,(
% 122.63/33.65 ![X0,X1]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(X0)),v_G))|~c_Natural_Oevaln(v_ca,v_s0,X0,X1)|v_P(sK499_skl,X1))),
% 122.63/33.65 inference(resolution,[status(thm)],[f25100,f19813])).
% 122.63/33.65 fof(f25112,plain,(
% 122.63/33.65 hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK496_skl(v_na)),v_G))|v_P(sK499_skl,v_s1)),
% 122.63/33.65 inference(resolution,[status(thm)],[f25111,f19794])).
% 122.63/33.65 fof(f25113,plain,(
% 122.63/33.65 v_P(sK499_skl,v_s1)|c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK496_skl(v_na))),
% 122.63/33.65 inference(resolution,[status(thm)],[f25112,f19812])).
% 122.63/33.65 fof(f25128,plain,(
% 122.63/33.65 ![X0,X1,X2]: (v_P(sK499_skl,v_s1)|~v_P(X0,X1)|~hBOOL(hAPP(v_ba,X1))|~c_Natural_Oevaln(v_ca,X1,v_na,X2)|v_P(X0,X2))),
% 122.63/33.65 inference(resolution,[status(thm)],[f25113,f24767])).
% 122.63/33.65 fof(f25159,plain,(
% 122.63/33.65 ![X0]: (v_P(sK499_skl,v_s1)|~hBOOL(hAPP(v_ba,v_s0))|~c_Natural_Oevaln(v_ca,v_s0,v_na,X0)|v_P(sK499_skl,X0))),
% 122.63/33.65 inference(resolution,[status(thm)],[f25128,f19813])).
% 122.63/33.65 fof(f25160,plain,(
% 122.63/33.65 ![X0]: (v_P(sK499_skl,v_s1)|~c_Natural_Oevaln(v_ca,v_s0,v_na,X0)|v_P(sK499_skl,X0))),
% 122.63/33.65 inference(forward_subsumption_resolution,[status(thm)],[f25159,f19793])).
% 122.63/33.65 fof(f25161,plain,(
% 122.63/33.65 v_P(sK499_skl,v_s1)|v_P(sK499_skl,v_s1)),
% 122.63/33.65 inference(resolution,[status(thm)],[f25160,f19794])).
% 122.63/33.65 fof(f25163,plain,(
% 122.63/33.65 v_P(sK499_skl,v_s1)),
% 122.63/33.65 inference(duplicate_literals_removal,[status(thm)],[f25161])).
% 122.63/33.65 fof(f25164,plain,(
% 122.63/33.65 hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK498_skl),v_G))|sP42_prd(sK499_skl)),
% 122.63/33.65 inference(resolution,[status(thm)],[f25163,f24764])).
% 122.63/33.65 fof(f25175,plain,(
% 122.63/33.65 sP42_prd(sK499_skl)|c_Hoare__Mirabelle_Otriple__valid(t_a,v_na,sK498_skl)),
% 122.63/33.65 inference(resolution,[status(thm)],[f25164,f19812])).
% 122.63/33.65 fof(f25182,plain,(
% 122.63/33.65 ![X0]: (sP42_prd(sK499_skl)|~v_P(X0,v_s1)|sP42_prd(X0))),
% 122.63/33.65 inference(resolution,[status(thm)],[f25175,f24762])).
% 122.63/33.65 fof(f25184,plain,(
% 122.63/33.65 sP42_prd(sK499_skl)|sP42_prd(sK499_skl)),
% 122.63/33.65 inference(resolution,[status(thm)],[f25182,f25163])).
% 122.63/33.65 fof(f25185,plain,(
% 122.63/33.65 sP42_prd(sK499_skl)),
% 122.63/33.65 inference(duplicate_literals_removal,[status(thm)],[f25184])).
% 122.63/33.65 fof(f27466,plain,(
% 122.63/33.65 v_P(sK499_skl,v_s2)),
% 122.63/33.65 inference(resolution,[status(thm)],[f20091,f25185])).
% 122.63/33.65 fof(f27467,plain,(
% 122.63/33.65 hBOOL(hAPP(v_ba,v_s2))),
% 122.63/33.65 inference(backward_subsumption_resolution,[status(thm)],[f23782,f27466])).
% 122.63/33.65 fof(f27468,plain,(
% 122.63/33.65 ![X0]: (~sP42_prd(X0))),
% 122.63/33.65 inference(backward_subsumption_resolution,[status(thm)],[f23861,f27467])).
% 122.63/33.65 fof(f27472,plain,(
% 122.63/33.65 $false),
% 122.63/33.65 inference(backward_subsumption_resolution,[status(thm)],[f25185,f27468])).
% 122.63/33.65 % SZS output end CNFRefutation for theBenchmark.p
% 161.26/33.82 % Elapsed time: 33.406109 seconds
% 161.26/33.82 % CPU time: 258.296391 seconds
% 161.26/33.82 % Total memory used: 2.080 GB
% 161.26/33.82 % Net memory used: 1.945 GB
%------------------------------------------------------------------------------