%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP623+1 : 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 : n010.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:36:56 PM UTC 2026
% Result : Theorem 0.12s 5.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP623+1 : 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/5.36 % Computer : n010.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Sun Sep 20 20:19:46 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.38 % Drodi V4.1.1
% 0.12/5.55 % Refutation found
% 0.12/5.55 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/5.55 % SZS output start CNFRefutation for theBenchmark
% 0.12/5.55 fof(f1,conjecture,(
% 0.12/5.55 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> r1_tarski(k4_autgroup(A),k1_autgroup(A)) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f2,negated_conjecture,(
% 0.12/5.55 ~((! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> r1_tarski(k4_autgroup(A),k1_autgroup(A)) ) ))),
% 0.12/5.55 inference(negated_conjecture,[status(cth)],[f1])).
% 0.12/5.55 fof(f13,axiom,(
% 0.12/5.55 (! [A,B] :( r1_tarski(A,B)<=> (! [C] :( r2_hidden(C,A)=> r2_hidden(C,B) ) )) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f15,axiom,(
% 0.12/5.55 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f19,axiom,(
% 0.12/5.55 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_fraenkel(k4_autgroup(A),u1_struct_0(A),u1_struct_0(A)) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f20,axiom,(
% 0.12/5.55 (! [A] :( l1_group_1(A)=> l1_struct_0(A) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f22,axiom,(
% 0.12/5.55 (! [A,B,C] :( m1_fraenkel(C,A,B)=> ( ~ v1_xboole_0(C)& v1_fraenkel(C) ) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f33,axiom,(
% 0.12/5.55 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f53,axiom,(
% 0.12/5.55 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> (? [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))& ~ v1_xboole_0(B) ) )) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f54,axiom,(
% 0.12/5.55 (! [A,B,C] :( ( ~ v1_xboole_0(B)& m1_fraenkel(C,A,B) )=> (! [D] :( m2_fraenkel(D,A,B,C)<=> m1_subset_1(D,C) ) )) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f57,axiom,(
% 0.12/5.55 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) )) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f58,axiom,(
% 0.12/5.55 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f59,axiom,(
% 0.12/5.55 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f60,axiom,(
% 0.12/5.55 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f64,axiom,(
% 0.12/5.55 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 0.12/5.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/5.55 fof(f66,plain,(
% 0.12/5.55 (?[A]: (((((~v3_struct_0(A)&v1_group_1(A))&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&~r1_tarski(k4_autgroup(A),k1_autgroup(A))))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/5.55 fof(f67,plain,(
% 0.12/5.55 (((((~v3_struct_0(sK0_skl)&v1_group_1(sK0_skl))&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&~r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl)))),
% 0.12/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f66])).
% 0.12/5.55 fof(f68,plain,(
% 0.12/5.55 ~v3_struct_0(sK0_skl)),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f69,plain,(
% 0.12/5.55 v1_group_1(sK0_skl)),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f70,plain,(
% 0.12/5.55 v3_group_1(sK0_skl)),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f71,plain,(
% 0.12/5.55 v4_group_1(sK0_skl)),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f72,plain,(
% 0.12/5.55 l1_group_1(sK0_skl)),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f73,plain,(
% 0.12/5.55 ~r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/5.55 fof(f106,plain,(
% 0.12/5.55 ![A,B]: (r1_tarski(A,B)<=>(![C]: (~r2_hidden(C,A)|r2_hidden(C,B))))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.12/5.55 fof(f107,plain,(
% 0.12/5.55 ![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.12/5.55 inference(NNF_transformation,[status(thm)],[f106])).
% 0.12/5.55 fof(f108,plain,(
% 0.12/5.55 (![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.12/5.55 inference(miniscoping,[status(thm)],[f107])).
% 0.12/5.55 fof(f109,plain,(
% 0.12/5.55 (![A,B]: (~r1_tarski(A,B)|(![C]: (~r2_hidden(C,A)|r2_hidden(C,B)))))&(![A,B]: (r1_tarski(A,B)|(r2_hidden(sK1_skl(B,A),A)&~r2_hidden(sK1_skl(B,A),B))))),
% 0.12/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f108])).
% 0.12/5.55 fof(f110,plain,(
% 0.12/5.55 ![X0,X1,X2]: (~r1_tarski(X0,X1)|~r2_hidden(X2,X0)|r2_hidden(X2,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/5.55 fof(f111,plain,(
% 0.12/5.55 ![X0,X1]: (r1_tarski(X0,X1)|r2_hidden(sK1_skl(X1,X0),X0))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/5.55 fof(f112,plain,(
% 0.12/5.55 ![X0,X1]: (r1_tarski(X0,X1)|~r2_hidden(sK1_skl(X1,X0),X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f109])).
% 0.12/5.55 fof(f116,plain,(
% 0.12/5.55 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_fraenkel(k1_autgroup(A),u1_struct_0(A),u1_struct_0(A)))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.12/5.55 fof(f117,plain,(
% 0.12/5.55 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_fraenkel(k1_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f116])).
% 0.12/5.55 fof(f118,plain,(
% 0.12/5.55 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_fraenkel(k4_autgroup(A),u1_struct_0(A),u1_struct_0(A)))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/5.55 fof(f119,plain,(
% 0.12/5.55 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_fraenkel(k4_autgroup(X0),u1_struct_0(X0),u1_struct_0(X0)))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f118])).
% 0.12/5.55 fof(f120,plain,(
% 0.12/5.55 ![A]: (~l1_group_1(A)|l1_struct_0(A))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.12/5.55 fof(f121,plain,(
% 0.12/5.55 ![X0]: (~l1_group_1(X0)|l1_struct_0(X0))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f120])).
% 0.12/5.55 fof(f122,plain,(
% 0.12/5.55 ![A,B,C]: (~m1_fraenkel(C,A,B)|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.12/5.55 fof(f123,plain,(
% 0.12/5.55 ![C]: ((![A,B]: ~m1_fraenkel(C,A,B))|(~v1_xboole_0(C)&v1_fraenkel(C)))),
% 0.12/5.55 inference(miniscoping,[status(thm)],[f122])).
% 0.12/5.55 fof(f124,plain,(
% 0.12/5.55 ![X0,X1,X2]: (~m1_fraenkel(X0,X1,X2)|~v1_xboole_0(X0))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f123])).
% 0.12/5.55 fof(f144,plain,(
% 0.12/5.55 ![A]: m1_subset_1(sK6_skl(A),A)),
% 0.12/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(B,sK6_skl(A))],[f33])).
% 0.12/5.55 fof(f145,plain,(
% 0.12/5.55 ![X0]: (m1_subset_1(sK6_skl(X0),X0))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f144])).
% 0.12/5.55 fof(f209,plain,(
% 0.12/5.55 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|(?[B]: (m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))&~v1_xboole_0(B))))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.12/5.55 fof(f210,plain,(
% 0.12/5.55 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|(m1_subset_1(sK22_skl(A),k1_zfmisc_1(u1_struct_0(A)))&~v1_xboole_0(sK22_skl(A))))),
% 0.12/5.55 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f209])).
% 0.12/5.55 fof(f211,plain,(
% 0.12/5.55 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|m1_subset_1(sK22_skl(X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f210])).
% 0.12/5.55 fof(f212,plain,(
% 0.12/5.55 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(sK22_skl(X0)))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f210])).
% 0.12/5.55 fof(f213,plain,(
% 0.12/5.55 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: (m2_fraenkel(D,A,B,C)<=>m1_subset_1(D,C))))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.12/5.55 fof(f214,plain,(
% 0.12/5.55 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|(![D]: ((~m2_fraenkel(D,A,B,C)|m1_subset_1(D,C))&(m2_fraenkel(D,A,B,C)|~m1_subset_1(D,C)))))),
% 0.12/5.55 inference(NNF_transformation,[status(thm)],[f213])).
% 0.12/5.55 fof(f215,plain,(
% 0.12/5.55 ![A,B,C]: ((v1_xboole_0(B)|~m1_fraenkel(C,A,B))|((![D]: (~m2_fraenkel(D,A,B,C)|m1_subset_1(D,C)))&(![D]: (m2_fraenkel(D,A,B,C)|~m1_subset_1(D,C)))))),
% 0.12/5.55 inference(miniscoping,[status(thm)],[f214])).
% 0.12/5.55 fof(f216,plain,(
% 0.12/5.55 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|~m2_fraenkel(X3,X2,X0,X1)|m1_subset_1(X3,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f215])).
% 0.12/5.55 fof(f217,plain,(
% 0.12/5.55 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_fraenkel(X1,X2,X0)|m2_fraenkel(X3,X2,X0,X1)|~m1_subset_1(X3,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f215])).
% 0.12/5.55 fof(f224,plain,(
% 0.12/5.55 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))|m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)))))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.12/5.55 fof(f225,plain,(
% 0.12/5.55 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))|m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f224])).
% 0.12/5.55 fof(f226,plain,(
% 0.12/5.55 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f58])).
% 0.12/5.55 fof(f227,plain,(
% 0.12/5.55 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f226])).
% 0.12/5.55 fof(f228,plain,(
% 0.12/5.55 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 0.12/5.55 fof(f229,plain,(
% 0.12/5.55 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f228])).
% 0.12/5.55 fof(f230,plain,(
% 0.12/5.55 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 0.12/5.55 inference(NNF_transformation,[status(thm)],[f60])).
% 0.12/5.55 fof(f231,plain,(
% 0.12/5.55 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 0.12/5.55 inference(miniscoping,[status(thm)],[f230])).
% 0.12/5.55 fof(f232,plain,(
% 0.12/5.55 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f231])).
% 0.12/5.55 fof(f242,plain,(
% 0.12/5.55 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 0.12/5.55 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 0.12/5.55 fof(f243,plain,(
% 0.12/5.55 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 0.12/5.55 inference(miniscoping,[status(thm)],[f242])).
% 0.12/5.55 fof(f244,plain,(
% 0.12/5.55 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 0.12/5.55 inference(cnf_transformation,[status(thm)],[f243])).
% 0.12/5.55 fof(f252,plain,(
% 0.12/5.55 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|m1_fraenkel(k1_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.12/5.55 inference(resolution,[status(thm)],[f117,f72])).
% 0.12/5.55 fof(f253,definition,(
% 0.12/5.55 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f254,plain,(
% 0.12/5.55 v3_struct_0(sK0_skl)|~sQ0_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f253])).
% 0.12/5.55 fof(f256,definition,(
% 0.12/5.55 sQ1_spl <=> (v1_group_1(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f258,plain,(
% 0.12/5.55 ~v1_group_1(sK0_skl)|sQ1_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f256])).
% 0.12/5.55 fof(f259,definition,(
% 0.12/5.55 sQ2_spl <=> (v3_group_1(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f261,plain,(
% 0.12/5.55 ~v3_group_1(sK0_skl)|sQ2_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f259])).
% 0.12/5.55 fof(f262,definition,(
% 0.12/5.55 sQ3_spl <=> (v4_group_1(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f264,plain,(
% 0.12/5.55 ~v4_group_1(sK0_skl)|sQ3_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f262])).
% 0.12/5.55 fof(f265,definition,(
% 0.12/5.55 sQ4_spl <=> (m1_fraenkel(k1_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f266,plain,(
% 0.12/5.55 m1_fraenkel(k1_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ4_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f265])).
% 0.12/5.55 fof(f268,plain,(
% 0.12/5.55 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ4_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f252,f253,f256,f259,f262,f265])).
% 0.12/5.55 fof(f269,plain,(
% 0.12/5.55 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 0.12/5.55 inference(resolution,[status(thm)],[f119,f72])).
% 0.12/5.55 fof(f270,definition,(
% 0.12/5.55 sQ5_spl <=> (m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f271,plain,(
% 0.12/5.55 m1_fraenkel(k4_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|~sQ5_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f270])).
% 0.12/5.55 fof(f273,plain,(
% 0.12/5.55 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ5_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f269,f253,f256,f259,f262,f270])).
% 0.12/5.55 fof(f274,plain,(
% 0.12/5.55 $false|sQ3_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f264,f71])).
% 0.12/5.55 fof(f275,plain,(
% 0.12/5.55 sQ3_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f274])).
% 0.12/5.55 fof(f276,plain,(
% 0.12/5.55 $false|sQ2_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f261,f70])).
% 0.12/5.55 fof(f277,plain,(
% 0.12/5.55 sQ2_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f276])).
% 0.12/5.55 fof(f278,plain,(
% 0.12/5.55 $false|sQ1_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f258,f69])).
% 0.12/5.55 fof(f279,plain,(
% 0.12/5.55 sQ1_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f278])).
% 0.12/5.55 fof(f280,plain,(
% 0.12/5.55 $false|~sQ0_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f254,f68])).
% 0.12/5.55 fof(f281,plain,(
% 0.12/5.55 ~sQ0_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f280])).
% 0.12/5.55 fof(f415,plain,(
% 0.12/5.55 l1_struct_0(sK0_skl)),
% 0.12/5.55 inference(resolution,[status(thm)],[f121,f72])).
% 0.12/5.55 fof(f433,plain,(
% 0.12/5.55 ~v1_xboole_0(k1_autgroup(sK0_skl))|~sQ4_spl),
% 0.12/5.55 inference(resolution,[status(thm)],[f124,f266])).
% 0.12/5.55 fof(f476,plain,(
% 0.12/5.55 ![X0,X1]: (r1_tarski(X0,X1)|m1_subset_1(sK1_skl(X1,X0),X0))),
% 0.12/5.55 inference(resolution,[status(thm)],[f111,f227])).
% 0.12/5.55 fof(f482,plain,(
% 0.12/5.55 ![X0]: (v1_xboole_0(X0)|r2_hidden(sK6_skl(X0),X0))),
% 0.12/5.55 inference(resolution,[status(thm)],[f229,f145])).
% 0.12/5.55 fof(f487,plain,(
% 0.12/5.55 ![X0,X1]: (v1_xboole_0(X0)|~r1_tarski(X0,X1)|r2_hidden(sK6_skl(X0),X1))),
% 0.12/5.55 inference(resolution,[status(thm)],[f482,f110])).
% 0.12/5.55 fof(f533,plain,(
% 0.12/5.55 v3_struct_0(sK0_skl)|m1_subset_1(sK22_skl(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.12/5.55 inference(resolution,[status(thm)],[f211,f415])).
% 0.12/5.55 fof(f534,definition,(
% 0.12/5.55 sQ40_spl <=> (m1_subset_1(sK22_skl(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f535,plain,(
% 0.12/5.55 m1_subset_1(sK22_skl(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ40_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f534])).
% 0.12/5.55 fof(f537,plain,(
% 0.12/5.55 sQ0_spl|sQ40_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f533,f253,f534])).
% 0.12/5.55 fof(f540,plain,(
% 0.12/5.55 r1_tarski(sK22_skl(sK0_skl),u1_struct_0(sK0_skl))|~sQ40_spl),
% 0.12/5.55 inference(resolution,[status(thm)],[f535,f232])).
% 0.12/5.55 fof(f547,definition,(
% 0.12/5.55 sQ42_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f548,plain,(
% 0.12/5.55 v1_xboole_0(u1_struct_0(sK0_skl))|~sQ42_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f547])).
% 0.12/5.55 fof(f570,plain,(
% 0.12/5.55 v1_xboole_0(sK22_skl(sK0_skl))|r2_hidden(sK6_skl(sK22_skl(sK0_skl)),u1_struct_0(sK0_skl))|~sQ40_spl),
% 0.12/5.55 inference(resolution,[status(thm)],[f540,f487])).
% 0.12/5.55 fof(f572,definition,(
% 0.12/5.55 sQ48_spl <=> (v1_xboole_0(sK22_skl(sK0_skl)))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f573,plain,(
% 0.12/5.55 v1_xboole_0(sK22_skl(sK0_skl))|~sQ48_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f572])).
% 0.12/5.55 fof(f575,definition,(
% 0.12/5.55 sQ49_spl <=> (r2_hidden(sK6_skl(sK22_skl(sK0_skl)),u1_struct_0(sK0_skl)))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f576,plain,(
% 0.12/5.55 r2_hidden(sK6_skl(sK22_skl(sK0_skl)),u1_struct_0(sK0_skl))|~sQ49_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f575])).
% 0.12/5.55 fof(f578,plain,(
% 0.12/5.55 sQ48_spl|sQ49_spl|~sQ40_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f570,f572,f575,f534])).
% 0.12/5.55 fof(f579,plain,(
% 0.12/5.55 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)|~sQ48_spl),
% 0.12/5.55 inference(resolution,[status(thm)],[f573,f212])).
% 0.12/5.55 fof(f584,definition,(
% 0.12/5.55 sQ50_spl <=> (l1_struct_0(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f586,plain,(
% 0.12/5.55 ~l1_struct_0(sK0_skl)|sQ50_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f584])).
% 0.12/5.55 fof(f587,plain,(
% 0.12/5.55 sQ0_spl|~sQ50_spl|~sQ48_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f579,f253,f584,f572])).
% 0.12/5.55 fof(f597,plain,(
% 0.12/5.55 $false|sQ50_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f586,f415])).
% 0.12/5.55 fof(f598,plain,(
% 0.12/5.55 sQ50_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f597])).
% 0.12/5.55 fof(f604,plain,(
% 0.12/5.55 ~v1_xboole_0(u1_struct_0(sK0_skl))|~sQ49_spl),
% 0.12/5.55 inference(resolution,[status(thm)],[f576,f244])).
% 0.12/5.55 fof(f634,plain,(
% 0.12/5.55 ![X0]: (v1_xboole_0(u1_struct_0(sK0_skl))|m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|~m1_subset_1(X0,k4_autgroup(sK0_skl))|~sQ5_spl)),
% 0.12/5.55 inference(resolution,[status(thm)],[f217,f271])).
% 0.12/5.55 fof(f644,definition,(
% 0.12/5.55 ![X0]: (sQ57_spl <=> (m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|~m1_subset_1(X0,k4_autgroup(sK0_skl))))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f645,plain,(
% 0.12/5.55 ![X0]: (m2_fraenkel(X0,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|~m1_subset_1(X0,k4_autgroup(sK0_skl))|~sQ57_spl)),
% 0.12/5.55 inference(component_clause,[status(thm)],[f644])).
% 0.12/5.55 fof(f647,plain,(
% 0.12/5.55 sQ42_spl|sQ57_spl|~sQ5_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f634,f547,f644,f270])).
% 0.12/5.55 fof(f656,plain,(
% 0.12/5.55 $false|~sQ49_spl|~sQ42_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f548,f604])).
% 0.12/5.55 fof(f657,plain,(
% 0.12/5.55 ~sQ49_spl|~sQ42_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f656])).
% 0.12/5.55 fof(f658,plain,(
% 0.12/5.55 ![X0]: (m2_fraenkel(sK1_skl(X0,k4_autgroup(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))|r1_tarski(k4_autgroup(sK0_skl),X0)|~sQ57_spl)),
% 0.12/5.55 inference(resolution,[status(thm)],[f645,f476])).
% 0.12/5.55 fof(f932,plain,(
% 0.12/5.55 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|m2_fraenkel(sK1_skl(X0,k4_autgroup(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|~sQ57_spl)),
% 0.12/5.55 inference(resolution,[status(thm)],[f658,f225])).
% 0.12/5.55 fof(f936,definition,(
% 0.12/5.55 ![X0]: (sQ74_spl <=> (r1_tarski(k4_autgroup(sK0_skl),X0)|m2_fraenkel(sK1_skl(X0,k4_autgroup(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f937,plain,(
% 0.12/5.55 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|m2_fraenkel(sK1_skl(X0,k4_autgroup(sK0_skl)),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|~sQ74_spl)),
% 0.12/5.55 inference(component_clause,[status(thm)],[f936])).
% 0.12/5.55 fof(f939,definition,(
% 0.12/5.55 sQ75_spl <=> (l1_group_1(sK0_skl))),
% 0.12/5.55 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.12/5.55 fof(f941,plain,(
% 0.12/5.55 ~l1_group_1(sK0_skl)|sQ75_spl),
% 0.12/5.55 inference(component_clause,[status(thm)],[f939])).
% 0.12/5.55 fof(f942,plain,(
% 0.12/5.55 sQ74_spl|sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl|~sQ75_spl|~sQ57_spl),
% 0.12/5.55 inference(split_clause,[status(thm)],[f932,f936,f253,f256,f259,f262,f939,f644])).
% 0.12/5.55 fof(f955,plain,(
% 0.12/5.55 $false|sQ75_spl),
% 0.12/5.55 inference(forward_subsumption_resolution,[status(thm)],[f941,f72])).
% 0.12/5.55 fof(f956,plain,(
% 0.12/5.55 sQ75_spl),
% 0.12/5.55 inference(contradiction_clause,[status(thm)],[f955])).
% 0.12/5.55 fof(f1039,plain,(
% 0.12/5.55 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|v1_xboole_0(u1_struct_0(sK0_skl))|~m1_fraenkel(k1_autgroup(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))|m1_subset_1(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))|~sQ74_spl)),
% 0.12/5.55 inference(resolution,[status(thm)],[f937,f216])).
% 0.12/5.55 fof(f1042,definition,(
% 0.12/5.55 ![X0]: (sQ88_spl <=> (r1_tarski(k4_autgroup(sK0_skl),X0)|m1_subset_1(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))))),
% 0.12/5.56 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.12/5.56 fof(f1043,plain,(
% 0.12/5.56 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|m1_subset_1(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))|~sQ88_spl)),
% 0.12/5.56 inference(component_clause,[status(thm)],[f1042])).
% 0.12/5.56 fof(f1045,plain,(
% 0.12/5.56 sQ88_spl|sQ42_spl|~sQ4_spl|~sQ74_spl),
% 0.12/5.56 inference(split_clause,[status(thm)],[f1039,f1042,f547,f265,f936])).
% 0.12/5.56 fof(f1047,plain,(
% 0.12/5.56 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|v1_xboole_0(k1_autgroup(sK0_skl))|r2_hidden(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))|~sQ88_spl)),
% 0.12/5.56 inference(resolution,[status(thm)],[f1043,f229])).
% 0.12/5.56 fof(f1050,definition,(
% 0.12/5.56 ![X0]: (sQ89_spl <=> (r1_tarski(k4_autgroup(sK0_skl),X0)|r2_hidden(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))))),
% 0.12/5.56 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.12/5.56 fof(f1051,plain,(
% 0.12/5.56 ![X0]: (r1_tarski(k4_autgroup(sK0_skl),X0)|r2_hidden(sK1_skl(X0,k4_autgroup(sK0_skl)),k1_autgroup(sK0_skl))|~sQ89_spl)),
% 0.12/5.56 inference(component_clause,[status(thm)],[f1050])).
% 0.12/5.56 fof(f1053,definition,(
% 0.12/5.56 sQ90_spl <=> (v1_xboole_0(k1_autgroup(sK0_skl)))),
% 0.12/5.56 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.12/5.56 fof(f1054,plain,(
% 0.12/5.56 v1_xboole_0(k1_autgroup(sK0_skl))|~sQ90_spl),
% 0.12/5.56 inference(component_clause,[status(thm)],[f1053])).
% 0.12/5.56 fof(f1056,plain,(
% 0.12/5.56 sQ89_spl|sQ90_spl|~sQ88_spl),
% 0.12/5.56 inference(split_clause,[status(thm)],[f1047,f1050,f1053,f1042])).
% 0.12/5.56 fof(f1070,plain,(
% 0.12/5.56 $false|~sQ4_spl|~sQ90_spl),
% 0.12/5.56 inference(forward_subsumption_resolution,[status(thm)],[f1054,f433])).
% 0.12/5.56 fof(f1071,plain,(
% 0.12/5.56 ~sQ4_spl|~sQ90_spl),
% 0.12/5.56 inference(contradiction_clause,[status(thm)],[f1070])).
% 0.12/5.56 fof(f1072,plain,(
% 0.12/5.56 r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl))|r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl))|~sQ89_spl),
% 0.12/5.56 inference(resolution,[status(thm)],[f1051,f112])).
% 0.12/5.56 fof(f1077,definition,(
% 0.12/5.56 sQ94_spl <=> (r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl)))),
% 0.12/5.56 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.12/5.56 fof(f1078,plain,(
% 0.12/5.56 r1_tarski(k4_autgroup(sK0_skl),k1_autgroup(sK0_skl))|~sQ94_spl),
% 0.12/5.56 inference(component_clause,[status(thm)],[f1077])).
% 0.12/5.56 fof(f1080,plain,(
% 0.12/5.56 sQ94_spl|~sQ89_spl),
% 0.12/5.56 inference(split_clause,[status(thm)],[f1072,f1077,f1050])).
% 0.12/5.56 fof(f1085,plain,(
% 0.12/5.56 $false|~sQ94_spl),
% 0.12/5.56 inference(forward_subsumption_resolution,[status(thm)],[f1078,f73])).
% 0.12/5.56 fof(f1086,plain,(
% 0.12/5.56 ~sQ94_spl),
% 0.12/5.56 inference(contradiction_clause,[status(thm)],[f1085])).
% 0.12/5.56 fof(f1087,plain,(
% 0.12/5.56 $false),
% 0.12/5.56 inference(sat_refutation,[status(thm)],[f268,f273,f275,f277,f279,f281,f537,f578,f587,f598,f647,f657,f942,f956,f1045,f1056,f1071,f1080,f1086])).
% 0.12/5.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/5.58 % Elapsed time: 0.197966 seconds
% 0.12/5.58 % CPU time: 1.347724 seconds
% 0.12/5.58 % Total memory used: 105.958 MB
% 0.12/5.58 % Net memory used: 104.535 MB
%------------------------------------------------------------------------------