%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO034-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 : n008.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:36 PM UTC 2026
% Result : Unsatisfiable 281.83s 41.01s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO034-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.08/5.37 % Computer : n008.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Sun Sep 20 08:30:33 UTC 2026
% 0.08/5.38 % CPUTime :
% 0.08/5.39 % Drodi V4.1.1
% 281.83/41.01 % Refutation found
% 281.83/41.01 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 281.83/41.01 % SZS output start CNFRefutation for theBenchmark
% 281.83/41.01 fof(f1,axiom,(
% 281.83/41.01 (![X,Y]: (equidistant(X,Y,Y,X) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.01 fof(f4,axiom,(
% 281.83/41.01 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.01 fof(f6,axiom,(
% 281.83/41.01 (![X,Y,X1,Y1,Z,Z1,V,V1]: (( ~ equidistant(X,Y,X1,Y1)| ~ equidistant(Y,Z,Y1,Z1)| ~ equidistant(X,V,X1,V1)| ~ equidistant(Y,V,Y1,V1)| ~ between(X,Y,Z)| ~ between(X1,Y1,Z1)| X = Y| equidistant(Z,V,Z1,V1) ) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.01 fof(f7,axiom,(
% 281.83/41.01 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.01 fof(f19,axiom,(
% 281.83/41.01 (![U,V]: (reflection(U,V) = extension(U,V,U,V) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.01 fof(f20,axiom,(
% 281.83/41.01 (![U,V]: (equidistant(U,V,U,V) ))),
% 281.83/41.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f31,axiom,(
% 281.83/41.02 (![U,V]: (between(U,V,reflection(U,V)) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f32,axiom,(
% 281.83/41.02 (![V,U]: (equidistant(V,reflection(U,V),U,V) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f33,axiom,(
% 281.83/41.02 (![U,V]: (( U != V| V = reflection(U,V) ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f35,axiom,(
% 281.83/41.02 (![V,U]: (( V != reflection(U,V)| U = V ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f38,axiom,(
% 281.83/41.02 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,V,X)| ~ equidistant(V,W,V,X)| U = V| W = X ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f39,axiom,(
% 281.83/41.02 (![U,V,W]: (( ~ between(U,V,W)| U = V| W = extension(U,V,V,W) ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f40,axiom,(
% 281.83/41.02 (![W,X,Y,Z,U,V]: (( ~ equidistant(W,X,Y,Z)| extension(U,V,W,X) = extension(U,V,Y,Z)| U = V ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f41,axiom,(
% 281.83/41.02 (![U,V]: (( extension(U,V,U,V) = extension(U,V,V,U)| U = V ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f43,axiom,(
% 281.83/41.02 (![U,V]: (U = reflection(reflection(U,V),V) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f44,axiom,(
% 281.83/41.02 (![U,V]: (between(U,V,V) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f46,axiom,(
% 281.83/41.02 (![U,V,W]: (( ~ between(U,V,W)| between(W,V,U) ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f53,axiom,(
% 281.83/41.02 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,W,X)| between(V,W,X) ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f54,axiom,(
% 281.83/41.02 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(V,W,X)| between(U,W,X)| V = W ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f65,axiom,(
% 281.83/41.02 (![U,V,W,W1]: (( ~ between(U,V,W)| ~ equidistant(U,W,U,W1)| ~ equidistant(V,W,V,W1)| U = V| W = W1 ) ))),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f69,hypothesis,(
% 281.83/41.02 between(u,v,w) ),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f70,hypothesis,(
% 281.83/41.02 equidistant(u,v,u,x) ),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f71,hypothesis,(
% 281.83/41.02 equidistant(w,v,w,x) ),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f72,negated_conjecture,(
% 281.83/41.02 v != x ),
% 281.83/41.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 281.83/41.02 fof(f73,plain,(
% 281.83/41.02 ![X0,X1]: (equidistant(X0,X1,X1,X0))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f1])).
% 281.83/41.02 fof(f78,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f4])).
% 281.83/41.02 fof(f80,plain,(
% 281.83/41.02 ![Z,Z1,V,V1]: ((![X,Y]: ((![X1,Y1]: (((((~equidistant(X,Y,X1,Y1)|~equidistant(Y,Z,Y1,Z1))|~equidistant(X,V,X1,V1))|~equidistant(Y,V,Y1,V1))|~between(X,Y,Z))|~between(X1,Y1,Z1)))|X=Y))|equidistant(Z,V,Z1,V1))),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f6])).
% 281.83/41.02 fof(f81,plain,(
% 281.83/41.02 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X5)|~equidistant(X0,X6,X2,X7)|~equidistant(X1,X6,X3,X7)|~between(X0,X1,X4)|~between(X2,X3,X5)|X0=X1|equidistant(X4,X6,X5,X7))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f80])).
% 281.83/41.02 fof(f82,plain,(
% 281.83/41.02 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f7])).
% 281.83/41.02 fof(f95,plain,(
% 281.83/41.02 ![X0,X1]: (reflection(X0,X1)=extension(X0,X1,X0,X1))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f19])).
% 281.83/41.02 fof(f96,plain,(
% 281.83/41.02 ![X0,X1]: (equidistant(X0,X1,X0,X1))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f20])).
% 281.83/41.02 fof(f109,plain,(
% 281.83/41.02 ![X0,X1]: (between(X0,X1,reflection(X0,X1)))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f31])).
% 281.83/41.02 fof(f110,plain,(
% 281.83/41.02 ![X0,X1]: (equidistant(X0,reflection(X1,X0),X1,X0))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f32])).
% 281.83/41.02 fof(f111,plain,(
% 281.83/41.02 ![X0,X1]: (~X0=X1|X1=reflection(X0,X1))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f33])).
% 281.83/41.02 fof(f113,plain,(
% 281.83/41.02 ![X0,X1]: (~X0=reflection(X1,X0)|X1=X0)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f35])).
% 281.83/41.02 fof(f117,plain,(
% 281.83/41.02 ![W,X]: ((![U,V]: (((~between(U,V,W)|~between(U,V,X))|~equidistant(V,W,V,X))|U=V))|W=X)),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f38])).
% 281.83/41.02 fof(f118,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|~equidistant(X1,X2,X1,X3)|X0=X1|X2=X3)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f117])).
% 281.83/41.02 fof(f119,plain,(
% 281.83/41.02 ![X0,X1,X2]: (~between(X0,X1,X2)|X0=X1|X2=extension(X0,X1,X1,X2))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f39])).
% 281.83/41.02 fof(f120,plain,(
% 281.83/41.02 ![U,V]: ((![W,X,Y,Z]: (~equidistant(W,X,Y,Z)|extension(U,V,W,X)=extension(U,V,Y,Z)))|U=V)),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f40])).
% 281.83/41.02 fof(f121,plain,(
% 281.83/41.02 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|extension(X4,X5,X0,X1)=extension(X4,X5,X2,X3)|X4=X5)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f120])).
% 281.83/41.02 fof(f122,plain,(
% 281.83/41.02 ![X0,X1]: (extension(X0,X1,X0,X1)=extension(X0,X1,X1,X0)|X0=X1)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f41])).
% 281.83/41.02 fof(f124,plain,(
% 281.83/41.02 ![X0,X1]: (X0=reflection(reflection(X0,X1),X1))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f43])).
% 281.83/41.02 fof(f125,plain,(
% 281.83/41.02 ![X0,X1]: (between(X0,X1,X1))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f44])).
% 281.83/41.02 fof(f128,plain,(
% 281.83/41.02 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X2,X1,X0))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f46])).
% 281.83/41.02 fof(f140,plain,(
% 281.83/41.02 ![V,W,X]: ((![U]: (~between(U,V,W)|~between(U,W,X)))|between(V,W,X))),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f53])).
% 281.83/41.02 fof(f141,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X2,X3)|between(X1,X2,X3))),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f140])).
% 281.83/41.02 fof(f142,plain,(
% 281.83/41.02 ![V,W]: ((![U,X]: ((~between(U,V,W)|~between(V,W,X))|between(U,W,X)))|V=W)),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f54])).
% 281.83/41.02 fof(f143,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X1,X2,X3)|between(X0,X2,X3)|X1=X2)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f142])).
% 281.83/41.02 fof(f157,plain,(
% 281.83/41.02 ![W,W1]: ((![U,V]: (((~between(U,V,W)|~equidistant(U,W,U,W1))|~equidistant(V,W,V,W1))|U=V))|W=W1)),
% 281.83/41.02 inference(miniscoping,[status(thm)],[f65])).
% 281.83/41.02 fof(f158,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~equidistant(X0,X2,X0,X3)|~equidistant(X1,X2,X1,X3)|X0=X1|X2=X3)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f157])).
% 281.83/41.02 fof(f165,plain,(
% 281.83/41.02 between(u,v,w)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f69])).
% 281.83/41.02 fof(f166,plain,(
% 281.83/41.02 equidistant(u,v,u,x)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f70])).
% 281.83/41.02 fof(f167,plain,(
% 281.83/41.02 equidistant(w,v,w,x)),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f71])).
% 281.83/41.02 fof(f168,plain,(
% 281.83/41.02 ~v=x),
% 281.83/41.02 inference(cnf_transformation,[status(thm)],[f72])).
% 281.83/41.02 fof(f170,plain,(
% 281.83/41.02 ![X0]: (X0=reflection(X0,X0))),
% 281.83/41.02 inference(destructive_equality_resolution,[status(thm)],[f111])).
% 281.83/41.02 fof(f212,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (X0=X1|extension(X0,X1,X2,X3)=extension(X0,X1,X1,extension(X0,X1,X2,X3)))),
% 281.83/41.02 inference(resolution,[status(thm)],[f119,f78])).
% 281.83/41.02 fof(f271,plain,(
% 281.83/41.02 ![X0]: (~between(X0,u,v)|between(X0,v,w)|u=v)),
% 281.83/41.02 inference(resolution,[status(thm)],[f143,f165])).
% 281.83/41.02 fof(f301,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (~equidistant(w,X0,w,X1)|~equidistant(X0,X2,X1,X3)|~equidistant(X0,v,X1,x)|~between(w,X0,X2)|~between(w,X1,X3)|w=X0|equidistant(X2,v,X3,x))),
% 281.83/41.02 inference(resolution,[status(thm)],[f81,f167])).
% 281.83/41.02 fof(f361,plain,(
% 281.83/41.02 ![X0,X1,X2]: (~equidistant(X0,X1,X0,X2)|~equidistant(X0,v,X0,x)|~between(w,X0,X1)|~between(w,X0,X2)|w=X0|equidistant(X1,v,X2,x))),
% 281.83/41.02 inference(resolution,[status(thm)],[f301,f96])).
% 281.83/41.02 fof(f384,plain,(
% 281.83/41.02 ![X0,X1]: (~equidistant(u,X0,u,X1)|~between(w,u,X0)|~between(w,u,X1)|w=u|equidistant(X0,v,X1,x))),
% 281.83/41.02 inference(resolution,[status(thm)],[f361,f166])).
% 281.83/41.02 fof(f391,plain,(
% 281.83/41.02 ![X0]: (~between(w,u,X0)|~between(w,u,X0)|w=u|equidistant(X0,v,X0,x))),
% 281.83/41.02 inference(resolution,[status(thm)],[f384,f96])).
% 281.83/41.02 fof(f397,plain,(
% 281.83/41.02 ![X0]: (~between(w,u,X0)|w=u|equidistant(X0,v,X0,x))),
% 281.83/41.02 inference(duplicate_literals_removal,[status(thm)],[f391])).
% 281.83/41.02 fof(f400,plain,(
% 281.83/41.02 w=u|equidistant(reflection(w,u),v,reflection(w,u),x)),
% 281.83/41.02 inference(resolution,[status(thm)],[f397,f109])).
% 281.83/41.02 fof(f1246,plain,(
% 281.83/41.02 ![X0,X1]: (X0=X1|extension(X0,X1,X1,X0)=extension(X0,X1,X1,extension(X0,X1,X0,X1))|X0=X1)),
% 281.83/41.02 inference(paramodulation,[status(thm)],[f122,f212])).
% 281.83/41.02 fof(f1266,plain,(
% 281.83/41.02 ![X0,X1]: (X0=X1|extension(X0,X1,X1,X0)=extension(X0,X1,X1,extension(X0,X1,X0,X1)))),
% 281.83/41.02 inference(duplicate_literals_removal,[status(thm)],[f1246])).
% 281.83/41.02 fof(f1530,plain,(
% 281.83/41.02 ![X0]: (~between(X0,u,v)|~between(X0,u,x)|X0=u|v=x)),
% 281.83/41.02 inference(resolution,[status(thm)],[f118,f166])).
% 281.83/41.02 fof(f1541,plain,(
% 281.83/41.02 ![X0]: (~between(X0,u,v)|~between(X0,u,x)|X0=u)),
% 281.83/41.02 inference(forward_subsumption_resolution,[status(thm)],[f1530,f168])).
% 281.83/41.02 fof(f1565,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (extension(X0,X1,X2,reflection(X3,X2))=extension(X0,X1,X3,X2)|X0=X1)),
% 281.83/41.02 inference(resolution,[status(thm)],[f121,f110])).
% 281.83/41.02 fof(f1568,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (extension(X0,X1,X2,X3)=extension(X0,X1,X3,X2)|X0=X1)),
% 281.83/41.02 inference(resolution,[status(thm)],[f121,f73])).
% 281.83/41.02 fof(f1603,plain,(
% 281.83/41.02 ![X0]: (~between(X0,u,v)|~equidistant(X0,v,X0,x)|X0=u|v=x)),
% 281.83/41.02 inference(resolution,[status(thm)],[f158,f166])).
% 281.83/41.02 fof(f1614,plain,(
% 281.83/41.02 ![X0]: (~between(X0,u,v)|~equidistant(X0,v,X0,x)|X0=u)),
% 281.83/41.02 inference(forward_subsumption_resolution,[status(thm)],[f1603,f168])).
% 281.83/41.02 fof(f1704,plain,(
% 281.83/41.02 ~between(reflection(w,u),u,v)|reflection(w,u)=u|w=u),
% 281.83/41.02 inference(resolution,[status(thm)],[f1614,f400])).
% 281.83/41.02 fof(f1707,plain,(
% 281.83/41.02 ~between(reflection(w,u),u,v)|w=u),
% 281.83/41.02 inference(forward_subsumption_resolution,[status(thm)],[f1704,f113])).
% 281.83/41.02 fof(f1882,plain,(
% 281.83/41.02 between(w,v,u)),
% 281.83/41.02 inference(resolution,[status(thm)],[f128,f165])).
% 281.83/41.02 fof(f1884,plain,(
% 281.83/41.02 ![X0,X1,X2,X3]: (between(extension(X0,X1,X2,X3),X1,X0))),
% 281.83/41.02 inference(resolution,[status(thm)],[f128,f78])).
% 281.83/41.02 fof(f1912,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,X0,X1)=u)),
% 281.83/41.02 inference(resolution,[status(thm)],[f1884,f1541])).
% 281.83/41.02 fof(f5689,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,X1,X0)=u|x=u)),
% 281.83/41.02 inference(paramodulation,[status(thm)],[f1568,f1912])).
% 281.83/41.02 fof(f8182,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,reflection(X0,X1),X1)=u|x=u|x=u)),
% 281.83/41.02 inference(paramodulation,[status(thm)],[f1565,f5689])).
% 281.83/41.02 fof(f8250,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,reflection(X0,X1),X1)=u|x=u)),
% 281.83/41.02 inference(duplicate_literals_removal,[status(thm)],[f8182])).
% 281.83/41.02 fof(f10646,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,reflection(X1,X0),X0)=u|x=u|x=u)),
% 281.83/41.02 inference(paramodulation,[status(thm)],[f1568,f8250])).
% 281.83/41.02 fof(f10659,plain,(
% 281.83/41.02 ![X0,X1]: (~between(extension(x,u,X0,X1),u,v)|extension(x,u,reflection(X1,X0),X0)=u|x=u)),
% 281.83/41.02 inference(duplicate_literals_removal,[status(thm)],[f10646])).
% 281.83/41.02 fof(f13737,plain,(
% 281.83/41.02 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X1,X2,reflection(X0,X2)))),
% 281.83/41.02 inference(resolution,[status(thm)],[f141,f109])).
% 281.83/41.02 fof(f19668,plain,(
% 281.83/41.02 ![X0,X1]: (X0=X1|extension(X0,X1,X1,X0)=extension(X0,X1,X1,reflection(X0,X1)))),
% 281.83/41.02 inference(forward_demodulation,[status(thm)],[f95,f1266])).
% 281.83/41.02 fof(f19682,plain,(
% 281.83/41.02 ~between(extension(x,u,u,x),u,v)|extension(x,u,reflection(reflection(x,u),u),u)=u|x=u|x=u),
% 281.83/41.02 inference(paramodulation,[status(thm)],[f19668,f10659])).
% 281.83/41.02 fof(f19797,plain,(
% 281.83/41.02 ~between(extension(x,u,u,x),u,v)|extension(x,u,x,u)=u|x=u|x=u),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f124,f19682])).
% 281.83/41.06 fof(f19798,plain,(
% 281.83/41.06 ~between(extension(x,u,u,x),u,v)|reflection(x,u)=u|x=u|x=u),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f95,f19797])).
% 281.83/41.06 fof(f19799,plain,(
% 281.83/41.06 ~between(extension(x,u,u,x),u,v)|reflection(x,u)=u|x=u),
% 281.83/41.06 inference(duplicate_literals_removal,[status(thm)],[f19798])).
% 281.83/41.06 fof(f19800,plain,(
% 281.83/41.06 ~between(extension(x,u,u,x),u,v)|x=u),
% 281.83/41.06 inference(forward_subsumption_resolution,[status(thm)],[f19799,f113])).
% 281.83/41.06 fof(f25894,plain,(
% 281.83/41.06 between(v,u,reflection(w,u))),
% 281.83/41.06 inference(resolution,[status(thm)],[f13737,f1882])).
% 281.83/41.06 fof(f26100,plain,(
% 281.83/41.06 between(reflection(w,u),u,v)),
% 281.83/41.06 inference(resolution,[status(thm)],[f25894,f128])).
% 281.83/41.06 fof(f26158,plain,(
% 281.83/41.06 w=u),
% 281.83/41.06 inference(backward_subsumption_resolution,[status(thm)],[f1707,f26100])).
% 281.83/41.06 fof(f26160,plain,(
% 281.83/41.06 between(reflection(w,u),v,w)|u=v),
% 281.83/41.06 inference(resolution,[status(thm)],[f26100,f271])).
% 281.83/41.06 fof(f29120,plain,(
% 281.83/41.06 between(reflection(w,u),v,u)|u=v),
% 281.83/41.06 inference(backward_demodulation,[status(thm)],[f26158,f26160])).
% 281.83/41.06 fof(f29323,plain,(
% 281.83/41.06 between(reflection(u,u),v,u)|u=v),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f26158,f29120])).
% 281.83/41.06 fof(f29324,plain,(
% 281.83/41.06 between(u,v,u)|u=v),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f170,f29323])).
% 281.83/41.06 fof(f29325,plain,(
% 281.83/41.06 u=v),
% 281.83/41.06 inference(forward_subsumption_resolution,[status(thm)],[f29324,f82])).
% 281.83/41.06 fof(f29695,plain,(
% 281.83/41.06 ~between(extension(x,u,u,x),u,v)|x=v),
% 281.83/41.06 inference(backward_demodulation,[status(thm)],[f29325,f19800])).
% 281.83/41.06 fof(f29898,plain,(
% 281.83/41.06 ~between(extension(x,v,u,x),u,v)|x=v),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f29325,f29695])).
% 281.83/41.06 fof(f29899,plain,(
% 281.83/41.06 ~between(extension(x,v,v,x),u,v)|x=v),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f29325,f29898])).
% 281.83/41.06 fof(f29900,plain,(
% 281.83/41.06 ~between(extension(x,v,v,x),v,v)|x=v),
% 281.83/41.06 inference(forward_demodulation,[status(thm)],[f29325,f29899])).
% 281.83/41.06 fof(f29901,plain,(
% 281.83/41.06 x=v),
% 281.83/41.06 inference(forward_subsumption_resolution,[status(thm)],[f29900,f125])).
% 281.83/41.06 fof(f30325,plain,(
% 281.83/41.06 $false),
% 281.83/41.06 inference(forward_subsumption_resolution,[status(thm)],[f29901,f168])).
% 281.83/41.06 % SZS output end CNFRefutation for theBenchmark.p
% 254.81/41.12 % Elapsed time: 35.725160 seconds
% 254.81/41.12 % CPU time: 283.218392 seconds
% 254.81/41.12 % Total memory used: 516.830 MB
% 254.81/41.12 % Net memory used: 440.619 MB
%------------------------------------------------------------------------------