%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO547+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 : n026.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:37 PM UTC 2026
% Result : Theorem 0.10s 0.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO547+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 17:24:51 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.46 % Refutation found
% 0.10/0.46 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.46 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.46 fof(f1,axiom,(
% 0.10/0.46 (! [A,B,C] :( coll(A,B,C)=> coll(A,C,B) ) )),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f2,axiom,(
% 0.10/0.46 (! [A,B,C] :( coll(A,B,C)=> coll(B,A,C) ) )),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f3,axiom,(
% 0.10/0.46 (! [A,B,C,D] :( ( coll(A,B,C)& coll(A,B,D) )=> coll(C,D,A) ) )),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f95,conjecture,(
% 0.10/0.46 (! [A,B,C,O,D,E,F,G,NWPNT1] :( ( circle(O,A,B,C)& circle(O,A,D,NWPNT1)& perp(E,D,B,C)& coll(E,B,C)& perp(F,D,A,C)& coll(F,A,C)& perp(G,D,A,B)& coll(G,A,B) )=> coll(E,F,G) ) )),
% 0.10/0.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.46 fof(f96,negated_conjecture,(
% 0.10/0.46 ~((! [A,B,C,O,D,E,F,G,NWPNT1] :( ( circle(O,A,B,C)& circle(O,A,D,NWPNT1)& perp(E,D,B,C)& coll(E,B,C)& perp(F,D,A,C)& coll(F,A,C)& perp(G,D,A,B)& coll(G,A,B) )=> coll(E,F,G) ) ))),
% 0.10/0.46 inference(negated_conjecture,[status(cth)],[f95])).
% 0.10/0.46 fof(f97,plain,(
% 0.10/0.46 ![A,B,C]: (~coll(A,B,C)|coll(A,C,B))),
% 0.10/0.46 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.10/0.46 fof(f98,plain,(
% 0.10/0.46 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X0,X2,X1))),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f97])).
% 0.10/0.46 fof(f99,plain,(
% 0.10/0.46 ![A,B,C]: (~coll(A,B,C)|coll(B,A,C))),
% 0.10/0.46 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.10/0.46 fof(f100,plain,(
% 0.10/0.46 ![X0,X1,X2]: (~coll(X0,X1,X2)|coll(X1,X0,X2))),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f99])).
% 0.10/0.46 fof(f101,plain,(
% 0.10/0.46 ![A,B,C,D]: ((~coll(A,B,C)|~coll(A,B,D))|coll(C,D,A))),
% 0.10/0.46 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.10/0.46 fof(f102,plain,(
% 0.10/0.46 ![A,C,D]: ((![B]: (~coll(A,B,C)|~coll(A,B,D)))|coll(C,D,A))),
% 0.10/0.46 inference(miniscoping,[status(thm)],[f101])).
% 0.10/0.46 fof(f103,plain,(
% 0.10/0.46 ![X0,X1,X2,X3]: (~coll(X0,X1,X2)|~coll(X0,X1,X3)|coll(X2,X3,X0))),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f102])).
% 0.10/0.46 fof(f369,plain,(
% 0.10/0.46 (?[A,B,C,O,D,E,F,G,NWPNT1]: ((((((((circle(O,A,B,C)&circle(O,A,D,NWPNT1))&perp(E,D,B,C))&coll(E,B,C))&perp(F,D,A,C))&coll(F,A,C))&perp(G,D,A,B))&coll(G,A,B))&~coll(E,F,G)))),
% 0.10/0.46 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 0.10/0.46 fof(f370,plain,(
% 0.10/0.46 ?[E,F,G]: ((?[A,B]: ((?[D]: ((?[C]: (((((?[O]: (circle(O,A,B,C)&(?[NWPNT1]: circle(O,A,D,NWPNT1))))&perp(E,D,B,C))&coll(E,B,C))&perp(F,D,A,C))&coll(F,A,C)))&perp(G,D,A,B)))&coll(G,A,B)))&~coll(E,F,G))),
% 0.10/0.46 inference(miniscoping,[status(thm)],[f369])).
% 0.10/0.46 fof(f371,plain,(
% 0.10/0.46 ((((((((circle(sK27_skl,sK23_skl,sK24_skl,sK26_skl)&circle(sK27_skl,sK23_skl,sK25_skl,sK28_skl))&perp(sK20_skl,sK25_skl,sK24_skl,sK26_skl))&coll(sK20_skl,sK24_skl,sK26_skl))&perp(sK21_skl,sK25_skl,sK23_skl,sK26_skl))&coll(sK21_skl,sK23_skl,sK26_skl))&perp(sK22_skl,sK25_skl,sK23_skl,sK24_skl))&coll(sK22_skl,sK23_skl,sK24_skl))&~coll(sK20_skl,sK21_skl,sK22_skl))),
% 0.10/0.46 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl]),skolemize(E,sK20_skl),skolemize(F,sK21_skl),skolemize(G,sK22_skl),skolemize(A,sK23_skl),skolemize(B,sK24_skl),skolemize(D,sK25_skl),skolemize(C,sK26_skl),skolemize(O,sK27_skl),skolemize(NWPNT1,sK28_skl)],[f370])).
% 0.10/0.46 fof(f375,plain,(
% 0.10/0.46 coll(sK20_skl,sK24_skl,sK26_skl)),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f371])).
% 0.10/0.46 fof(f377,plain,(
% 0.10/0.46 coll(sK21_skl,sK23_skl,sK26_skl)),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f371])).
% 0.10/0.46 fof(f379,plain,(
% 0.10/0.46 coll(sK22_skl,sK23_skl,sK24_skl)),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f371])).
% 0.10/0.46 fof(f380,plain,(
% 0.10/0.46 ~coll(sK20_skl,sK21_skl,sK22_skl)),
% 0.10/0.46 inference(cnf_transformation,[status(thm)],[f371])).
% 0.10/0.46 fof(f381,plain,(
% 0.10/0.46 ~coll(sK20_skl,sK22_skl,sK21_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f98,f380])).
% 0.10/0.46 fof(f383,plain,(
% 0.10/0.46 ~coll(sK22_skl,sK20_skl,sK21_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f100,f381])).
% 0.10/0.46 fof(f386,plain,(
% 0.10/0.46 ~coll(sK22_skl,sK21_skl,sK20_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f383,f98])).
% 0.10/0.46 fof(f393,plain,(
% 0.10/0.46 ![X0]: (~coll(sK22_skl,sK23_skl,X0)|coll(X0,sK24_skl,sK22_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f103,f379])).
% 0.10/0.46 fof(f394,plain,(
% 0.10/0.46 ![X0]: (~coll(sK21_skl,sK23_skl,X0)|coll(X0,sK26_skl,sK21_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f103,f377])).
% 0.10/0.46 fof(f395,plain,(
% 0.10/0.46 ![X0]: (~coll(sK20_skl,sK24_skl,X0)|coll(X0,sK26_skl,sK20_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f103,f375])).
% 0.10/0.46 fof(f396,plain,(
% 0.10/0.46 ![X0,X1,X2,X3]: (~coll(X0,X1,X2)|coll(X2,X3,X0)|~coll(X1,X0,X3))),
% 0.10/0.46 inference(resolution,[status(thm)],[f103,f100])).
% 0.10/0.46 fof(f397,plain,(
% 0.10/0.46 ![X0,X1,X2,X3]: (~coll(X0,X1,X2)|coll(X2,X3,X0)|~coll(X0,X3,X1))),
% 0.10/0.46 inference(resolution,[status(thm)],[f103,f98])).
% 0.10/0.46 fof(f404,plain,(
% 0.10/0.46 ![X0,X1]: (~coll(sK22_skl,sK23_skl,X0)|~coll(X0,sK24_skl,X1)|coll(X1,sK22_skl,X0))),
% 0.10/0.46 inference(resolution,[status(thm)],[f393,f103])).
% 0.10/0.46 fof(f405,plain,(
% 0.10/0.46 ![X0,X1]: (~coll(sK21_skl,sK23_skl,X0)|~coll(X0,sK26_skl,X1)|coll(X1,sK21_skl,X0))),
% 0.10/0.46 inference(resolution,[status(thm)],[f394,f103])).
% 0.10/0.46 fof(f407,plain,(
% 0.10/0.46 ![X0]: (~coll(sK24_skl,sK24_skl,X0)|coll(X0,sK22_skl,sK24_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f404,f379])).
% 0.10/0.46 fof(f410,plain,(
% 0.10/0.46 ![X0]: (~coll(sK26_skl,sK26_skl,X0)|coll(X0,sK21_skl,sK26_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f405,f377])).
% 0.10/0.46 fof(f419,plain,(
% 0.10/0.46 ![X0]: (~coll(sK20_skl,X0,sK22_skl)|~coll(X0,sK20_skl,sK21_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f396,f386])).
% 0.10/0.46 fof(f432,plain,(
% 0.10/0.46 ![X0]: (~coll(sK20_skl,X0,sK22_skl)|~coll(X0,sK21_skl,sK20_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f419,f98])).
% 0.10/0.46 fof(f457,plain,(
% 0.10/0.46 ![X0]: (~coll(sK20_skl,X0,sK22_skl)|~coll(sK21_skl,X0,sK20_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f432,f100])).
% 0.10/0.46 fof(f495,plain,(
% 0.10/0.46 ![X0]: (~coll(sK21_skl,X0,sK20_skl)|~coll(sK20_skl,sK22_skl,X0))),
% 0.10/0.46 inference(resolution,[status(thm)],[f457,f98])).
% 0.10/0.46 fof(f532,plain,(
% 0.10/0.46 ~coll(sK21_skl,sK24_skl,sK20_skl)|~coll(sK24_skl,sK24_skl,sK20_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f495,f407])).
% 0.10/0.46 fof(f611,plain,(
% 0.10/0.46 ![X0]: (~coll(sK20_skl,sK26_skl,X0)|coll(X0,sK24_skl,sK20_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f397,f375])).
% 0.10/0.46 fof(f634,plain,(
% 0.10/0.46 ![X0]: (coll(X0,sK24_skl,sK20_skl)|~coll(sK20_skl,X0,sK26_skl))),
% 0.10/0.46 inference(resolution,[status(thm)],[f611,f98])).
% 0.10/0.46 fof(f662,plain,(
% 0.10/0.46 coll(sK24_skl,sK24_skl,sK20_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f634,f375])).
% 0.10/0.46 fof(f664,plain,(
% 0.10/0.46 coll(sK21_skl,sK24_skl,sK20_skl)|~coll(sK26_skl,sK26_skl,sK20_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f634,f410])).
% 0.10/0.46 fof(f668,plain,(
% 0.10/0.46 ~coll(sK21_skl,sK24_skl,sK20_skl)),
% 0.10/0.46 inference(backward_subsumption_resolution,[status(thm)],[f532,f662])).
% 0.10/0.46 fof(f670,plain,(
% 0.10/0.46 ~coll(sK26_skl,sK26_skl,sK20_skl)),
% 0.10/0.46 inference(backward_subsumption_resolution,[status(thm)],[f664,f668])).
% 0.10/0.46 fof(f683,plain,(
% 0.10/0.46 ~coll(sK20_skl,sK24_skl,sK26_skl)),
% 0.10/0.46 inference(resolution,[status(thm)],[f670,f395])).
% 0.10/0.46 fof(f687,plain,(
% 0.10/0.46 $false),
% 0.10/0.46 inference(forward_subsumption_resolution,[status(thm)],[f683,f375])).
% 0.10/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/0.49 % Elapsed time: 0.114992 seconds
% 0.18/0.49 % CPU time: 0.534554 seconds
% 0.18/0.49 % Total memory used: 90.771 MB
% 0.18/0.49 % Net memory used: 90.302 MB
%------------------------------------------------------------------------------