%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT359+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 : n020.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 01:03:50 PM UTC 2026
% Result : Theorem 7.17s 1.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT359+1 : 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.19/0.43 % Computer : n020.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 20 23:50:02 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 7.17/1.61 % Refutation found
% 7.17/1.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.17/1.61 % SZS output start CNFRefutation for theBenchmark
% 7.17/1.61 fof(f1,conjecture,(
% 7.17/1.61 (! [A] :( ( ~ v3_struct_0(A)& l2_altcat_1(A) )=> (! [B,C,D] :~ ( r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C))& (! [E] :( m1_subset_1(E,u1_struct_0(A))=> (! [F] :( m1_subset_1(F,u1_struct_0(A))=> ~ ( E = B& F = C& r2_hidden(D,k1_altcat_1(A,E,F))& m1_subset_1(D,k1_altcat_1(A,E,F)) ) ) )) )) )) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f2,negated_conjecture,(
% 7.17/1.61 ~((! [A] :( ( ~ v3_struct_0(A)& l2_altcat_1(A) )=> (! [B,C,D] :~ ( r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C))& (! [E] :( m1_subset_1(E,u1_struct_0(A))=> (! [F] :( m1_subset_1(F,u1_struct_0(A))=> ~ ( E = B& F = C& r2_hidden(D,k1_altcat_1(A,E,F))& m1_subset_1(D,k1_altcat_1(A,E,F)) ) ) )) )) )) ))),
% 7.17/1.61 inference(negated_conjecture,[status(cth)],[f1])).
% 7.17/1.61 fof(f19,axiom,(
% 7.17/1.61 (! [A] :( ( v1_relat_1(A)& v1_funct_1(A) )=> (! [B,C] : k1_binop_1(A,B,C) = k1_funct_1(A,k4_tarski(B,C)) )) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f20,axiom,(
% 7.17/1.61 (! [A] :( l1_altcat_1(A)=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> k1_altcat_1(A,B,C) = k1_binop_1(u1_altcat_1(A),B,C) ) )) )) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f21,axiom,(
% 7.17/1.61 (! [A,B] :( ( v1_relat_1(B)& v1_funct_1(B) )=> ( m1_pboole(B,A)<=> k1_relat_1(B) = A ) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f22,axiom,(
% 7.17/1.61 (! [A] :( ( v1_relat_1(A)& v1_funct_1(A) )=> (! [B,C] :( ( r2_hidden(B,k1_relat_1(A))=> ( C = k1_funct_1(A,B)<=> r2_hidden(k4_tarski(B,C),A) ) )& ( ~ r2_hidden(B,k1_relat_1(A))=> ( C = k1_funct_1(A,B)<=> C = k1_xboole_0 ) ) ) )) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f35,axiom,(
% 7.17/1.61 (! [A] :( l2_altcat_1(A)=> l1_altcat_1(A) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f36,axiom,(
% 7.17/1.61 (! [A,B] :( m1_pboole(B,A)=> ( v1_relat_1(B)& v1_funct_1(B) ) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f38,axiom,(
% 7.17/1.61 (! [A] :( l1_altcat_1(A)=> m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f58,axiom,(
% 7.17/1.61 ( v1_xboole_0(k1_xboole_0)& v1_membered(k1_xboole_0)& v2_membered(k1_xboole_0)& v3_membered(k1_xboole_0)& v4_membered(k1_xboole_0)& v5_membered(k1_xboole_0) ) ),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f69,axiom,(
% 7.17/1.61 (! [A,B,C,D] :( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))<=> ( r2_hidden(A,C)& r2_hidden(B,D) ) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f70,axiom,(
% 7.17/1.61 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f73,axiom,(
% 7.17/1.61 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 7.17/1.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 7.17/1.61 fof(f75,plain,(
% 7.17/1.61 (?[A]: ((~v3_struct_0(A)&l2_altcat_1(A))&(?[B,C,D]: (r2_hidden(D,k1_binop_1(u1_altcat_1(A),B,C))&(![E]: (~m1_subset_1(E,u1_struct_0(A))|(![F]: (~m1_subset_1(F,u1_struct_0(A))|(((~E=B|~F=C)|~r2_hidden(D,k1_altcat_1(A,E,F)))|~m1_subset_1(D,k1_altcat_1(A,E,F)))))))))))),
% 7.17/1.61 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 7.17/1.61 fof(f76,plain,(
% 7.17/1.61 ((~v3_struct_0(sK0_skl)&l2_altcat_1(sK0_skl))&(r2_hidden(sK3_skl,k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,sK2_skl))&(![E]: (~m1_subset_1(E,u1_struct_0(sK0_skl))|(![F]: (~m1_subset_1(F,u1_struct_0(sK0_skl))|(((~E=sK1_skl|~F=sK2_skl)|~r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,E,F)))|~m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,E,F)))))))))),
% 7.17/1.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f75])).
% 7.17/1.61 fof(f78,plain,(
% 7.17/1.61 l2_altcat_1(sK0_skl)),
% 7.17/1.61 inference(cnf_transformation,[status(thm)],[f76])).
% 7.17/1.61 fof(f79,plain,(
% 7.17/1.61 r2_hidden(sK3_skl,k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,sK2_skl))),
% 7.17/1.61 inference(cnf_transformation,[status(thm)],[f76])).
% 7.17/1.61 fof(f80,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|~X0=sK1_skl|~X1=sK2_skl|~r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,X0,X1))|~m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,X0,X1)))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f76])).
% 7.17/1.62 fof(f128,plain,(
% 7.17/1.62 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|(![B,C]: k1_binop_1(A,B,C)=k1_funct_1(A,k4_tarski(B,C))))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 7.17/1.62 fof(f129,plain,(
% 7.17/1.62 ![X0,X1,X2]: (~v1_relat_1(X0)|~v1_funct_1(X0)|k1_binop_1(X0,X1,X2)=k1_funct_1(X0,k4_tarski(X1,X2)))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f128])).
% 7.17/1.62 fof(f130,plain,(
% 7.17/1.62 ![A]: (~l1_altcat_1(A)|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|k1_altcat_1(A,B,C)=k1_binop_1(u1_altcat_1(A),B,C))))))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 7.17/1.62 fof(f131,plain,(
% 7.17/1.62 ![X0,X1,X2]: (~l1_altcat_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k1_altcat_1(X0,X1,X2)=k1_binop_1(u1_altcat_1(X0),X1,X2))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f130])).
% 7.17/1.62 fof(f132,plain,(
% 7.17/1.62 ![A,B]: ((~v1_relat_1(B)|~v1_funct_1(B))|(m1_pboole(B,A)<=>k1_relat_1(B)=A))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 7.17/1.62 fof(f133,plain,(
% 7.17/1.62 ![A,B]: ((~v1_relat_1(B)|~v1_funct_1(B))|((~m1_pboole(B,A)|k1_relat_1(B)=A)&(m1_pboole(B,A)|~k1_relat_1(B)=A)))),
% 7.17/1.62 inference(NNF_transformation,[status(thm)],[f132])).
% 7.17/1.62 fof(f134,plain,(
% 7.17/1.62 ![B]: ((~v1_relat_1(B)|~v1_funct_1(B))|((![A]: (~m1_pboole(B,A)|k1_relat_1(B)=A))&(![A]: (m1_pboole(B,A)|~k1_relat_1(B)=A))))),
% 7.17/1.62 inference(miniscoping,[status(thm)],[f133])).
% 7.17/1.62 fof(f135,plain,(
% 7.17/1.62 ![X0,X1]: (~v1_relat_1(X0)|~v1_funct_1(X0)|~m1_pboole(X0,X1)|k1_relat_1(X0)=X1)),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f134])).
% 7.17/1.62 fof(f137,plain,(
% 7.17/1.62 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|(![B,C]: ((~r2_hidden(B,k1_relat_1(A))|(C=k1_funct_1(A,B)<=>r2_hidden(k4_tarski(B,C),A)))&(r2_hidden(B,k1_relat_1(A))|(C=k1_funct_1(A,B)<=>C=k1_xboole_0)))))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 7.17/1.62 fof(f138,plain,(
% 7.17/1.62 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|(![B,C]: ((~r2_hidden(B,k1_relat_1(A))|((~C=k1_funct_1(A,B)|r2_hidden(k4_tarski(B,C),A))&(C=k1_funct_1(A,B)|~r2_hidden(k4_tarski(B,C),A))))&(r2_hidden(B,k1_relat_1(A))|((~C=k1_funct_1(A,B)|C=k1_xboole_0)&(C=k1_funct_1(A,B)|~C=k1_xboole_0))))))),
% 7.17/1.62 inference(NNF_transformation,[status(thm)],[f137])).
% 7.17/1.62 fof(f139,plain,(
% 7.17/1.62 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|((![B]: (~r2_hidden(B,k1_relat_1(A))|((![C]: (~C=k1_funct_1(A,B)|r2_hidden(k4_tarski(B,C),A)))&(![C]: (C=k1_funct_1(A,B)|~r2_hidden(k4_tarski(B,C),A))))))&(![B]: (r2_hidden(B,k1_relat_1(A))|((![C]: (~C=k1_funct_1(A,B)|C=k1_xboole_0))&(![C]: (C=k1_funct_1(A,B)|~C=k1_xboole_0)))))))),
% 7.17/1.62 inference(miniscoping,[status(thm)],[f138])).
% 7.17/1.62 fof(f142,plain,(
% 7.17/1.62 ![X0,X1,X2]: (~v1_relat_1(X0)|~v1_funct_1(X0)|r2_hidden(X1,k1_relat_1(X0))|~X2=k1_funct_1(X0,X1)|X2=k1_xboole_0)),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f139])).
% 7.17/1.62 fof(f147,plain,(
% 7.17/1.62 ![A]: (~l2_altcat_1(A)|l1_altcat_1(A))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 7.17/1.62 fof(f148,plain,(
% 7.17/1.62 ![X0]: (~l2_altcat_1(X0)|l1_altcat_1(X0))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f147])).
% 7.17/1.62 fof(f149,plain,(
% 7.17/1.62 ![A,B]: (~m1_pboole(B,A)|(v1_relat_1(B)&v1_funct_1(B)))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 7.17/1.62 fof(f150,plain,(
% 7.17/1.62 ![B]: ((![A]: ~m1_pboole(B,A))|(v1_relat_1(B)&v1_funct_1(B)))),
% 7.17/1.62 inference(miniscoping,[status(thm)],[f149])).
% 7.17/1.62 fof(f151,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_pboole(X0,X1)|v1_relat_1(X0))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f150])).
% 7.17/1.62 fof(f152,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_pboole(X0,X1)|v1_funct_1(X0))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f150])).
% 7.17/1.62 fof(f153,plain,(
% 7.17/1.62 ![A]: (~l1_altcat_1(A)|m1_pboole(u1_altcat_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A))))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 7.17/1.62 fof(f154,plain,(
% 7.17/1.62 ![X0]: (~l1_altcat_1(X0)|m1_pboole(u1_altcat_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0))))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f153])).
% 7.17/1.62 fof(f212,plain,(
% 7.17/1.62 v1_xboole_0(k1_xboole_0)),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f58])).
% 7.17/1.62 fof(f254,plain,(
% 7.17/1.62 ![A,B,C,D]: ((~r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))|(r2_hidden(A,C)&r2_hidden(B,D)))&(r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))|(~r2_hidden(A,C)|~r2_hidden(B,D))))),
% 7.17/1.62 inference(NNF_transformation,[status(thm)],[f69])).
% 7.17/1.62 fof(f255,plain,(
% 7.17/1.62 (![A,B,C,D]: (~r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))|(r2_hidden(A,C)&r2_hidden(B,D))))&(![A,B,C,D]: (r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))|(~r2_hidden(A,C)|~r2_hidden(B,D))))),
% 7.17/1.62 inference(miniscoping,[status(thm)],[f254])).
% 7.17/1.62 fof(f256,plain,(
% 7.17/1.62 ![X0,X1,X2,X3]: (~r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))|r2_hidden(X0,X2))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f255])).
% 7.17/1.62 fof(f257,plain,(
% 7.17/1.62 ![X0,X1,X2,X3]: (~r2_hidden(k4_tarski(X0,X1),k2_zfmisc_1(X2,X3))|r2_hidden(X1,X3))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f255])).
% 7.17/1.62 fof(f259,plain,(
% 7.17/1.62 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 7.17/1.62 fof(f260,plain,(
% 7.17/1.62 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f259])).
% 7.17/1.62 fof(f265,plain,(
% 7.17/1.62 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 7.17/1.62 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 7.17/1.62 fof(f266,plain,(
% 7.17/1.62 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 7.17/1.62 inference(miniscoping,[status(thm)],[f265])).
% 7.17/1.62 fof(f267,plain,(
% 7.17/1.62 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 7.17/1.62 inference(cnf_transformation,[status(thm)],[f266])).
% 7.17/1.62 fof(f271,plain,(
% 7.17/1.62 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))|~m1_subset_1(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))),
% 7.17/1.62 inference(destructive_equality_resolution,[status(thm)],[f80])).
% 7.17/1.62 fof(f275,plain,(
% 7.17/1.62 ![X0,X1]: (~v1_relat_1(X0)|~v1_funct_1(X0)|r2_hidden(X1,k1_relat_1(X0))|k1_funct_1(X0,X1)=k1_xboole_0)),
% 7.17/1.62 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 7.17/1.62 fof(f277,plain,(
% 7.17/1.62 ![X0,X1]: (~v1_funct_1(X0)|~m1_pboole(X0,X1)|k1_relat_1(X0)=X1)),
% 7.17/1.62 inference(backward_subsumption_resolution,[status(thm)],[f135,f151])).
% 7.17/1.62 fof(f278,plain,(
% 7.17/1.62 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|~r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))),
% 7.17/1.62 inference(backward_subsumption_resolution,[status(thm)],[f271,f260])).
% 7.17/1.62 fof(f279,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_pboole(X0,X1)|k1_relat_1(X0)=X1)),
% 7.17/1.62 inference(forward_subsumption_resolution,[status(thm)],[f277,f152])).
% 7.17/1.62 fof(f281,plain,(
% 7.17/1.62 ![X0,X1,X2]: (~l2_altcat_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k1_altcat_1(X0,X1,X2)=k1_binop_1(u1_altcat_1(X0),X1,X2))),
% 7.17/1.62 inference(resolution,[status(thm)],[f148,f131])).
% 7.17/1.62 fof(f282,plain,(
% 7.17/1.62 ~r2_hidden(sK2_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f260,f278])).
% 7.17/1.62 fof(f283,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|k1_altcat_1(sK0_skl,X0,X1)=k1_binop_1(u1_altcat_1(sK0_skl),X0,X1))),
% 7.17/1.62 inference(resolution,[status(thm)],[f281,f78])).
% 7.17/1.62 fof(f284,plain,(
% 7.17/1.62 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k1_altcat_1(sK0_skl,X0,X1)=k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)|~r2_hidden(X1,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(resolution,[status(thm)],[f283,f260])).
% 7.17/1.62 fof(f297,plain,(
% 7.17/1.62 ![X0]: (k1_relat_1(u1_altcat_1(X0))=k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0))|~l1_altcat_1(X0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f279,f154])).
% 7.17/1.62 fof(f298,plain,(
% 7.17/1.62 ![X0]: (k1_relat_1(u1_altcat_1(X0))=k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0))|~l2_altcat_1(X0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f297,f148])).
% 7.17/1.62 fof(f300,plain,(
% 7.17/1.62 k1_relat_1(u1_altcat_1(sK0_skl))=k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f298,f78])).
% 7.17/1.62 fof(f305,plain,(
% 7.17/1.62 ![X0,X1]: (~r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sK0_skl)))|r2_hidden(X1,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(paramodulation,[status(thm)],[f300,f257])).
% 7.17/1.62 fof(f306,plain,(
% 7.17/1.62 ![X0,X1]: (~r2_hidden(k4_tarski(X0,X1),k1_relat_1(u1_altcat_1(sK0_skl)))|r2_hidden(X0,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(paramodulation,[status(thm)],[f300,f256])).
% 7.17/1.62 fof(f336,plain,(
% 7.17/1.62 ![X0]: (v1_relat_1(u1_altcat_1(X0))|~l1_altcat_1(X0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f151,f154])).
% 7.17/1.62 fof(f339,plain,(
% 7.17/1.62 ![X0]: (v1_funct_1(u1_altcat_1(X0))|~l1_altcat_1(X0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f152,f154])).
% 7.17/1.62 fof(f358,plain,(
% 7.17/1.62 ![X0]: (v1_funct_1(u1_altcat_1(X0))|~l2_altcat_1(X0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f339,f148])).
% 7.17/1.62 fof(f377,plain,(
% 7.17/1.62 v1_funct_1(u1_altcat_1(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f358,f78])).
% 7.17/1.62 fof(f378,plain,(
% 7.17/1.62 ![X0]: (~v1_relat_1(u1_altcat_1(sK0_skl))|r2_hidden(X0,k1_relat_1(u1_altcat_1(sK0_skl)))|k1_funct_1(u1_altcat_1(sK0_skl),X0)=k1_xboole_0)),
% 7.17/1.62 inference(resolution,[status(thm)],[f377,f275])).
% 7.17/1.62 fof(f382,plain,(
% 7.17/1.62 ![X0,X1]: (~v1_relat_1(u1_altcat_1(sK0_skl))|k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)))),
% 7.17/1.62 inference(resolution,[status(thm)],[f377,f129])).
% 7.17/1.62 fof(f383,plain,(
% 7.17/1.62 ![X0]: (r2_hidden(X0,k1_relat_1(u1_altcat_1(sK0_skl)))|k1_funct_1(u1_altcat_1(sK0_skl),X0)=k1_xboole_0|~l1_altcat_1(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f378,f336])).
% 7.17/1.62 fof(f398,plain,(
% 7.17/1.62 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1))|~l1_altcat_1(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f382,f336])).
% 7.17/1.62 fof(f399,plain,(
% 7.17/1.62 ![X0]: (r2_hidden(X0,k1_relat_1(u1_altcat_1(sK0_skl)))|k1_funct_1(u1_altcat_1(sK0_skl),X0)=k1_xboole_0|~l2_altcat_1(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f383,f148])).
% 7.17/1.62 fof(f400,plain,(
% 7.17/1.62 ![X0]: (r2_hidden(X0,k1_relat_1(u1_altcat_1(sK0_skl)))|k1_funct_1(u1_altcat_1(sK0_skl),X0)=k1_xboole_0)),
% 7.17/1.62 inference(forward_subsumption_resolution,[status(thm)],[f399,f78])).
% 7.17/1.62 fof(f421,plain,(
% 7.17/1.62 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 7.17/1.62 inference(resolution,[status(thm)],[f212,f267])).
% 7.17/1.62 fof(f423,plain,(
% 7.17/1.62 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1))|~l2_altcat_1(sK0_skl))),
% 7.17/1.62 inference(resolution,[status(thm)],[f398,f148])).
% 7.17/1.62 fof(f426,plain,(
% 7.17/1.62 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1)))),
% 7.17/1.62 inference(forward_subsumption_resolution,[status(thm)],[f423,f78])).
% 7.17/1.62 fof(f427,plain,(
% 7.17/1.62 ![X0,X1]: (k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1))=k1_xboole_0|r2_hidden(X0,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(resolution,[status(thm)],[f400,f306])).
% 7.17/1.62 fof(f428,plain,(
% 7.17/1.62 ![X0,X1]: (k1_funct_1(u1_altcat_1(sK0_skl),k4_tarski(X0,X1))=k1_xboole_0|r2_hidden(X1,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(resolution,[status(thm)],[f400,f305])).
% 7.17/1.62 fof(f430,plain,(
% 7.17/1.62 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0|r2_hidden(X0,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(forward_demodulation,[status(thm)],[f426,f427])).
% 7.17/1.62 fof(f431,plain,(
% 7.17/1.62 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0|r2_hidden(X1,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(forward_demodulation,[status(thm)],[f426,f428])).
% 7.17/1.62 fof(f505,plain,(
% 7.17/1.62 ![X0,X1,X2]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0|~m1_subset_1(X2,u1_struct_0(sK0_skl))|k1_altcat_1(sK0_skl,X2,X1)=k1_binop_1(u1_altcat_1(sK0_skl),X2,X1))),
% 7.17/1.62 inference(resolution,[status(thm)],[f431,f284])).
% 7.17/1.62 fof(f523,plain,(
% 7.17/1.62 ![X0,X1,X2]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0|k1_altcat_1(sK0_skl,X2,X1)=k1_binop_1(u1_altcat_1(sK0_skl),X2,X1)|~r2_hidden(X2,u1_struct_0(sK0_skl)))),
% 7.17/1.62 inference(resolution,[status(thm)],[f505,f260])).
% 7.17/1.62 fof(f557,plain,(
% 7.17/1.62 ![X0,X1,X2,X3]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0|k1_altcat_1(sK0_skl,X2,X1)=k1_binop_1(u1_altcat_1(sK0_skl),X2,X1)|k1_binop_1(u1_altcat_1(sK0_skl),X2,X3)=k1_xboole_0)),
% 7.17/1.62 inference(resolution,[status(thm)],[f523,f430])).
% 7.17/1.62 fof(f2302,plain,(
% 7.17/1.62 ![X0,X1]: (r2_hidden(sK3_skl,k1_xboole_0)|k1_altcat_1(sK0_skl,X0,sK2_skl)=k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)|k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0)),
% 7.17/1.62 inference(paramodulation,[status(thm)],[f557,f79])).
% 7.17/1.65 fof(f2330,plain,(
% 7.17/1.65 ![X0,X1]: (k1_altcat_1(sK0_skl,X0,sK2_skl)=k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)|k1_binop_1(u1_altcat_1(sK0_skl),X0,X1)=k1_xboole_0)),
% 7.17/1.65 inference(forward_subsumption_resolution,[status(thm)],[f2302,f421])).
% 7.17/1.65 fof(f2363,plain,(
% 7.17/1.65 ![X0]: (r2_hidden(sK3_skl,k1_altcat_1(sK0_skl,sK1_skl,sK2_skl))|k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0)=k1_xboole_0)),
% 7.17/1.65 inference(paramodulation,[status(thm)],[f2330,f79])).
% 7.17/1.65 fof(f4877,plain,(
% 7.17/1.65 ![X0]: (k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0)=k1_xboole_0|~r2_hidden(sK2_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)))),
% 7.17/1.65 inference(resolution,[status(thm)],[f2363,f282])).
% 7.17/1.65 fof(f4879,plain,(
% 7.17/1.65 ![X0]: (k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0)=k1_xboole_0|~r2_hidden(sK2_skl,u1_struct_0(sK0_skl))|~r2_hidden(sK1_skl,u1_struct_0(sK0_skl)))),
% 7.17/1.65 inference(resolution,[status(thm)],[f4877,f260])).
% 7.17/1.65 fof(f4880,plain,(
% 7.17/1.65 ![X0]: (k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0)=k1_xboole_0|~r2_hidden(sK2_skl,u1_struct_0(sK0_skl)))),
% 7.17/1.65 inference(forward_subsumption_resolution,[status(thm)],[f4879,f430])).
% 7.17/1.65 fof(f4908,plain,(
% 7.17/1.65 ![X0,X1]: (k1_binop_1(u1_altcat_1(sK0_skl),sK1_skl,X0)=k1_xboole_0|k1_binop_1(u1_altcat_1(sK0_skl),X1,sK2_skl)=k1_xboole_0)),
% 7.17/1.65 inference(resolution,[status(thm)],[f4880,f431])).
% 7.17/1.65 fof(f4946,plain,(
% 7.17/1.65 ![X0]: (r2_hidden(sK3_skl,k1_xboole_0)|k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)=k1_xboole_0)),
% 7.17/1.65 inference(paramodulation,[status(thm)],[f4908,f79])).
% 7.17/1.65 fof(f4982,plain,(
% 7.17/1.65 r2_hidden(sK3_skl,k1_xboole_0)),
% 7.17/1.65 inference(backward_demodulation,[status(thm)],[f4993,f79])).
% 7.17/1.65 fof(f4993,plain,(
% 7.17/1.65 ![X0]: (k1_binop_1(u1_altcat_1(sK0_skl),X0,sK2_skl)=k1_xboole_0)),
% 7.17/1.65 inference(forward_subsumption_resolution,[status(thm)],[f4946,f421])).
% 7.17/1.65 fof(f4999,plain,(
% 7.17/1.65 $false),
% 7.17/1.65 inference(forward_subsumption_resolution,[status(thm)],[f4982,f421])).
% 7.17/1.65 % SZS output end CNFRefutation for theBenchmark.p
% 7.17/1.68 % Elapsed time: 1.219507 seconds
% 7.17/1.68 % CPU time: 8.887944 seconds
% 7.17/1.68 % Total memory used: 227.655 MB
% 7.17/1.68 % Net memory used: 223.003 MB
%------------------------------------------------------------------------------