%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW337+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:59 PM UTC 2026
% Result : Theorem 1.32s 1.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW337+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n019.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 09:48:05 UTC 2026
% 0.17/0.44 % CPUTime :
% 1.26/1.52 % Drodi V4.1.1
% 1.32/1.64 % Refutation found
% 1.32/1.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.32/1.64 % SZS output start CNFRefutation for theBenchmark
% 1.32/1.64 fof(f639,axiom,(
% 1.32/1.64 (! [V_c_2,V_B_2,V_A_2,T_b] :( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))=> ( hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_A_2))=> hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_B_2)) ) ) )),
% 1.32/1.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/1.64 fof(f666,axiom,(
% 1.32/1.64 (! [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)) ) )),
% 1.32/1.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/1.64 fof(f5225,hypothesis,(
% 1.32/1.64 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),v_ts),v_G)) ),
% 1.32/1.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/1.64 fof(f5226,conjecture,(
% 1.32/1.64 (! [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_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))=> c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,B_x) ) )) )),
% 1.32/1.64 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.32/1.64 fof(f5227,negated_conjecture,(
% 1.32/1.64 ~((! [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_x] :( hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))=> c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,B_x) ) )) ))),
% 1.32/1.64 inference(negated_conjecture,[status(cth)],[f5226])).
% 1.32/1.64 fof(f7125,plain,(
% 1.32/1.64 ![V_c_2,V_B_2,V_A_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|(~hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_A_2))|hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_B_2))))),
% 1.32/1.64 inference(pre_NNF_transformation,[status(thm)],[f639])).
% 1.32/1.64 fof(f7126,plain,(
% 1.32/1.64 ![V_B_2,V_A_2,T_b]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|(![V_c_2]: (~hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_A_2))|hBOOL(hAPP(hAPP(c_member(T_b),V_c_2),V_B_2)))))),
% 1.32/1.64 inference(miniscoping,[status(thm)],[f7125])).
% 1.32/1.64 fof(f7127,plain,(
% 1.32/1.64 ![X0,X1,X2,X3]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X2))|~hBOOL(hAPP(hAPP(c_member(X0),X3),X1))|hBOOL(hAPP(hAPP(c_member(X0),X3),X2)))),
% 1.32/1.64 inference(cnf_transformation,[status(thm)],[f7126])).
% 1.32/1.64 fof(f7198,plain,(
% 1.32/1.64 ![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))))),
% 1.32/1.64 inference(NNF_transformation,[status(thm)],[f666])).
% 1.32/1.64 fof(f7199,plain,(
% 1.32/1.64 (![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))))),
% 1.32/1.64 inference(miniscoping,[status(thm)],[f7198])).
% 1.32/1.64 fof(f7200,plain,(
% 1.32/1.64 ![X0,X1,X2]: (~hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|hBOOL(hAPP(X2,X1)))),
% 1.32/1.64 inference(cnf_transformation,[status(thm)],[f7199])).
% 1.32/1.64 fof(f7201,plain,(
% 1.32/1.64 ![X0,X1,X2]: (hBOOL(hAPP(hAPP(c_member(X0),X1),X2))|~hBOOL(hAPP(X2,X1)))),
% 1.32/1.64 inference(cnf_transformation,[status(thm)],[f7199])).
% 1.32/1.64 fof(f20136,plain,(
% 1.32/1.64 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_HOL_Obool)),v_ts),v_G))),
% 1.32/1.64 inference(cnf_transformation,[status(thm)],[f5225])).
% 1.32/1.64 fof(f20137,plain,(
% 1.32/1.64 (?[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_x]: (hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_ts))&~c_Hoare__Mirabelle_Otriple__valid(t_a,B_n,B_x)))))),
% 1.32/1.64 inference(pre_NNF_transformation,[status(thm)],[f5227])).
% 1.32/1.64 fof(f20138,plain,(
% 1.32/1.64 ((![B_x]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),B_x),v_G))|c_Hoare__Mirabelle_Otriple__valid(t_a,sK579_skl,B_x)))&(hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK580_skl),v_ts))&~c_Hoare__Mirabelle_Otriple__valid(t_a,sK579_skl,sK580_skl)))),
% 1.32/1.64 inference(skolemize,[status(esa),new_symbols(skolem,[sK579_skl,sK580_skl]),skolemize(B_n,sK579_skl),skolemize(B_x,sK580_skl)],[f20137])).
% 1.33/1.71 fof(f20139,plain,(
% 1.33/1.71 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G))|c_Hoare__Mirabelle_Otriple__valid(t_a,sK579_skl,X0))),
% 1.33/1.71 inference(cnf_transformation,[status(thm)],[f20138])).
% 1.33/1.71 fof(f20140,plain,(
% 1.33/1.71 hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK580_skl),v_ts))),
% 1.33/1.71 inference(cnf_transformation,[status(thm)],[f20138])).
% 1.33/1.71 fof(f20141,plain,(
% 1.33/1.71 ~c_Hoare__Mirabelle_Otriple__valid(t_a,sK579_skl,sK580_skl)),
% 1.33/1.71 inference(cnf_transformation,[status(thm)],[f20138])).
% 1.33/1.71 fof(f20948,plain,(
% 1.33/1.71 hBOOL(hAPP(v_ts,sK580_skl))),
% 1.33/1.71 inference(resolution,[status(thm)],[f7200,f20140])).
% 1.33/1.71 fof(f20952,plain,(
% 1.33/1.71 ![X0]: (hBOOL(hAPP(hAPP(c_member(X0),sK580_skl),v_ts)))),
% 1.33/1.71 inference(resolution,[status(thm)],[f20948,f7201])).
% 1.33/1.71 fof(f20960,plain,(
% 1.33/1.71 ![X0]: (~hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_ts))|hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_G)))),
% 1.33/1.71 inference(resolution,[status(thm)],[f20136,f7127])).
% 1.33/1.71 fof(f20962,plain,(
% 1.33/1.71 hBOOL(hAPP(hAPP(c_member(tc_Hoare__Mirabelle_Otriple(t_a)),sK580_skl),v_G))),
% 1.33/1.71 inference(resolution,[status(thm)],[f20960,f20952])).
% 1.33/1.71 fof(f20968,plain,(
% 1.33/1.71 c_Hoare__Mirabelle_Otriple__valid(t_a,sK579_skl,sK580_skl)),
% 1.33/1.71 inference(resolution,[status(thm)],[f20962,f20139])).
% 1.33/1.71 fof(f20972,plain,(
% 1.33/1.71 $false),
% 1.33/1.71 inference(forward_subsumption_resolution,[status(thm)],[f20968,f20141])).
% 1.33/1.71 % SZS output end CNFRefutation for theBenchmark.p
% 1.33/1.89 % Elapsed time: 1.415471 seconds
% 1.33/1.89 % CPU time: 2.142378 seconds
% 1.33/1.89 % Total memory used: 456.387 MB
% 1.33/1.89 % Net memory used: 452.541 MB
%------------------------------------------------------------------------------