%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO010-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:32 PM UTC 2026
% Result : Unsatisfiable 1.04s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO010-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n018.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 08:17:13 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 1.04/0.66 % Refutation found
% 1.04/0.66 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.04/0.66 % SZS output start CNFRefutation for theBenchmark
% 1.04/0.66 fof(f1,axiom,(
% 1.04/0.66 (![X,Y]: (equidistant(X,Y,Y,X) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f2,axiom,(
% 1.04/0.66 (![X,Y,Z,V,V2,W]: (( ~ equidistant(X,Y,Z,V)| ~ equidistant(X,Y,V2,W)| equidistant(Z,V,V2,W) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f3,axiom,(
% 1.04/0.66 (![X,Y,Z]: (( ~ equidistant(X,Y,Z,Z)| X = Y ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f4,axiom,(
% 1.04/0.66 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f5,axiom,(
% 1.04/0.66 (![Y,X,W,V]: (equidistant(Y,extension(X,Y,W,V),W,V) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f7,axiom,(
% 1.04/0.66 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f8,axiom,(
% 1.04/0.66 (![U,V,W,Y,X]: (( ~ between(U,V,W)| ~ between(Y,X,W)| between(V,inner_pasch(U,V,W,X,Y),Y) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f9,axiom,(
% 1.04/0.66 (![U,V,W,Y,X]: (( ~ between(U,V,W)| ~ between(Y,X,W)| between(X,inner_pasch(U,V,W,X,Y),U) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f19,axiom,(
% 1.04/0.66 (![X,Y,Z]: (( ~ between(X,Y,Z)| colinear(X,Y,Z) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f20,axiom,(
% 1.04/0.66 (![Y,Z,X]: (( ~ between(Y,Z,X)| colinear(X,Y,Z) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f21,axiom,(
% 1.04/0.66 (![Z,X,Y]: (( ~ between(Z,X,Y)| colinear(X,Y,Z) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f22,axiom,(
% 1.04/0.66 (![X,Y,Z]: (( ~ colinear(X,Y,Z)| between(X,Y,Z)| between(Y,Z,X)| between(Z,X,Y) ) ))),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f23,hypothesis,(
% 1.04/0.66 colinear(a,b,c) ),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f24,negated_conjecture,(
% 1.04/0.66 ( ~ colinear(a,c,b)| ~ colinear(b,a,c)| ~ colinear(b,c,a)| ~ colinear(c,a,b)| ~ colinear(c,b,a) ) ),
% 1.04/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.04/0.66 fof(f25,plain,(
% 1.04/0.66 ![X0,X1]: (equidistant(X0,X1,X1,X0))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f1])).
% 1.04/0.66 fof(f26,plain,(
% 1.04/0.66 ![Z,V,V2,W]: ((![X,Y]: (~equidistant(X,Y,Z,V)|~equidistant(X,Y,V2,W)))|equidistant(Z,V,V2,W))),
% 1.04/0.66 inference(miniscoping,[status(thm)],[f2])).
% 1.04/0.66 fof(f27,plain,(
% 1.04/0.66 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|~equidistant(X0,X1,X4,X5)|equidistant(X2,X3,X4,X5))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f26])).
% 1.04/0.66 fof(f28,plain,(
% 1.04/0.66 ![X,Y]: ((![Z]: ~equidistant(X,Y,Z,Z))|X=Y)),
% 1.04/0.66 inference(miniscoping,[status(thm)],[f3])).
% 1.04/0.66 fof(f29,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~equidistant(X0,X1,X2,X2)|X0=X1)),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f28])).
% 1.04/0.66 fof(f30,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f4])).
% 1.04/0.66 fof(f31,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X2,X3))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f5])).
% 1.04/0.66 fof(f34,plain,(
% 1.04/0.66 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f7])).
% 1.04/0.66 fof(f35,plain,(
% 1.04/0.66 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X4,X2)|between(X1,inner_pasch(X0,X1,X2,X4,X3),X3))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f8])).
% 1.04/0.66 fof(f36,plain,(
% 1.04/0.66 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X4,X2)|between(X4,inner_pasch(X0,X1,X2,X4,X3),X0))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f9])).
% 1.04/0.66 fof(f47,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X0,X1,X2))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f19])).
% 1.04/0.66 fof(f48,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X2,X0,X1))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f20])).
% 1.04/0.66 fof(f49,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X1,X2,X0))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f21])).
% 1.04/0.66 fof(f50,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~colinear(X0,X1,X2)|between(X0,X1,X2)|between(X1,X2,X0)|between(X2,X0,X1))),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f22])).
% 1.04/0.66 fof(f51,plain,(
% 1.04/0.66 colinear(a,b,c)),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f23])).
% 1.04/0.66 fof(f52,plain,(
% 1.04/0.66 ~colinear(a,c,b)|~colinear(b,a,c)|~colinear(b,c,a)|~colinear(c,a,b)|~colinear(c,b,a)),
% 1.04/0.66 inference(cnf_transformation,[status(thm)],[f24])).
% 1.04/0.66 fof(f53,definition,(
% 1.04/0.66 sQ0_spl <=> (colinear(a,c,b))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f56,definition,(
% 1.04/0.66 sQ1_spl <=> (colinear(b,a,c))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f58,plain,(
% 1.04/0.66 ~colinear(b,a,c)|sQ1_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f56])).
% 1.04/0.66 fof(f59,definition,(
% 1.04/0.66 sQ2_spl <=> (colinear(b,c,a))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f61,plain,(
% 1.04/0.66 ~colinear(b,c,a)|sQ2_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f59])).
% 1.04/0.66 fof(f62,definition,(
% 1.04/0.66 sQ3_spl <=> (colinear(c,a,b))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f64,plain,(
% 1.04/0.66 ~colinear(c,a,b)|sQ3_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f62])).
% 1.04/0.66 fof(f65,definition,(
% 1.04/0.66 sQ4_spl <=> (colinear(c,b,a))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f67,plain,(
% 1.04/0.66 ~colinear(c,b,a)|sQ4_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f65])).
% 1.04/0.66 fof(f68,plain,(
% 1.04/0.66 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl),
% 1.04/0.66 inference(split_clause,[status(thm)],[f52,f53,f56,f59,f62,f65])).
% 1.04/0.66 fof(f69,plain,(
% 1.04/0.66 between(a,b,c)|between(b,c,a)|between(c,a,b)),
% 1.04/0.66 inference(resolution,[status(thm)],[f50,f51])).
% 1.04/0.66 fof(f70,definition,(
% 1.04/0.66 sQ5_spl <=> (between(a,b,c))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f71,plain,(
% 1.04/0.66 between(a,b,c)|~sQ5_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f70])).
% 1.04/0.66 fof(f73,definition,(
% 1.04/0.66 sQ6_spl <=> (between(b,c,a))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f74,plain,(
% 1.04/0.66 between(b,c,a)|~sQ6_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f73])).
% 1.04/0.66 fof(f76,definition,(
% 1.04/0.66 sQ7_spl <=> (between(c,a,b))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f77,plain,(
% 1.04/0.66 between(c,a,b)|~sQ7_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f76])).
% 1.04/0.66 fof(f79,plain,(
% 1.04/0.66 sQ5_spl|sQ6_spl|sQ7_spl),
% 1.04/0.66 inference(split_clause,[status(thm)],[f69,f70,f73,f76])).
% 1.04/0.66 fof(f81,plain,(
% 1.04/0.66 colinear(b,c,a)|~sQ7_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f77,f48])).
% 1.04/0.66 fof(f82,plain,(
% 1.04/0.66 colinear(c,a,b)|~sQ7_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f77,f47])).
% 1.04/0.66 fof(f83,plain,(
% 1.04/0.66 colinear(c,a,b)|~sQ6_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f74,f49])).
% 1.04/0.66 fof(f86,plain,(
% 1.04/0.66 colinear(b,c,a)|~sQ5_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f71,f49])).
% 1.04/0.66 fof(f87,plain,(
% 1.04/0.66 colinear(c,a,b)|~sQ5_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f71,f48])).
% 1.04/0.66 fof(f94,plain,(
% 1.04/0.66 ![X0,X1]: (~between(X0,X1,a)|between(X1,inner_pasch(X0,X1,a,c,b),b)|~sQ6_spl)),
% 1.04/0.66 inference(resolution,[status(thm)],[f35,f74])).
% 1.04/0.66 fof(f97,plain,(
% 1.04/0.66 ![X0,X1]: (~between(X0,X1,a)|between(c,inner_pasch(X0,X1,a,c,b),X0)|~sQ6_spl)),
% 1.04/0.66 inference(resolution,[status(thm)],[f36,f74])).
% 1.04/0.66 fof(f108,plain,(
% 1.04/0.66 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~equidistant(X0,X1,X2,X3)|equidistant(X2,X3,X4,X5)|~equidistant(X6,X7,X0,X1)|~equidistant(X6,X7,X4,X5))),
% 1.04/0.66 inference(resolution,[status(thm)],[f27,f27])).
% 1.04/0.66 fof(f109,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (~equidistant(X0,X1,X2,X3)|equidistant(X2,X3,X1,X0))),
% 1.04/0.66 inference(resolution,[status(thm)],[f27,f25])).
% 1.04/0.66 fof(f111,plain,(
% 1.04/0.66 ![X0,X1,X2,X3,X4]: (~equidistant(X0,X1,X2,X3)|~equidistant(X0,X1,X4,X4)|X2=X3)),
% 1.04/0.66 inference(resolution,[status(thm)],[f27,f29])).
% 1.04/0.66 fof(f113,plain,(
% 1.04/0.66 ![X0,X1,X2]: (X0=extension(X1,X0,X2,X2))),
% 1.04/0.66 inference(resolution,[status(thm)],[f31,f29])).
% 1.04/0.66 fof(f166,plain,(
% 1.04/0.66 ![X0,X1]: (equidistant(X0,X0,X1,X1))),
% 1.04/0.66 inference(paramodulation,[status(thm)],[f113,f31])).
% 1.04/0.66 fof(f170,plain,(
% 1.04/0.66 ![X0,X1]: (between(X0,X1,X1))),
% 1.04/0.66 inference(paramodulation,[status(thm)],[f113,f30])).
% 1.04/0.66 fof(f175,plain,(
% 1.04/0.66 ![X0]: (between(c,inner_pasch(X0,a,a,c,b),X0)|~sQ6_spl)),
% 1.04/0.66 inference(resolution,[status(thm)],[f170,f97])).
% 1.04/0.66 fof(f176,plain,(
% 1.04/0.66 ![X0]: (between(a,inner_pasch(X0,a,a,c,b),b)|~sQ6_spl)),
% 1.04/0.66 inference(resolution,[status(thm)],[f170,f94])).
% 1.04/0.66 fof(f177,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|between(X2,inner_pasch(X0,X1,X2,X2,X3),X0))),
% 1.04/0.66 inference(resolution,[status(thm)],[f170,f36])).
% 1.04/0.66 fof(f178,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|between(X1,inner_pasch(X0,X1,X2,X2,X3),X3))),
% 1.04/0.66 inference(resolution,[status(thm)],[f170,f35])).
% 1.04/0.66 fof(f183,plain,(
% 1.04/0.66 ![X0,X1,X2,X3]: (~equidistant(X0,X0,X1,X2)|equidistant(X1,X2,X3,X3))),
% 1.04/0.66 inference(resolution,[status(thm)],[f166,f27])).
% 1.04/0.66 fof(f186,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~equidistant(X0,X0,X1,X2)|X1=X2)),
% 1.04/0.66 inference(resolution,[status(thm)],[f109,f29])).
% 1.04/0.66 fof(f192,plain,(
% 1.04/0.66 ![X0,X1,X2]: (~equidistant(X0,X0,X1,X1)|X2=X2)),
% 1.04/0.66 inference(resolution,[status(thm)],[f183,f186])).
% 1.04/0.66 fof(f195,definition,(
% 1.04/0.66 ![X0,X1]: (sQ11_spl <=> (~equidistant(X0,X0,X1,X1)))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f196,plain,(
% 1.04/0.66 ![X0,X1]: (~equidistant(X0,X0,X1,X1)|~sQ11_spl)),
% 1.04/0.66 inference(component_clause,[status(thm)],[f195])).
% 1.04/0.66 fof(f198,definition,(
% 1.04/0.66 ![X2]: (sQ12_spl <=> (X2=X2))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f201,plain,(
% 1.04/0.66 sQ11_spl|sQ12_spl),
% 1.04/0.66 inference(split_clause,[status(thm)],[f192,f195,f198])).
% 1.04/0.66 fof(f202,plain,(
% 1.04/0.66 $false|~sQ11_spl),
% 1.04/0.66 inference(forward_subsumption_resolution,[status(thm)],[f196,f166])).
% 1.04/0.66 fof(f203,plain,(
% 1.04/0.66 ~sQ11_spl),
% 1.04/0.66 inference(contradiction_clause,[status(thm)],[f202])).
% 1.04/0.66 fof(f246,plain,(
% 1.04/0.66 c=inner_pasch(c,a,a,c,b)|~sQ6_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f175,f34])).
% 1.04/0.66 fof(f268,plain,(
% 1.04/0.66 between(a,c,b)|~sQ6_spl),
% 1.04/0.66 inference(paramodulation,[status(thm)],[f246,f176])).
% 1.04/0.66 fof(f284,plain,(
% 1.04/0.66 colinear(c,b,a)|~sQ6_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f268,f49])).
% 1.04/0.66 fof(f287,plain,(
% 1.04/0.66 $false|sQ4_spl|~sQ6_spl),
% 1.04/0.66 inference(forward_subsumption_resolution,[status(thm)],[f284,f67])).
% 1.04/0.66 fof(f288,plain,(
% 1.04/0.66 sQ4_spl|~sQ6_spl),
% 1.04/0.66 inference(contradiction_clause,[status(thm)],[f287])).
% 1.04/0.66 fof(f289,plain,(
% 1.04/0.66 $false|~sQ7_spl|sQ3_spl),
% 1.04/0.66 inference(forward_subsumption_resolution,[status(thm)],[f64,f82])).
% 1.04/0.66 fof(f290,plain,(
% 1.04/0.66 ~sQ7_spl|sQ3_spl),
% 1.04/0.66 inference(contradiction_clause,[status(thm)],[f289])).
% 1.04/0.66 fof(f298,definition,(
% 1.04/0.66 sQ15_spl <=> (between(a,c,b))),
% 1.04/0.66 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.04/0.66 fof(f299,plain,(
% 1.04/0.66 between(a,c,b)|~sQ15_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f298])).
% 1.04/0.66 fof(f300,plain,(
% 1.04/0.66 ~between(a,c,b)|sQ15_spl),
% 1.04/0.66 inference(component_clause,[status(thm)],[f298])).
% 1.04/0.66 fof(f304,plain,(
% 1.04/0.66 $false|sQ2_spl|~sQ5_spl),
% 1.04/0.66 inference(forward_subsumption_resolution,[status(thm)],[f86,f61])).
% 1.04/0.66 fof(f305,plain,(
% 1.04/0.66 sQ2_spl|~sQ5_spl),
% 1.04/0.66 inference(contradiction_clause,[status(thm)],[f304])).
% 1.04/0.66 fof(f309,plain,(
% 1.04/0.66 colinear(b,a,c)|~sQ15_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f299,f48])).
% 1.04/0.66 fof(f310,plain,(
% 1.04/0.66 colinear(a,c,b)|~sQ15_spl),
% 1.04/0.66 inference(resolution,[status(thm)],[f299,f47])).
% 1.04/0.67 fof(f325,plain,(
% 1.04/0.67 colinear(b,c,a)|~sQ6_spl),
% 1.04/0.67 inference(resolution,[status(thm)],[f74,f47])).
% 1.04/0.67 fof(f343,plain,(
% 1.04/0.67 $false|sQ1_spl|~sQ15_spl),
% 1.04/0.67 inference(forward_subsumption_resolution,[status(thm)],[f309,f58])).
% 1.04/0.67 fof(f344,plain,(
% 1.04/0.67 sQ1_spl|~sQ15_spl),
% 1.04/0.67 inference(contradiction_clause,[status(thm)],[f343])).
% 1.04/0.67 fof(f358,plain,(
% 1.04/0.67 $false|~sQ6_spl|sQ15_spl),
% 1.04/0.67 inference(forward_subsumption_resolution,[status(thm)],[f300,f268])).
% 1.04/0.67 fof(f359,plain,(
% 1.04/0.67 ~sQ6_spl|sQ15_spl),
% 1.04/0.67 inference(contradiction_clause,[status(thm)],[f358])).
% 1.04/0.67 fof(f361,plain,(
% 1.04/0.67 sQ0_spl|~sQ15_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f310,f53,f298])).
% 1.04/0.67 fof(f374,plain,(
% 1.04/0.67 $false|~sQ5_spl|sQ3_spl),
% 1.04/0.67 inference(forward_subsumption_resolution,[status(thm)],[f64,f87])).
% 1.04/0.67 fof(f375,plain,(
% 1.04/0.67 ~sQ5_spl|sQ3_spl),
% 1.04/0.67 inference(contradiction_clause,[status(thm)],[f374])).
% 1.04/0.67 fof(f389,plain,(
% 1.04/0.67 $false|sQ3_spl|~sQ6_spl),
% 1.04/0.67 inference(forward_subsumption_resolution,[status(thm)],[f83,f64])).
% 1.04/0.67 fof(f390,plain,(
% 1.04/0.67 sQ3_spl|~sQ6_spl),
% 1.04/0.67 inference(contradiction_clause,[status(thm)],[f389])).
% 1.04/0.67 fof(f396,plain,(
% 1.04/0.67 sQ2_spl|~sQ6_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f325,f59,f73])).
% 1.04/0.67 fof(f422,plain,(
% 1.04/0.67 ![X0,X1,X2,X3,X4]: (~equidistant(X0,X1,X2,X3)|X2=X3|~equidistant(X4,X4,X0,X1))),
% 1.04/0.67 inference(resolution,[status(thm)],[f111,f183])).
% 1.04/0.67 fof(f430,plain,(
% 1.04/0.67 ![X0,X1,X2,X3,X4]: (~equidistant(X0,X0,X1,X2)|X1=X2|~equidistant(X3,X3,X4,X4))),
% 1.04/0.67 inference(resolution,[status(thm)],[f422,f183])).
% 1.04/0.67 fof(f436,definition,(
% 1.04/0.67 ![X0,X1,X2]: (sQ16_spl <=> (~equidistant(X0,X0,X1,X2)|X1=X2))),
% 1.04/0.67 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.04/0.67 fof(f439,plain,(
% 1.04/0.67 sQ16_spl|sQ11_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f430,f436,f195])).
% 1.04/0.67 fof(f459,plain,(
% 1.04/0.67 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|colinear(inner_pasch(X0,X1,X2,X2,X3),X0,X2))),
% 1.04/0.67 inference(resolution,[status(thm)],[f177,f49])).
% 1.04/0.67 fof(f460,plain,(
% 1.04/0.67 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|colinear(X0,X2,inner_pasch(X0,X1,X2,X2,X3)))),
% 1.04/0.67 inference(resolution,[status(thm)],[f177,f48])).
% 1.04/0.67 fof(f461,plain,(
% 1.04/0.67 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|colinear(X2,inner_pasch(X0,X1,X2,X2,X3),X0))),
% 1.04/0.67 inference(resolution,[status(thm)],[f177,f47])).
% 1.04/0.67 fof(f474,plain,(
% 1.04/0.67 ![X0,X1,X2]: (~between(X0,X1,X2)|X1=inner_pasch(X0,X1,X2,X2,X1))),
% 1.04/0.67 inference(resolution,[status(thm)],[f178,f34])).
% 1.04/0.67 fof(f498,plain,(
% 1.04/0.67 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X0,X1,X2)|equidistant(X1,X2,X0,X0)|~equidistant(X3,X3,X4,X5))),
% 1.04/0.67 inference(resolution,[status(thm)],[f108,f183])).
% 1.04/0.67 fof(f518,definition,(
% 1.04/0.67 ![X0,X1,X2]: (sQ17_spl <=> (~equidistant(X0,X0,X1,X2)|equidistant(X1,X2,X0,X0)))),
% 1.04/0.67 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.04/0.67 fof(f521,definition,(
% 1.04/0.67 ![X3,X4,X5]: (sQ18_spl <=> (~equidistant(X3,X3,X4,X5)))),
% 1.04/0.67 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 1.04/0.67 fof(f522,plain,(
% 1.04/0.67 ![X0,X1,X2]: (~equidistant(X0,X0,X1,X2)|~sQ18_spl)),
% 1.04/0.67 inference(component_clause,[status(thm)],[f521])).
% 1.04/0.67 fof(f524,plain,(
% 1.04/0.67 sQ17_spl|sQ18_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f498,f518,f521])).
% 1.04/0.67 fof(f552,plain,(
% 1.04/0.67 b=inner_pasch(a,b,c,c,b)|~sQ5_spl),
% 1.04/0.67 inference(resolution,[status(thm)],[f474,f71])).
% 1.04/0.67 fof(f597,plain,(
% 1.04/0.67 $false|~sQ18_spl),
% 1.04/0.67 inference(backward_subsumption_resolution,[status(thm)],[f166,f522])).
% 1.04/0.67 fof(f603,plain,(
% 1.04/0.67 ~sQ18_spl),
% 1.04/0.67 inference(contradiction_clause,[status(thm)],[f597])).
% 1.04/0.67 fof(f718,plain,(
% 1.04/0.67 ~between(a,b,c)|colinear(c,b,a)|~sQ5_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f552,f461])).
% 1.04/0.67 fof(f719,plain,(
% 1.04/0.67 ~between(a,b,c)|colinear(a,c,b)|~sQ5_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f552,f460])).
% 1.04/0.67 fof(f720,plain,(
% 1.04/0.67 ~between(a,b,c)|colinear(b,a,c)|~sQ5_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f552,f459])).
% 1.04/0.67 fof(f729,plain,(
% 1.04/0.67 ~sQ5_spl|sQ4_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f718,f70,f65])).
% 1.04/0.67 fof(f730,plain,(
% 1.04/0.67 ~sQ5_spl|sQ0_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f719,f70,f53])).
% 1.04/0.67 fof(f731,plain,(
% 1.04/0.67 ~sQ5_spl|sQ1_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f720,f70,f56])).
% 1.04/0.67 fof(f737,plain,(
% 1.04/0.67 sQ2_spl|~sQ7_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f81,f59,f76])).
% 1.04/0.67 fof(f741,plain,(
% 1.04/0.67 a=inner_pasch(c,a,b,b,a)|~sQ7_spl),
% 1.04/0.67 inference(resolution,[status(thm)],[f77,f474])).
% 1.04/0.67 fof(f750,plain,(
% 1.04/0.67 ~between(c,a,b)|colinear(b,a,c)|~sQ7_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f741,f461])).
% 1.04/0.67 fof(f751,plain,(
% 1.04/0.67 ~between(c,a,b)|colinear(c,b,a)|~sQ7_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f741,f460])).
% 1.04/0.67 fof(f752,plain,(
% 1.04/0.67 ~between(c,a,b)|colinear(a,c,b)|~sQ7_spl),
% 1.04/0.67 inference(paramodulation,[status(thm)],[f741,f459])).
% 1.04/0.67 fof(f761,plain,(
% 1.04/0.67 ~sQ7_spl|sQ1_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f750,f76,f56])).
% 1.04/0.67 fof(f762,plain,(
% 1.04/0.67 ~sQ7_spl|sQ4_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f751,f76,f65])).
% 1.04/0.67 fof(f763,plain,(
% 1.04/0.67 ~sQ7_spl|sQ0_spl),
% 1.04/0.67 inference(split_clause,[status(thm)],[f752,f76,f53])).
% 1.04/0.67 fof(f769,plain,(
% 1.04/0.67 $false),
% 1.04/0.67 inference(sat_refutation,[status(thm)],[f68,f79,f201,f203,f288,f290,f305,f344,f359,f361,f375,f390,f396,f439,f524,f603,f729,f730,f731,f737,f761,f762,f763])).
% 1.04/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.04/0.67 % Elapsed time: 0.290569 seconds
% 1.04/0.67 % CPU time: 2.136770 seconds
% 1.04/0.67 % Total memory used: 102.675 MB
% 1.04/0.67 % Net memory used: 99.206 MB
%------------------------------------------------------------------------------