%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO006-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:31 PM UTC 2026
% Result : Unsatisfiable 4.46s 1.18s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GEO006-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n016.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:20:21 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 4.46/1.18 % Refutation found
% 4.46/1.18 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.46/1.18 % SZS output start CNFRefutation for theBenchmark
% 4.46/1.18 fof(f1,axiom,(
% 4.46/1.18 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f2,axiom,(
% 4.46/1.18 (![X,Y,V,Z]: (( ~ between(X,Y,V)| ~ between(Y,Z,V)| between(X,Y,Z) ) ))),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f3,axiom,(
% 4.46/1.18 (![X,Y,Z,V]: (( ~ between(X,Y,Z)| ~ between(X,Y,V)| X = Y| between(X,Z,V)| between(X,V,Z) ) ))),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f7,axiom,(
% 4.46/1.18 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(X,outer_pasch(W,X,Y,Z,V),Y) ) ))),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f8,axiom,(
% 4.46/1.18 (![X,W,V,Y,Z]: (( ~ between(X,W,V)| ~ between(Y,V,Z)| between(Z,W,outer_pasch(W,X,Y,Z,V)) ) ))),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f21,hypothesis,(
% 4.46/1.18 a != c ),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f23,hypothesis,(
% 4.46/1.18 c != d ),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f24,hypothesis,(
% 4.46/1.18 between(a,c,d) ),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f25,negated_conjecture,(
% 4.46/1.18 ( between(c,a,d)| between(a,d,c) ) ),
% 4.46/1.18 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.46/1.18 fof(f26,plain,(
% 4.46/1.18 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f1])).
% 4.46/1.18 fof(f27,plain,(
% 4.46/1.18 ![X,Y,Z]: ((![V]: (~between(X,Y,V)|~between(Y,Z,V)))|between(X,Y,Z))),
% 4.46/1.18 inference(miniscoping,[status(thm)],[f2])).
% 4.46/1.18 fof(f28,plain,(
% 4.46/1.18 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X1,X3,X2)|between(X0,X1,X3))),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f27])).
% 4.46/1.18 fof(f29,plain,(
% 4.46/1.18 ![X,Z,V]: (((![Y]: ((~between(X,Y,Z)|~between(X,Y,V))|X=Y))|between(X,Z,V))|between(X,V,Z))),
% 4.46/1.18 inference(miniscoping,[status(thm)],[f3])).
% 4.46/1.18 fof(f30,plain,(
% 4.46/1.18 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|X0=X1|between(X0,X2,X3)|between(X0,X3,X2))),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f29])).
% 4.46/1.18 fof(f36,plain,(
% 4.46/1.18 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X0,outer_pasch(X1,X0,X3,X4,X2),X3))),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f7])).
% 4.46/1.18 fof(f37,plain,(
% 4.46/1.18 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X2,X4)|between(X4,X1,outer_pasch(X1,X0,X3,X4,X2)))),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f8])).
% 4.46/1.18 fof(f52,plain,(
% 4.46/1.18 ~a=c),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f21])).
% 4.46/1.18 fof(f54,plain,(
% 4.46/1.18 ~c=d),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f23])).
% 4.46/1.18 fof(f55,plain,(
% 4.46/1.18 between(a,c,d)),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f24])).
% 4.46/1.18 fof(f56,plain,(
% 4.46/1.18 between(c,a,d)|between(a,d,c)),
% 4.46/1.18 inference(cnf_transformation,[status(thm)],[f25])).
% 4.46/1.18 fof(f57,plain,(
% 4.46/1.18 ![X0,X1,X2]: (~between(X0,X1,X2)|~between(X1,X0,X2)|X0=X1)),
% 4.46/1.18 inference(resolution,[status(thm)],[f28,f26])).
% 4.46/1.18 fof(f58,plain,(
% 4.46/1.18 ~between(c,a,d)|c=a),
% 4.46/1.18 inference(resolution,[status(thm)],[f57,f55])).
% 4.46/1.18 fof(f61,plain,(
% 4.46/1.18 ~between(c,a,d)),
% 4.46/1.18 inference(forward_subsumption_resolution,[status(thm)],[f58,f52])).
% 4.46/1.19 fof(f63,plain,(
% 4.46/1.19 between(a,d,c)),
% 4.46/1.19 inference(backward_subsumption_resolution,[status(thm)],[f56,f61])).
% 4.46/1.19 fof(f79,plain,(
% 4.46/1.19 ![X0]: (~between(a,c,X0)|a=c|between(a,X0,d)|between(a,d,X0))),
% 4.46/1.19 inference(resolution,[status(thm)],[f30,f55])).
% 4.46/1.19 fof(f82,plain,(
% 4.46/1.19 ![X0]: (~between(a,c,X0)|between(a,X0,d)|between(a,d,X0))),
% 4.46/1.19 inference(forward_subsumption_resolution,[status(thm)],[f79,f52])).
% 4.46/1.19 fof(f127,plain,(
% 4.46/1.19 between(a,d,d)|between(a,d,d)),
% 4.46/1.19 inference(resolution,[status(thm)],[f82,f55])).
% 4.46/1.19 fof(f129,plain,(
% 4.46/1.19 between(a,d,d)),
% 4.46/1.19 inference(duplicate_literals_removal,[status(thm)],[f127])).
% 4.46/1.19 fof(f225,plain,(
% 4.46/1.19 ![X0,X1]: (~between(X0,X1,d)|between(X0,outer_pasch(X1,X0,a,d,d),a))),
% 4.46/1.19 inference(resolution,[status(thm)],[f36,f129])).
% 4.46/1.19 fof(f226,plain,(
% 4.46/1.19 ![X0,X1]: (~between(X0,X1,d)|between(X0,outer_pasch(X1,X0,a,c,d),a))),
% 4.46/1.19 inference(resolution,[status(thm)],[f36,f63])).
% 4.46/1.19 fof(f231,plain,(
% 4.46/1.19 between(a,outer_pasch(d,a,a,c,d),a)),
% 4.46/1.19 inference(resolution,[status(thm)],[f226,f129])).
% 4.46/1.19 fof(f247,plain,(
% 4.77/1.21 a=outer_pasch(d,a,a,c,d)),
% 4.77/1.21 inference(resolution,[status(thm)],[f231,f26])).
% 4.77/1.21 fof(f289,plain,(
% 4.77/1.21 between(a,outer_pasch(c,a,a,d,d),a)),
% 4.77/1.21 inference(resolution,[status(thm)],[f225,f55])).
% 4.77/1.21 fof(f319,plain,(
% 4.77/1.21 a=outer_pasch(c,a,a,d,d)),
% 4.77/1.21 inference(resolution,[status(thm)],[f289,f26])).
% 4.77/1.21 fof(f575,plain,(
% 4.77/1.21 ![X0,X1]: (~between(X0,X1,d)|between(d,X1,outer_pasch(X1,X0,a,d,d)))),
% 4.77/1.21 inference(resolution,[status(thm)],[f37,f129])).
% 4.77/1.21 fof(f576,plain,(
% 4.77/1.21 ![X0,X1]: (~between(X0,X1,d)|between(c,X1,outer_pasch(X1,X0,a,c,d)))),
% 4.77/1.21 inference(resolution,[status(thm)],[f37,f63])).
% 4.77/1.21 fof(f633,plain,(
% 4.77/1.21 between(c,d,outer_pasch(d,a,a,c,d))),
% 4.77/1.21 inference(resolution,[status(thm)],[f576,f129])).
% 4.77/1.21 fof(f636,plain,(
% 4.77/1.21 between(c,d,a)),
% 4.77/1.21 inference(forward_demodulation,[status(thm)],[f247,f633])).
% 4.77/1.21 fof(f659,plain,(
% 4.77/1.21 ~between(d,c,a)|d=c),
% 4.77/1.21 inference(resolution,[status(thm)],[f636,f57])).
% 4.77/1.21 fof(f666,plain,(
% 4.77/1.21 ~between(d,c,a)),
% 4.77/1.21 inference(forward_subsumption_resolution,[status(thm)],[f659,f54])).
% 4.77/1.21 fof(f906,plain,(
% 4.77/1.21 between(d,c,outer_pasch(c,a,a,d,d))),
% 4.77/1.21 inference(resolution,[status(thm)],[f575,f55])).
% 4.77/1.21 fof(f909,plain,(
% 4.77/1.21 between(d,c,a)),
% 4.77/1.21 inference(forward_demodulation,[status(thm)],[f319,f906])).
% 4.77/1.21 fof(f910,plain,(
% 4.77/1.21 $false),
% 4.77/1.21 inference(forward_subsumption_resolution,[status(thm)],[f909,f666])).
% 4.77/1.21 % SZS output end CNFRefutation for theBenchmark.p
% 1.10/1.23 % Elapsed time: 0.765637 seconds
% 1.10/1.23 % CPU time: 5.590422 seconds
% 1.10/1.23 % Total memory used: 100.949 MB
% 1.10/1.23 % Net memory used: 96.771 MB
%------------------------------------------------------------------------------