%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO010-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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 20.87s 3.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO010-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n007.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 08:12:34 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 20.87/3.51 % Refutation found
% 20.87/3.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 20.87/3.51 % SZS output start CNFRefutation for theBenchmark
% 20.87/3.51 fof(f1,axiom,(
% 20.87/3.51 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f3,axiom,(
% 20.87/3.51 (![X,Y,Z,V]: (( ~ between(X,Y,Z)| ~ between(X,Y,V)| X = Y| between(X,Z,V)| between(X,V,Z) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f5,axiom,(
% 20.87/3.51 (![X,Y,Z]: (( ~ equidistant(X,Y,Z,Z)| X = Y ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f7,axiom,(
% 20.87/3.51 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(X,outer_pasch(W,X,Y,Z,V),Y) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f8,axiom,(
% 20.87/3.51 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(Z,W,outer_pasch(W,X,Y,Z,V)) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f9,axiom,(
% 20.87/3.51 (![X,V,W,Y,Z]: (( ~ between(X,V,W)| ~ between(Y,V,Z)| X = V| between(X,Z,euclid1(W,X,Y,Z,V)) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f10,axiom,(
% 20.87/3.51 (![X,V,W,Y,Z]: (( ~ between(X,V,W)| ~ between(Y,V,Z)| X = V| between(X,Y,euclid2(W,X,Y,Z,V)) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f11,axiom,(
% 20.87/3.51 (![X,V,W,Y,Z]: (( ~ between(X,V,W)| ~ between(Y,V,Z)| X = V| between(euclid1(W,X,Y,Z,V),W,euclid2(W,X,Y,Z,V)) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f13,axiom,(
% 20.87/3.51 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f14,axiom,(
% 20.87/3.51 (![Y,X,W,V]: (equidistant(Y,extension(X,Y,W,V),W,V) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f21,axiom,(
% 20.87/3.51 (![X,Y,Z]: (( ~ colinear(X,Y,Z)| between(X,Y,Z)| between(Y,X,Z)| between(X,Z,Y) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f22,axiom,(
% 20.87/3.51 (![X,Y,Z]: (( ~ between(X,Y,Z)| colinear(X,Y,Z) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f23,axiom,(
% 20.87/3.51 (![Y,X,Z]: (( ~ between(Y,X,Z)| colinear(X,Y,Z) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f24,axiom,(
% 20.87/3.51 (![X,Z,Y]: (( ~ between(X,Z,Y)| colinear(X,Y,Z) ) ))),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f25,hypothesis,(
% 20.87/3.51 colinear(a,b,c) ),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f26,negated_conjecture,(
% 20.87/3.51 ( ~ colinear(a,c,b)| ~ colinear(b,a,c)| ~ colinear(b,c,a)| ~ colinear(c,a,b)| ~ colinear(c,b,a) ) ),
% 20.87/3.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.87/3.51 fof(f27,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f1])).
% 20.87/3.51 fof(f30,plain,(
% 20.87/3.51 ![X,Z,V]: (((![Y]: ((~between(X,Y,Z)|~between(X,Y,V))|X=Y))|between(X,Z,V))|between(X,V,Z))),
% 20.87/3.51 inference(miniscoping,[status(thm)],[f3])).
% 20.87/3.51 fof(f31,plain,(
% 20.87/3.51 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|X0=X1|between(X0,X2,X3)|between(X0,X3,X2))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f30])).
% 20.87/3.51 fof(f33,plain,(
% 20.87/3.51 ![X,Y]: ((![Z]: ~equidistant(X,Y,Z,Z))|X=Y)),
% 20.87/3.51 inference(miniscoping,[status(thm)],[f5])).
% 20.87/3.51 fof(f34,plain,(
% 20.87/3.51 ![X0,X1,X2]: (~equidistant(X0,X1,X2,X2)|X0=X1)),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f33])).
% 20.87/3.51 fof(f37,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X0,outer_pasch(X1,X0,X3,X4,X2),X3))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f7])).
% 20.87/3.51 fof(f38,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X4,X1,outer_pasch(X1,X0,X3,X4,X2)))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f8])).
% 20.87/3.51 fof(f39,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X1,X4)|X0=X1|between(X0,X4,euclid1(X2,X0,X3,X4,X1)))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f9])).
% 20.87/3.51 fof(f40,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X1,X4)|X0=X1|between(X0,X3,euclid2(X2,X0,X3,X4,X1)))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f10])).
% 20.87/3.51 fof(f41,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X1,X4)|X0=X1|between(euclid1(X2,X0,X3,X4,X1),X2,euclid2(X2,X0,X3,X4,X1)))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f11])).
% 20.87/3.51 fof(f44,plain,(
% 20.87/3.51 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f13])).
% 20.87/3.51 fof(f45,plain,(
% 20.87/3.51 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X2,X3))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f14])).
% 20.87/3.51 fof(f53,plain,(
% 20.87/3.51 ![X0,X1,X2]: (~colinear(X0,X1,X2)|between(X0,X1,X2)|between(X1,X0,X2)|between(X0,X2,X1))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f21])).
% 20.87/3.51 fof(f54,plain,(
% 20.87/3.51 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X0,X1,X2))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f22])).
% 20.87/3.51 fof(f55,plain,(
% 20.87/3.51 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X1,X0,X2))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f23])).
% 20.87/3.51 fof(f56,plain,(
% 20.87/3.51 ![X0,X1,X2]: (~between(X0,X1,X2)|colinear(X0,X2,X1))),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f24])).
% 20.87/3.51 fof(f57,plain,(
% 20.87/3.51 colinear(a,b,c)),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f25])).
% 20.87/3.51 fof(f58,plain,(
% 20.87/3.51 ~colinear(a,c,b)|~colinear(b,a,c)|~colinear(b,c,a)|~colinear(c,a,b)|~colinear(c,b,a)),
% 20.87/3.51 inference(cnf_transformation,[status(thm)],[f26])).
% 20.87/3.51 fof(f59,definition,(
% 20.87/3.51 sQ0_spl <=> (colinear(a,c,b))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f61,plain,(
% 20.87/3.51 ~colinear(a,c,b)|sQ0_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f59])).
% 20.87/3.51 fof(f62,definition,(
% 20.87/3.51 sQ1_spl <=> (colinear(b,a,c))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f64,plain,(
% 20.87/3.51 ~colinear(b,a,c)|sQ1_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f62])).
% 20.87/3.51 fof(f65,definition,(
% 20.87/3.51 sQ2_spl <=> (colinear(b,c,a))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f68,definition,(
% 20.87/3.51 sQ3_spl <=> (colinear(c,a,b))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f69,plain,(
% 20.87/3.51 colinear(c,a,b)|~sQ3_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f68])).
% 20.87/3.51 fof(f70,plain,(
% 20.87/3.51 ~colinear(c,a,b)|sQ3_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f68])).
% 20.87/3.51 fof(f71,definition,(
% 20.87/3.51 sQ4_spl <=> (colinear(c,b,a))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f74,plain,(
% 20.87/3.51 ~sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ4_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f58,f59,f62,f65,f68,f71])).
% 20.87/3.51 fof(f75,plain,(
% 20.87/3.51 between(a,b,c)|between(b,a,c)|between(a,c,b)),
% 20.87/3.51 inference(resolution,[status(thm)],[f53,f57])).
% 20.87/3.51 fof(f76,definition,(
% 20.87/3.51 sQ5_spl <=> (between(a,b,c))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f77,plain,(
% 20.87/3.51 between(a,b,c)|~sQ5_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f76])).
% 20.87/3.51 fof(f79,definition,(
% 20.87/3.51 sQ6_spl <=> (between(b,a,c))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f80,plain,(
% 20.87/3.51 between(b,a,c)|~sQ6_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f79])).
% 20.87/3.51 fof(f82,definition,(
% 20.87/3.51 sQ7_spl <=> (between(a,c,b))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f83,plain,(
% 20.87/3.51 between(a,c,b)|~sQ7_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f82])).
% 20.87/3.51 fof(f84,plain,(
% 20.87/3.51 ~between(a,c,b)|sQ7_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f82])).
% 20.87/3.51 fof(f85,plain,(
% 20.87/3.51 sQ5_spl|sQ6_spl|sQ7_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f75,f76,f79,f82])).
% 20.87/3.51 fof(f86,plain,(
% 20.87/3.51 colinear(c,a,b)|~sQ7_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f83,f55])).
% 20.87/3.51 fof(f87,plain,(
% 20.87/3.51 colinear(a,c,b)|~sQ7_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f83,f54])).
% 20.87/3.51 fof(f89,plain,(
% 20.87/3.51 colinear(b,a,c)|~sQ6_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f80,f54])).
% 20.87/3.51 fof(f93,definition,(
% 20.87/3.51 sQ8_spl <=> (between(c,a,b))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f94,plain,(
% 20.87/3.51 between(c,a,b)|~sQ8_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f93])).
% 20.87/3.51 fof(f96,definition,(
% 20.87/3.51 sQ9_spl <=> (between(c,b,a))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f97,plain,(
% 20.87/3.51 between(c,b,a)|~sQ9_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f96])).
% 20.87/3.51 fof(f103,definition,(
% 20.87/3.51 sQ10_spl <=> (between(b,c,a))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f104,plain,(
% 20.87/3.51 between(b,c,a)|~sQ10_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f103])).
% 20.87/3.51 fof(f107,plain,(
% 20.87/3.51 colinear(b,c,a)|~sQ6_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f56,f80])).
% 20.87/3.51 fof(f108,plain,(
% 20.87/3.51 colinear(a,c,b)|~sQ5_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f56,f77])).
% 20.87/3.51 fof(f172,plain,(
% 20.87/3.51 $false|~sQ7_spl|sQ3_spl),
% 20.87/3.51 inference(forward_subsumption_resolution,[status(thm)],[f70,f86])).
% 20.87/3.51 fof(f173,plain,(
% 20.87/3.51 ~sQ7_spl|sQ3_spl),
% 20.87/3.51 inference(contradiction_clause,[status(thm)],[f172])).
% 20.87/3.51 fof(f184,plain,(
% 20.87/3.51 colinear(b,a,c)|~sQ5_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f77,f55])).
% 20.87/3.51 fof(f236,plain,(
% 20.87/3.51 $false|~sQ5_spl|sQ1_spl),
% 20.87/3.51 inference(forward_subsumption_resolution,[status(thm)],[f64,f184])).
% 20.87/3.51 fof(f237,plain,(
% 20.87/3.51 ~sQ5_spl|sQ1_spl),
% 20.87/3.51 inference(contradiction_clause,[status(thm)],[f236])).
% 20.87/3.51 fof(f240,plain,(
% 20.87/3.51 colinear(c,b,a)|~sQ8_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f94,f56])).
% 20.87/3.51 fof(f260,plain,(
% 20.87/3.51 ![X0]: (~between(c,b,X0)|c=b|between(c,X0,a)|between(c,a,X0)|~sQ9_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f31])).
% 20.87/3.51 fof(f262,plain,(
% 20.87/3.51 colinear(c,a,b)|~sQ9_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f56])).
% 20.87/3.51 fof(f263,plain,(
% 20.87/3.51 colinear(b,c,a)|~sQ9_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f55])).
% 20.87/3.51 fof(f264,plain,(
% 20.87/3.51 colinear(c,b,a)|~sQ9_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f54])).
% 20.87/3.51 fof(f265,definition,(
% 20.87/3.51 ![X0]: (sQ24_spl <=> (~between(c,b,X0)|between(c,X0,a)|between(c,a,X0)))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f268,definition,(
% 20.87/3.51 sQ25_spl <=> (c=b)),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f269,plain,(
% 20.87/3.51 c=b|~sQ25_spl),
% 20.87/3.51 inference(component_clause,[status(thm)],[f268])).
% 20.87/3.51 fof(f271,plain,(
% 20.87/3.51 sQ24_spl|sQ25_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f260,f265,f268,f96])).
% 20.87/3.51 fof(f306,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,c)|between(b,X1,outer_pasch(X1,X0,a,b,c))|~sQ7_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f83,f38])).
% 20.87/3.51 fof(f307,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,c)|between(X0,outer_pasch(X1,X0,a,b,c),a)|~sQ7_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f83,f37])).
% 20.87/3.51 fof(f398,plain,(
% 20.87/3.51 $false|sQ0_spl|~sQ5_spl),
% 20.87/3.51 inference(forward_subsumption_resolution,[status(thm)],[f108,f61])).
% 20.87/3.51 fof(f399,plain,(
% 20.87/3.51 sQ0_spl|~sQ5_spl),
% 20.87/3.51 inference(contradiction_clause,[status(thm)],[f398])).
% 20.87/3.51 fof(f400,plain,(
% 20.87/3.51 sQ1_spl|~sQ6_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f89,f62,f79])).
% 20.87/3.51 fof(f430,plain,(
% 20.87/3.51 between(c,a,b)|between(a,c,b)|between(c,b,a)|~sQ3_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f69,f53])).
% 20.87/3.51 fof(f431,plain,(
% 20.87/3.51 sQ8_spl|sQ7_spl|sQ9_spl|~sQ3_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f430,f93,f82,f96,f68])).
% 20.87/3.51 fof(f432,plain,(
% 20.87/3.51 sQ4_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f264,f71,f96])).
% 20.87/3.51 fof(f433,plain,(
% 20.87/3.51 sQ4_spl|~sQ8_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f240,f71,f93])).
% 20.87/3.51 fof(f490,plain,(
% 20.87/3.51 colinear(c,b,a)|~sQ10_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f104,f55])).
% 20.87/3.51 fof(f501,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|X0=X1|between(euclid1(X2,X0,X3,extension(X3,X1,X4,X5),X1),X2,euclid2(X2,X0,X3,extension(X3,X1,X4,X5),X1)))),
% 20.87/3.51 inference(resolution,[status(thm)],[f44,f41])).
% 20.87/3.51 fof(f502,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|X0=X1|between(X0,X3,euclid2(X2,X0,X3,extension(X3,X1,X4,X5),X1)))),
% 20.87/3.51 inference(resolution,[status(thm)],[f44,f40])).
% 20.87/3.51 fof(f503,plain,(
% 20.87/3.51 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|X0=X1|between(X0,extension(X3,X1,X4,X5),euclid1(X2,X0,X3,extension(X3,X1,X4,X5),X1)))),
% 20.87/3.51 inference(resolution,[status(thm)],[f44,f39])).
% 20.87/3.51 fof(f512,plain,(
% 20.87/3.51 ![X0,X1,X2]: (X0=extension(X1,X0,X2,X2))),
% 20.87/3.51 inference(resolution,[status(thm)],[f45,f34])).
% 20.87/3.51 fof(f524,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,b)|between(c,X1,outer_pasch(X1,X0,a,c,b))|~sQ5_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f77,f38])).
% 20.87/3.51 fof(f525,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,b)|between(X0,outer_pasch(X1,X0,a,c,b),a)|~sQ5_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f77,f37])).
% 20.87/3.51 fof(f551,plain,(
% 20.87/3.51 ![X0,X1]: (between(X0,X1,X1))),
% 20.87/3.51 inference(paramodulation,[status(thm)],[f512,f44])).
% 20.87/3.51 fof(f614,plain,(
% 20.87/3.51 sQ2_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f263,f65,f96])).
% 20.87/3.51 fof(f615,plain,(
% 20.87/3.51 sQ3_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f262,f68,f96])).
% 20.87/3.51 fof(f617,plain,(
% 20.87/3.51 sQ0_spl|~sQ7_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f87,f59,f82])).
% 20.87/3.51 fof(f845,plain,(
% 20.87/3.51 sQ4_spl|~sQ10_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f490,f71,f103])).
% 20.87/3.51 fof(f849,plain,(
% 20.87/3.51 sQ2_spl|~sQ6_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f107,f65,f79])).
% 20.87/3.51 fof(f867,plain,(
% 20.87/3.51 colinear(b,a,c)|~sQ10_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f104,f56])).
% 20.87/3.51 fof(f869,plain,(
% 20.87/3.51 colinear(b,c,a)|~sQ10_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f104,f54])).
% 20.87/3.51 fof(f872,plain,(
% 20.87/3.51 sQ2_spl|~sQ10_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f869,f65,f103])).
% 20.87/3.51 fof(f1119,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,a)|between(c,X1,outer_pasch(X1,X0,b,c,a))|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f80,f38])).
% 20.87/3.51 fof(f1120,plain,(
% 20.87/3.51 ![X0,X1]: (~between(X0,X1,a)|between(X0,outer_pasch(X1,X0,b,c,a),b)|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f80,f37])).
% 20.87/3.51 fof(f1142,plain,(
% 20.87/3.51 ![X0,X1,X2]: (c=b|between(c,extension(X0,b,X1,X2),euclid1(a,c,X0,extension(X0,b,X1,X2),b))|~sQ9_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f503])).
% 20.87/3.51 fof(f1143,plain,(
% 20.87/3.51 ![X0,X1,X2]: (c=b|between(c,X0,euclid2(a,c,X0,extension(X0,b,X1,X2),b))|~sQ9_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f502])).
% 20.87/3.51 fof(f1144,plain,(
% 20.87/3.51 ![X0,X1,X2]: (c=b|between(euclid1(a,c,X0,extension(X0,b,X1,X2),b),a,euclid2(a,c,X0,extension(X0,b,X1,X2),b))|~sQ9_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f97,f501])).
% 20.87/3.51 fof(f1158,definition,(
% 20.87/3.51 ![X0,X1,X2]: (sQ58_spl <=> (between(c,extension(X0,b,X1,X2),euclid1(a,c,X0,extension(X0,b,X1,X2),b))))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f1161,plain,(
% 20.87/3.51 sQ25_spl|sQ58_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f1142,f268,f1158,f96])).
% 20.87/3.51 fof(f1162,definition,(
% 20.87/3.51 ![X0,X1,X2]: (sQ59_spl <=> (between(c,X0,euclid2(a,c,X0,extension(X0,b,X1,X2),b))))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f1165,plain,(
% 20.87/3.51 sQ25_spl|sQ59_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f1143,f268,f1162,f96])).
% 20.87/3.51 fof(f1166,definition,(
% 20.87/3.51 ![X0,X1,X2]: (sQ60_spl <=> (between(euclid1(a,c,X0,extension(X0,b,X1,X2),b),a,euclid2(a,c,X0,extension(X0,b,X1,X2),b))))),
% 20.87/3.51 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 20.87/3.51 fof(f1169,plain,(
% 20.87/3.51 sQ25_spl|sQ60_spl|~sQ9_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f1144,f268,f1166,f96])).
% 20.87/3.51 fof(f1231,plain,(
% 20.87/3.51 ![X0]: (between(c,a,outer_pasch(a,X0,b,c,a))|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f1119,f551])).
% 20.87/3.51 fof(f1249,plain,(
% 20.87/3.51 ![X0]: (colinear(a,c,outer_pasch(a,X0,b,c,a))|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f1231,f55])).
% 20.87/3.51 fof(f1250,plain,(
% 20.87/3.51 ![X0]: (colinear(c,a,outer_pasch(a,X0,b,c,a))|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f1231,f54])).
% 20.87/3.51 fof(f1274,plain,(
% 20.87/3.51 ![X0]: (between(X0,outer_pasch(a,X0,b,c,a),b)|~sQ6_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f1120,f551])).
% 20.87/3.51 fof(f1291,plain,(
% 20.87/3.51 b=outer_pasch(a,b,b,c,a)|~sQ6_spl),
% 20.87/3.51 inference(resolution,[status(thm)],[f1274,f27])).
% 20.87/3.51 fof(f1296,plain,(
% 20.87/3.51 colinear(c,a,b)|~sQ6_spl),
% 20.87/3.51 inference(paramodulation,[status(thm)],[f1291,f1250])).
% 20.87/3.51 fof(f1297,plain,(
% 20.87/3.51 colinear(a,c,b)|~sQ6_spl),
% 20.87/3.51 inference(paramodulation,[status(thm)],[f1291,f1249])).
% 20.87/3.51 fof(f1300,plain,(
% 20.87/3.51 sQ3_spl|~sQ6_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f1296,f68,f79])).
% 20.87/3.51 fof(f1301,plain,(
% 20.87/3.51 sQ0_spl|~sQ6_spl),
% 20.87/3.51 inference(split_clause,[status(thm)],[f1297,f59,f79])).
% 20.87/3.51 fof(f1480,plain,(
% 20.87/3.51 ![X0]: (between(c,b,outer_pasch(b,X0,a,c,b))|~sQ5_spl)),
% 20.87/3.51 inference(resolution,[status(thm)],[f524,f551])).
% 20.87/3.51 fof(f1541,plain,(
% 20.87/3.51 ~between(a,b,b)|~sQ25_spl|sQ7_spl),
% 20.87/3.51 inference(backward_demodulation,[status(thm)],[f269,f84])).
% 20.87/3.54 fof(f1558,plain,(
% 20.87/3.54 sQ1_spl|~sQ10_spl),
% 20.87/3.54 inference(split_clause,[status(thm)],[f867,f62,f103])).
% 20.87/3.54 fof(f1559,plain,(
% 20.87/3.54 $false|~sQ25_spl|sQ7_spl),
% 20.87/3.54 inference(forward_subsumption_resolution,[status(thm)],[f1541,f551])).
% 20.87/3.54 fof(f1560,plain,(
% 20.87/3.54 ~sQ25_spl|sQ7_spl),
% 20.87/3.54 inference(contradiction_clause,[status(thm)],[f1559])).
% 20.87/3.54 fof(f2112,plain,(
% 20.87/3.54 ![X0]: (between(X0,outer_pasch(b,X0,a,c,b),a)|~sQ5_spl)),
% 20.87/3.54 inference(resolution,[status(thm)],[f525,f551])).
% 20.87/3.54 fof(f2345,plain,(
% 20.87/3.54 a=outer_pasch(b,a,a,c,b)|~sQ5_spl),
% 20.87/3.54 inference(resolution,[status(thm)],[f2112,f27])).
% 20.87/3.54 fof(f2353,plain,(
% 20.87/3.54 between(c,b,a)|~sQ5_spl),
% 20.87/3.54 inference(paramodulation,[status(thm)],[f2345,f1480])).
% 20.87/3.54 fof(f2355,plain,(
% 20.87/3.54 sQ9_spl|~sQ5_spl),
% 20.87/3.54 inference(split_clause,[status(thm)],[f2353,f96,f76])).
% 20.87/3.54 fof(f3091,plain,(
% 20.87/3.54 ![X0]: (between(b,c,outer_pasch(c,X0,a,b,c))|~sQ7_spl)),
% 20.87/3.54 inference(resolution,[status(thm)],[f306,f551])).
% 20.87/3.54 fof(f3141,plain,(
% 20.87/3.54 ![X0]: (between(X0,outer_pasch(c,X0,a,b,c),a)|~sQ7_spl)),
% 20.87/3.54 inference(resolution,[status(thm)],[f307,f551])).
% 20.87/3.54 fof(f3241,plain,(
% 20.87/3.54 a=outer_pasch(c,a,a,b,c)|~sQ7_spl),
% 20.87/3.54 inference(resolution,[status(thm)],[f3141,f27])).
% 20.87/3.54 fof(f3314,plain,(
% 20.87/3.54 between(b,c,a)|~sQ7_spl),
% 20.87/3.54 inference(paramodulation,[status(thm)],[f3241,f3091])).
% 20.87/3.54 fof(f3335,plain,(
% 20.87/3.54 sQ10_spl|~sQ7_spl),
% 20.87/3.54 inference(split_clause,[status(thm)],[f3314,f103,f82])).
% 20.87/3.54 fof(f3336,plain,(
% 20.87/3.54 $false),
% 20.87/3.54 inference(sat_refutation,[status(thm)],[f74,f85,f173,f237,f271,f399,f400,f431,f432,f433,f614,f615,f617,f845,f849,f872,f1161,f1165,f1169,f1300,f1301,f1558,f1560,f2355,f3335])).
% 20.87/3.54 % SZS output end CNFRefutation for theBenchmark.p
% 20.87/3.55 % Elapsed time: 3.087163 seconds
% 20.87/3.55 % CPU time: 23.932129 seconds
% 20.87/3.55 % Total memory used: 138.406 MB
% 20.87/3.55 % Net memory used: 125.398 MB
%------------------------------------------------------------------------------