%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP642+3 : 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 : n003.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 2.10s 2.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:27:06 UTC 2026
% 0.08/0.36 % CPUTime :
% 1.80/2.11 % Drodi V4.1.1
% 2.10/2.97 % Refutation found
% 2.10/2.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.10/2.97 % SZS output start CNFRefutation for theBenchmark
% 2.10/2.97 fof(f29,axiom,(
% 2.10/2.97 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 2.10/2.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/2.97 fof(f13983,axiom,(
% 2.10/2.97 (! [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)) ) )) )),
% 2.10/2.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/2.97 fof(f13984,conjecture,(
% 2.10/2.97 (! [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 ) )) )),
% 2.10/2.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.10/2.97 fof(f13985,negated_conjecture,(
% 2.10/2.97 ~((! [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 ) )) ))),
% 2.10/2.97 inference(negated_conjecture,[status(cth)],[f13984])).
% 2.10/2.97 fof(f14075,plain,(
% 2.10/2.97 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 2.10/2.97 inference(NNF_transformation,[status(thm)],[f29])).
% 2.10/2.97 fof(f14076,plain,(
% 2.10/2.97 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 2.10/2.97 inference(miniscoping,[status(thm)],[f14075])).
% 2.10/2.97 fof(f14077,plain,(
% 2.10/2.97 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 2.10/2.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f14076])).
% 2.10/2.97 fof(f14078,plain,(
% 2.10/2.97 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f14077])).
% 2.10/2.97 fof(f59577,plain,(
% 2.10/2.97 ![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)))))),
% 2.10/2.97 inference(pre_NNF_transformation,[status(thm)],[f13983])).
% 2.10/2.97 fof(f59578,plain,(
% 2.10/2.97 ![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)))),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 2.10/2.97 fof(f59579,plain,(
% 2.10/2.97 (?[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))))),
% 2.10/2.97 inference(pre_NNF_transformation,[status(thm)],[f13985])).
% 2.10/2.97 fof(f59580,plain,(
% 2.10/2.97 ((((~v3_struct_0(sK4179_skl)&v3_group_1(sK4179_skl))&v4_group_1(sK4179_skl))&l1_group_1(sK4179_skl))&((v1_group_1(sK4180_skl)&m1_group_2(sK4180_skl,sK4179_skl))&k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl)=k1_xboole_0))),
% 2.10/2.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK4179_skl,sK4180_skl]),skolemize(A,sK4179_skl),skolemize(B,sK4180_skl)],[f59579])).
% 2.10/2.97 fof(f59581,plain,(
% 2.10/2.97 ~v3_struct_0(sK4179_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59582,plain,(
% 2.10/2.97 v3_group_1(sK4179_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59583,plain,(
% 2.10/2.97 v4_group_1(sK4179_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59584,plain,(
% 2.10/2.97 l1_group_1(sK4179_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59585,plain,(
% 2.10/2.97 v1_group_1(sK4180_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59586,plain,(
% 2.10/2.97 m1_group_2(sK4180_skl,sK4179_skl)),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f59587,plain,(
% 2.10/2.97 k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl)=k1_xboole_0),
% 2.10/2.97 inference(cnf_transformation,[status(thm)],[f59580])).
% 2.10/2.97 fof(f62888,plain,(
% 2.10/2.97 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 2.10/2.97 inference(destructive_equality_resolution,[status(thm)],[f14078])).
% 2.10/2.97 fof(f66613,plain,(
% 2.10/2.97 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))),
% 2.10/2.97 inference(resolution,[status(thm)],[f59578,f59586])).
% 2.10/2.97 fof(f66618,plain,(
% 2.10/2.97 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(forward_demodulation,[status(thm)],[f59587,f66613])).
% 9.36/3.15 fof(f66619,plain,(
% 9.36/3.15 ~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(forward_subsumption_resolution,[status(thm)],[f66618,f59581])).
% 9.36/3.15 fof(f66738,plain,(
% 9.36/3.15 ~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(forward_subsumption_resolution,[status(thm)],[f66619,f59582])).
% 9.36/3.15 fof(f66739,plain,(
% 9.36/3.15 ~v4_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(resolution,[status(thm)],[f66738,f59584])).
% 9.36/3.15 fof(f66740,plain,(
% 9.36/3.15 ~v1_group_1(sK4180_skl)|r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(forward_subsumption_resolution,[status(thm)],[f66739,f59583])).
% 9.36/3.15 fof(f66741,plain,(
% 9.36/3.15 r2_hidden(k2_group_1(sK4179_skl),k1_xboole_0)),
% 9.36/3.15 inference(forward_subsumption_resolution,[status(thm)],[f66740,f59585])).
% 9.36/3.15 fof(f66742,plain,(
% 9.36/3.15 $false),
% 9.36/3.15 inference(resolution,[status(thm)],[f66741,f62888])).
% 9.36/3.15 % SZS output end CNFRefutation for theBenchmark.p
% 2.13/3.27 % Elapsed time: 2.855622 seconds
% 2.13/3.27 % CPU time: 8.817179 seconds
% 2.13/3.27 % Total memory used: 3.911 GB
% 2.13/3.27 % Net memory used: 3.889 GB
%------------------------------------------------------------------------------