%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 02:50:41 PM UTC 2026
% Result : Theorem 0.07s 0.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 08:44:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.07/0.33 % Refutation found
% 0.07/0.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.07/0.33 % SZS output start CNFRefutation for theBenchmark
% 0.07/0.33 fof(f42,axiom,(
% 0.07/0.33 ( (! [U,V,W,X,Y,Z] :( succ_cpq(triple(U,V,W),triple(X,Y,Z))=> ( ( ~ check_cpq(triple(X,Y,Z))| ~ ok(triple(X,Y,Z)) )=> ( ~ check_cpq(im_succ_cpq(triple(X,Y,Z)))| ~ ok(im_succ_cpq(triple(X,Y,Z))) ) ) ))=> (! [X1,X2,X3] :( ( ~ check_cpq(triple(X1,X2,X3))| ~ ok(triple(X1,X2,X3)) )=> (! [X4,X5,X6] :( succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))=> ( ~ ok(triple(X4,X5,X6))| ~ check_cpq(triple(X4,X5,X6)) ) ) )) )) ),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f43,lemma,(
% 0.07/0.33 (! [U,V,W] :( ( ~ check_cpq(triple(U,V,W))| ~ ok(triple(U,V,W)) )=> ( ~ check_cpq(im_succ_cpq(triple(U,V,W)))| ~ ok(im_succ_cpq(triple(U,V,W))) ) ) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f44,conjecture,(
% 0.07/0.33 (! [U,V,W] :( ( ~ check_cpq(triple(U,V,W))| ~ ok(triple(U,V,W)) )=> (! [X,Y,Z] :( succ_cpq(triple(U,V,W),triple(X,Y,Z))=> ( ~ ok(triple(X,Y,Z))| ~ check_cpq(triple(X,Y,Z)) ) ) )) )),
% 0.07/0.33 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.07/0.33 fof(f45,negated_conjecture,(
% 0.07/0.33 ~((! [U,V,W] :( ( ~ check_cpq(triple(U,V,W))| ~ ok(triple(U,V,W)) )=> (! [X,Y,Z] :( succ_cpq(triple(U,V,W),triple(X,Y,Z))=> ( ~ ok(triple(X,Y,Z))| ~ check_cpq(triple(X,Y,Z)) ) ) )) ))),
% 0.07/0.33 inference(negated_conjecture,[status(cth)],[f44])).
% 0.07/0.33 fof(f146,plain,(
% 0.07/0.33 (?[U,V,W,X,Y,Z]: (succ_cpq(triple(U,V,W),triple(X,Y,Z))&((~check_cpq(triple(X,Y,Z))|~ok(triple(X,Y,Z)))&(check_cpq(im_succ_cpq(triple(X,Y,Z)))&ok(im_succ_cpq(triple(X,Y,Z)))))))|(![X1,X2,X3]: ((check_cpq(triple(X1,X2,X3))&ok(triple(X1,X2,X3)))|(![X4,X5,X6]: (~succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))|(~ok(triple(X4,X5,X6))|~check_cpq(triple(X4,X5,X6)))))))),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 0.07/0.33 fof(f147,definition,(
% 0.07/0.33 ![U,V,W,X,Y,Z]: (sP0_prd(Z,Y,X,W,V,U)<=>(succ_cpq(triple(U,V,W),triple(X,Y,Z))&((~check_cpq(triple(X,Y,Z))|~ok(triple(X,Y,Z)))&(check_cpq(im_succ_cpq(triple(X,Y,Z)))&ok(im_succ_cpq(triple(X,Y,Z)))))))),
% 0.07/0.33 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.07/0.33 fof(f148,plain,(
% 0.07/0.33 (?[U,V,W,X,Y,Z]: sP0_prd(Z,Y,X,W,V,U))|(![X1,X2,X3]: ((check_cpq(triple(X1,X2,X3))&ok(triple(X1,X2,X3)))|(![X4,X5,X6]: (~succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))|(~ok(triple(X4,X5,X6))|~check_cpq(triple(X4,X5,X6)))))))),
% 0.07/0.33 inference(formula_renaming,[status(thm)],[f146,f147])).
% 0.07/0.33 fof(f149,plain,(
% 0.07/0.33 sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|(![X1,X2,X3]: ((check_cpq(triple(X1,X2,X3))&ok(triple(X1,X2,X3)))|(![X4,X5,X6]: (~succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))|(~ok(triple(X4,X5,X6))|~check_cpq(triple(X4,X5,X6)))))))),
% 0.07/0.33 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl),skolemize(W,sK2_skl),skolemize(X,sK3_skl),skolemize(Y,sK4_skl),skolemize(Z,sK5_skl)],[f148])).
% 0.07/0.33 fof(f150,plain,(
% 0.07/0.33 ![X0,X1,X2,X3,X4,X5]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|check_cpq(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(X3,X4,X5))|~ok(triple(X3,X4,X5))|~check_cpq(triple(X3,X4,X5)))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f149])).
% 0.07/0.33 fof(f151,plain,(
% 0.07/0.33 ![X0,X1,X2,X3,X4,X5]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|ok(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(X3,X4,X5))|~ok(triple(X3,X4,X5))|~check_cpq(triple(X3,X4,X5)))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f149])).
% 0.07/0.33 fof(f152,plain,(
% 0.07/0.33 ![U,V,W]: ((check_cpq(triple(U,V,W))&ok(triple(U,V,W)))|(~check_cpq(im_succ_cpq(triple(U,V,W)))|~ok(im_succ_cpq(triple(U,V,W)))))),
% 0.07/0.33 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 0.07/0.33 fof(f153,plain,(
% 0.07/0.33 ![X0,X1,X2]: (check_cpq(triple(X0,X1,X2))|~check_cpq(im_succ_cpq(triple(X0,X1,X2)))|~ok(im_succ_cpq(triple(X0,X1,X2))))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f152])).
% 0.07/0.33 fof(f154,plain,(
% 0.07/0.33 ![X0,X1,X2]: (ok(triple(X0,X1,X2))|~check_cpq(im_succ_cpq(triple(X0,X1,X2)))|~ok(im_succ_cpq(triple(X0,X1,X2))))),
% 0.07/0.33 inference(cnf_transformation,[status(thm)],[f152])).
% 0.07/0.33 fof(f155,plain,(
% 0.07/0.33 (?[U,V,W]: ((~check_cpq(triple(U,V,W))|~ok(triple(U,V,W)))&(?[X,Y,Z]: (succ_cpq(triple(U,V,W),triple(X,Y,Z))&(ok(triple(X,Y,Z))&check_cpq(triple(X,Y,Z)))))))),
% 0.07/0.34 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 0.07/0.34 fof(f156,plain,(
% 0.07/0.34 ((~check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|~ok(triple(sK6_skl,sK7_skl,sK8_skl)))&(succ_cpq(triple(sK6_skl,sK7_skl,sK8_skl),triple(sK9_skl,sK10_skl,sK11_skl))&(ok(triple(sK9_skl,sK10_skl,sK11_skl))&check_cpq(triple(sK9_skl,sK10_skl,sK11_skl)))))),
% 0.07/0.34 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl]),skolemize(U,sK6_skl),skolemize(V,sK7_skl),skolemize(W,sK8_skl),skolemize(X,sK9_skl),skolemize(Y,sK10_skl),skolemize(Z,sK11_skl)],[f155])).
% 0.07/0.34 fof(f157,plain,(
% 0.07/0.34 ~check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|~ok(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f156])).
% 0.07/0.34 fof(f158,plain,(
% 0.07/0.34 succ_cpq(triple(sK6_skl,sK7_skl,sK8_skl),triple(sK9_skl,sK10_skl,sK11_skl))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f156])).
% 0.07/0.34 fof(f159,plain,(
% 0.07/0.34 ok(triple(sK9_skl,sK10_skl,sK11_skl))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f156])).
% 0.07/0.34 fof(f160,plain,(
% 0.07/0.34 check_cpq(triple(sK9_skl,sK10_skl,sK11_skl))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f156])).
% 0.07/0.34 fof(f161,plain,(
% 0.07/0.34 ![U,V,W,X,Y,Z]: ((~sP0_prd(Z,Y,X,W,V,U)|(succ_cpq(triple(U,V,W),triple(X,Y,Z))&((~check_cpq(triple(X,Y,Z))|~ok(triple(X,Y,Z)))&(check_cpq(im_succ_cpq(triple(X,Y,Z)))&ok(im_succ_cpq(triple(X,Y,Z)))))))&(sP0_prd(Z,Y,X,W,V,U)|(~succ_cpq(triple(U,V,W),triple(X,Y,Z))|((check_cpq(triple(X,Y,Z))&ok(triple(X,Y,Z)))|(~check_cpq(im_succ_cpq(triple(X,Y,Z)))|~ok(im_succ_cpq(triple(X,Y,Z))))))))),
% 0.07/0.34 inference(NNF_transformation,[status(thm)],[f147])).
% 0.07/0.34 fof(f162,plain,(
% 0.07/0.34 (![U,V,W,X,Y,Z]: (~sP0_prd(Z,Y,X,W,V,U)|(succ_cpq(triple(U,V,W),triple(X,Y,Z))&((~check_cpq(triple(X,Y,Z))|~ok(triple(X,Y,Z)))&(check_cpq(im_succ_cpq(triple(X,Y,Z)))&ok(im_succ_cpq(triple(X,Y,Z))))))))&(![U,V,W,X,Y,Z]: (sP0_prd(Z,Y,X,W,V,U)|(~succ_cpq(triple(U,V,W),triple(X,Y,Z))|((check_cpq(triple(X,Y,Z))&ok(triple(X,Y,Z)))|(~check_cpq(im_succ_cpq(triple(X,Y,Z)))|~ok(im_succ_cpq(triple(X,Y,Z))))))))),
% 0.07/0.34 inference(miniscoping,[status(thm)],[f161])).
% 0.07/0.34 fof(f164,plain,(
% 0.07/0.34 ![X0,X1,X2,X3,X4,X5]: (~sP0_prd(X0,X1,X2,X3,X4,X5)|~check_cpq(triple(X2,X1,X0))|~ok(triple(X2,X1,X0)))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f162])).
% 0.07/0.34 fof(f165,plain,(
% 0.07/0.34 ![X0,X1,X2,X3,X4,X5]: (~sP0_prd(X0,X1,X2,X3,X4,X5)|check_cpq(im_succ_cpq(triple(X2,X1,X0))))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f162])).
% 0.07/0.34 fof(f166,plain,(
% 0.07/0.34 ![X0,X1,X2,X3,X4,X5]: (~sP0_prd(X0,X1,X2,X3,X4,X5)|ok(im_succ_cpq(triple(X2,X1,X0))))),
% 0.07/0.34 inference(cnf_transformation,[status(thm)],[f162])).
% 0.07/0.34 fof(f259,plain,(
% 0.07/0.34 ![X0,X1,X2]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|check_cpq(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(sK9_skl,sK10_skl,sK11_skl))|~check_cpq(triple(sK9_skl,sK10_skl,sK11_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f150,f159])).
% 0.07/0.34 fof(f262,plain,(
% 0.07/0.34 ![X0,X1,X2]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|check_cpq(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(sK9_skl,sK10_skl,sK11_skl)))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f259,f160])).
% 0.07/0.34 fof(f265,plain,(
% 0.07/0.34 sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f262,f158])).
% 0.07/0.34 fof(f287,plain,(
% 0.07/0.34 ![X0,X1,X2]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|ok(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(sK9_skl,sK10_skl,sK11_skl))|~check_cpq(triple(sK9_skl,sK10_skl,sK11_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f151,f159])).
% 0.07/0.34 fof(f290,plain,(
% 0.07/0.34 ![X0,X1,X2]: (sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|ok(triple(X0,X1,X2))|~succ_cpq(triple(X0,X1,X2),triple(sK9_skl,sK10_skl,sK11_skl)))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f287,f160])).
% 0.07/0.34 fof(f300,plain,(
% 0.07/0.34 ~check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))|~ok(triple(sK3_skl,sK4_skl,sK5_skl))|check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f164,f265])).
% 0.07/0.34 fof(f301,plain,(
% 0.07/0.34 check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))|check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f165,f265])).
% 0.07/0.34 fof(f302,plain,(
% 0.07/0.34 sP0_prd(sK5_skl,sK4_skl,sK3_skl,sK2_skl,sK1_skl,sK0_skl)|ok(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f290,f158])).
% 0.07/0.34 fof(f308,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f302,f165])).
% 0.07/0.34 fof(f309,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|~check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))|~ok(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f302,f164])).
% 0.07/0.34 fof(f319,plain,(
% 0.07/0.34 ok(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))|ok(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f166,f302])).
% 0.07/0.34 fof(f320,plain,(
% 0.07/0.34 ok(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))|check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(resolution,[status(thm)],[f166,f265])).
% 0.07/0.34 fof(f330,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|ok(triple(sK3_skl,sK4_skl,sK5_skl))|~check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f319,f154])).
% 0.07/0.34 fof(f331,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))|~check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f319,f153])).
% 0.07/0.34 fof(f332,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|ok(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f330,f308])).
% 0.07/0.34 fof(f333,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f331,f308])).
% 0.07/0.34 fof(f334,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))|~check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(backward_subsumption_resolution,[status(thm)],[f309,f332])).
% 0.07/0.34 fof(f347,plain,(
% 0.07/0.34 check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|ok(triple(sK3_skl,sK4_skl,sK5_skl))|~check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f320,f154])).
% 0.07/0.34 fof(f348,plain,(
% 0.07/0.34 check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))|~check_cpq(im_succ_cpq(triple(sK3_skl,sK4_skl,sK5_skl)))),
% 0.07/0.34 inference(resolution,[status(thm)],[f320,f153])).
% 0.07/0.34 fof(f349,plain,(
% 0.07/0.34 check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|ok(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f347,f301])).
% 0.07/0.34 fof(f350,plain,(
% 0.07/0.34 check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))|check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f348,f301])).
% 0.07/0.34 fof(f351,plain,(
% 0.07/0.34 ~check_cpq(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(backward_subsumption_resolution,[status(thm)],[f157,f352])).
% 0.07/0.34 fof(f352,plain,(
% 0.07/0.34 ok(triple(sK6_skl,sK7_skl,sK8_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f334,f333])).
% 0.07/0.34 fof(f358,plain,(
% 0.07/0.34 ~check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))|~ok(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(backward_subsumption_resolution,[status(thm)],[f300,f351])).
% 0.07/0.34 fof(f383,plain,(
% 0.07/0.34 ~check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(backward_subsumption_resolution,[status(thm)],[f358,f384])).
% 0.07/0.34 fof(f384,plain,(
% 0.07/0.34 ok(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f349,f351])).
% 0.07/0.34 fof(f466,plain,(
% 0.07/0.34 check_cpq(triple(sK3_skl,sK4_skl,sK5_skl))),
% 0.07/0.34 inference(forward_subsumption_resolution,[status(thm)],[f350,f351])).
% 0.07/0.34 fof(f467,plain,(
% 0.07/0.34 $false),
% 0.07/0.34 inference(backward_subsumption_resolution,[status(thm)],[f383,f466])).
% 0.07/0.34 % SZS output end CNFRefutation for theBenchmark.p
% 0.07/0.35 % Elapsed time: 0.050824 seconds
% 0.07/0.35 % CPU time: 0.173570 seconds
% 0.07/0.35 % Total memory used: 107.412 MB
% 0.07/0.35 % Net memory used: 107.128 MB
%------------------------------------------------------------------------------