%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO068-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 : n013.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:41 PM UTC 2026
% Result : Unsatisfiable 12.56s 2.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO068-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.09/0.37 % Computer : n013.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 09:32:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 12.56/2.05 % Refutation found
% 12.56/2.05 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 12.56/2.05 % SZS output start CNFRefutation for theBenchmark
% 12.56/2.05 fof(f19,axiom,(
% 12.56/2.05 (![X,Y,Z]: (( ~ between(X,Y,Z)| colinear(X,Y,Z) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f20,axiom,(
% 12.56/2.05 (![Y,Z,X]: (( ~ between(Y,Z,X)| colinear(X,Y,Z) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f21,axiom,(
% 12.56/2.05 (![Z,X,Y]: (( ~ between(Z,X,Y)| colinear(X,Y,Z) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f22,axiom,(
% 12.56/2.05 (![X,Y,Z]: (( ~ colinear(X,Y,Z)| between(X,Y,Z)| between(Y,Z,X)| between(Z,X,Y) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f29,axiom,(
% 12.56/2.05 (![U,V,W,X]: (( ~ equidistant(U,V,W,X)| equidistant(V,U,X,W) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f41,axiom,(
% 12.56/2.05 (![U,V]: (equidistant(U,U,V,V) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f42,axiom,(
% 12.56/2.05 (![U,V,U1,V1,W,W1]: (( ~ equidistant(U,V,U1,V1)| ~ equidistant(V,W,V1,W1)| ~ between(U,V,W)| ~ between(U1,V1,W1)| equidistant(U,W,U1,W1) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f49,axiom,(
% 12.56/2.05 (![U,V]: (between(U,V,V) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f80,axiom,(
% 12.56/2.05 (![U,V,U1,V1,W,W1]: (( ~ equidistant(U,V,U1,V1)| ~ equidistant(V,W,V1,W1)| ~ equidistant(U,W,U1,W1)| ~ between(U,V,W)| between(U1,V1,W1) ) ))),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f101,hypothesis,(
% 12.56/2.05 equidistant(u,v,u1,v1) ),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f102,hypothesis,(
% 12.56/2.05 equidistant(v,w,v1,w1) ),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f103,hypothesis,(
% 12.56/2.05 equidistant(u,w,u1,w1) ),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f104,hypothesis,(
% 12.56/2.05 colinear(u,v,w) ),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f105,negated_conjecture,(
% 12.56/2.05 ~ colinear(u1,v1,w1) ),
% 12.56/2.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.56/2.05 fof(f128,plain,(
% 12.56/2.05 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X0,X1,X2))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f19])).
% 12.56/2.05 fof(f129,plain,(
% 12.56/2.05 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X2,X0,X1))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f20])).
% 12.56/2.05 fof(f130,plain,(
% 12.56/2.05 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X1,X2,X0))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f21])).
% 12.56/2.05 fof(f131,plain,(
% 12.56/2.05 ![X0,X1,X2]: (~colinear(X0,X1,X2)|between(X0,X1,X2)|between(X1,X2,X0)|between(X2,X0,X1))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f22])).
% 12.56/2.05 fof(f138,plain,(
% 12.56/2.05 ![X0,X1,X2,X3]: (~equidistant(X0,X1,X2,X3)|equidistant(X1,X0,X3,X2))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f29])).
% 12.56/2.05 fof(f152,plain,(
% 12.56/2.05 ![X0,X1]: (equidistant(X0,X0,X1,X1))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f41])).
% 12.56/2.05 fof(f153,plain,(
% 12.56/2.05 ![U,U1,W,W1]: ((![V1]: ((![V]: ((~equidistant(U,V,U1,V1)|~equidistant(V,W,V1,W1))|~between(U,V,W)))|~between(U1,V1,W1)))|equidistant(U,W,U1,W1))),
% 12.56/2.05 inference(miniscoping,[status(thm)],[f42])).
% 12.56/2.05 fof(f154,plain,(
% 12.56/2.05 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X5)|~between(X0,X1,X4)|~between(X2,X3,X5)|equidistant(X0,X4,X2,X5))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f153])).
% 12.56/2.05 fof(f163,plain,(
% 12.56/2.05 ![X0,X1]: (between(X0,X1,X1))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f49])).
% 12.56/2.05 fof(f212,plain,(
% 12.56/2.05 ![U1,V1,W1]: ((![U,V,W]: (((~equidistant(U,V,U1,V1)|~equidistant(V,W,V1,W1))|~equidistant(U,W,U1,W1))|~between(U,V,W)))|between(U1,V1,W1))),
% 12.56/2.05 inference(miniscoping,[status(thm)],[f80])).
% 12.56/2.05 fof(f213,plain,(
% 12.56/2.05 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X5)|~equidistant(X0,X4,X2,X5)|~between(X0,X1,X4)|between(X2,X3,X5))),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f212])).
% 12.56/2.05 fof(f242,plain,(
% 12.56/2.05 equidistant(u,v,u1,v1)),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f101])).
% 12.56/2.05 fof(f243,plain,(
% 12.56/2.05 equidistant(v,w,v1,w1)),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f102])).
% 12.56/2.05 fof(f244,plain,(
% 12.56/2.05 equidistant(u,w,u1,w1)),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f103])).
% 12.56/2.05 fof(f245,plain,(
% 12.56/2.05 colinear(u,v,w)),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f104])).
% 12.56/2.05 fof(f246,plain,(
% 12.56/2.05 ~colinear(u1,v1,w1)),
% 12.56/2.05 inference(cnf_transformation,[status(thm)],[f105])).
% 12.56/2.05 fof(f424,definition,(
% 12.56/2.05 sQ7_spl <=> (between(u,v,w))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f427,definition,(
% 12.56/2.05 sQ8_spl <=> (between(u1,v1,w1))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f428,plain,(
% 12.56/2.05 between(u1,v1,w1)|~sQ8_spl),
% 12.56/2.05 inference(component_clause,[status(thm)],[f427])).
% 12.56/2.05 fof(f434,definition,(
% 12.56/2.05 sQ10_spl <=> (between(u,v,v))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f436,plain,(
% 12.56/2.05 ~between(u,v,v)|sQ10_spl),
% 12.56/2.05 inference(component_clause,[status(thm)],[f434])).
% 12.56/2.05 fof(f437,definition,(
% 12.56/2.05 sQ11_spl <=> (between(u1,v1,v1))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f439,plain,(
% 12.56/2.05 ~between(u1,v1,v1)|sQ11_spl),
% 12.56/2.05 inference(component_clause,[status(thm)],[f437])).
% 12.56/2.05 fof(f451,plain,(
% 12.56/2.05 $false|sQ11_spl),
% 12.56/2.05 inference(forward_subsumption_resolution,[status(thm)],[f439,f163])).
% 12.56/2.05 fof(f452,plain,(
% 12.56/2.05 sQ11_spl),
% 12.56/2.05 inference(contradiction_clause,[status(thm)],[f451])).
% 12.56/2.05 fof(f453,plain,(
% 12.56/2.05 $false|sQ10_spl),
% 12.56/2.05 inference(forward_subsumption_resolution,[status(thm)],[f436,f163])).
% 12.56/2.05 fof(f454,plain,(
% 12.56/2.05 sQ10_spl),
% 12.56/2.05 inference(contradiction_clause,[status(thm)],[f453])).
% 12.56/2.05 fof(f603,definition,(
% 12.56/2.05 sQ20_spl <=> (between(u,w,w))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f605,plain,(
% 12.56/2.05 ~between(u,w,w)|sQ20_spl),
% 12.56/2.05 inference(component_clause,[status(thm)],[f603])).
% 12.56/2.05 fof(f678,definition,(
% 12.56/2.05 sQ26_spl <=> (between(u1,w1,w1))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f680,plain,(
% 12.56/2.05 ~between(u1,w1,w1)|sQ26_spl),
% 12.56/2.05 inference(component_clause,[status(thm)],[f678])).
% 12.56/2.05 fof(f689,plain,(
% 12.56/2.05 $false|sQ20_spl),
% 12.56/2.05 inference(forward_subsumption_resolution,[status(thm)],[f605,f163])).
% 12.56/2.05 fof(f690,plain,(
% 12.56/2.05 sQ20_spl),
% 12.56/2.05 inference(contradiction_clause,[status(thm)],[f689])).
% 12.56/2.05 fof(f810,plain,(
% 12.56/2.05 $false|sQ26_spl),
% 12.56/2.05 inference(forward_subsumption_resolution,[status(thm)],[f680,f163])).
% 12.56/2.05 fof(f811,plain,(
% 12.56/2.05 sQ26_spl),
% 12.56/2.05 inference(contradiction_clause,[status(thm)],[f810])).
% 12.56/2.05 fof(f817,plain,(
% 12.56/2.05 equidistant(w,u,w1,u1)),
% 12.56/2.05 inference(resolution,[status(thm)],[f244,f138])).
% 12.56/2.05 fof(f860,plain,(
% 12.56/2.05 ![X0,X1]: (~equidistant(v,X0,v1,X1)|~between(u,v,X0)|~between(u1,v1,X1)|equidistant(u,X0,u1,X1))),
% 12.56/2.05 inference(resolution,[status(thm)],[f242,f154])).
% 12.56/2.05 fof(f865,plain,(
% 12.56/2.05 equidistant(v,u,v1,u1)),
% 12.56/2.05 inference(resolution,[status(thm)],[f242,f138])).
% 12.56/2.05 fof(f990,plain,(
% 12.56/2.05 equidistant(w,v,w1,v1)),
% 12.56/2.05 inference(resolution,[status(thm)],[f243,f138])).
% 12.56/2.05 fof(f998,plain,(
% 12.56/2.05 ![X0,X1]: (~equidistant(w,X0,w1,X1)|~between(u,w,X0)|~between(u1,w1,X1)|equidistant(u,X0,u1,X1))),
% 12.56/2.05 inference(resolution,[status(thm)],[f244,f154])).
% 12.56/2.05 fof(f1003,plain,(
% 12.56/2.05 equidistant(w,u,w1,u1)),
% 12.56/2.05 inference(resolution,[status(thm)],[f244,f138])).
% 12.56/2.05 fof(f1015,plain,(
% 12.56/2.05 between(u,v,w)|between(v,w,u)|between(w,u,v)),
% 12.56/2.05 inference(resolution,[status(thm)],[f245,f131])).
% 12.56/2.05 fof(f1016,definition,(
% 12.56/2.05 sQ41_spl <=> (between(v,w,u))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f1019,definition,(
% 12.56/2.05 sQ42_spl <=> (between(w,u,v))),
% 12.56/2.05 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 12.56/2.05 fof(f1022,plain,(
% 12.56/2.05 sQ7_spl|sQ41_spl|sQ42_spl),
% 12.56/2.05 inference(split_clause,[status(thm)],[f1015,f424,f1016,f1019])).
% 12.56/2.05 fof(f1703,plain,(
% 12.56/2.05 ![X0,X1]: (~equidistant(w,X0,w1,X1)|~equidistant(v,X0,v1,X1)|~between(v,w,X0)|between(v1,w1,X1))),
% 12.56/2.05 inference(resolution,[status(thm)],[f213,f243])).
% 12.56/2.05 fof(f1705,plain,(
% 12.56/2.05 ![X0,X1]: (~equidistant(v,X0,v1,X1)|~equidistant(u,X0,u1,X1)|~between(u,v,X0)|between(u1,v1,X1))),
% 12.56/2.05 inference(resolution,[status(thm)],[f213,f242])).
% 12.56/2.05 fof(f1887,plain,(
% 12.56/2.05 ![X0,X1]: (~equidistant(u,X0,u1,X1)|~equidistant(w,X0,w1,X1)|~between(w,u,X0)|between(w1,u1,X1))),
% 12.56/2.06 inference(resolution,[status(thm)],[f817,f213])).
% 12.56/2.06 fof(f2067,definition,(
% 12.56/2.06 sQ113_spl <=> (between(v1,w1,u1))),
% 12.56/2.06 introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition])).
% 12.56/2.06 fof(f2068,plain,(
% 12.56/2.06 between(v1,w1,u1)|~sQ113_spl),
% 12.56/2.06 inference(component_clause,[status(thm)],[f2067])).
% 12.56/2.06 fof(f2122,plain,(
% 12.56/2.06 ~between(u,v,v)|~between(u1,v1,v1)|equidistant(u,v,u1,v1)),
% 12.56/2.06 inference(resolution,[status(thm)],[f860,f152])).
% 12.56/2.06 fof(f2124,definition,(
% 12.56/2.06 sQ120_spl <=> (equidistant(u,w,u1,w1))),
% 12.56/2.06 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 12.56/2.06 fof(f2132,definition,(
% 12.56/2.06 sQ122_spl <=> (equidistant(u,v,u1,v1))),
% 12.56/2.06 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 12.56/2.06 fof(f2135,plain,(
% 12.56/2.06 ~sQ10_spl|~sQ11_spl|sQ122_spl),
% 12.56/2.06 inference(split_clause,[status(thm)],[f2122,f434,f437,f2132])).
% 12.56/2.06 fof(f3529,plain,(
% 12.56/2.06 ~between(u,w,w)|~between(u1,w1,w1)|equidistant(u,w,u1,w1)),
% 12.56/2.06 inference(resolution,[status(thm)],[f998,f152])).
% 12.56/2.06 fof(f3539,plain,(
% 12.56/2.06 ~sQ20_spl|~sQ26_spl|sQ120_spl),
% 12.56/2.06 inference(split_clause,[status(thm)],[f3529,f603,f678,f2124])).
% 12.56/2.06 fof(f5280,definition,(
% 12.56/2.06 sQ299_spl <=> (equidistant(v,u,v1,u1))),
% 12.56/2.06 introduced(definition,[new_symbols(definition,[sQ299_spl])],[split_symbol_definition])).
% 12.56/2.06 fof(f5282,plain,(
% 12.56/2.06 ~equidistant(v,u,v1,u1)|sQ299_spl),
% 12.56/2.06 inference(component_clause,[status(thm)],[f5280])).
% 12.56/2.06 fof(f5989,plain,(
% 12.56/2.06 ~equidistant(v,u,v1,u1)|~between(v,w,u)|between(v1,w1,u1)),
% 12.56/2.06 inference(resolution,[status(thm)],[f1703,f1003])).
% 12.56/2.06 fof(f6002,plain,(
% 12.56/2.06 ~sQ299_spl|~sQ41_spl|sQ113_spl),
% 12.56/2.06 inference(split_clause,[status(thm)],[f5989,f5280,f1016,f2067])).
% 12.56/2.06 fof(f6008,plain,(
% 12.56/2.06 $false|sQ299_spl),
% 12.56/2.06 inference(forward_subsumption_resolution,[status(thm)],[f5282,f865])).
% 12.56/2.06 fof(f6009,plain,(
% 12.56/2.06 sQ299_spl),
% 12.56/2.06 inference(contradiction_clause,[status(thm)],[f6008])).
% 12.56/2.06 fof(f6055,plain,(
% 12.56/2.06 colinear(u1,v1,w1)|~sQ113_spl),
% 12.56/2.06 inference(resolution,[status(thm)],[f2068,f129])).
% 12.56/2.06 fof(f6114,plain,(
% 12.56/2.06 $false|~sQ113_spl),
% 12.56/2.06 inference(forward_subsumption_resolution,[status(thm)],[f6055,f246])).
% 12.56/2.06 fof(f6115,plain,(
% 12.56/2.06 ~sQ113_spl),
% 12.56/2.06 inference(contradiction_clause,[status(thm)],[f6114])).
% 12.56/2.06 fof(f6251,plain,(
% 12.56/2.06 ~equidistant(u,w,u1,w1)|~between(u,v,w)|between(u1,v1,w1)),
% 12.56/2.06 inference(resolution,[status(thm)],[f1705,f243])).
% 12.56/2.06 fof(f6264,plain,(
% 12.56/2.06 ~sQ120_spl|~sQ7_spl|sQ8_spl),
% 12.56/2.06 inference(split_clause,[status(thm)],[f6251,f2124,f424,f427])).
% 12.56/2.06 fof(f13333,definition,(
% 12.56/2.06 sQ739_spl <=> (between(w1,u1,v1))),
% 12.56/2.06 introduced(definition,[new_symbols(definition,[sQ739_spl])],[split_symbol_definition])).
% 12.56/2.06 fof(f13334,plain,(
% 12.56/2.06 between(w1,u1,v1)|~sQ739_spl),
% 12.56/2.06 inference(component_clause,[status(thm)],[f13333])).
% 12.56/2.06 fof(f16316,plain,(
% 12.56/2.06 ~equidistant(u,v,u1,v1)|~between(w,u,v)|between(w1,u1,v1)),
% 12.56/2.06 inference(resolution,[status(thm)],[f1887,f990])).
% 12.56/2.06 fof(f16333,plain,(
% 12.56/2.06 ~sQ122_spl|~sQ42_spl|sQ739_spl),
% 12.56/2.06 inference(split_clause,[status(thm)],[f16316,f2132,f1019,f13333])).
% 12.56/2.06 fof(f16406,plain,(
% 12.56/2.06 colinear(u1,v1,w1)|~sQ739_spl),
% 12.56/2.06 inference(resolution,[status(thm)],[f13334,f130])).
% 12.56/2.06 fof(f16500,plain,(
% 12.56/2.06 $false|~sQ739_spl),
% 12.56/2.06 inference(forward_subsumption_resolution,[status(thm)],[f16406,f246])).
% 12.56/2.06 fof(f16501,plain,(
% 12.56/2.06 ~sQ739_spl),
% 12.56/2.06 inference(contradiction_clause,[status(thm)],[f16500])).
% 12.56/2.06 fof(f16823,plain,(
% 12.56/2.06 colinear(u1,v1,w1)|~sQ8_spl),
% 12.56/2.06 inference(resolution,[status(thm)],[f428,f128])).
% 12.56/2.06 fof(f16912,plain,(
% 12.56/2.06 $false|~sQ8_spl),
% 12.56/2.06 inference(forward_subsumption_resolution,[status(thm)],[f16823,f246])).
% 12.56/2.06 fof(f16913,plain,(
% 12.56/2.06 ~sQ8_spl),
% 12.56/2.06 inference(contradiction_clause,[status(thm)],[f16912])).
% 12.56/2.06 fof(f16914,plain,(
% 12.56/2.06 $false),
% 12.56/2.06 inference(sat_refutation,[status(thm)],[f452,f454,f690,f811,f1022,f2135,f3539,f6002,f6009,f6115,f6264,f16333,f16501,f16913])).
% 12.56/2.06 % SZS output end CNFRefutation for theBenchmark.p
% 12.56/2.09 % Elapsed time: 1.707929 seconds
% 12.56/2.09 % CPU time: 13.262427 seconds
% 12.56/2.09 % Total memory used: 156.857 MB
% 12.56/2.09 % Net memory used: 146.727 MB
%------------------------------------------------------------------------------