%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP642+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:37:01 PM UTC 2026
% Result : Theorem 32.38s 13.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP642+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n002.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Sun Sep 20 20:28:07 UTC 2026
% 0.14/0.42 % CPUTime :
% 9.97/10.23 % Drodi V4.1.1
% 32.38/13.25 % Refutation found
% 32.38/13.25 % SZS status Theorem for theBenchmark: Theorem is valid
% 32.38/13.25 % SZS output start CNFRefutation for theBenchmark
% 32.38/13.25 fof(f8,axiom,(
% 32.38/13.25 (! [A,B] :( r1_tarski(A,B)<=> (! [C] :( r2_hidden(C,A)=> r2_hidden(C,B) ) )) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f25,axiom,(
% 32.38/13.25 (? [A] : v1_xboole_0(A) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f29,axiom,(
% 32.38/13.25 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f33,axiom,(
% 32.38/13.25 (! [A] :( v1_xboole_0(A)<=> A = k1_xboole_0 ) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f41,axiom,(
% 32.38/13.25 (! [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) ) ) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f918,axiom,(
% 32.38/13.25 (? [A] :( v1_relat_1(A)& v1_xboole_0(A)& v1_funct_1(A) ) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f36509,axiom,(
% 32.38/13.25 (! [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)) ) )) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f36510,conjecture,(
% 32.38/13.25 (! [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 ) )) )),
% 32.38/13.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.38/13.25 fof(f36511,negated_conjecture,(
% 32.38/13.25 ~((! [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 ) )) ))),
% 32.38/13.25 inference(negated_conjecture,[status(cth)],[f36510])).
% 32.38/13.25 fof(f36535,plain,(
% 32.38/13.25 ![A,B]: (r1_tarski(A,B)<=>(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))),
% 32.38/13.25 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 32.38/13.25 fof(f36536,plain,(
% 32.38/13.25 ![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)))))),
% 32.38/13.25 inference(NNF_transformation,[status(thm)],[f36535])).
% 32.38/13.25 fof(f36537,plain,(
% 32.38/13.25 (![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)))))),
% 32.38/13.25 inference(miniscoping,[status(thm)],[f36536])).
% 32.38/13.25 fof(f36538,plain,(
% 32.38/13.25 (![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))))),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f36537])).
% 32.38/13.25 fof(f36539,plain,(
% 32.38/13.25 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r2_hidden(X2,X0)|r2_hidden(X2,X1))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36538])).
% 32.38/13.25 fof(f36540,plain,(
% 32.38/13.25 ![X0,X1]: (r1_tarski(X0,X1)|r2_hidden(sK3_skl(X1,X0),X0))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36538])).
% 32.38/13.25 fof(f36591,plain,(
% 32.38/13.25 v1_xboole_0(sK20_skl)),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f25])).
% 32.38/13.25 fof(f36592,plain,(
% 32.38/13.25 v1_xboole_0(sK20_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36591])).
% 32.38/13.25 fof(f36601,plain,(
% 32.38/13.25 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 32.38/13.25 inference(NNF_transformation,[status(thm)],[f29])).
% 32.38/13.25 fof(f36602,plain,(
% 32.38/13.25 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 32.38/13.25 inference(miniscoping,[status(thm)],[f36601])).
% 32.38/13.25 fof(f36603,plain,(
% 32.38/13.25 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f36602])).
% 32.38/13.25 fof(f36604,plain,(
% 32.38/13.25 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36603])).
% 32.38/13.25 fof(f36633,plain,(
% 32.38/13.25 ![A]: ((~v1_xboole_0(A)|A=k1_xboole_0)&(v1_xboole_0(A)|~A=k1_xboole_0))),
% 32.38/13.25 inference(NNF_transformation,[status(thm)],[f33])).
% 32.38/13.25 fof(f36634,plain,(
% 32.38/13.25 (![A]: (~v1_xboole_0(A)|A=k1_xboole_0))&(![A]: (v1_xboole_0(A)|~A=k1_xboole_0))),
% 32.38/13.25 inference(miniscoping,[status(thm)],[f36633])).
% 32.38/13.25 fof(f36635,plain,(
% 32.38/13.25 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36634])).
% 32.38/13.25 fof(f36671,plain,(
% 32.38/13.25 ![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)))),
% 32.38/13.25 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 32.38/13.25 fof(f36672,plain,(
% 32.38/13.25 (![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)))),
% 32.38/13.25 inference(miniscoping,[status(thm)],[f36671])).
% 32.38/13.25 fof(f36673,plain,(
% 32.38/13.25 (![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)))),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(C,sK27_skl(B,A))],[f36672])).
% 32.38/13.25 fof(f36674,plain,(
% 32.38/13.25 ![X0,X1]: (r1_xboole_0(X0,X1)|r2_hidden(sK27_skl(X1,X0),X0))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36673])).
% 32.38/13.25 fof(f36676,plain,(
% 32.38/13.25 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~r2_hidden(X0,X2)|~r1_xboole_0(X1,X2))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f36673])).
% 32.38/13.25 fof(f38637,plain,(
% 32.38/13.25 ((v1_relat_1(sK168_skl)&v1_xboole_0(sK168_skl))&v1_funct_1(sK168_skl))),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK168_skl]),skolemize(A,sK168_skl)],[f918])).
% 32.38/13.25 fof(f38639,plain,(
% 32.38/13.25 v1_xboole_0(sK168_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f38637])).
% 32.38/13.25 fof(f162772,plain,(
% 32.38/13.25 ![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)))))),
% 32.38/13.25 inference(pre_NNF_transformation,[status(thm)],[f36509])).
% 32.38/13.25 fof(f162773,plain,(
% 32.38/13.25 ![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)))),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162772])).
% 32.38/13.25 fof(f162774,plain,(
% 32.38/13.25 (?[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))))),
% 32.38/13.25 inference(pre_NNF_transformation,[status(thm)],[f36511])).
% 32.38/13.25 fof(f162775,plain,(
% 32.38/13.25 ((((~v3_struct_0(sK12737_skl)&v3_group_1(sK12737_skl))&v4_group_1(sK12737_skl))&l1_group_1(sK12737_skl))&((v1_group_1(sK12738_skl)&m1_group_2(sK12738_skl,sK12737_skl))&k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)=k1_xboole_0))),
% 32.38/13.25 inference(skolemize,[status(esa),new_symbols(skolem,[sK12737_skl,sK12738_skl]),skolemize(A,sK12737_skl),skolemize(B,sK12738_skl)],[f162774])).
% 32.38/13.25 fof(f162776,plain,(
% 32.38/13.25 ~v3_struct_0(sK12737_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162777,plain,(
% 32.38/13.25 v3_group_1(sK12737_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162778,plain,(
% 32.38/13.25 v4_group_1(sK12737_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162779,plain,(
% 32.38/13.25 l1_group_1(sK12737_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162780,plain,(
% 32.38/13.25 v1_group_1(sK12738_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162781,plain,(
% 32.38/13.25 m1_group_2(sK12738_skl,sK12737_skl)),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f162782,plain,(
% 32.38/13.25 k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)=k1_xboole_0),
% 32.38/13.25 inference(cnf_transformation,[status(thm)],[f162775])).
% 32.38/13.25 fof(f183645,plain,(
% 32.38/13.25 sK20_skl=k1_xboole_0),
% 32.38/13.25 inference(resolution,[status(thm)],[f36592,f36635])).
% 32.38/13.25 fof(f183718,plain,(
% 32.38/13.25 ![X0,X1]: (r1_tarski(X0,X1)|~X0=k1_xboole_0)),
% 32.38/13.25 inference(resolution,[status(thm)],[f36540,f36604])).
% 32.38/13.25 fof(f183875,plain,(
% 32.38/13.25 k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl)=sK20_skl),
% 32.38/13.25 inference(backward_demodulation,[status(thm)],[f183645,f162782])).
% 32.38/13.25 fof(f183881,plain,(
% 32.38/13.25 ![X0]: (~v1_xboole_0(X0)|X0=sK20_skl)),
% 32.38/13.25 inference(backward_demodulation,[status(thm)],[f183645,f36635])).
% 32.38/13.25 fof(f183882,plain,(
% 32.38/13.25 ![X0,X1]: (~X0=sK20_skl|~r2_hidden(X1,X0))),
% 32.38/13.25 inference(backward_demodulation,[status(thm)],[f183645,f36604])).
% 37.52/13.96 fof(f184116,plain,(
% 37.52/13.96 ![X0,X1]: (r1_tarski(X0,X1)|~X0=sK20_skl)),
% 37.52/13.96 inference(forward_demodulation,[status(thm)],[f183645,f183718])).
% 37.52/13.96 fof(f184118,plain,(
% 37.52/13.96 ![X0]: (r1_tarski(k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl),X0))),
% 37.52/13.96 inference(resolution,[status(thm)],[f184116,f183875])).
% 37.52/13.96 fof(f184123,plain,(
% 37.52/13.96 ![X0]: (r1_tarski(sK20_skl,X0))),
% 37.52/13.96 inference(forward_demodulation,[status(thm)],[f183875,f184118])).
% 37.52/13.96 fof(f184144,plain,(
% 37.52/13.96 v3_struct_0(sK12737_skl)|~v3_group_1(sK12737_skl)|~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)|r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))),
% 37.52/13.96 inference(resolution,[status(thm)],[f162773,f162781])).
% 37.52/13.96 fof(f184146,plain,(
% 37.52/13.96 v3_struct_0(sK12737_skl)|~v3_group_1(sK12737_skl)|~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)|r2_hidden(k2_group_1(sK12737_skl),sK20_skl)),
% 37.52/13.96 inference(forward_demodulation,[status(thm)],[f183875,f184144])).
% 37.52/13.96 fof(f184147,plain,(
% 37.52/13.96 ~v3_group_1(sK12737_skl)|~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)|r2_hidden(k2_group_1(sK12737_skl),sK20_skl)),
% 37.52/13.96 inference(forward_subsumption_resolution,[status(thm)],[f184146,f162776])).
% 37.52/13.96 fof(f184398,plain,(
% 37.52/13.96 ![X0,X1]: (~r2_hidden(X0,sK20_skl)|r2_hidden(X0,X1))),
% 37.52/13.96 inference(resolution,[status(thm)],[f184123,f36539])).
% 37.52/13.96 fof(f184414,plain,(
% 37.52/13.96 sK168_skl=sK20_skl),
% 37.52/13.96 inference(resolution,[status(thm)],[f38639,f183881])).
% 37.52/13.96 fof(f185480,plain,(
% 37.52/13.96 ![X0,X1]: (r1_xboole_0(X0,X1)|~X0=sK20_skl)),
% 37.52/13.96 inference(resolution,[status(thm)],[f36674,f183882])).
% 37.52/13.96 fof(f185711,plain,(
% 37.52/13.96 ![X0]: (r1_xboole_0(sK168_skl,X0))),
% 37.52/13.96 inference(resolution,[status(thm)],[f185480,f184414])).
% 37.52/13.96 fof(f185717,plain,(
% 37.52/13.96 ![X0]: (r1_xboole_0(sK20_skl,X0))),
% 37.52/13.96 inference(forward_demodulation,[status(thm)],[f184414,f185711])).
% 37.52/13.96 fof(f185722,plain,(
% 37.52/13.96 ![X0,X1]: (~r2_hidden(X0,sK20_skl)|~r2_hidden(X0,X1))),
% 37.52/13.96 inference(resolution,[status(thm)],[f185717,f36676])).
% 37.52/13.96 fof(f185724,plain,(
% 37.52/13.96 ![X0]: (~r2_hidden(X0,sK20_skl))),
% 37.52/13.96 inference(forward_subsumption_resolution,[status(thm)],[f185722,f184398])).
% 37.52/13.96 fof(f185947,plain,(
% 37.52/13.96 ~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)|r2_hidden(k2_group_1(sK12737_skl),sK20_skl)),
% 37.52/13.96 inference(forward_subsumption_resolution,[status(thm)],[f184147,f162777])).
% 37.52/13.96 fof(f186033,plain,(
% 37.52/13.96 ~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)),
% 37.52/13.96 inference(backward_subsumption_resolution,[status(thm)],[f185947,f185724])).
% 37.52/13.96 fof(f186072,plain,(
% 37.52/13.96 ~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)),
% 37.52/13.96 inference(forward_subsumption_resolution,[status(thm)],[f186033,f162778])).
% 37.52/13.96 fof(f186508,plain,(
% 37.52/13.96 ~v1_group_1(sK12738_skl)),
% 37.52/13.96 inference(forward_subsumption_resolution,[status(thm)],[f186072,f162779])).
% 37.52/13.96 fof(f186509,plain,(
% 37.52/13.96 $false),
% 37.52/13.96 inference(backward_subsumption_resolution,[status(thm)],[f162780,f186508])).
% 37.52/13.96 % SZS output end CNFRefutation for theBenchmark.p
% 10.96/14.53 % Elapsed time: 13.944487 seconds
% 10.96/14.53 % CPU time: 34.496915 seconds
% 10.96/14.53 % Total memory used: 11.445 GB
% 10.96/14.53 % Net memory used: 11.387 GB
%------------------------------------------------------------------------------