%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO052-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 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 12:25:39 PM UTC 2026
% Result : Unsatisfiable 6.71s 1.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO052-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.40 % Computer : n012.cluster.edu
% 0.10/0.40 % Model : x86_64 x86_64
% 0.10/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.40 % Memory : 8046.5625MB
% 0.10/0.40 % OS : Linux 6.8.0-71-generic
% 0.10/0.40 % CPULimit : 300
% 0.10/0.40 % WCLimit : 300
% 0.10/0.40 % DateTime : Sun Sep 20 08:45:53 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.10/0.42 % Drodi V4.1.1
% 6.71/1.38 % Refutation found
% 6.71/1.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.71/1.38 % SZS output start CNFRefutation for theBenchmark
% 6.71/1.38 fof(f45,axiom,(
% 6.71/1.38 (![U,V]: (between(U,V,V) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f47,axiom,(
% 6.71/1.38 (![U,V,W]: (( ~ between(U,V,W)| between(W,V,U) ) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f50,axiom,(
% 6.71/1.38 (![U,V,W]: (( ~ between(U,V,W)| ~ between(U,W,V)| V = W ) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f55,axiom,(
% 6.71/1.38 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(V,W,X)| between(U,W,X)| V = W ) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f78,axiom,(
% 6.71/1.38 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,V,X)| U = V| between(V,W,X)| between(V,X,W) ) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f80,axiom,(
% 6.71/1.38 (![U,V,X,W]: (( ~ between(U,V,X)| ~ between(U,W,X)| between(U,V,W)| between(U,W,V) ) ))),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f81,hypothesis,(
% 6.71/1.38 between(u,v,x) ),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f82,hypothesis,(
% 6.71/1.38 between(u,w,x) ),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f83,hypothesis,(
% 6.71/1.38 ~ between(v,w,x) ),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f84,negated_conjecture,(
% 6.71/1.38 ~ between(w,v,x) ),
% 6.71/1.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.71/1.38 fof(f138,plain,(
% 6.71/1.38 ![X0,X1]: (between(X0,X1,X1))),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f45])).
% 6.71/1.38 fof(f141,plain,(
% 6.71/1.38 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X2,X1,X0))),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f47])).
% 6.71/1.38 fof(f145,plain,(
% 6.71/1.38 ![V,W]: ((![U]: (~between(U,V,W)|~between(U,W,V)))|V=W)),
% 6.71/1.38 inference(miniscoping,[status(thm)],[f50])).
% 6.71/1.38 fof(f146,plain,(
% 6.71/1.38 ![X0,X1,X2]: (~between(X0,X1,X2)|~between(X0,X2,X1)|X1=X2)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f145])).
% 6.71/1.38 fof(f155,plain,(
% 6.71/1.38 ![V,W]: ((![U,X]: ((~between(U,V,W)|~between(V,W,X))|between(U,W,X)))|V=W)),
% 6.71/1.38 inference(miniscoping,[status(thm)],[f55])).
% 6.71/1.38 fof(f156,plain,(
% 6.71/1.38 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X1,X2,X3)|between(X0,X2,X3)|X1=X2)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f155])).
% 6.71/1.38 fof(f191,plain,(
% 6.71/1.38 ![V,W,X]: (((![U]: ((~between(U,V,W)|~between(U,V,X))|U=V))|between(V,W,X))|between(V,X,W))),
% 6.71/1.38 inference(miniscoping,[status(thm)],[f78])).
% 6.71/1.38 fof(f192,plain,(
% 6.71/1.38 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|X0=X1|between(X1,X2,X3)|between(X1,X3,X2))),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f191])).
% 6.71/1.38 fof(f195,plain,(
% 6.71/1.38 ![U,V,W]: (((![X]: (~between(U,V,X)|~between(U,W,X)))|between(U,V,W))|between(U,W,V))),
% 6.71/1.38 inference(miniscoping,[status(thm)],[f80])).
% 6.71/1.38 fof(f196,plain,(
% 6.71/1.38 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X3,X2)|between(X0,X1,X3)|between(X0,X3,X1))),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f195])).
% 6.71/1.38 fof(f197,plain,(
% 6.71/1.38 between(u,v,x)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f81])).
% 6.71/1.38 fof(f198,plain,(
% 6.71/1.38 between(u,w,x)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f82])).
% 6.71/1.38 fof(f199,plain,(
% 6.71/1.38 ~between(v,w,x)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f83])).
% 6.71/1.38 fof(f200,plain,(
% 6.71/1.38 ~between(w,v,x)),
% 6.71/1.38 inference(cnf_transformation,[status(thm)],[f84])).
% 6.71/1.38 fof(f383,plain,(
% 6.71/1.38 ![X0]: (~between(u,X0,x)|between(u,v,X0)|between(u,X0,v))),
% 6.71/1.38 inference(resolution,[status(thm)],[f197,f196])).
% 6.71/1.38 fof(f387,plain,(
% 6.71/1.38 ![X0]: (~between(u,v,X0)|u=v|between(v,x,X0)|between(v,X0,x))),
% 6.71/1.38 inference(resolution,[status(thm)],[f197,f192])).
% 6.71/1.38 fof(f395,plain,(
% 6.71/1.38 ![X0]: (~between(v,x,X0)|between(u,x,X0)|v=x)),
% 6.71/1.38 inference(resolution,[status(thm)],[f197,f156])).
% 6.71/1.38 fof(f397,plain,(
% 6.71/1.38 ~between(u,x,v)|v=x),
% 6.71/1.38 inference(resolution,[status(thm)],[f197,f146])).
% 6.71/1.38 fof(f399,plain,(
% 6.71/1.38 between(x,v,u)),
% 6.71/1.38 inference(resolution,[status(thm)],[f197,f141])).
% 6.71/1.38 fof(f403,definition,(
% 6.71/1.38 sQ1_spl <=> (u=v)),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f404,plain,(
% 6.71/1.38 u=v|~sQ1_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f403])).
% 6.71/1.38 fof(f414,definition,(
% 6.71/1.38 sQ4_spl <=> (v=x)),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f415,plain,(
% 6.71/1.38 v=x|~sQ4_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f414])).
% 6.71/1.38 fof(f418,definition,(
% 6.71/1.38 ![X0]: (sQ5_spl <=> (~between(u,v,X0)|between(v,x,X0)|between(v,X0,x)))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f419,plain,(
% 6.71/1.38 ![X0]: (~between(u,v,X0)|between(v,x,X0)|between(v,X0,x)|~sQ5_spl)),
% 6.71/1.38 inference(component_clause,[status(thm)],[f418])).
% 6.71/1.38 fof(f421,plain,(
% 6.71/1.38 sQ5_spl|sQ1_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f387,f418,f403])).
% 6.71/1.38 fof(f430,definition,(
% 6.71/1.38 ![X0]: (sQ8_spl <=> (~between(v,x,X0)|between(u,x,X0)))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f431,plain,(
% 6.71/1.38 ![X0]: (~between(v,x,X0)|between(u,x,X0)|~sQ8_spl)),
% 6.71/1.38 inference(component_clause,[status(thm)],[f430])).
% 6.71/1.38 fof(f433,plain,(
% 6.71/1.38 sQ8_spl|sQ4_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f395,f430,f414])).
% 6.71/1.38 fof(f434,definition,(
% 6.71/1.38 sQ9_spl <=> (between(u,x,v))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f436,plain,(
% 6.71/1.38 ~between(u,x,v)|sQ9_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f434])).
% 6.71/1.38 fof(f437,plain,(
% 6.71/1.38 ~sQ9_spl|sQ4_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f397,f434,f414])).
% 6.71/1.38 fof(f468,plain,(
% 6.71/1.38 ~between(w,v,v)|~sQ4_spl),
% 6.71/1.38 inference(backward_demodulation,[status(thm)],[f415,f200])).
% 6.71/1.38 fof(f469,plain,(
% 6.71/1.38 $false|~sQ4_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f468,f138])).
% 6.71/1.38 fof(f470,plain,(
% 6.71/1.38 ~sQ4_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f469])).
% 6.71/1.38 fof(f497,plain,(
% 6.71/1.38 ~between(u,w,x)|~sQ1_spl),
% 6.71/1.38 inference(backward_demodulation,[status(thm)],[f404,f199])).
% 6.71/1.38 fof(f505,plain,(
% 6.71/1.38 ![X0]: (~between(u,w,X0)|u=w|between(w,x,X0)|between(w,X0,x))),
% 6.71/1.38 inference(resolution,[status(thm)],[f198,f192])).
% 6.71/1.38 fof(f513,plain,(
% 6.71/1.38 ![X0]: (~between(w,x,X0)|between(u,x,X0)|w=x)),
% 6.71/1.38 inference(resolution,[status(thm)],[f198,f156])).
% 6.71/1.38 fof(f515,plain,(
% 6.71/1.38 ~between(u,x,w)|w=x),
% 6.71/1.38 inference(resolution,[status(thm)],[f198,f146])).
% 6.71/1.38 fof(f521,definition,(
% 6.71/1.38 sQ13_spl <=> (u=w)),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f522,plain,(
% 6.71/1.38 u=w|~sQ13_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f521])).
% 6.71/1.38 fof(f536,definition,(
% 6.71/1.38 sQ17_spl <=> (w=x)),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f537,plain,(
% 6.71/1.38 w=x|~sQ17_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f536])).
% 6.71/1.38 fof(f540,definition,(
% 6.71/1.38 ![X0]: (sQ18_spl <=> (~between(u,w,X0)|between(w,x,X0)|between(w,X0,x)))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f541,plain,(
% 6.71/1.38 ![X0]: (~between(u,w,X0)|between(w,x,X0)|between(w,X0,x)|~sQ18_spl)),
% 6.71/1.38 inference(component_clause,[status(thm)],[f540])).
% 6.71/1.38 fof(f543,plain,(
% 6.71/1.38 sQ18_spl|sQ13_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f505,f540,f521])).
% 6.71/1.38 fof(f552,definition,(
% 6.71/1.38 ![X0]: (sQ21_spl <=> (~between(w,x,X0)|between(u,x,X0)))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f553,plain,(
% 6.71/1.38 ![X0]: (~between(w,x,X0)|between(u,x,X0)|~sQ21_spl)),
% 6.71/1.38 inference(component_clause,[status(thm)],[f552])).
% 6.71/1.38 fof(f555,plain,(
% 6.71/1.38 sQ21_spl|sQ17_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f513,f552,f536])).
% 6.71/1.38 fof(f556,definition,(
% 6.71/1.38 sQ22_spl <=> (between(u,x,w))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f558,plain,(
% 6.71/1.38 ~between(u,x,w)|sQ22_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f556])).
% 6.71/1.38 fof(f559,plain,(
% 6.71/1.38 ~sQ22_spl|sQ17_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f515,f556,f536])).
% 6.71/1.38 fof(f611,plain,(
% 6.71/1.38 $false|~sQ1_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f497,f198])).
% 6.71/1.38 fof(f612,plain,(
% 6.71/1.38 ~sQ1_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f611])).
% 6.71/1.38 fof(f614,plain,(
% 6.71/1.38 ~between(v,x,x)|~sQ17_spl),
% 6.71/1.38 inference(forward_demodulation,[status(thm)],[f537,f199])).
% 6.71/1.38 fof(f615,plain,(
% 6.71/1.38 $false|~sQ17_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f614,f138])).
% 6.71/1.38 fof(f616,plain,(
% 6.71/1.38 ~sQ17_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f615])).
% 6.71/1.38 fof(f617,plain,(
% 6.71/1.38 ~between(u,v,x)|~sQ13_spl),
% 6.71/1.38 inference(backward_demodulation,[status(thm)],[f522,f200])).
% 6.71/1.38 fof(f649,plain,(
% 6.71/1.38 between(u,v,x)),
% 6.71/1.38 inference(resolution,[status(thm)],[f399,f141])).
% 6.71/1.38 fof(f690,plain,(
% 6.71/1.38 $false|~sQ13_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f649,f617])).
% 6.71/1.38 fof(f691,plain,(
% 6.71/1.38 ~sQ13_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f690])).
% 6.71/1.38 fof(f1964,plain,(
% 6.71/1.38 between(u,v,w)|between(u,w,v)),
% 6.71/1.38 inference(resolution,[status(thm)],[f383,f198])).
% 6.71/1.38 fof(f1975,definition,(
% 6.71/1.38 sQ85_spl <=> (between(u,v,w))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f1976,plain,(
% 6.71/1.38 between(u,v,w)|~sQ85_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f1975])).
% 6.71/1.38 fof(f1978,definition,(
% 6.71/1.38 sQ86_spl <=> (between(u,w,v))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f1979,plain,(
% 6.71/1.38 between(u,w,v)|~sQ86_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f1978])).
% 6.71/1.38 fof(f1981,plain,(
% 6.71/1.38 sQ85_spl|sQ86_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f1964,f1975,f1978])).
% 6.71/1.38 fof(f3759,plain,(
% 6.71/1.38 between(w,x,v)|between(w,v,x)|~sQ18_spl|~sQ86_spl),
% 6.71/1.38 inference(resolution,[status(thm)],[f541,f1979])).
% 6.71/1.38 fof(f3766,definition,(
% 6.71/1.38 sQ200_spl <=> (between(w,x,v))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f3767,plain,(
% 6.71/1.38 between(w,x,v)|~sQ200_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f3766])).
% 6.71/1.38 fof(f3769,definition,(
% 6.71/1.38 sQ201_spl <=> (between(w,v,x))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f3770,plain,(
% 6.71/1.38 between(w,v,x)|~sQ201_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f3769])).
% 6.71/1.38 fof(f3772,plain,(
% 6.71/1.38 sQ200_spl|sQ201_spl|~sQ18_spl|~sQ86_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f3759,f3766,f3769,f540,f1978])).
% 6.71/1.38 fof(f3842,plain,(
% 6.71/1.38 between(u,x,v)|~sQ200_spl|~sQ21_spl),
% 6.71/1.38 inference(resolution,[status(thm)],[f3767,f553])).
% 6.71/1.38 fof(f3888,plain,(
% 6.71/1.38 $false|sQ9_spl|~sQ200_spl|~sQ21_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f3842,f436])).
% 6.71/1.38 fof(f3889,plain,(
% 6.71/1.38 sQ9_spl|~sQ200_spl|~sQ21_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f3888])).
% 6.71/1.38 fof(f3956,plain,(
% 6.71/1.38 between(v,x,w)|between(v,w,x)|~sQ85_spl|~sQ5_spl),
% 6.71/1.38 inference(resolution,[status(thm)],[f1976,f419])).
% 6.71/1.38 fof(f4002,definition,(
% 6.71/1.38 sQ209_spl <=> (between(v,x,w))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f4003,plain,(
% 6.71/1.38 between(v,x,w)|~sQ209_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f4002])).
% 6.71/1.38 fof(f4005,definition,(
% 6.71/1.38 sQ210_spl <=> (between(v,w,x))),
% 6.71/1.38 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 6.71/1.38 fof(f4006,plain,(
% 6.71/1.38 between(v,w,x)|~sQ210_spl),
% 6.71/1.38 inference(component_clause,[status(thm)],[f4005])).
% 6.71/1.38 fof(f4008,plain,(
% 6.71/1.38 sQ209_spl|sQ210_spl|~sQ85_spl|~sQ5_spl),
% 6.71/1.38 inference(split_clause,[status(thm)],[f3956,f4002,f4005,f1975,f418])).
% 6.71/1.38 fof(f4138,plain,(
% 6.71/1.38 between(u,x,w)|~sQ209_spl|~sQ8_spl),
% 6.71/1.38 inference(resolution,[status(thm)],[f4003,f431])).
% 6.71/1.38 fof(f4184,plain,(
% 6.71/1.38 $false|sQ22_spl|~sQ209_spl|~sQ8_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f4138,f558])).
% 6.71/1.38 fof(f4185,plain,(
% 6.71/1.38 sQ22_spl|~sQ209_spl|~sQ8_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f4184])).
% 6.71/1.38 fof(f4186,plain,(
% 6.71/1.38 $false|~sQ210_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f4006,f199])).
% 6.71/1.38 fof(f4187,plain,(
% 6.71/1.38 ~sQ210_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f4186])).
% 6.71/1.38 fof(f4188,plain,(
% 6.71/1.38 $false|~sQ201_spl),
% 6.71/1.38 inference(forward_subsumption_resolution,[status(thm)],[f3770,f200])).
% 6.71/1.38 fof(f4189,plain,(
% 6.71/1.38 ~sQ201_spl),
% 6.71/1.38 inference(contradiction_clause,[status(thm)],[f4188])).
% 6.71/1.38 fof(f4190,plain,(
% 6.71/1.38 $false),
% 6.71/1.38 inference(sat_refutation,[status(thm)],[f421,f433,f437,f470,f543,f555,f559,f612,f616,f691,f1981,f3772,f3889,f4008,f4185,f4187,f4189])).
% 6.71/1.38 % SZS output end CNFRefutation for theBenchmark.p
% 6.71/1.39 % Elapsed time: 0.974177 seconds
% 6.71/1.39 % CPU time: 7.436569 seconds
% 6.71/1.39 % Total memory used: 141.287 MB
% 6.71/1.39 % Net memory used: 134.971 MB
%------------------------------------------------------------------------------