%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW298+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 : n019.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:56 PM UTC 2026
% Result : Theorem 0.91s 1.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW298+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.35 % Computer : n019.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:46:20 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.81/1.13 % Drodi V4.1.1
% 0.91/1.24 % Refutation found
% 0.91/1.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.91/1.24 % SZS output start CNFRefutation for theBenchmark
% 0.91/1.24 fof(f2,axiom,(
% 0.91/1.24 (! [V_t,V_n,T_a] :( c_Hoare__Mirabelle_Otriple__valid(T_a,hAPP(c_Nat_OSuc,V_n),V_t)=> c_Hoare__Mirabelle_Otriple__valid(T_a,V_n,V_t) ) )),
% 0.91/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.91/1.24 fof(f2445,axiom,(
% 0.91/1.24 (! [V_A_2,V_x_2,T_b] :( hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))<=> hBOOL(hAPP(V_A_2,V_x_2)) ) )),
% 0.91/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.91/1.24 fof(f5224,hypothesis,(
% 0.91/1.24 (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))=> c_Hoare__Mirabelle_Otriple__valid(t_a,hAPP(c_Nat_OSuc,v_n),B_x) ) )),
% 0.91/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.91/1.24 fof(f5225,conjecture,(
% 0.91/1.24 (! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,B_x) ) )),
% 0.91/1.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.91/1.24 fof(f5226,negated_conjecture,(
% 0.91/1.24 ~((! [B_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))=> c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,B_x) ) ))),
% 0.91/1.24 inference(negated_conjecture,[status(cth)],[f5225])).
% 0.91/1.24 fof(f5230,plain,(
% 0.91/1.24 ![V_t,V_n,T_a]: (~c_Hoare__Mirabelle_Otriple__valid(T_a,hAPP(c_Nat_OSuc,V_n),V_t)|c_Hoare__Mirabelle_Otriple__valid(T_a,V_n,V_t))),
% 0.91/1.24 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.91/1.24 fof(f5231,plain,(
% 0.91/1.24 ![X0,X1,X2]: (~c_Hoare__Mirabelle_Otriple__valid(X0,hAPP(c_Nat_OSuc,X1),X2)|c_Hoare__Mirabelle_Otriple__valid(X0,X1,X2))),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f5230])).
% 0.91/1.24 fof(f12747,plain,(
% 0.91/1.24 ![V_A_2,V_x_2,T_b]: ((~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))|hBOOL(hAPP(V_A_2,V_x_2)))&(hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 0.91/1.24 inference(NNF_transformation,[status(thm)],[f2445])).
% 0.91/1.24 fof(f12748,plain,(
% 0.91/1.24 (![V_A_2,V_x_2]: ((![T_b]: ~hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2)))|hBOOL(hAPP(V_A_2,V_x_2))))&(![V_A_2,V_x_2]: ((![T_b]: hBOOL(hAPP(hAPP(c_member(T_b),V_x_2),V_A_2)))|~hBOOL(hAPP(V_A_2,V_x_2))))),
% 0.91/1.24 inference(miniscoping,[status(thm)],[f12747])).
% 0.91/1.24 fof(f12749,plain,(
% 0.91/1.24 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hBOOL(hAPP(X2,X1)))),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f12748])).
% 0.91/1.24 fof(f12750,plain,(
% 0.91/1.24 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|~hBOOL(hAPP(X2,X1)))),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f12748])).
% 0.91/1.24 fof(f20179,plain,(
% 0.91/1.24 ![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))|c_Hoare__Mirabelle_Otriple__valid(t_a,hAPP(c_Nat_OSuc,v_n),B_x))),
% 0.91/1.24 inference(pre_NNF_transformation,[status(thm)],[f5224])).
% 0.91/1.24 fof(f20180,plain,(
% 0.91/1.24 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_ts))|c_Hoare__Mirabelle_Otriple__valid(t_a,hAPP(c_Nat_OSuc,v_n),X0))),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f20179])).
% 0.91/1.24 fof(f20181,plain,(
% 0.91/1.24 (?[B_x]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))&~c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,B_x)))),
% 0.91/1.24 inference(pre_NNF_transformation,[status(thm)],[f5226])).
% 0.91/1.24 fof(f20182,plain,(
% 0.91/1.24 (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK557_skl),v_ts))&~c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,sK557_skl))),
% 0.91/1.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK557_skl]),skolemize(B_x,sK557_skl)],[f20181])).
% 0.91/1.24 fof(f20183,plain,(
% 0.91/1.24 hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK557_skl),v_ts))),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f20182])).
% 0.91/1.24 fof(f20184,plain,(
% 0.91/1.24 ~c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,sK557_skl)),
% 0.91/1.24 inference(cnf_transformation,[status(thm)],[f20182])).
% 0.91/1.24 fof(f21018,plain,(
% 0.91/1.24 hBOOL(hAPP(v_ts,sK557_skl))),
% 0.91/1.24 inference(resolution,[status(thm)],[f12749,f20183])).
% 0.91/1.24 fof(f21019,plain,(
% 0.91/1.24 ![X0]: (hBOOL(hAPP(hAPP(c_member(X0),sK557_skl),v_ts)))),
% 0.91/1.24 inference(resolution,[status(thm)],[f12750,f21018])).
% 0.91/1.24 fof(f21027,plain,(
% 0.91/1.24 c_Hoare__Mirabelle_Otriple__valid(t_a,hAPP(c_Nat_OSuc,v_n),sK557_skl)),
% 0.91/1.24 inference(resolution,[status(thm)],[f20180,f21019])).
% 0.91/1.24 fof(f21028,plain,(
% 0.91/1.24 c_Hoare__Mirabelle_Otriple__valid(t_a,v_n,sK557_skl)),
% 0.94/1.33 inference(resolution,[status(thm)],[f21027,f5231])).
% 0.94/1.33 fof(f21029,plain,(
% 0.94/1.33 $false),
% 0.94/1.33 inference(forward_subsumption_resolution,[status(thm)],[f21028,f20184])).
% 0.94/1.33 % SZS output end CNFRefutation for theBenchmark.p
% 0.94/1.38 % Elapsed time: 1.006168 seconds
% 0.94/1.38 % CPU time: 1.879229 seconds
% 0.94/1.38 % Total memory used: 646.262 MB
% 0.94/1.38 % Net memory used: 640.682 MB
%------------------------------------------------------------------------------