%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO579+1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:40 PM UTC 2026
% Result : Theorem 1.34s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO579+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n002.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 17:41:32 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 1.34/0.67 % Refutation found
% 1.34/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.34/0.67 % SZS output start CNFRefutation for theBenchmark
% 1.34/0.67 fof(f1,axiom,(
% 1.34/0.67 (! [A,B,C] :( coll(A,B,C)=> coll(A,C,B) ) )),
% 1.34/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.67 fof(f2,axiom,(
% 1.34/0.67 (! [A,B,C] :( coll(A,B,C)=> coll(B,A,C) ) )),
% 1.34/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.67 fof(f3,axiom,(
% 1.34/0.67 (! [A,B,C,D] :( ( coll(A,B,C)& coll(A,B,D) )=> coll(C,D,A) ) )),
% 1.34/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.67 fof(f95,conjecture,(
% 1.34/0.67 (! [A,B,C,I,Y,L,X] :( ( eqangle(I,A,A,B,I,A,A,C)& eqangle(I,B,B,C,I,B,B,A)& eqangle(I,C,C,A,I,C,C,B)& perp(Y,I,A,C)& coll(Y,A,C)& perp(L,I,B,C)& coll(L,B,C)& perp(X,B,A,I)& coll(X,A,I) )=> coll(X,Y,L) ) )),
% 1.34/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.34/0.67 fof(f96,negated_conjecture,(
% 1.34/0.67 ~((! [A,B,C,I,Y,L,X] :( ( eqangle(I,A,A,B,I,A,A,C)& eqangle(I,B,B,C,I,B,B,A)& eqangle(I,C,C,A,I,C,C,B)& perp(Y,I,A,C)& coll(Y,A,C)& perp(L,I,B,C)& coll(L,B,C)& perp(X,B,A,I)& coll(X,A,I) )=> coll(X,Y,L) ) ))),
% 1.34/0.67 inference(negated_conjecture,[status(cth)],[f95])).
% 1.34/0.67 fof(f97,plain,(
% 1.34/0.67 ![A,B,C]: (~coll(A,B,C)|coll(A,C,B))),
% 1.34/0.67 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 1.34/0.67 fof(f98,plain,(
% 1.34/0.67 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X0,X2,X1))),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f97])).
% 1.34/0.67 fof(f99,plain,(
% 1.34/0.67 ![A,B,C]: (~coll(A,B,C)|coll(B,A,C))),
% 1.34/0.67 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 1.34/0.67 fof(f100,plain,(
% 1.34/0.67 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X1,X0,X2))),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f99])).
% 1.34/0.67 fof(f101,plain,(
% 1.34/0.67 ![A,B,C,D]: ((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A))),
% 1.34/0.67 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 1.34/0.67 fof(f102,plain,(
% 1.34/0.67 ![A,C,D]: ((![B]: (~coll(A,B,C)|~coll(A,B,D)))|coll(C,D,A))),
% 1.34/0.67 inference(miniscoping,[status(thm)],[f101])).
% 1.34/0.67 fof(f103,plain,(
% 1.34/0.67 ![X0,X1,X2,X3]: (~coll(X0,X1,X2)|~coll(X0,X1,X3)|coll(X2,X3,X0))),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f102])).
% 1.34/0.67 fof(f369,plain,(
% 1.34/0.67 (?[A,B,C,I,Y,L,X]: (((((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&perp(Y,I,A,C))&coll(Y,A,C))&perp(L,I,B,C))&coll(L,B,C))&perp(X,B,A,I))&coll(X,A,I))&~coll(X,Y,L)))),
% 1.34/0.67 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 1.34/0.67 fof(f370,plain,(
% 1.34/0.67 ?[Y,L,X]: ((?[A,I]: ((?[B]: ((?[C]: ((((((eqangle(I,A,A,B,I,A,A,C)&eqangle(I,B,B,C,I,B,B,A))&eqangle(I,C,C,A,I,C,C,B))&perp(Y,I,A,C))&coll(Y,A,C))&perp(L,I,B,C))&coll(L,B,C)))&perp(X,B,A,I)))&coll(X,A,I)))&~coll(X,Y,L))),
% 1.34/0.67 inference(miniscoping,[status(thm)],[f369])).
% 1.34/0.67 fof(f371,plain,(
% 1.34/0.67 (((((((((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))&eqangle(sK24_skl,sK26_skl,sK26_skl,sK23_skl,sK24_skl,sK26_skl,sK26_skl,sK25_skl))&perp(sK20_skl,sK24_skl,sK23_skl,sK26_skl))&coll(sK20_skl,sK23_skl,sK26_skl))&perp(sK21_skl,sK24_skl,sK25_skl,sK26_skl))&coll(sK21_skl,sK25_skl,sK26_skl))&perp(sK22_skl,sK25_skl,sK23_skl,sK24_skl))&coll(sK22_skl,sK23_skl,sK24_skl))&~coll(sK22_skl,sK20_skl,sK21_skl))),
% 1.34/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(Y,sK20_skl),skolemize(L,sK21_skl),skolemize(X,sK22_skl),skolemize(A,sK23_skl),skolemize(I,sK24_skl),skolemize(B,sK25_skl),skolemize(C,sK26_skl)],[f370])).
% 1.34/0.67 fof(f376,plain,(
% 1.34/0.67 coll(sK20_skl,sK23_skl,sK26_skl)),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f371])).
% 1.34/0.67 fof(f378,plain,(
% 1.34/0.67 coll(sK21_skl,sK25_skl,sK26_skl)),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f371])).
% 1.34/0.67 fof(f380,plain,(
% 1.34/0.67 coll(sK22_skl,sK23_skl,sK24_skl)),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f371])).
% 1.34/0.67 fof(f381,plain,(
% 1.34/0.67 ~coll(sK22_skl,sK20_skl,sK21_skl)),
% 1.34/0.67 inference(cnf_transformation,[status(thm)],[f371])).
% 1.34/0.67 fof(f382,plain,(
% 1.34/0.67 coll(sK22_skl,sK24_skl,sK23_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f98,f380])).
% 1.34/0.67 fof(f384,plain,(
% 1.34/0.67 coll(sK20_skl,sK26_skl,sK23_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f98,f376])).
% 1.34/0.67 fof(f391,plain,(
% 1.34/0.67 coll(sK25_skl,sK21_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f100,f378])).
% 1.34/0.67 fof(f392,plain,(
% 1.34/0.67 coll(sK26_skl,sK20_skl,sK23_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f100,f384])).
% 1.34/0.67 fof(f401,plain,(
% 1.34/0.67 coll(sK25_skl,sK26_skl,sK21_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f391,f98])).
% 1.34/0.67 fof(f403,plain,(
% 1.34/0.67 coll(sK26_skl,sK23_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f392,f98])).
% 1.34/0.67 fof(f404,plain,(
% 1.34/0.67 ![X0]: (~coll(sK25_skl,sK21_skl,X0)|coll(X0,sK26_skl,sK25_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f103,f391])).
% 1.34/0.67 fof(f405,plain,(
% 1.34/0.67 ![X0]: (~coll(sK26_skl,sK20_skl,X0)|coll(X0,sK23_skl,sK26_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f103,f392])).
% 1.34/0.67 fof(f409,plain,(
% 1.34/0.67 ![X0]: (~coll(sK22_skl,sK24_skl,X0)|coll(X0,sK23_skl,sK22_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f103,f382])).
% 1.34/0.67 fof(f414,plain,(
% 1.34/0.67 ![X0]: (~coll(sK20_skl,sK23_skl,X0)|coll(X0,sK26_skl,sK20_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f103,f376])).
% 1.34/0.67 fof(f428,plain,(
% 1.34/0.67 ![X0]: (~coll(sK25_skl,sK26_skl,X0)|coll(X0,sK21_skl,sK25_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f401,f103])).
% 1.34/0.67 fof(f431,plain,(
% 1.34/0.67 ![X0]: (~coll(sK26_skl,sK23_skl,X0)|coll(X0,sK20_skl,sK26_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f403,f103])).
% 1.34/0.67 fof(f442,plain,(
% 1.34/0.67 coll(sK26_skl,sK26_skl,sK25_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f404,f391])).
% 1.34/0.67 fof(f443,plain,(
% 1.34/0.67 ![X0]: (~coll(sK26_skl,sK26_skl,X0)|coll(X0,sK25_skl,sK26_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f442,f103])).
% 1.34/0.67 fof(f522,plain,(
% 1.34/0.67 coll(sK23_skl,sK23_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f405,f392])).
% 1.34/0.67 fof(f523,plain,(
% 1.34/0.67 ![X0]: (~coll(sK23_skl,sK23_skl,X0)|coll(X0,sK26_skl,sK23_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f522,f103])).
% 1.34/0.67 fof(f570,plain,(
% 1.34/0.67 coll(sK23_skl,sK23_skl,sK22_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f409,f382])).
% 1.34/0.67 fof(f611,plain,(
% 1.34/0.67 coll(sK26_skl,sK26_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f414,f376])).
% 1.34/0.67 fof(f746,plain,(
% 1.34/0.67 coll(sK20_skl,sK25_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f443,f611])).
% 1.34/0.67 fof(f763,plain,(
% 1.34/0.67 coll(sK25_skl,sK20_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f746,f100])).
% 1.34/0.67 fof(f764,plain,(
% 1.34/0.67 coll(sK20_skl,sK26_skl,sK25_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f746,f98])).
% 1.34/0.67 fof(f774,plain,(
% 1.34/0.67 coll(sK25_skl,sK26_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f763,f98])).
% 1.34/0.67 fof(f776,plain,(
% 1.34/0.67 ![X0]: (~coll(sK20_skl,sK26_skl,X0)|coll(X0,sK25_skl,sK20_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f764,f103])).
% 1.34/0.67 fof(f790,plain,(
% 1.34/0.67 coll(sK20_skl,sK21_skl,sK25_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f774,f428])).
% 1.34/0.67 fof(f813,plain,(
% 1.34/0.67 coll(sK20_skl,sK25_skl,sK21_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f790,f98])).
% 1.34/0.67 fof(f843,plain,(
% 1.34/0.67 ![X0]: (~coll(sK20_skl,sK25_skl,X0)|coll(X0,sK21_skl,sK20_skl))),
% 1.34/0.67 inference(resolution,[status(thm)],[f813,f103])).
% 1.34/0.67 fof(f1020,plain,(
% 1.34/0.67 coll(sK22_skl,sK26_skl,sK23_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f523,f570])).
% 1.34/0.67 fof(f1024,plain,(
% 1.34/0.67 coll(sK26_skl,sK22_skl,sK23_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f1020,f100])).
% 1.34/0.67 fof(f1037,plain,(
% 1.34/0.67 coll(sK26_skl,sK23_skl,sK22_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f1024,f98])).
% 1.34/0.67 fof(f1049,plain,(
% 1.34/0.67 coll(sK22_skl,sK20_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f1037,f431])).
% 1.34/0.67 fof(f1084,plain,(
% 1.34/0.67 coll(sK20_skl,sK22_skl,sK26_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f1049,f100])).
% 1.34/0.67 fof(f1105,plain,(
% 1.34/0.67 coll(sK20_skl,sK26_skl,sK22_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f1084,f98])).
% 1.34/0.67 fof(f2613,plain,(
% 1.34/0.67 coll(sK22_skl,sK25_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f776,f1105])).
% 1.34/0.67 fof(f2623,plain,(
% 1.34/0.67 coll(sK25_skl,sK22_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f2613,f100])).
% 1.34/0.67 fof(f2657,plain,(
% 1.34/0.67 coll(sK25_skl,sK20_skl,sK22_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f2623,f98])).
% 1.34/0.67 fof(f2670,plain,(
% 1.34/0.67 coll(sK20_skl,sK25_skl,sK22_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f2657,f100])).
% 1.34/0.67 fof(f2882,plain,(
% 1.34/0.67 coll(sK22_skl,sK21_skl,sK20_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f843,f2670])).
% 1.34/0.67 fof(f2891,plain,(
% 1.34/0.67 coll(sK22_skl,sK20_skl,sK21_skl)),
% 1.34/0.67 inference(resolution,[status(thm)],[f2882,f98])).
% 1.34/0.67 fof(f2892,plain,(
% 1.34/0.67 $false),
% 1.34/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2891,f381])).
% 1.34/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 1.34/0.69 % Elapsed time: 0.325879 seconds
% 1.34/0.69 % CPU time: 2.245196 seconds
% 1.34/0.69 % Total memory used: 103.542 MB
% 1.34/0.69 % Net memory used: 101.778 MB
%------------------------------------------------------------------------------