%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO646+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 : n005.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:46 PM UTC 2026
% Result : Theorem 5.00s 1.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GEO646+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 20 18:10:34 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 5.00/1.41 % Refutation found
% 5.00/1.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.00/1.41 % SZS output start CNFRefutation for theBenchmark
% 5.00/1.41 fof(f4,axiom,(
% 5.00/1.41 (! [A,B,C,D] :( para(A,B,C,D)=> para(A,B,D,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f5,axiom,(
% 5.00/1.41 (! [A,B,C,D] :( para(A,B,C,D)=> para(C,D,A,B) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f6,axiom,(
% 5.00/1.41 (! [A,B,C,D,E,F] :( ( para(A,B,C,D)& para(C,D,E,F) )=> para(A,B,E,F) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f9,axiom,(
% 5.00/1.41 (! [A,B,C,D,E,F] :( ( perp(A,B,C,D)& perp(C,D,E,F) )=> para(A,B,E,F) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f11,axiom,(
% 5.00/1.41 (! [A,B,M] :( midp(M,B,A)=> midp(M,A,B) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f18,axiom,(
% 5.00/1.41 (! [A,B,C,D,P,Q,U,V] :( eqangle(A,B,C,D,P,Q,U,V)=> eqangle(B,A,C,D,P,Q,U,V) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f19,axiom,(
% 5.00/1.41 (! [A,B,C,D,P,Q,U,V] :( eqangle(A,B,C,D,P,Q,U,V)=> eqangle(C,D,A,B,U,V,P,Q) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f23,axiom,(
% 5.00/1.41 (! [A,B,C,D] :( cong(A,B,C,D)=> cong(A,B,D,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f24,axiom,(
% 5.00/1.41 (! [A,B,C,D] :( cong(A,B,C,D)=> cong(C,D,A,B) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f25,axiom,(
% 5.00/1.41 (! [A,B,C,D,E,F] :( ( cong(A,B,C,D)& cong(C,D,E,F) )=> cong(A,B,E,F) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f39,axiom,(
% 5.00/1.41 (! [A,B,C,D,P,Q] :( eqangle(A,B,P,Q,C,D,P,Q)=> para(A,B,C,D) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f40,axiom,(
% 5.00/1.41 (! [A,B,C,D,P,Q] :( para(A,B,C,D)=> eqangle(A,B,P,Q,C,D,P,Q) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f57,axiom,(
% 5.00/1.41 (! [A,B,P,Q] :( ( cong(A,P,B,P)& cong(A,Q,B,Q) )=> perp(A,B,P,Q) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f64,axiom,(
% 5.00/1.41 (! [A,B,C,D,M] :( ( midp(M,A,B)& midp(M,C,D) )=> para(A,C,B,D) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f65,axiom,(
% 5.00/1.41 (! [A,B,C,D,M] :( ( midp(M,A,B)& para(A,C,B,D)& para(A,D,B,C) )=> midp(M,C,D) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f67,axiom,(
% 5.00/1.41 (! [A,B,C] :( para(A,B,A,C)=> coll(A,B,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f68,axiom,(
% 5.00/1.41 (! [A,B,C] :( ( cong(A,B,A,C)& coll(A,B,C) )=> midp(A,B,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f69,axiom,(
% 5.00/1.41 (! [A,B,C] :( midp(A,B,C)=> cong(A,B,A,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f70,axiom,(
% 5.00/1.41 (! [A,B,C] :( midp(A,B,C)=> coll(A,B,C) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f95,conjecture,(
% 5.00/1.41 (! [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6] :( ( circle(A,B,NWPNT1,NWPNT2)& perp(A,B,B,D)& circle(A,B,C,NWPNT3)& perp(A,C,C,D)& circle(A,B,E,NWPNT4)& coll(F,D,E)& circle(A,B,F,NWPNT5)& midp(G,E,F)& coll(C,G,H)& circle(A,C,H,NWPNT6) )=> para(E,F,B,H) ) )),
% 5.00/1.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.00/1.41 fof(f96,negated_conjecture,(
% 5.00/1.41 ~((! [A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6] :( ( circle(A,B,NWPNT1,NWPNT2)& perp(A,B,B,D)& circle(A,B,C,NWPNT3)& perp(A,C,C,D)& circle(A,B,E,NWPNT4)& coll(F,D,E)& circle(A,B,F,NWPNT5)& midp(G,E,F)& coll(C,G,H)& circle(A,C,H,NWPNT6) )=> para(E,F,B,H) ) ))),
% 5.00/1.41 inference(negated_conjecture,[status(cth)],[f95])).
% 5.00/1.41 fof(f104,plain,(
% 5.00/1.41 ![A,B,C,D]: (~para(A,B,C,D)|para(A,B,D,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 5.00/1.41 fof(f105,plain,(
% 5.00/1.41 ![X0,X1,X2,X3]: (~para(X0,X1,X2,X3)|para(X0,X1,X3,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f104])).
% 5.00/1.41 fof(f106,plain,(
% 5.00/1.41 ![A,B,C,D]: (~para(A,B,C,D)|para(C,D,A,B))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 5.00/1.41 fof(f107,plain,(
% 5.00/1.41 ![X0,X1,X2,X3]: (~para(X0,X1,X2,X3)|para(X2,X3,X0,X1))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f106])).
% 5.00/1.41 fof(f108,plain,(
% 5.00/1.41 ![A,B,C,D,E,F]: ((~para(A,B,C,D)|~para(C,D,E,F))|para(A,B,E,F))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 5.00/1.41 fof(f109,plain,(
% 5.00/1.41 ![A,B,E,F]: ((![C,D]: (~para(A,B,C,D)|~para(C,D,E,F)))|para(A,B,E,F))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f108])).
% 5.00/1.41 fof(f110,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5]: (~para(X0,X1,X2,X3)|~para(X2,X3,X4,X5)|para(X0,X1,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f109])).
% 5.00/1.41 fof(f115,plain,(
% 5.00/1.41 ![A,B,C,D,E,F]: ((~perp(A,B,C,D)|~perp(C,D,E,F))|para(A,B,E,F))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 5.00/1.41 fof(f116,plain,(
% 5.00/1.41 ![A,B,E,F]: ((![C,D]: (~perp(A,B,C,D)|~perp(C,D,E,F)))|para(A,B,E,F))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f115])).
% 5.00/1.41 fof(f117,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5]: (~perp(X0,X1,X2,X3)|~perp(X2,X3,X4,X5)|para(X0,X1,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f116])).
% 5.00/1.41 fof(f121,plain,(
% 5.00/1.41 ![A,B,M]: (~midp(M,B,A)|midp(M,A,B))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 5.00/1.41 fof(f122,plain,(
% 5.00/1.41 ![X0,X1,X2]: (~midp(X0,X1,X2)|midp(X0,X2,X1))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f121])).
% 5.00/1.41 fof(f137,plain,(
% 5.00/1.41 ![A,B,C,D,P,Q,U,V]: (~eqangle(A,B,C,D,P,Q,U,V)|eqangle(B,A,C,D,P,Q,U,V))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 5.00/1.41 fof(f138,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~eqangle(X0,X1,X2,X3,X4,X5,X6,X7)|eqangle(X1,X0,X2,X3,X4,X5,X6,X7))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f137])).
% 5.00/1.41 fof(f139,plain,(
% 5.00/1.41 ![A,B,C,D,P,Q,U,V]: (~eqangle(A,B,C,D,P,Q,U,V)|eqangle(C,D,A,B,U,V,P,Q))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 5.00/1.41 fof(f140,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~eqangle(X0,X1,X2,X3,X4,X5,X6,X7)|eqangle(X2,X3,X0,X1,X6,X7,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f139])).
% 5.00/1.41 fof(f148,plain,(
% 5.00/1.41 ![A,B,C,D]: (~cong(A,B,C,D)|cong(A,B,D,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 5.00/1.41 fof(f149,plain,(
% 5.00/1.41 ![X0,X1,X2,X3]: (~cong(X0,X1,X2,X3)|cong(X0,X1,X3,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f148])).
% 5.00/1.41 fof(f150,plain,(
% 5.00/1.41 ![A,B,C,D]: (~cong(A,B,C,D)|cong(C,D,A,B))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 5.00/1.41 fof(f151,plain,(
% 5.00/1.41 ![X0,X1,X2,X3]: (~cong(X0,X1,X2,X3)|cong(X2,X3,X0,X1))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f150])).
% 5.00/1.41 fof(f152,plain,(
% 5.00/1.41 ![A,B,C,D,E,F]: ((~cong(A,B,C,D)|~cong(C,D,E,F))|cong(A,B,E,F))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 5.00/1.41 fof(f153,plain,(
% 5.00/1.41 ![A,B,E,F]: ((![C,D]: (~cong(A,B,C,D)|~cong(C,D,E,F)))|cong(A,B,E,F))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f152])).
% 5.00/1.41 fof(f154,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5]: (~cong(X0,X1,X2,X3)|~cong(X2,X3,X4,X5)|cong(X0,X1,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f153])).
% 5.00/1.41 fof(f184,plain,(
% 5.00/1.41 ![A,B,C,D,P,Q]: (~eqangle(A,B,P,Q,C,D,P,Q)|para(A,B,C,D))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 5.00/1.41 fof(f185,plain,(
% 5.00/1.41 ![A,B,C,D]: ((![P,Q]: ~eqangle(A,B,P,Q,C,D,P,Q))|para(A,B,C,D))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f184])).
% 5.00/1.41 fof(f186,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5]: (~eqangle(X0,X1,X2,X3,X4,X5,X2,X3)|para(X0,X1,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f185])).
% 5.00/1.41 fof(f187,plain,(
% 5.00/1.41 ![A,B,C,D,P,Q]: (~para(A,B,C,D)|eqangle(A,B,P,Q,C,D,P,Q))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 5.00/1.41 fof(f188,plain,(
% 5.00/1.41 ![A,B,C,D]: (~para(A,B,C,D)|(![P,Q]: eqangle(A,B,P,Q,C,D,P,Q)))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f187])).
% 5.00/1.41 fof(f189,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4,X5]: (~para(X0,X1,X2,X3)|eqangle(X0,X1,X4,X5,X2,X3,X4,X5))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f188])).
% 5.00/1.41 fof(f231,plain,(
% 5.00/1.41 ![A,B,P,Q]: ((~cong(A,P,B,P)|~cong(A,Q,B,Q))|perp(A,B,P,Q))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 5.00/1.41 fof(f232,plain,(
% 5.00/1.41 ![X0,X1,X2,X3]: (~cong(X0,X1,X2,X1)|~cong(X0,X3,X2,X3)|perp(X0,X2,X1,X3))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f231])).
% 5.00/1.41 fof(f247,plain,(
% 5.00/1.41 ![A,B,C,D,M]: ((~midp(M,A,B)|~midp(M,C,D))|para(A,C,B,D))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 5.00/1.41 fof(f248,plain,(
% 5.00/1.41 ![A,B,C,D]: ((![M]: (~midp(M,A,B)|~midp(M,C,D)))|para(A,C,B,D))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f247])).
% 5.00/1.41 fof(f249,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4]: (~midp(X0,X1,X2)|~midp(X0,X3,X4)|para(X1,X3,X2,X4))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f248])).
% 5.00/1.41 fof(f250,plain,(
% 5.00/1.41 ![A,B,C,D,M]: (((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C))|midp(M,C,D))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 5.00/1.41 fof(f251,plain,(
% 5.00/1.41 ![C,D,M]: ((![A,B]: ((~midp(M,A,B)|~para(A,C,B,D))|~para(A,D,B,C)))|midp(M,C,D))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f250])).
% 5.00/1.41 fof(f252,plain,(
% 5.00/1.41 ![X0,X1,X2,X3,X4]: (~midp(X0,X1,X2)|~para(X1,X3,X2,X4)|~para(X1,X4,X2,X3)|midp(X0,X3,X4))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f251])).
% 5.00/1.41 fof(f255,plain,(
% 5.00/1.41 ![A,B,C]: (~para(A,B,A,C)|coll(A,B,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 5.00/1.41 fof(f256,plain,(
% 5.00/1.41 ![X0,X1,X2]: (~para(X0,X1,X0,X2)|coll(X0,X1,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f255])).
% 5.00/1.41 fof(f257,plain,(
% 5.00/1.41 ![A,B,C]: ((~cong(A,B,A,C)|~coll(A,B,C))|midp(A,B,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 5.00/1.41 fof(f258,plain,(
% 5.00/1.41 ![X0,X1,X2]: (~cong(X0,X1,X0,X2)|~coll(X0,X1,X2)|midp(X0,X1,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f257])).
% 5.00/1.41 fof(f259,plain,(
% 5.00/1.41 ![A,B,C]: (~midp(A,B,C)|cong(A,B,A,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 5.00/1.41 fof(f260,plain,(
% 5.00/1.41 ![X0,X1,X2]: (~midp(X0,X1,X2)|cong(X0,X1,X0,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f259])).
% 5.00/1.41 fof(f261,plain,(
% 5.00/1.41 ![A,B,C]: (~midp(A,B,C)|coll(A,B,C))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 5.00/1.41 fof(f262,plain,(
% 5.00/1.41 ![X0,X1,X2]: (~midp(X0,X1,X2)|coll(X0,X1,X2))),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f261])).
% 5.00/1.41 fof(f369,plain,(
% 5.00/1.41 (?[A,B,C,D,E,F,G,H,NWPNT1,NWPNT2,NWPNT3,NWPNT4,NWPNT5,NWPNT6]: ((((((((((circle(A,B,NWPNT1,NWPNT2)&perp(A,B,B,D))&circle(A,B,C,NWPNT3))&perp(A,C,C,D))&circle(A,B,E,NWPNT4))&coll(F,D,E))&circle(A,B,F,NWPNT5))&midp(G,E,F))&coll(C,G,H))&circle(A,C,H,NWPNT6))&~para(E,F,B,H)))),
% 5.00/1.41 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 5.00/1.41 fof(f370,plain,(
% 5.00/1.41 ?[B,E,F,H]: ((?[A,C]: ((?[G]: ((((?[D]: ((((((?[NWPNT1,NWPNT2]: circle(A,B,NWPNT1,NWPNT2))&perp(A,B,B,D))&(?[NWPNT3]: circle(A,B,C,NWPNT3)))&perp(A,C,C,D))&(?[NWPNT4]: circle(A,B,E,NWPNT4)))&coll(F,D,E)))&(?[NWPNT5]: circle(A,B,F,NWPNT5)))&midp(G,E,F))&coll(C,G,H)))&(?[NWPNT6]: circle(A,C,H,NWPNT6))))&~para(E,F,B,H))),
% 5.00/1.41 inference(miniscoping,[status(thm)],[f369])).
% 5.00/1.41 fof(f371,plain,(
% 5.00/1.41 ((((((((((circle(sK24_skl,sK20_skl,sK28_skl,sK29_skl)&perp(sK24_skl,sK20_skl,sK20_skl,sK27_skl))&circle(sK24_skl,sK20_skl,sK25_skl,sK30_skl))&perp(sK24_skl,sK25_skl,sK25_skl,sK27_skl))&circle(sK24_skl,sK20_skl,sK21_skl,sK31_skl))&coll(sK22_skl,sK27_skl,sK21_skl))&circle(sK24_skl,sK20_skl,sK22_skl,sK32_skl))&midp(sK26_skl,sK21_skl,sK22_skl))&coll(sK25_skl,sK26_skl,sK23_skl))&circle(sK24_skl,sK25_skl,sK23_skl,sK33_skl))&~para(sK21_skl,sK22_skl,sK20_skl,sK23_skl))),
% 5.00/1.41 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,sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl]),skolemize(B,sK20_skl),skolemize(E,sK21_skl),skolemize(F,sK22_skl),skolemize(H,sK23_skl),skolemize(A,sK24_skl),skolemize(C,sK25_skl),skolemize(G,sK26_skl),skolemize(D,sK27_skl),skolemize(NWPNT1,sK28_skl),skolemize(NWPNT2,sK29_skl),skolemize(NWPNT3,sK30_skl),skolemize(NWPNT4,sK31_skl),skolemize(NWPNT5,sK32_skl),skolemize(NWPNT6,sK33_skl)],[f370])).
% 5.00/1.41 fof(f379,plain,(
% 5.00/1.41 midp(sK26_skl,sK21_skl,sK22_skl)),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f371])).
% 5.00/1.41 fof(f382,plain,(
% 5.00/1.41 ~para(sK21_skl,sK22_skl,sK20_skl,sK23_skl)),
% 5.00/1.41 inference(cnf_transformation,[status(thm)],[f371])).
% 5.00/1.41 fof(f384,plain,(
% 5.00/1.41 ![X0,X1,X2]: (coll(X0,X1,X2)|~midp(X0,X2,X1))),
% 5.00/1.41 inference(resolution,[status(thm)],[f262,f122])).
% 5.00/1.41 fof(f385,plain,(
% 5.00/1.41 ![X0,X1]: (~para(sK21_skl,sK22_skl,X0,X1)|~para(X0,X1,sK20_skl,sK23_skl))),
% 5.00/1.41 inference(resolution,[status(thm)],[f382,f110])).
% 5.00/1.41 fof(f388,plain,(
% 5.00/1.41 coll(sK26_skl,sK22_skl,sK21_skl)),
% 5.00/1.41 inference(resolution,[status(thm)],[f384,f379])).
% 5.00/1.41 fof(f421,plain,(
% 5.00/1.41 ![X0,X1,X2]: (coll(X0,X1,X2)|~para(X0,X2,X0,X1))),
% 5.00/1.41 inference(resolution,[status(thm)],[f256,f107])).
% 5.00/1.41 fof(f434,plain,(
% 5.00/1.42 cong(sK26_skl,sK21_skl,sK26_skl,sK22_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f260,f379])).
% 5.00/1.42 fof(f435,plain,(
% 5.00/1.42 ![X0,X1,X2]: (cong(X0,X1,X0,X2)|~midp(X0,X2,X1))),
% 5.00/1.42 inference(resolution,[status(thm)],[f260,f122])).
% 5.00/1.42 fof(f444,plain,(
% 5.00/1.42 ![X0,X1,X2]: (coll(X0,X1,X2)|~para(X0,X2,X1,X0))),
% 5.00/1.42 inference(resolution,[status(thm)],[f421,f105])).
% 5.00/1.42 fof(f450,plain,(
% 5.00/1.42 cong(sK26_skl,sK22_skl,sK26_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f435,f379])).
% 5.00/1.42 fof(f459,plain,(
% 5.00/1.42 ![X0,X1,X2]: (coll(X0,X1,X2)|~para(X1,X0,X0,X2))),
% 5.00/1.42 inference(resolution,[status(thm)],[f444,f107])).
% 5.00/1.42 fof(f468,plain,(
% 5.00/1.42 ![X0,X1,X2]: (coll(X0,X1,X2)|~para(X1,X0,X2,X0))),
% 5.00/1.42 inference(resolution,[status(thm)],[f459,f105])).
% 5.00/1.42 fof(f494,plain,(
% 5.00/1.42 cong(sK26_skl,sK22_skl,sK21_skl,sK26_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f149,f450])).
% 5.00/1.42 fof(f498,plain,(
% 5.00/1.42 ![X0,X1,X2,X3]: (~cong(X0,X1,X2,X3)|cong(X2,X3,X1,X0))),
% 5.00/1.42 inference(resolution,[status(thm)],[f151,f149])).
% 5.00/1.42 fof(f511,plain,(
% 5.00/1.42 ![X0,X1,X2,X3,X4,X5]: (~eqangle(X0,X1,X2,X3,X4,X5,X2,X3)|para(X1,X0,X4,X5))),
% 5.00/1.42 inference(resolution,[status(thm)],[f138,f186])).
% 5.00/1.42 fof(f512,plain,(
% 5.00/1.42 ![X0,X1,X2,X3,X4,X5]: (~eqangle(X0,X1,X2,X3,X0,X1,X4,X5)|para(X2,X3,X4,X5))),
% 5.00/1.42 inference(resolution,[status(thm)],[f140,f186])).
% 5.00/1.42 fof(f564,plain,(
% 5.00/1.42 ~coll(sK26_skl,sK22_skl,sK21_skl)|midp(sK26_skl,sK22_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f258,f450])).
% 5.00/1.42 fof(f566,plain,(
% 5.00/1.42 ![X0,X1,X2]: (~coll(X0,X1,X2)|midp(X0,X1,X2)|~cong(X2,X0,X0,X1))),
% 5.00/1.42 inference(resolution,[status(thm)],[f258,f498])).
% 5.00/1.42 fof(f568,plain,(
% 5.00/1.42 midp(sK26_skl,sK22_skl,sK21_skl)),
% 5.00/1.42 inference(forward_subsumption_resolution,[status(thm)],[f564,f388])).
% 5.00/1.42 fof(f580,plain,(
% 5.00/1.42 ![X0,X1]: (~midp(sK26_skl,X0,X1)|para(X0,sK22_skl,X1,sK21_skl))),
% 5.00/1.42 inference(resolution,[status(thm)],[f568,f249])).
% 5.00/1.42 fof(f588,plain,(
% 5.00/1.42 para(sK21_skl,sK22_skl,sK22_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f580,f379])).
% 5.00/1.42 fof(f589,plain,(
% 5.00/1.42 ![X0,X1]: (para(X0,sK22_skl,X1,sK21_skl)|~midp(sK26_skl,X1,X0))),
% 5.00/1.42 inference(resolution,[status(thm)],[f580,f122])).
% 5.00/1.42 fof(f598,plain,(
% 5.00/1.42 ![X0,X1]: (~cong(X0,X1,sK26_skl,sK22_skl)|cong(X0,X1,sK21_skl,sK26_skl))),
% 5.00/1.42 inference(resolution,[status(thm)],[f154,f494])).
% 5.00/1.42 fof(f705,plain,(
% 5.00/1.42 ![X0,X1,X2,X3]: (para(X0,X1,X2,X3)|~para(X1,X0,X2,X3))),
% 5.00/1.42 inference(resolution,[status(thm)],[f511,f189])).
% 5.00/1.42 fof(f708,plain,(
% 5.00/1.42 para(sK22_skl,sK21_skl,sK22_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f705,f588])).
% 5.00/1.42 fof(f797,plain,(
% 5.00/1.42 ![X0,X1,X2,X3]: (para(X0,X1,X0,X1)|~para(X2,X3,X2,X3))),
% 5.00/1.42 inference(resolution,[status(thm)],[f512,f189])).
% 5.00/1.42 fof(f816,plain,(
% 5.00/1.42 ![X0,X1]: (para(X0,X1,X0,X1))),
% 5.00/1.42 inference(resolution,[status(thm)],[f797,f708])).
% 5.00/1.42 fof(f840,plain,(
% 5.00/1.42 ![X0,X1]: (coll(X0,X1,X1))),
% 5.00/1.42 inference(resolution,[status(thm)],[f816,f468])).
% 5.00/1.42 fof(f954,plain,(
% 5.00/1.42 cong(sK26_skl,sK21_skl,sK21_skl,sK26_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f598,f434])).
% 5.00/1.42 fof(f957,plain,(
% 5.00/1.42 ~coll(sK21_skl,sK26_skl,sK26_skl)|midp(sK21_skl,sK26_skl,sK26_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f954,f566])).
% 5.00/1.42 fof(f959,plain,(
% 5.00/1.42 cong(sK26_skl,sK21_skl,sK26_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f954,f149])).
% 5.00/1.42 fof(f960,plain,(
% 5.00/1.42 midp(sK21_skl,sK26_skl,sK26_skl)),
% 5.00/1.42 inference(forward_subsumption_resolution,[status(thm)],[f957,f840])).
% 5.00/1.42 fof(f968,plain,(
% 5.00/1.42 ![X0,X1]: (~para(sK26_skl,X0,sK26_skl,X1)|~para(sK26_skl,X1,sK26_skl,X0)|midp(sK21_skl,X0,X1))),
% 5.00/1.42 inference(resolution,[status(thm)],[f960,f252])).
% 5.00/1.42 fof(f978,plain,(
% 5.00/1.42 ![X0,X1]: (~para(sK26_skl,X0,sK26_skl,X1)|midp(sK21_skl,X1,X0))),
% 5.00/1.42 inference(forward_subsumption_resolution,[status(thm)],[f968,f107])).
% 5.00/1.42 fof(f981,plain,(
% 5.00/1.42 ~coll(sK26_skl,sK21_skl,sK21_skl)|midp(sK26_skl,sK21_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f959,f258])).
% 5.00/1.42 fof(f988,plain,(
% 5.00/1.42 midp(sK26_skl,sK21_skl,sK21_skl)),
% 5.00/1.42 inference(forward_subsumption_resolution,[status(thm)],[f981,f840])).
% 5.00/1.42 fof(f989,plain,(
% 5.00/1.42 para(sK21_skl,sK22_skl,sK21_skl,sK21_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f988,f589])).
% 5.00/1.42 fof(f1023,plain,(
% 5.00/1.42 ~para(sK21_skl,sK21_skl,sK20_skl,sK23_skl)),
% 5.00/1.42 inference(resolution,[status(thm)],[f989,f385])).
% 5.00/1.42 fof(f1088,plain,(
% 5.00/1.43 ![X0,X1]: (~perp(sK21_skl,sK21_skl,X0,X1)|~perp(X0,X1,sK20_skl,sK23_skl))),
% 5.00/1.43 inference(resolution,[status(thm)],[f1023,f117])).
% 5.00/1.43 fof(f1191,plain,(
% 5.00/1.43 ![X0]: (midp(sK21_skl,X0,X0))),
% 5.00/1.43 inference(resolution,[status(thm)],[f978,f816])).
% 5.00/1.43 fof(f1211,plain,(
% 5.00/1.43 ![X0]: (cong(sK21_skl,X0,sK21_skl,X0))),
% 5.00/1.43 inference(resolution,[status(thm)],[f1191,f435])).
% 5.00/1.43 fof(f1224,plain,(
% 5.00/1.43 ![X0,X1]: (~cong(sK21_skl,X0,sK21_skl,X0)|perp(sK21_skl,sK21_skl,X0,X1))),
% 5.00/1.43 inference(resolution,[status(thm)],[f1211,f232])).
% 5.00/1.43 fof(f1238,plain,(
% 5.00/1.43 ![X0,X1]: (~perp(X0,X1,sK20_skl,sK23_skl))),
% 5.00/1.43 inference(backward_subsumption_resolution,[status(thm)],[f1088,f1240])).
% 5.00/1.43 fof(f1240,plain,(
% 5.00/1.43 ![X0,X1]: (perp(sK21_skl,sK21_skl,X0,X1))),
% 5.00/1.43 inference(forward_subsumption_resolution,[status(thm)],[f1224,f1211])).
% 5.00/1.43 fof(f1295,plain,(
% 5.00/1.43 $false),
% 5.00/1.43 inference(resolution,[status(thm)],[f1238,f1240])).
% 5.00/1.43 % SZS output end CNFRefutation for theBenchmark.p
% 7.88/1.45 % Elapsed time: 1.059630 seconds
% 7.88/1.45 % CPU time: 8.133881 seconds
% 7.88/1.45 % Total memory used: 129.998 MB
% 7.88/1.45 % Net memory used: 124.891 MB
%------------------------------------------------------------------------------