%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO620+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:44 PM UTC 2026
% Result : Theorem 0.14s 0.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO620+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n004.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Sun Sep 20 17:59:06 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.59 % Drodi V4.1.1
% 0.14/0.81 % Refutation found
% 0.14/0.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.81 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.81 fof(f1,axiom,(
% 0.14/0.81 (! [A,B,C] :( coll(A,B,C)=> coll(A,C,B) ) )),
% 0.14/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.81 fof(f2,axiom,(
% 0.14/0.81 (! [A,B,C] :( coll(A,B,C)=> coll(B,A,C) ) )),
% 0.14/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.81 fof(f3,axiom,(
% 0.14/0.81 (! [A,B,C,D] :( ( coll(A,B,C)& coll(A,B,D) )=> coll(C,D,A) ) )),
% 0.14/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.81 fof(f95,conjecture,(
% 0.14/0.81 (! [A,B,C,O,I,E,J,L] :( ( eqangle(O,A,A,B,O,A,A,C)& eqangle(O,B,B,C,O,B,B,A)& eqangle(O,C,C,A,O,C,C,B)& perp(I,C,A,O)& coll(I,A,O)& perp(A,O,A,E)& perp(J,C,A,E)& coll(J,A,E)& perp(L,C,B,O)& coll(L,B,O) )=> coll(I,L,J) ) )),
% 0.14/0.81 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.81 fof(f96,negated_conjecture,(
% 0.14/0.81 ~((! [A,B,C,O,I,E,J,L] :( ( eqangle(O,A,A,B,O,A,A,C)& eqangle(O,B,B,C,O,B,B,A)& eqangle(O,C,C,A,O,C,C,B)& perp(I,C,A,O)& coll(I,A,O)& perp(A,O,A,E)& perp(J,C,A,E)& coll(J,A,E)& perp(L,C,B,O)& coll(L,B,O) )=> coll(I,L,J) ) ))),
% 0.14/0.81 inference(negated_conjecture,[status(cth)],[f95])).
% 0.14/0.81 fof(f97,plain,(
% 0.14/0.81 ![A,B,C]: (~coll(A,B,C)|coll(A,C,B))),
% 0.14/0.81 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.14/0.81 fof(f98,plain,(
% 0.14/0.81 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X0,X2,X1))),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f97])).
% 0.14/0.81 fof(f99,plain,(
% 0.14/0.81 ![A,B,C]: (~coll(A,B,C)|coll(B,A,C))),
% 0.14/0.81 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.81 fof(f100,plain,(
% 0.14/0.81 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X1,X0,X2))),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f99])).
% 0.14/0.81 fof(f101,plain,(
% 0.14/0.81 ![A,B,C,D]: ((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A))),
% 0.14/0.81 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/0.81 fof(f102,plain,(
% 0.14/0.81 ![A,C,D]: ((![B]: (~coll(A,B,C)|~coll(A,B,D)))|coll(C,D,A))),
% 0.14/0.81 inference(miniscoping,[status(thm)],[f101])).
% 0.14/0.81 fof(f103,plain,(
% 0.14/0.81 ![X0,X1,X2,X3]: (~coll(X0,X1,X2)|~coll(X0,X1,X3)|coll(X2,X3,X0))),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f102])).
% 0.14/0.81 fof(f369,plain,(
% 0.14/0.81 (?[A,B,C,O,I,E,J,L]: ((((((((((eqangle(O,A,A,B,O,A,A,C)&eqangle(O,B,B,C,O,B,B,A))&eqangle(O,C,C,A,O,C,C,B))&perp(I,C,A,O))&coll(I,A,O))&perp(A,O,A,E))&perp(J,C,A,E))&coll(J,A,E))&perp(L,C,B,O))&coll(L,B,O))&~coll(I,L,J)))),
% 0.14/0.81 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.14/0.81 fof(f370,plain,(
% 0.14/0.81 ?[I,J,L]: ((?[B,O]: ((?[C]: ((?[A,E]: (((((((eqangle(O,A,A,B,O,A,A,C)&eqangle(O,B,B,C,O,B,B,A))&eqangle(O,C,C,A,O,C,C,B))&perp(I,C,A,O))&coll(I,A,O))&perp(A,O,A,E))&perp(J,C,A,E))&coll(J,A,E)))&perp(L,C,B,O)))&coll(L,B,O)))&~coll(I,L,J))),
% 0.14/0.81 inference(miniscoping,[status(thm)],[f369])).
% 0.14/0.81 fof(f371,plain,(
% 0.14/0.81 ((((((((((eqangle(sK24_skl,sK26_skl,sK26_skl,sK23_skl,sK24_skl,sK26_skl,sK26_skl,sK25_skl)&eqangle(sK24_skl,sK23_skl,sK23_skl,sK25_skl,sK24_skl,sK23_skl,sK23_skl,sK26_skl))&eqangle(sK24_skl,sK25_skl,sK25_skl,sK26_skl,sK24_skl,sK25_skl,sK25_skl,sK23_skl))&perp(sK20_skl,sK25_skl,sK26_skl,sK24_skl))&coll(sK20_skl,sK26_skl,sK24_skl))&perp(sK26_skl,sK24_skl,sK26_skl,sK27_skl))&perp(sK21_skl,sK25_skl,sK26_skl,sK27_skl))&coll(sK21_skl,sK26_skl,sK27_skl))&perp(sK22_skl,sK25_skl,sK23_skl,sK24_skl))&coll(sK22_skl,sK23_skl,sK24_skl))&~coll(sK20_skl,sK22_skl,sK21_skl))),
% 0.14/0.81 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl]),skolemize(I,sK20_skl),skolemize(J,sK21_skl),skolemize(L,sK22_skl),skolemize(B,sK23_skl),skolemize(O,sK24_skl),skolemize(C,sK25_skl),skolemize(A,sK26_skl),skolemize(E,sK27_skl)],[f370])).
% 0.14/0.81 fof(f376,plain,(
% 0.14/0.81 coll(sK20_skl,sK26_skl,sK24_skl)),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f371])).
% 0.14/0.81 fof(f379,plain,(
% 0.14/0.81 coll(sK21_skl,sK26_skl,sK27_skl)),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f371])).
% 0.14/0.81 fof(f381,plain,(
% 0.14/0.81 coll(sK22_skl,sK23_skl,sK24_skl)),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f371])).
% 0.14/0.81 fof(f382,plain,(
% 0.14/0.81 ~coll(sK20_skl,sK22_skl,sK21_skl)),
% 0.14/0.81 inference(cnf_transformation,[status(thm)],[f371])).
% 0.14/0.81 fof(f383,plain,(
% 0.14/0.81 coll(sK22_skl,sK24_skl,sK23_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f98,f381])).
% 0.14/0.81 fof(f384,plain,(
% 0.14/0.81 coll(sK21_skl,sK27_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f98,f379])).
% 0.14/0.81 fof(f385,plain,(
% 0.14/0.81 coll(sK20_skl,sK24_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f98,f376])).
% 0.14/0.81 fof(f389,plain,(
% 0.14/0.81 coll(sK24_skl,sK22_skl,sK23_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f100,f383])).
% 0.14/0.81 fof(f390,plain,(
% 0.14/0.81 coll(sK23_skl,sK22_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f100,f381])).
% 0.14/0.81 fof(f391,plain,(
% 0.14/0.81 coll(sK27_skl,sK21_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f100,f384])).
% 0.14/0.81 fof(f394,plain,(
% 0.14/0.81 coll(sK26_skl,sK20_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f100,f376])).
% 0.14/0.81 fof(f396,plain,(
% 0.14/0.81 coll(sK24_skl,sK23_skl,sK22_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f389,f98])).
% 0.14/0.81 fof(f400,plain,(
% 0.14/0.81 coll(sK27_skl,sK26_skl,sK21_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f391,f98])).
% 0.14/0.81 fof(f406,plain,(
% 0.14/0.81 coll(sK26_skl,sK24_skl,sK20_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f394,f98])).
% 0.14/0.81 fof(f409,plain,(
% 0.14/0.81 ![X0]: (~coll(sK26_skl,sK20_skl,X0)|coll(X0,sK24_skl,sK26_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f394])).
% 0.14/0.81 fof(f411,plain,(
% 0.14/0.81 ![X0]: (~coll(sK27_skl,sK21_skl,X0)|coll(X0,sK26_skl,sK27_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f391])).
% 0.14/0.81 fof(f412,plain,(
% 0.14/0.81 ![X0]: (~coll(sK23_skl,sK22_skl,X0)|coll(X0,sK24_skl,sK23_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f390])).
% 0.14/0.81 fof(f413,plain,(
% 0.14/0.81 ![X0]: (~coll(sK24_skl,sK23_skl,X0)|coll(X0,sK22_skl,sK24_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f396])).
% 0.14/0.81 fof(f420,plain,(
% 0.14/0.81 ![X0]: (~coll(sK20_skl,sK24_skl,X0)|coll(X0,sK26_skl,sK20_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f385])).
% 0.14/0.81 fof(f423,plain,(
% 0.14/0.81 ![X0]: (~coll(sK21_skl,X0,sK20_skl)|~coll(sK21_skl,X0,sK22_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f103,f382])).
% 0.14/0.81 fof(f432,plain,(
% 0.14/0.81 ![X0]: (~coll(sK27_skl,sK26_skl,X0)|coll(X0,sK21_skl,sK27_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f400,f103])).
% 0.14/0.81 fof(f441,plain,(
% 0.14/0.81 ![X0]: (~coll(sK26_skl,sK24_skl,X0)|coll(X0,sK20_skl,sK26_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f406,f103])).
% 0.14/0.81 fof(f455,plain,(
% 0.14/0.81 coll(sK24_skl,sK24_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f409,f394])).
% 0.14/0.81 fof(f457,plain,(
% 0.14/0.81 ![X0]: (~coll(sK24_skl,sK24_skl,X0)|coll(X0,sK26_skl,sK24_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f455,f103])).
% 0.14/0.81 fof(f606,plain,(
% 0.14/0.81 coll(sK26_skl,sK26_skl,sK27_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f411,f391])).
% 0.14/0.81 fof(f608,plain,(
% 0.14/0.81 ![X0]: (~coll(sK26_skl,sK26_skl,X0)|coll(X0,sK27_skl,sK26_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f606,f103])).
% 0.14/0.81 fof(f617,plain,(
% 0.14/0.81 coll(sK24_skl,sK24_skl,sK23_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f412,f390])).
% 0.14/0.81 fof(f623,plain,(
% 0.14/0.81 coll(sK24_skl,sK23_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f617,f98])).
% 0.14/0.81 fof(f630,plain,(
% 0.14/0.81 coll(sK24_skl,sK22_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f413,f623])).
% 0.14/0.81 fof(f635,plain,(
% 0.14/0.81 coll(sK24_skl,sK24_skl,sK22_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f630,f98])).
% 0.14/0.81 fof(f750,plain,(
% 0.14/0.81 coll(sK26_skl,sK26_skl,sK20_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f420,f385])).
% 0.14/0.81 fof(f843,plain,(
% 0.14/0.81 coll(sK22_skl,sK26_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f457,f635])).
% 0.14/0.81 fof(f859,plain,(
% 0.14/0.81 coll(sK26_skl,sK22_skl,sK24_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f843,f100])).
% 0.14/0.81 fof(f866,plain,(
% 0.14/0.81 coll(sK26_skl,sK24_skl,sK22_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f859,f98])).
% 0.14/0.81 fof(f883,plain,(
% 0.14/0.81 coll(sK22_skl,sK20_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f866,f441])).
% 0.14/0.81 fof(f1706,plain,(
% 0.14/0.81 coll(sK20_skl,sK27_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f608,f750])).
% 0.14/0.81 fof(f1711,plain,(
% 0.14/0.81 ![X0,X1]: (coll(X0,sK27_skl,sK26_skl)|~coll(X0,X1,sK26_skl)|~coll(X0,X1,sK26_skl))),
% 0.14/0.81 inference(resolution,[status(thm)],[f608,f103])).
% 0.14/0.81 fof(f1712,plain,(
% 0.14/0.81 ![X0,X1]: (coll(X0,sK27_skl,sK26_skl)|~coll(X0,X1,sK26_skl))),
% 0.14/0.81 inference(duplicate_literals_removal,[status(thm)],[f1711])).
% 0.14/0.81 fof(f1719,plain,(
% 0.14/0.81 coll(sK27_skl,sK20_skl,sK26_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f1706,f100])).
% 0.14/0.81 fof(f1736,plain,(
% 0.14/0.81 coll(sK27_skl,sK26_skl,sK20_skl)),
% 0.14/0.81 inference(resolution,[status(thm)],[f1719,f98])).
% 0.14/0.81 fof(f1767,plain,(
% 0.14/0.82 coll(sK20_skl,sK21_skl,sK27_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f1736,f432])).
% 0.14/0.82 fof(f1855,plain,(
% 0.14/0.82 coll(sK21_skl,sK20_skl,sK27_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f1767,f100])).
% 0.14/0.82 fof(f1947,plain,(
% 0.14/0.82 coll(sK21_skl,sK27_skl,sK20_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f1855,f98])).
% 0.14/0.82 fof(f2531,plain,(
% 0.14/0.82 coll(sK22_skl,sK27_skl,sK26_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f1712,f883])).
% 0.14/0.82 fof(f2663,plain,(
% 0.14/0.82 coll(sK27_skl,sK22_skl,sK26_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f2531,f100])).
% 0.14/0.82 fof(f2709,plain,(
% 0.14/0.82 coll(sK27_skl,sK26_skl,sK22_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f2663,f98])).
% 0.14/0.82 fof(f2758,plain,(
% 0.14/0.82 coll(sK22_skl,sK21_skl,sK27_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f2709,f432])).
% 0.14/0.82 fof(f3079,plain,(
% 0.14/0.82 coll(sK21_skl,sK22_skl,sK27_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f2758,f100])).
% 0.14/0.82 fof(f3199,plain,(
% 0.14/0.82 coll(sK21_skl,sK27_skl,sK22_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f3079,f98])).
% 0.14/0.82 fof(f3326,plain,(
% 0.14/0.82 ~coll(sK21_skl,sK27_skl,sK20_skl)),
% 0.14/0.82 inference(resolution,[status(thm)],[f3199,f423])).
% 0.14/0.82 fof(f3336,plain,(
% 0.14/0.82 $false),
% 0.14/0.82 inference(forward_subsumption_resolution,[status(thm)],[f3326,f1947])).
% 0.14/0.82 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.85 % Elapsed time: 0.247936 seconds
% 0.14/0.85 % CPU time: 1.768198 seconds
% 0.14/0.85 % Total memory used: 104.097 MB
% 0.14/0.85 % Net memory used: 102.573 MB
%------------------------------------------------------------------------------