%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.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:37:01 PM UTC 2026
% Result : Theorem 0.73s 1.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.61 % Computer : n005.cluster.edu
% 0.14/0.61 % Model : x86_64 x86_64
% 0.14/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.61 % Memory : 8046.5625MB
% 0.14/0.61 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Sun Sep 20 20:25:04 UTC 2026
% 0.14/0.61 % CPUTime :
% 0.60/1.12 % Drodi V4.1.1
% 0.73/1.57 % Refutation found
% 0.73/1.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.73/1.57 % SZS output start CNFRefutation for theBenchmark
% 0.73/1.57 fof(f8,axiom,(
% 0.73/1.57 (! [A,B] :( r1_tarski(A,B)<=> (! [C] :( r2_hidden(C,A)=> r2_hidden(C,B) ) )) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f29,axiom,(
% 0.73/1.57 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f31,axiom,(
% 0.73/1.57 (! [A,B,C] :( C = k3_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& r2_hidden(D,B) ) ) )) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f35,axiom,(
% 0.73/1.57 (! [A,B] :( r1_xboole_0(A,B)<=> k3_xboole_0(A,B) = k1_xboole_0 ) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f41,axiom,(
% 0.73/1.57 (! [A,B] :( ~ ( ~ r1_xboole_0(A,B)& (! [C] :~ ( r2_hidden(C,A)& r2_hidden(C,B) ) ))& ~ ( (? [C] :( r2_hidden(C,A)& r2_hidden(C,B) ))& r1_xboole_0(A,B) ) ) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f5658,axiom,(
% 0.73/1.57 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_group_1(B)& m1_group_2(B,A) )=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) )) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f5659,conjecture,(
% 0.73/1.57 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_group_1(B)& m1_group_2(B,A) )=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) )) )),
% 0.73/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.73/1.57 fof(f5660,negated_conjecture,(
% 0.73/1.57 ~((! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_group_1(B)& m1_group_2(B,A) )=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) )) ))),
% 0.73/1.57 inference(negated_conjecture,[status(cth)],[f5659])).
% 0.73/1.57 fof(f5684,plain,(
% 0.73/1.57 ![A,B]: (r1_tarski(A,B)<=>(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))),
% 0.73/1.57 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.73/1.57 fof(f5685,plain,(
% 0.73/1.57 ![A,B]: ((~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))&(r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 0.73/1.58 inference(NNF_transformation,[status(thm)],[f5684])).
% 0.73/1.58 fof(f5686,plain,(
% 0.73/1.58 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(?[C]: (r2_hidden(C,A)&~r2_hidden(C,B)))))),
% 0.73/1.58 inference(miniscoping,[status(thm)],[f5685])).
% 0.73/1.58 fof(f5687,plain,(
% 0.73/1.58 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(r2_hidden(sK3_skl(B,A),A)&~r2_hidden(sK3_skl(B,A),B))))),
% 0.73/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f5686])).
% 0.73/1.58 fof(f5688,plain,(
% 0.73/1.58 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r2_hidden(X2,X0)|r2_hidden(X2,X1))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5687])).
% 0.73/1.58 fof(f5689,plain,(
% 0.73/1.58 ![X0,X1]: (r1_tarski(X0,X1)|r2_hidden(sK3_skl(X1,X0),X0))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5687])).
% 0.73/1.58 fof(f5750,plain,(
% 0.73/1.58 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 0.73/1.58 inference(NNF_transformation,[status(thm)],[f29])).
% 0.73/1.58 fof(f5751,plain,(
% 0.73/1.58 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 0.73/1.58 inference(miniscoping,[status(thm)],[f5750])).
% 0.73/1.58 fof(f5752,plain,(
% 0.73/1.58 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 0.73/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f5751])).
% 0.73/1.58 fof(f5753,plain,(
% 0.73/1.58 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5752])).
% 0.73/1.58 fof(f5764,plain,(
% 0.73/1.58 ![A,B,C]: ((~C=k3_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B))))))&(C=k3_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))))))),
% 0.73/1.58 inference(NNF_transformation,[status(thm)],[f31])).
% 0.73/1.58 fof(f5765,plain,(
% 0.73/1.58 (![A,B,C]: (~C=k3_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))))))&(![A,B,C]: (C=k3_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B)))))))),
% 0.73/1.58 inference(miniscoping,[status(thm)],[f5764])).
% 0.73/1.58 fof(f5766,plain,(
% 0.73/1.58 (![A,B,C]: (~C=k3_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|~r2_hidden(D,B)))))))&(![A,B,C]: (C=k3_xboole_0(A,B)|((~r2_hidden(sK24_skl(C,B,A),C)|(~r2_hidden(sK24_skl(C,B,A),A)|~r2_hidden(sK24_skl(C,B,A),B)))&(r2_hidden(sK24_skl(C,B,A),C)|(r2_hidden(sK24_skl(C,B,A),A)&r2_hidden(sK24_skl(C,B,A),B))))))),
% 0.73/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(D,sK24_skl(C,B,A))],[f5765])).
% 0.73/1.58 fof(f5771,plain,(
% 0.73/1.58 ![X0,X1,X2]: (X0=k3_xboole_0(X1,X2)|r2_hidden(sK24_skl(X0,X2,X1),X0)|r2_hidden(sK24_skl(X0,X2,X1),X1))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5766])).
% 0.73/1.58 fof(f5787,plain,(
% 0.73/1.58 ![A,B]: ((~r1_xboole_0(A,B)|k3_xboole_0(A,B)=k1_xboole_0)&(r1_xboole_0(A,B)|~k3_xboole_0(A,B)=k1_xboole_0))),
% 0.73/1.58 inference(NNF_transformation,[status(thm)],[f35])).
% 0.73/1.58 fof(f5788,plain,(
% 0.73/1.58 (![A,B]: (~r1_xboole_0(A,B)|k3_xboole_0(A,B)=k1_xboole_0))&(![A,B]: (r1_xboole_0(A,B)|~k3_xboole_0(A,B)=k1_xboole_0))),
% 0.73/1.58 inference(miniscoping,[status(thm)],[f5787])).
% 0.73/1.58 fof(f5790,plain,(
% 0.73/1.58 ![X0,X1]: (r1_xboole_0(X0,X1)|~k3_xboole_0(X0,X1)=k1_xboole_0)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5788])).
% 0.73/1.58 fof(f5820,plain,(
% 0.73/1.58 ![A,B]: ((r1_xboole_0(A,B)|(?[C]: (r2_hidden(C,A)&r2_hidden(C,B))))&((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 0.73/1.58 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.73/1.58 fof(f5821,plain,(
% 0.73/1.58 (![A,B]: (r1_xboole_0(A,B)|(?[C]: (r2_hidden(C,A)&r2_hidden(C,B)))))&(![A,B]: ((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 0.73/1.58 inference(miniscoping,[status(thm)],[f5820])).
% 0.73/1.58 fof(f5822,plain,(
% 0.73/1.58 (![A,B]: (r1_xboole_0(A,B)|(r2_hidden(sK27_skl(B,A),A)&r2_hidden(sK27_skl(B,A),B))))&(![A,B]: ((![C]: (~r2_hidden(C,A)|~r2_hidden(C,B)))|~r1_xboole_0(A,B)))),
% 0.73/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(C,sK27_skl(B,A))],[f5821])).
% 0.73/1.58 fof(f5825,plain,(
% 0.73/1.58 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~r2_hidden(X0,X2)|~r1_xboole_0(X1,X2))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f5822])).
% 0.73/1.58 fof(f22086,plain,(
% 0.73/1.58 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((~v1_group_1(B)|~m1_group_2(B,A))|r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)))))),
% 0.73/1.58 inference(pre_NNF_transformation,[status(thm)],[f5658])).
% 0.73/1.58 fof(f22087,plain,(
% 0.73/1.58 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_group_1(X1)|~m1_group_2(X1,X0)|r2_hidden(k2_group_1(X0),k1_funct_1(k1_latsubgr(X0),X1)))),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22086])).
% 0.73/1.58 fof(f22088,plain,(
% 0.73/1.58 (?[A]: ((((~v3_struct_0(A)&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: ((v1_group_1(B)&m1_group_2(B,A))&k1_funct_1(k1_latsubgr(A),B)=k1_xboole_0))))),
% 0.73/1.58 inference(pre_NNF_transformation,[status(thm)],[f5660])).
% 0.73/1.58 fof(f22089,plain,(
% 0.73/1.58 ((((~v3_struct_0(sK1495_skl)&v3_group_1(sK1495_skl))&v4_group_1(sK1495_skl))&l1_group_1(sK1495_skl))&((v1_group_1(sK1496_skl)&m1_group_2(sK1496_skl,sK1495_skl))&k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=k1_xboole_0))),
% 0.73/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK1495_skl,sK1496_skl]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl)],[f22088])).
% 0.73/1.58 fof(f22090,plain,(
% 0.73/1.58 ~v3_struct_0(sK1495_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22091,plain,(
% 0.73/1.58 v3_group_1(sK1495_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22092,plain,(
% 0.73/1.58 v4_group_1(sK1495_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22093,plain,(
% 0.73/1.58 l1_group_1(sK1495_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22094,plain,(
% 0.73/1.58 v1_group_1(sK1496_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22095,plain,(
% 0.73/1.58 m1_group_2(sK1496_skl,sK1495_skl)),
% 0.73/1.58 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.73/1.58 fof(f22096,plain,(
% 0.73/1.58 k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=k1_xboole_0),
% 0.74/1.61 inference(cnf_transformation,[status(thm)],[f22089])).
% 0.74/1.61 fof(f23878,plain,(
% 0.74/1.61 ![X0,X1]: (r1_tarski(X0,X1)|~X0=k1_xboole_0)),
% 0.74/1.61 inference(resolution,[status(thm)],[f5689,f5753])).
% 0.74/1.61 fof(f23912,plain,(
% 0.74/1.61 ![X0]: (r1_tarski(k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl),X0))),
% 0.74/1.61 inference(resolution,[status(thm)],[f23878,f22096])).
% 0.74/1.61 fof(f23914,plain,(
% 0.74/1.61 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 0.74/1.61 inference(forward_demodulation,[status(thm)],[f22096,f23912])).
% 0.74/1.61 fof(f23915,plain,(
% 0.74/1.61 ![X0,X1]: (~r2_hidden(X0,k1_xboole_0)|r2_hidden(X0,X1))),
% 0.74/1.61 inference(resolution,[status(thm)],[f23914,f5688])).
% 0.74/1.61 fof(f24132,plain,(
% 0.74/1.61 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)|r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))),
% 0.74/1.61 inference(resolution,[status(thm)],[f22087,f22095])).
% 0.74/1.61 fof(f24134,plain,(
% 0.74/1.61 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)|r2_hidden(k2_group_1(sK1495_skl),k1_xboole_0)),
% 0.74/1.61 inference(forward_demodulation,[status(thm)],[f22096,f24132])).
% 0.74/1.61 fof(f24135,plain,(
% 0.74/1.61 ~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)|r2_hidden(k2_group_1(sK1495_skl),k1_xboole_0)),
% 0.74/1.61 inference(forward_subsumption_resolution,[status(thm)],[f24134,f22090])).
% 0.74/1.61 fof(f24712,plain,(
% 0.74/1.61 ![X0,X1]: (X0=k3_xboole_0(X0,X1)|~X0=k1_xboole_0)),
% 0.74/1.61 inference(resolution,[status(thm)],[f5771,f5753])).
% 0.74/1.61 fof(f25000,plain,(
% 0.74/1.61 ![X0]: (k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=k3_xboole_0(k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl),X0))),
% 0.74/1.61 inference(resolution,[status(thm)],[f24712,f22096])).
% 0.74/1.61 fof(f25004,plain,(
% 0.74/1.61 ![X0]: (k1_xboole_0=k3_xboole_0(k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl),X0))),
% 0.74/1.61 inference(forward_demodulation,[status(thm)],[f22096,f25000])).
% 0.74/1.61 fof(f25005,plain,(
% 0.74/1.61 ![X0]: (k1_xboole_0=k3_xboole_0(k1_xboole_0,X0))),
% 0.74/1.61 inference(forward_demodulation,[status(thm)],[f22096,f25004])).
% 0.74/1.61 fof(f25174,plain,(
% 0.74/1.61 ![X0]: (r1_xboole_0(k1_xboole_0,X0))),
% 0.74/1.61 inference(resolution,[status(thm)],[f5790,f25005])).
% 0.74/1.61 fof(f25187,plain,(
% 0.74/1.61 ~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)|r2_hidden(k2_group_1(sK1495_skl),k1_xboole_0)),
% 0.74/1.61 inference(forward_subsumption_resolution,[status(thm)],[f24135,f22091])).
% 0.74/1.61 fof(f25833,plain,(
% 0.74/1.61 ![X0,X1]: (~r2_hidden(X0,k1_xboole_0)|~r2_hidden(X0,X1))),
% 0.74/1.61 inference(resolution,[status(thm)],[f5825,f25174])).
% 0.74/1.61 fof(f25835,plain,(
% 0.74/1.61 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 0.74/1.61 inference(forward_subsumption_resolution,[status(thm)],[f25833,f23915])).
% 0.74/1.61 fof(f25836,plain,(
% 0.74/1.61 ~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)),
% 0.74/1.61 inference(backward_subsumption_resolution,[status(thm)],[f25187,f25835])).
% 0.74/1.61 fof(f25876,plain,(
% 0.74/1.61 ~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)),
% 0.74/1.61 inference(forward_subsumption_resolution,[status(thm)],[f25836,f22092])).
% 0.74/1.61 fof(f26163,plain,(
% 0.74/1.61 ~v1_group_1(sK1496_skl)),
% 0.74/1.61 inference(forward_subsumption_resolution,[status(thm)],[f25876,f22093])).
% 0.74/1.61 fof(f26164,plain,(
% 0.74/1.61 $false),
% 0.74/1.61 inference(backward_subsumption_resolution,[status(thm)],[f22094,f26163])).
% 0.74/1.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.75/1.77 % Elapsed time: 1.136658 seconds
% 0.75/1.77 % CPU time: 4.250837 seconds
% 0.75/1.77 % Total memory used: 995.765 MB
% 0.75/1.77 % Net memory used: 988.029 MB
%------------------------------------------------------------------------------