%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO342+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:26:23 PM UTC 2026
% Result : Theorem 0.79s 0.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO342+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 15:34:20 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.41 % Drodi V4.1.1
% 0.79/0.74 % Refutation found
% 0.79/0.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.79/0.74 % SZS output start CNFRefutation for theBenchmark
% 0.79/0.74 fof(f1,conjecture,(
% 0.79/0.74 (? [Vd1416] :( ron(vd1399,Vd1416)& ron(vd1401,Vd1416)& rline(Vd1416) ) )),
% 0.79/0.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.79/0.74 fof(f2,negated_conjecture,(
% 0.79/0.74 ~((? [Vd1416] :( ron(vd1399,Vd1416)& ron(vd1401,Vd1416)& rline(Vd1416) ) ))),
% 0.79/0.74 inference(negated_conjecture,[status(cth)],[f1])).
% 0.79/0.74 fof(f6,axiom,(
% 0.79/0.74 vf(vd1399,vd1401) = vf(vd1399,vd1409) ),
% 0.79/0.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.79/0.74 fof(f8,axiom,(
% 0.79/0.74 rpoint(vd1409) ),
% 0.79/0.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.79/0.74 fof(f9,axiom,(
% 0.79/0.74 ( vd1406 = vd1407& ron(vd1400,vd1406)& ron(vd1399,vd1406)& rline(vd1407)& vd1400 != vd1401& vd1399 != vd1401& vd1399 != vd1400& (? [Vd1405] :( vd1401 = Vd1405& rpoint(Vd1405) ))& (? [Vd1404] :( vd1400 = Vd1404& rpoint(Vd1404) ))& (? [Vd1403] :( vd1399 = Vd1403& rpoint(Vd1403) ) )) ),
% 0.79/0.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.79/0.74 fof(f36,axiom,(
% 0.79/0.74 (! [Vd217,Vd218] :( ( Vd217 != Vd218& (? [Vd221] :( Vd218 = Vd221& rpoint(Vd221) ))& (? [Vd220] :( Vd217 = Vd220& rpoint(Vd220) ) ))=> (? [Vd223] :( ron(Vd218,Vd223)& ron(Vd217,Vd223)& rline(Vd223) ) )) )),
% 0.79/0.74 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.79/0.74 fof(f126,plain,(
% 0.79/0.74 (![Vd1416]: ((~ron(vd1399,Vd1416)|~ron(vd1401,Vd1416))|~rline(Vd1416)))),
% 0.79/0.74 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.79/0.74 fof(f127,plain,(
% 0.79/0.74 ![X0]: (~ron(vd1399,X0)|~ron(vd1401,X0)|~rline(X0))),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f126])).
% 0.79/0.74 fof(f131,plain,(
% 0.79/0.74 vf(vd1399,vd1401)=vf(vd1399,vd1409)),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f6])).
% 0.79/0.74 fof(f133,plain,(
% 0.79/0.74 rpoint(vd1409)),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f8])).
% 0.79/0.74 fof(f134,plain,(
% 0.79/0.74 ((((((((vd1406=vd1407&ron(vd1400,vd1406))&ron(vd1399,vd1406))&rline(vd1407))&~vd1400=vd1401)&~vd1399=vd1401)&~vd1399=vd1400)&(vd1401=sK0_skl&rpoint(sK0_skl)))&(vd1400=sK1_skl&rpoint(sK1_skl)))&(vd1399=sK2_skl&rpoint(sK2_skl))),
% 0.79/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(Vd1405,sK0_skl),skolemize(Vd1404,sK1_skl),skolemize(Vd1403,sK2_skl)],[f9])).
% 0.79/0.74 fof(f139,plain,(
% 0.79/0.74 ~vd1400=vd1401),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f140,plain,(
% 0.79/0.74 ~vd1399=vd1401),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f141,plain,(
% 0.79/0.74 ~vd1399=vd1400),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f142,plain,(
% 0.79/0.74 vd1401=sK0_skl),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f143,plain,(
% 0.79/0.74 rpoint(sK0_skl)),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f144,plain,(
% 0.79/0.74 vd1400=sK1_skl),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f145,plain,(
% 0.79/0.74 rpoint(sK1_skl)),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f146,plain,(
% 0.79/0.74 vd1399=sK2_skl),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f147,plain,(
% 0.79/0.74 rpoint(sK2_skl)),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f134])).
% 0.79/0.74 fof(f232,plain,(
% 0.79/0.74 ![Vd217,Vd218]: (((Vd217=Vd218|(![Vd221]: (~Vd218=Vd221|~rpoint(Vd221))))|(![Vd220]: (~Vd217=Vd220|~rpoint(Vd220))))|(?[Vd223]: ((ron(Vd218,Vd223)&ron(Vd217,Vd223))&rline(Vd223))))),
% 0.79/0.74 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.79/0.74 fof(f233,plain,(
% 0.79/0.74 ![Vd217,Vd218]: (((Vd217=Vd218|(![Vd221]: (~Vd218=Vd221|~rpoint(Vd221))))|(![Vd220]: (~Vd217=Vd220|~rpoint(Vd220))))|((ron(Vd218,sK7_skl(Vd218,Vd217))&ron(Vd217,sK7_skl(Vd218,Vd217)))&rline(sK7_skl(Vd218,Vd217))))),
% 0.79/0.74 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Vd223,sK7_skl(Vd218,Vd217))],[f232])).
% 0.79/0.74 fof(f234,plain,(
% 0.79/0.74 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|ron(X1,sK7_skl(X1,X0)))),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f233])).
% 0.79/0.74 fof(f235,plain,(
% 0.79/0.74 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|ron(X0,sK7_skl(X1,X0)))),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f233])).
% 0.79/0.74 fof(f236,plain,(
% 0.79/0.74 ![X0,X1,X2,X3]: (X0=X1|~X1=X2|~rpoint(X2)|~X0=X3|~rpoint(X3)|rline(sK7_skl(X1,X0)))),
% 0.79/0.74 inference(cnf_transformation,[status(thm)],[f233])).
% 0.79/0.74 fof(f750,plain,(
% 0.79/0.74 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|ron(X1,sK7_skl(X1,X0)))),
% 0.79/0.74 inference(destructive_equality_resolution,[status(thm)],[f234])).
% 0.79/0.74 fof(f751,plain,(
% 0.79/0.74 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|ron(X0,sK7_skl(X1,X0)))),
% 0.79/0.74 inference(destructive_equality_resolution,[status(thm)],[f235])).
% 0.79/0.74 fof(f752,plain,(
% 0.79/0.74 ![X0,X1]: (X0=X1|~rpoint(X1)|~rpoint(X0)|rline(sK7_skl(X1,X0)))),
% 0.79/0.74 inference(destructive_equality_resolution,[status(thm)],[f236])).
% 0.79/0.74 fof(f935,plain,(
% 0.79/0.74 rpoint(vd1401)),
% 0.79/0.74 inference(forward_demodulation,[status(thm)],[f142,f143])).
% 0.79/0.74 fof(f936,plain,(
% 0.79/0.74 rpoint(vd1399)),
% 0.79/0.74 inference(forward_demodulation,[status(thm)],[f146,f147])).
% 0.79/0.74 fof(f1016,definition,(
% 0.79/0.74 sQ11_spl <=> (rpoint(vd1399))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1018,plain,(
% 0.79/0.74 ~rpoint(vd1399)|sQ11_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1016])).
% 0.79/0.74 fof(f1033,definition,(
% 0.79/0.74 sQ16_spl <=> (rpoint(vd1400))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1035,plain,(
% 0.79/0.74 ~rpoint(vd1400)|sQ16_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1033])).
% 0.79/0.74 fof(f1056,plain,(
% 0.79/0.74 ![X0]: (X0=vd1401|~rpoint(X0)|rline(sK7_skl(vd1401,X0)))),
% 0.79/0.74 inference(resolution,[status(thm)],[f752,f935])).
% 0.79/0.74 fof(f1103,definition,(
% 0.79/0.74 sQ30_spl <=> (sK1_skl=vd1399)),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1104,plain,(
% 0.79/0.74 sK1_skl=vd1399|~sQ30_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1103])).
% 0.79/0.74 fof(f1110,definition,(
% 0.79/0.74 sQ32_spl <=> (vd1401=vd1399)),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1111,plain,(
% 0.79/0.74 vd1401=vd1399|~sQ32_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1110])).
% 0.79/0.74 fof(f1117,plain,(
% 0.79/0.74 $false|~sQ32_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1111,f140])).
% 0.79/0.74 fof(f1118,plain,(
% 0.79/0.74 ~sQ32_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1117])).
% 0.79/0.74 fof(f1138,definition,(
% 0.79/0.74 sQ38_spl <=> (vd1401=sK1_skl)),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1139,plain,(
% 0.79/0.74 vd1401=sK1_skl|~sQ38_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1138])).
% 0.79/0.74 fof(f1146,plain,(
% 0.79/0.74 vd1399=vd1401|rline(sK7_skl(vd1401,vd1399))),
% 0.79/0.74 inference(resolution,[status(thm)],[f1056,f936])).
% 0.79/0.74 fof(f1153,definition,(
% 0.79/0.74 sQ41_spl <=> (rline(sK7_skl(vd1401,vd1399)))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1156,plain,(
% 0.79/0.74 sQ32_spl|sQ41_spl),
% 0.79/0.74 inference(split_clause,[status(thm)],[f1146,f1110,f1153])).
% 0.79/0.74 fof(f1292,plain,(
% 0.79/0.74 ![X0]: (X0=vd1401|~rpoint(X0)|ron(X0,sK7_skl(vd1401,X0)))),
% 0.79/0.74 inference(resolution,[status(thm)],[f751,f935])).
% 0.79/0.74 fof(f1354,plain,(
% 0.79/0.74 vd1399=vd1401|ron(vd1399,sK7_skl(vd1401,vd1399))),
% 0.79/0.74 inference(resolution,[status(thm)],[f1292,f936])).
% 0.79/0.74 fof(f1361,definition,(
% 0.79/0.74 sQ80_spl <=> (ron(vd1399,sK7_skl(vd1401,vd1399)))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1362,plain,(
% 0.79/0.74 ron(vd1399,sK7_skl(vd1401,vd1399))|~sQ80_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1361])).
% 0.79/0.74 fof(f1364,plain,(
% 0.79/0.74 sQ32_spl|sQ80_spl),
% 0.79/0.74 inference(split_clause,[status(thm)],[f1354,f1110,f1361])).
% 0.79/0.74 fof(f1376,plain,(
% 0.79/0.74 ![X0]: (X0=vd1401|~rpoint(X0)|ron(vd1401,sK7_skl(vd1401,X0)))),
% 0.79/0.74 inference(resolution,[status(thm)],[f750,f935])).
% 0.79/0.74 fof(f1566,plain,(
% 0.79/0.74 vd1399=vd1401|ron(vd1401,sK7_skl(vd1401,vd1399))),
% 0.79/0.74 inference(resolution,[status(thm)],[f1376,f936])).
% 0.79/0.74 fof(f1573,definition,(
% 0.79/0.74 sQ121_spl <=> (ron(vd1401,sK7_skl(vd1401,vd1399)))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1576,plain,(
% 0.79/0.74 sQ32_spl|sQ121_spl),
% 0.79/0.74 inference(split_clause,[status(thm)],[f1566,f1110,f1573])).
% 0.79/0.74 fof(f1687,definition,(
% 0.79/0.74 sQ141_spl <=> (rpoint(vd1409))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1689,plain,(
% 0.79/0.74 ~rpoint(vd1409)|sQ141_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1687])).
% 0.79/0.74 fof(f1690,definition,(
% 0.79/0.74 sQ142_spl <=> (rpoint(vd1401))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1692,plain,(
% 0.79/0.74 ~rpoint(vd1401)|sQ142_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1690])).
% 0.79/0.74 fof(f1705,plain,(
% 0.79/0.74 $false|sQ11_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1018,f936])).
% 0.79/0.74 fof(f1706,plain,(
% 0.79/0.74 sQ11_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1705])).
% 0.79/0.74 fof(f1707,plain,(
% 0.79/0.74 $false|sQ141_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1689,f133])).
% 0.79/0.74 fof(f1708,plain,(
% 0.79/0.74 sQ141_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1707])).
% 0.79/0.74 fof(f1709,plain,(
% 0.79/0.74 $false|sQ142_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1692,f935])).
% 0.79/0.74 fof(f1710,plain,(
% 0.79/0.74 sQ142_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1709])).
% 0.79/0.74 fof(f1732,definition,(
% 0.79/0.74 sQ150_spl <=> (vf(vd1399,vd1409)=vf(vd1399,vd1401))),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1734,plain,(
% 0.79/0.74 ~vf(vd1399,vd1409)=vf(vd1399,vd1401)|sQ150_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1732])).
% 0.79/0.74 fof(f1755,plain,(
% 0.79/0.74 ~vf(vd1399,vd1409)=vf(vd1399,vd1409)|sQ150_spl),
% 0.79/0.74 inference(forward_demodulation,[status(thm)],[f131,f1734])).
% 0.79/0.74 fof(f1756,plain,(
% 0.79/0.74 $false|sQ150_spl),
% 0.79/0.74 inference(trivial_equality_resolution,[status(thm)],[f1755])).
% 0.79/0.74 fof(f1757,plain,(
% 0.79/0.74 sQ150_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1756])).
% 0.79/0.74 fof(f1862,plain,(
% 0.79/0.74 vd1400=vd1399|~sQ30_spl),
% 0.79/0.74 inference(backward_demodulation,[status(thm)],[f144,f1104])).
% 0.79/0.74 fof(f1863,plain,(
% 0.79/0.74 $false|~sQ30_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1862,f141])).
% 0.79/0.74 fof(f1864,plain,(
% 0.79/0.74 ~sQ30_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1863])).
% 0.79/0.74 fof(f1883,plain,(
% 0.79/0.74 vd1401=vd1400|~sQ38_spl),
% 0.79/0.74 inference(forward_demodulation,[status(thm)],[f144,f1139])).
% 0.79/0.74 fof(f1884,plain,(
% 0.79/0.74 $false|~sQ38_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1883,f139])).
% 0.79/0.74 fof(f1885,plain,(
% 0.79/0.74 ~sQ38_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1884])).
% 0.79/0.74 fof(f1908,plain,(
% 0.79/0.74 rpoint(vd1400)),
% 0.79/0.74 inference(forward_demodulation,[status(thm)],[f144,f145])).
% 0.79/0.74 fof(f1909,plain,(
% 0.79/0.74 $false|sQ16_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1908,f1035])).
% 0.79/0.74 fof(f1910,plain,(
% 0.79/0.74 sQ16_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f1909])).
% 0.79/0.74 fof(f1950,definition,(
% 0.79/0.74 sQ170_spl <=> (vd1400=vd1401)),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1951,plain,(
% 0.79/0.74 vd1400=vd1401|~sQ170_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1950])).
% 0.79/0.74 fof(f1957,definition,(
% 0.79/0.74 sQ172_spl <=> (vd1400=vd1399)),
% 0.79/0.74 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 0.79/0.74 fof(f1958,plain,(
% 0.79/0.74 vd1400=vd1399|~sQ172_spl),
% 0.79/0.74 inference(component_clause,[status(thm)],[f1957])).
% 0.79/0.74 fof(f2031,plain,(
% 0.79/0.74 $false|~sQ170_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1951,f139])).
% 0.79/0.74 fof(f2032,plain,(
% 0.79/0.74 ~sQ170_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f2031])).
% 0.79/0.74 fof(f2033,plain,(
% 0.79/0.74 $false|~sQ172_spl),
% 0.79/0.74 inference(forward_subsumption_resolution,[status(thm)],[f1958,f141])).
% 0.79/0.74 fof(f2034,plain,(
% 0.79/0.74 ~sQ172_spl),
% 0.79/0.74 inference(contradiction_clause,[status(thm)],[f2033])).
% 0.79/0.74 fof(f2116,plain,(
% 0.79/0.74 ~ron(vd1401,sK7_skl(vd1401,vd1399))|~rline(sK7_skl(vd1401,vd1399))|~sQ80_spl),
% 0.79/0.74 inference(resolution,[status(thm)],[f1362,f127])).
% 0.79/0.74 fof(f2137,plain,(
% 0.79/0.74 ~sQ121_spl|~sQ41_spl|~sQ80_spl),
% 0.79/0.74 inference(split_clause,[status(thm)],[f2116,f1573,f1153,f1361])).
% 0.79/0.74 fof(f2194,plain,(
% 0.79/0.74 $false),
% 0.79/0.74 inference(sat_refutation,[status(thm)],[f1118,f1156,f1364,f1576,f1706,f1708,f1710,f1757,f1864,f1885,f1910,f2032,f2034,f2137])).
% 0.79/0.74 % SZS output end CNFRefutation for theBenchmark.p
% 0.79/0.76 % Elapsed time: 0.363514 seconds
% 0.79/0.76 % CPU time: 2.429877 seconds
% 0.79/0.76 % Total memory used: 138.196 MB
% 0.79/0.76 % Net memory used: 135.315 MB
%------------------------------------------------------------------------------