%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT294+1 : 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 : n008.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:33 PM UTC 2026
% Result : Theorem 0.14s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT294+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.42 % Computer : n008.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 23:29:24 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.44 % Drodi V4.1.1
% 0.14/0.48 % Refutation found
% 0.14/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.48 fof(f1,conjecture,(
% 0.14/0.48 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(A)) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m2_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,k2_zfmisc_1(A,A),A)& m2_relset_1(D,k2_zfmisc_1(A,A),A) )=> (! [E] :( ( v1_funct_1(E)& v1_funct_2(E,k2_zfmisc_1(B,B),B)& m2_relset_1(E,k2_zfmisc_1(B,B),B) )=> (! [F] :( ( v1_funct_1(F)& v1_funct_2(F,k2_zfmisc_1(B,B),B)& m2_relset_1(F,k2_zfmisc_1(B,B),B) )=> ( ( E = k1_realset1(C,B)& F = k1_realset1(D,B)& r6_binop_1(A,C,D) )=> r6_binop_1(B,E,F) ) ) )) )) )) )) )) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f2,negated_conjecture,(
% 0.14/0.48 ~((! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(A)) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m2_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,k2_zfmisc_1(A,A),A)& m2_relset_1(D,k2_zfmisc_1(A,A),A) )=> (! [E] :( ( v1_funct_1(E)& v1_funct_2(E,k2_zfmisc_1(B,B),B)& m2_relset_1(E,k2_zfmisc_1(B,B),B) )=> (! [F] :( ( v1_funct_1(F)& v1_funct_2(F,k2_zfmisc_1(B,B),B)& m2_relset_1(F,k2_zfmisc_1(B,B),B) )=> ( ( E = k1_realset1(C,B)& F = k1_realset1(D,B)& r6_binop_1(A,C,D) )=> r6_binop_1(B,E,F) ) ) )) )) )) )) )) ))),
% 0.14/0.48 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.48 fof(f5,axiom,(
% 0.14/0.48 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> v1_relat_1(C) ) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f7,axiom,(
% 0.14/0.48 (! [A,B] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m2_relset_1(B,k2_zfmisc_1(A,A),A) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m2_relset_1(C,k2_zfmisc_1(A,A),A) )=> ( r6_binop_1(A,B,C)<=> ( r4_binop_1(A,B,C)& r5_binop_1(A,B,C) ) ) ) )) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f8,axiom,(
% 0.14/0.48 (! [A] :( v1_relat_1(A)=> (! [B] : k1_realset1(A,B) = k7_relat_1(A,k2_zfmisc_1(B,B)) )) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f16,axiom,(
% 0.14/0.48 (! [A,B,C] :( m2_relset_1(C,A,B)=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f23,axiom,(
% 0.14/0.48 (! [A,B] :( ( v1_relat_1(A)& v1_funct_1(A) )=> ( v1_relat_1(k1_realset1(A,B))& v1_funct_1(k1_realset1(A,B)) ) ) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f24,axiom,(
% 0.14/0.48 (! [A,B] :( ( v1_relat_1(A)& v1_funct_1(A) )=> ( v1_relat_1(k7_relat_1(A,B))& v1_funct_1(k7_relat_1(A,B)) ) ) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f37,axiom,(
% 0.14/0.48 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(A)) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m2_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D] :( ( v1_funct_1(D)& v1_funct_2(D,k2_zfmisc_1(A,A),A)& m2_relset_1(D,k2_zfmisc_1(A,A),A) )=> (! [E] :( ( v1_funct_1(E)& v1_funct_2(E,k2_zfmisc_1(B,B),B)& m2_relset_1(E,k2_zfmisc_1(B,B),B) )=> (! [F] :( ( v1_funct_1(F)& v1_funct_2(F,k2_zfmisc_1(B,B),B)& m2_relset_1(F,k2_zfmisc_1(B,B),B) )=> ( ( E = k1_realset1(C,B)& F = k1_realset1(D,B) )=> ( ( r4_binop_1(A,C,D)=> r4_binop_1(B,E,F) )& ( r5_binop_1(A,C,D)=> r5_binop_1(B,E,F) ) ) ) ) )) )) )) )) )) )),
% 0.14/0.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.14/0.48 fof(f44,plain,(
% 0.14/0.48 (?[A]: (~v1_xboole_0(A)&(?[B]: ((~v1_xboole_0(B)&m1_subset_1(B,k1_zfmisc_1(A)))&(?[C]: (((v1_funct_1(C)&v1_funct_2(C,k2_zfmisc_1(A,A),A))&m2_relset_1(C,k2_zfmisc_1(A,A),A))&(?[D]: (((v1_funct_1(D)&v1_funct_2(D,k2_zfmisc_1(A,A),A))&m2_relset_1(D,k2_zfmisc_1(A,A),A))&(?[E]: (((v1_funct_1(E)&v1_funct_2(E,k2_zfmisc_1(B,B),B))&m2_relset_1(E,k2_zfmisc_1(B,B),B))&(?[F]: (((v1_funct_1(F)&v1_funct_2(F,k2_zfmisc_1(B,B),B))&m2_relset_1(F,k2_zfmisc_1(B,B),B))&(((E=k1_realset1(C,B)&F=k1_realset1(D,B))&r6_binop_1(A,C,D))&~r6_binop_1(B,E,F))))))))))))))),
% 0.14/0.48 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.48 fof(f45,plain,(
% 0.14/0.49 (~v1_xboole_0(sK0_skl)&((~v1_xboole_0(sK1_skl)&m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl)))&(((v1_funct_1(sK2_skl)&v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))&m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))&(((v1_funct_1(sK3_skl)&v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))&m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))&(((v1_funct_1(sK4_skl)&v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))&m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))&(((v1_funct_1(sK5_skl)&v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))&m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))&(((sK4_skl=k1_realset1(sK2_skl,sK1_skl)&sK5_skl=k1_realset1(sK3_skl,sK1_skl))&r6_binop_1(sK0_skl,sK2_skl,sK3_skl))&~r6_binop_1(sK1_skl,sK4_skl,sK5_skl))))))))),
% 0.14/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl),skolemize(E,sK4_skl),skolemize(F,sK5_skl)],[f44])).
% 0.14/0.49 fof(f46,plain,(
% 0.14/0.49 ~v1_xboole_0(sK0_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f47,plain,(
% 0.14/0.49 ~v1_xboole_0(sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f48,plain,(
% 0.14/0.49 m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f49,plain,(
% 0.14/0.49 v1_funct_1(sK2_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f50,plain,(
% 0.14/0.49 v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f51,plain,(
% 0.14/0.49 m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f52,plain,(
% 0.14/0.49 v1_funct_1(sK3_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f53,plain,(
% 0.14/0.49 v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f54,plain,(
% 0.14/0.49 m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f56,plain,(
% 0.14/0.49 v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f57,plain,(
% 0.14/0.49 m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f59,plain,(
% 0.14/0.49 v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f60,plain,(
% 0.14/0.49 m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f61,plain,(
% 0.14/0.49 sK4_skl=k1_realset1(sK2_skl,sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f62,plain,(
% 0.14/0.49 sK5_skl=k1_realset1(sK3_skl,sK1_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f63,plain,(
% 0.14/0.49 r6_binop_1(sK0_skl,sK2_skl,sK3_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f64,plain,(
% 0.14/0.49 ~r6_binop_1(sK1_skl,sK4_skl,sK5_skl)),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f45])).
% 0.14/0.49 fof(f69,plain,(
% 0.14/0.49 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|v1_relat_1(C))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.14/0.49 fof(f70,plain,(
% 0.14/0.49 ![C]: ((![A,B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|v1_relat_1(C))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f69])).
% 0.14/0.49 fof(f71,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|v1_relat_1(X0))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f70])).
% 0.14/0.49 fof(f76,plain,(
% 0.14/0.49 ![A,B]: (((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m2_relset_1(B,k2_zfmisc_1(A,A),A))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m2_relset_1(C,k2_zfmisc_1(A,A),A))|(r6_binop_1(A,B,C)<=>(r4_binop_1(A,B,C)&r5_binop_1(A,B,C))))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.14/0.49 fof(f77,plain,(
% 0.14/0.49 ![A,B]: (((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m2_relset_1(B,k2_zfmisc_1(A,A),A))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m2_relset_1(C,k2_zfmisc_1(A,A),A))|((~r6_binop_1(A,B,C)|(r4_binop_1(A,B,C)&r5_binop_1(A,B,C)))&(r6_binop_1(A,B,C)|(~r4_binop_1(A,B,C)|~r5_binop_1(A,B,C)))))))),
% 0.14/0.49 inference(NNF_transformation,[status(thm)],[f76])).
% 0.14/0.49 fof(f78,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~r6_binop_1(X1,X0,X2)|r4_binop_1(X1,X0,X2))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.49 fof(f79,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~r6_binop_1(X1,X0,X2)|r5_binop_1(X1,X0,X2))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.49 fof(f80,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|r6_binop_1(X1,X0,X2)|~r4_binop_1(X1,X0,X2)|~r5_binop_1(X1,X0,X2))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.49 fof(f81,plain,(
% 0.14/0.49 ![A]: (~v1_relat_1(A)|(![B]: k1_realset1(A,B)=k7_relat_1(A,k2_zfmisc_1(B,B))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.14/0.49 fof(f82,plain,(
% 0.14/0.49 ![X0,X1]: (~v1_relat_1(X0)|k1_realset1(X0,X1)=k7_relat_1(X0,k2_zfmisc_1(X1,X1)))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f81])).
% 0.14/0.49 fof(f86,plain,(
% 0.14/0.49 ![A,B,C]: (~m2_relset_1(C,A,B)|m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.14/0.49 fof(f87,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f86])).
% 0.14/0.49 fof(f99,plain,(
% 0.14/0.49 ![A,B]: ((~v1_relat_1(A)|~v1_funct_1(A))|(v1_relat_1(k1_realset1(A,B))&v1_funct_1(k1_realset1(A,B))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.14/0.49 fof(f100,plain,(
% 0.14/0.49 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|((![B]: v1_relat_1(k1_realset1(A,B)))&(![B]: v1_funct_1(k1_realset1(A,B)))))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f99])).
% 0.14/0.49 fof(f102,plain,(
% 0.14/0.49 ![X0,X1]: (~v1_relat_1(X0)|~v1_funct_1(X0)|v1_funct_1(k1_realset1(X0,X1)))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/0.49 fof(f103,plain,(
% 0.14/0.49 ![A,B]: ((~v1_relat_1(A)|~v1_funct_1(A))|(v1_relat_1(k7_relat_1(A,B))&v1_funct_1(k7_relat_1(A,B))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.14/0.49 fof(f104,plain,(
% 0.14/0.49 ![A]: ((~v1_relat_1(A)|~v1_funct_1(A))|((![B]: v1_relat_1(k7_relat_1(A,B)))&(![B]: v1_funct_1(k7_relat_1(A,B)))))),
% 0.14/0.49 inference(miniscoping,[status(thm)],[f103])).
% 0.14/0.49 fof(f106,plain,(
% 0.14/0.49 ![X0,X1]: (~v1_relat_1(X0)|~v1_funct_1(X0)|v1_funct_1(k7_relat_1(X0,X1)))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f104])).
% 0.14/0.49 fof(f141,plain,(
% 0.14/0.49 ![A]: (v1_xboole_0(A)|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(A)))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m2_relset_1(C,k2_zfmisc_1(A,A),A))|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,k2_zfmisc_1(A,A),A))|~m2_relset_1(D,k2_zfmisc_1(A,A),A))|(![E]: (((~v1_funct_1(E)|~v1_funct_2(E,k2_zfmisc_1(B,B),B))|~m2_relset_1(E,k2_zfmisc_1(B,B),B))|(![F]: (((~v1_funct_1(F)|~v1_funct_2(F,k2_zfmisc_1(B,B),B))|~m2_relset_1(F,k2_zfmisc_1(B,B),B))|((~E=k1_realset1(C,B)|~F=k1_realset1(D,B))|((~r4_binop_1(A,C,D)|r4_binop_1(B,E,F))&(~r5_binop_1(A,C,D)|r5_binop_1(B,E,F)))))))))))))))),
% 0.14/0.49 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.14/0.49 fof(f142,plain,(
% 0.14/0.49 ![X0,X1,X2,X3,X4,X5]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X3)|~v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X4)|~v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X5)|~v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)|~X4=k1_realset1(X2,X1)|~X5=k1_realset1(X3,X1)|~r4_binop_1(X0,X2,X3)|r4_binop_1(X1,X4,X5))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.49 fof(f143,plain,(
% 0.14/0.49 ![X0,X1,X2,X3,X4,X5]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X3)|~v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X4)|~v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X5)|~v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)|~X4=k1_realset1(X2,X1)|~X5=k1_realset1(X3,X1)|~r5_binop_1(X0,X2,X3)|r5_binop_1(X1,X4,X5))),
% 0.14/0.49 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.49 fof(f162,plain,(
% 0.14/0.49 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X3)|~v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(X2,X1))|~v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(k1_realset1(X3,X1))|~v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)|~r4_binop_1(X0,X2,X3)|r4_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1)))),
% 0.14/0.49 inference(destructive_equality_resolution,[status(thm)],[f142])).
% 0.14/0.49 fof(f163,plain,(
% 0.14/0.49 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X3)|~v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(X2,X1))|~v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(k1_realset1(X3,X1))|~v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)|~m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)|~r5_binop_1(X0,X2,X3)|r5_binop_1(X1,k1_realset1(X2,X1),k1_realset1(X3,X1)))),
% 0.14/0.49 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 0.14/0.49 fof(f195,plain,(
% 0.14/0.49 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|v1_relat_1(X0))),
% 0.14/0.49 inference(resolution,[status(thm)],[f87,f71])).
% 0.14/0.49 fof(f204,plain,(
% 0.14/0.49 v1_relat_1(sK3_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f195,f54])).
% 0.14/0.49 fof(f205,plain,(
% 0.14/0.49 v1_relat_1(sK2_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f195,f51])).
% 0.14/0.49 fof(f208,definition,(
% 0.14/0.49 sQ2_spl <=> (v1_relat_1(sK3_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f210,plain,(
% 0.14/0.49 ~v1_relat_1(sK3_skl)|sQ2_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f208])).
% 0.14/0.49 fof(f215,definition,(
% 0.14/0.49 sQ4_spl <=> (v1_relat_1(sK2_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f217,plain,(
% 0.14/0.49 ~v1_relat_1(sK2_skl)|sQ4_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f215])).
% 0.14/0.49 fof(f222,plain,(
% 0.14/0.49 $false|sQ4_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f217,f205])).
% 0.14/0.49 fof(f223,plain,(
% 0.14/0.49 sQ4_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f222])).
% 0.14/0.49 fof(f224,plain,(
% 0.14/0.49 $false|sQ2_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f210,f204])).
% 0.14/0.49 fof(f225,plain,(
% 0.14/0.49 sQ2_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f224])).
% 0.14/0.49 fof(f227,plain,(
% 0.14/0.49 ~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(sK3_skl)|~v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|r4_binop_1(sK0_skl,sK2_skl,sK3_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f78,f63])).
% 0.14/0.49 fof(f228,definition,(
% 0.14/0.49 sQ6_spl <=> (v1_funct_1(sK2_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f230,plain,(
% 0.14/0.49 ~v1_funct_1(sK2_skl)|sQ6_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f228])).
% 0.14/0.49 fof(f231,definition,(
% 0.14/0.49 sQ7_spl <=> (v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f233,plain,(
% 0.14/0.49 ~v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|sQ7_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f231])).
% 0.14/0.49 fof(f234,definition,(
% 0.14/0.49 sQ8_spl <=> (m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f236,plain,(
% 0.14/0.49 ~m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|sQ8_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f234])).
% 0.14/0.49 fof(f237,definition,(
% 0.14/0.49 sQ9_spl <=> (v1_funct_1(sK3_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f239,plain,(
% 0.14/0.49 ~v1_funct_1(sK3_skl)|sQ9_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f237])).
% 0.14/0.49 fof(f240,definition,(
% 0.14/0.49 sQ10_spl <=> (v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f242,plain,(
% 0.14/0.49 ~v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|sQ10_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f240])).
% 0.14/0.49 fof(f243,definition,(
% 0.14/0.49 sQ11_spl <=> (m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f245,plain,(
% 0.14/0.49 ~m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|sQ11_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f243])).
% 0.14/0.49 fof(f246,definition,(
% 0.14/0.49 sQ12_spl <=> (r4_binop_1(sK0_skl,sK2_skl,sK3_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f247,plain,(
% 0.14/0.49 r4_binop_1(sK0_skl,sK2_skl,sK3_skl)|~sQ12_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f246])).
% 0.14/0.49 fof(f249,plain,(
% 0.14/0.49 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|sQ12_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f227,f228,f231,f234,f237,f240,f243,f246])).
% 0.14/0.49 fof(f250,plain,(
% 0.14/0.49 ~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(sK3_skl)|~v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|r5_binop_1(sK0_skl,sK2_skl,sK3_skl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f79,f63])).
% 0.14/0.49 fof(f251,definition,(
% 0.14/0.49 sQ13_spl <=> (r5_binop_1(sK0_skl,sK2_skl,sK3_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f252,plain,(
% 0.14/0.49 r5_binop_1(sK0_skl,sK2_skl,sK3_skl)|~sQ13_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f251])).
% 0.14/0.49 fof(f254,plain,(
% 0.14/0.49 ~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|sQ13_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f250,f228,f231,f234,f237,f240,f243,f251])).
% 0.14/0.49 fof(f255,plain,(
% 0.14/0.49 $false|sQ11_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f245,f54])).
% 0.14/0.49 fof(f256,plain,(
% 0.14/0.49 sQ11_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f255])).
% 0.14/0.49 fof(f257,plain,(
% 0.14/0.49 $false|sQ10_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f242,f53])).
% 0.14/0.49 fof(f258,plain,(
% 0.14/0.49 sQ10_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f257])).
% 0.14/0.49 fof(f259,plain,(
% 0.14/0.49 $false|sQ9_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f239,f52])).
% 0.14/0.49 fof(f260,plain,(
% 0.14/0.49 sQ9_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f259])).
% 0.14/0.49 fof(f261,plain,(
% 0.14/0.49 $false|sQ8_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f236,f51])).
% 0.14/0.49 fof(f262,plain,(
% 0.14/0.49 sQ8_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f261])).
% 0.14/0.49 fof(f263,plain,(
% 0.14/0.49 $false|sQ7_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f233,f50])).
% 0.14/0.49 fof(f264,plain,(
% 0.14/0.49 sQ7_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f263])).
% 0.14/0.49 fof(f265,plain,(
% 0.14/0.49 $false|sQ6_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f230,f49])).
% 0.14/0.49 fof(f266,plain,(
% 0.14/0.49 sQ6_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f265])).
% 0.14/0.49 fof(f272,plain,(
% 0.14/0.49 ~v1_relat_1(sK3_skl)|~v1_funct_1(sK3_skl)|v1_funct_1(sK5_skl)),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f62,f102])).
% 0.14/0.49 fof(f273,plain,(
% 0.14/0.49 ~v1_relat_1(sK2_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(sK4_skl)),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f61,f102])).
% 0.14/0.49 fof(f274,definition,(
% 0.14/0.49 sQ15_spl <=> (v1_funct_1(sK5_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f277,plain,(
% 0.14/0.49 ~sQ2_spl|~sQ9_spl|sQ15_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f272,f208,f237,f274])).
% 0.14/0.49 fof(f278,definition,(
% 0.14/0.49 sQ16_spl <=> (v1_funct_1(sK4_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f281,plain,(
% 0.14/0.49 ~sQ4_spl|~sQ6_spl|sQ16_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f273,f215,f228,f278])).
% 0.14/0.49 fof(f288,plain,(
% 0.14/0.49 ![X0]: (k1_realset1(sK2_skl,X0)=k7_relat_1(sK2_skl,k2_zfmisc_1(X0,X0)))),
% 0.14/0.49 inference(resolution,[status(thm)],[f82,f205])).
% 0.14/0.49 fof(f289,plain,(
% 0.14/0.49 ![X0]: (k1_realset1(sK3_skl,X0)=k7_relat_1(sK3_skl,k2_zfmisc_1(X0,X0)))),
% 0.14/0.49 inference(resolution,[status(thm)],[f82,f204])).
% 0.14/0.49 fof(f329,plain,(
% 0.14/0.49 ![X0]: (~v1_relat_1(sK2_skl)|~v1_funct_1(sK2_skl)|v1_funct_1(k1_realset1(sK2_skl,X0)))),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f288,f106])).
% 0.14/0.49 fof(f331,definition,(
% 0.14/0.49 ![X0]: (sQ17_spl <=> (v1_funct_1(k1_realset1(sK2_skl,X0))))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f332,plain,(
% 0.14/0.49 ![X0]: (v1_funct_1(k1_realset1(sK2_skl,X0))|~sQ17_spl)),
% 0.14/0.49 inference(component_clause,[status(thm)],[f331])).
% 0.14/0.49 fof(f334,plain,(
% 0.14/0.49 ~sQ4_spl|~sQ6_spl|sQ17_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f329,f215,f228,f331])).
% 0.14/0.49 fof(f343,plain,(
% 0.14/0.49 ![X0]: (~v1_relat_1(sK3_skl)|~v1_funct_1(sK3_skl)|v1_funct_1(k1_realset1(sK3_skl,X0)))),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f289,f106])).
% 0.14/0.49 fof(f345,definition,(
% 0.14/0.49 ![X0]: (sQ19_spl <=> (v1_funct_1(k1_realset1(sK3_skl,X0))))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f346,plain,(
% 0.14/0.49 ![X0]: (v1_funct_1(k1_realset1(sK3_skl,X0))|~sQ19_spl)),
% 0.14/0.49 inference(component_clause,[status(thm)],[f345])).
% 0.14/0.49 fof(f348,plain,(
% 0.14/0.49 ~sQ2_spl|~sQ9_spl|sQ19_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f343,f208,f237,f345])).
% 0.14/0.49 fof(f404,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(sK0_skl)|v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(sK3_skl)|~v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r4_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ12_spl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f162,f247])).
% 0.14/0.49 fof(f405,definition,(
% 0.14/0.49 sQ26_spl <=> (v1_xboole_0(sK0_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f406,plain,(
% 0.14/0.49 v1_xboole_0(sK0_skl)|~sQ26_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f405])).
% 0.14/0.49 fof(f408,definition,(
% 0.14/0.49 ![X0]: (sQ27_spl <=> (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r4_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f409,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r4_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ27_spl)),
% 0.14/0.49 inference(component_clause,[status(thm)],[f408])).
% 0.14/0.49 fof(f411,plain,(
% 0.14/0.49 sQ26_spl|sQ27_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f404,f405,f408,f228,f231,f234,f237,f240,f243,f246])).
% 0.14/0.49 fof(f412,plain,(
% 0.14/0.49 $false|~sQ26_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f406,f46])).
% 0.14/0.49 fof(f413,plain,(
% 0.14/0.49 ~sQ26_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f412])).
% 0.14/0.49 fof(f414,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r4_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ17_spl|~sQ27_spl)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f409,f332])).
% 0.14/0.49 fof(f415,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(sK0_skl)|v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK2_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(sK3_skl)|~v1_funct_2(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~m2_relset_1(sK3_skl,k2_zfmisc_1(sK0_skl,sK0_skl),sK0_skl)|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r5_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ13_spl)),
% 0.14/0.49 inference(resolution,[status(thm)],[f163,f252])).
% 0.14/0.49 fof(f416,definition,(
% 0.14/0.49 ![X0]: (sQ28_spl <=> (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r5_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f417,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_1(k1_realset1(sK2_skl,X0))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r5_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ28_spl)),
% 0.14/0.49 inference(component_clause,[status(thm)],[f416])).
% 0.14/0.49 fof(f419,plain,(
% 0.14/0.49 sQ26_spl|sQ28_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f415,f405,f416,f228,f231,f234,f237,f240,f243,f251])).
% 0.14/0.49 fof(f420,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(k1_realset1(sK3_skl,X0))|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r5_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ17_spl|~sQ28_spl)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f417,f332])).
% 0.14/0.49 fof(f435,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r4_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ19_spl|~sQ17_spl|~sQ27_spl)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f414,f346])).
% 0.14/0.49 fof(f436,plain,(
% 0.14/0.49 v1_xboole_0(sK1_skl)|~m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl))|~sQ19_spl|~sQ17_spl|~sQ27_spl),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f62,f435])).
% 0.14/0.49 fof(f437,definition,(
% 0.14/0.49 sQ31_spl <=> (v1_xboole_0(sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f438,plain,(
% 0.14/0.49 v1_xboole_0(sK1_skl)|~sQ31_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f437])).
% 0.14/0.49 fof(f440,definition,(
% 0.14/0.49 sQ32_spl <=> (m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl)))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f442,plain,(
% 0.14/0.49 ~m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))|sQ32_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f440])).
% 0.14/0.49 fof(f443,definition,(
% 0.14/0.49 sQ33_spl <=> (v1_funct_2(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f445,plain,(
% 0.14/0.49 ~v1_funct_2(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ33_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f443])).
% 0.14/0.49 fof(f446,definition,(
% 0.14/0.49 sQ34_spl <=> (m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f448,plain,(
% 0.14/0.49 ~m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ34_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f446])).
% 0.14/0.49 fof(f449,definition,(
% 0.14/0.49 sQ35_spl <=> (v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f451,plain,(
% 0.14/0.49 ~v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ35_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f449])).
% 0.14/0.49 fof(f452,definition,(
% 0.14/0.49 sQ36_spl <=> (m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f454,plain,(
% 0.14/0.49 ~m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ36_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f452])).
% 0.14/0.49 fof(f455,definition,(
% 0.14/0.49 sQ37_spl <=> (r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl)))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f456,plain,(
% 0.14/0.49 r4_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl))|~sQ37_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f455])).
% 0.14/0.49 fof(f458,plain,(
% 0.14/0.49 sQ31_spl|~sQ32_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|sQ37_spl|~sQ19_spl|~sQ17_spl|~sQ27_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f436,f437,f440,f443,f446,f449,f452,f455,f345,f331,f408])).
% 0.14/0.49 fof(f459,plain,(
% 0.14/0.49 r4_binop_1(sK1_skl,sK4_skl,k1_realset1(sK3_skl,sK1_skl))|~sQ37_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f61,f456])).
% 0.14/0.49 fof(f460,plain,(
% 0.14/0.49 r4_binop_1(sK1_skl,sK4_skl,sK5_skl)|~sQ37_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f62,f459])).
% 0.14/0.49 fof(f471,definition,(
% 0.14/0.49 sQ39_spl <=> (v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f473,plain,(
% 0.14/0.49 ~v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ39_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f471])).
% 0.14/0.49 fof(f474,definition,(
% 0.14/0.49 sQ40_spl <=> (m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f476,plain,(
% 0.14/0.49 ~m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ40_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f474])).
% 0.14/0.49 fof(f477,definition,(
% 0.14/0.49 sQ41_spl <=> (m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f479,plain,(
% 0.14/0.49 ~m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ41_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f477])).
% 0.14/0.49 fof(f481,plain,(
% 0.14/0.49 $false|sQ35_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f451,f59])).
% 0.14/0.49 fof(f482,plain,(
% 0.14/0.49 sQ35_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f481])).
% 0.14/0.49 fof(f483,plain,(
% 0.14/0.49 $false|~sQ31_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f438,f47])).
% 0.14/0.49 fof(f484,plain,(
% 0.14/0.49 ~sQ31_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f483])).
% 0.14/0.49 fof(f485,plain,(
% 0.14/0.49 $false|sQ41_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f479,f60])).
% 0.14/0.49 fof(f486,plain,(
% 0.14/0.49 sQ41_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f485])).
% 0.14/0.49 fof(f487,plain,(
% 0.14/0.49 $false|sQ40_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f476,f57])).
% 0.14/0.49 fof(f488,plain,(
% 0.14/0.49 sQ40_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f487])).
% 0.14/0.49 fof(f489,plain,(
% 0.14/0.49 $false|sQ39_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f473,f56])).
% 0.14/0.49 fof(f490,plain,(
% 0.14/0.49 sQ39_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f489])).
% 0.14/0.49 fof(f492,plain,(
% 0.14/0.49 ~m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ36_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f62,f454])).
% 0.14/0.49 fof(f493,plain,(
% 0.14/0.49 $false|sQ36_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f492,f60])).
% 0.14/0.49 fof(f494,plain,(
% 0.14/0.49 sQ36_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f493])).
% 0.14/0.49 fof(f495,plain,(
% 0.14/0.49 ~m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ34_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f61,f448])).
% 0.14/0.49 fof(f496,plain,(
% 0.14/0.49 $false|sQ34_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f495,f57])).
% 0.14/0.49 fof(f497,plain,(
% 0.14/0.49 sQ34_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f496])).
% 0.14/0.49 fof(f499,plain,(
% 0.14/0.49 ~v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|sQ33_spl),
% 0.14/0.49 inference(forward_demodulation,[status(thm)],[f61,f445])).
% 0.14/0.49 fof(f500,plain,(
% 0.14/0.49 $false|sQ33_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f499,f56])).
% 0.14/0.49 fof(f501,plain,(
% 0.14/0.49 sQ33_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f500])).
% 0.14/0.49 fof(f503,plain,(
% 0.14/0.49 $false|sQ32_spl),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f442,f48])).
% 0.14/0.49 fof(f504,plain,(
% 0.14/0.49 sQ32_spl),
% 0.14/0.49 inference(contradiction_clause,[status(thm)],[f503])).
% 0.14/0.49 fof(f583,plain,(
% 0.14/0.49 ![X0]: (v1_xboole_0(X0)|~m1_subset_1(X0,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK2_skl,X0),k2_zfmisc_1(X0,X0),X0)|~v1_funct_2(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|~m2_relset_1(k1_realset1(sK3_skl,X0),k2_zfmisc_1(X0,X0),X0)|r5_binop_1(X0,k1_realset1(sK2_skl,X0),k1_realset1(sK3_skl,X0))|~sQ19_spl|~sQ17_spl|~sQ28_spl)),
% 0.14/0.49 inference(forward_subsumption_resolution,[status(thm)],[f420,f346])).
% 0.14/0.49 fof(f584,plain,(
% 0.14/0.49 v1_xboole_0(sK1_skl)|~m1_subset_1(sK1_skl,k1_zfmisc_1(sK0_skl))|~v1_funct_2(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(k1_realset1(sK2_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(k1_realset1(sK3_skl,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl))|~sQ19_spl|~sQ17_spl|~sQ28_spl),
% 0.14/0.49 inference(paramodulation,[status(thm)],[f62,f583])).
% 0.14/0.49 fof(f585,definition,(
% 0.14/0.49 sQ52_spl <=> (r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl)))),
% 0.14/0.49 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.49 fof(f586,plain,(
% 0.14/0.49 r5_binop_1(sK1_skl,k1_realset1(sK2_skl,sK1_skl),k1_realset1(sK3_skl,sK1_skl))|~sQ52_spl),
% 0.14/0.49 inference(component_clause,[status(thm)],[f585])).
% 0.14/0.49 fof(f588,plain,(
% 0.14/0.49 sQ31_spl|~sQ32_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|sQ52_spl|~sQ19_spl|~sQ17_spl|~sQ28_spl),
% 0.14/0.49 inference(split_clause,[status(thm)],[f584,f437,f440,f443,f446,f449,f452,f585,f345,f331,f416])).
% 0.14/0.49 fof(f589,plain,(
% 0.14/0.49 r5_binop_1(sK1_skl,sK4_skl,k1_realset1(sK3_skl,sK1_skl))|~sQ52_spl),
% 0.14/0.50 inference(forward_demodulation,[status(thm)],[f61,f586])).
% 0.14/0.50 fof(f590,plain,(
% 0.14/0.50 r5_binop_1(sK1_skl,sK4_skl,sK5_skl)|~sQ52_spl),
% 0.14/0.50 inference(forward_demodulation,[status(thm)],[f62,f589])).
% 0.14/0.50 fof(f592,plain,(
% 0.14/0.50 ~v1_funct_1(sK4_skl)|~v1_funct_2(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(sK4_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~v1_funct_1(sK5_skl)|~v1_funct_2(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|~m2_relset_1(sK5_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)|r6_binop_1(sK1_skl,sK4_skl,sK5_skl)|~r4_binop_1(sK1_skl,sK4_skl,sK5_skl)|~sQ52_spl),
% 0.14/0.50 inference(resolution,[status(thm)],[f590,f80])).
% 0.14/0.50 fof(f597,definition,(
% 0.14/0.50 sQ54_spl <=> (r6_binop_1(sK1_skl,sK4_skl,sK5_skl))),
% 0.14/0.50 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.14/0.50 fof(f598,plain,(
% 0.14/0.50 r6_binop_1(sK1_skl,sK4_skl,sK5_skl)|~sQ54_spl),
% 0.14/0.50 inference(component_clause,[status(thm)],[f597])).
% 0.14/0.50 fof(f600,definition,(
% 0.14/0.50 sQ55_spl <=> (r4_binop_1(sK1_skl,sK4_skl,sK5_skl))),
% 0.14/0.50 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.14/0.50 fof(f602,plain,(
% 0.14/0.50 ~r4_binop_1(sK1_skl,sK4_skl,sK5_skl)|sQ55_spl),
% 0.14/0.50 inference(component_clause,[status(thm)],[f600])).
% 0.14/0.50 fof(f603,plain,(
% 0.14/0.50 ~sQ16_spl|~sQ39_spl|~sQ40_spl|~sQ15_spl|~sQ35_spl|~sQ41_spl|sQ54_spl|~sQ55_spl|~sQ52_spl),
% 0.14/0.50 inference(split_clause,[status(thm)],[f592,f278,f471,f474,f274,f449,f477,f597,f600,f585])).
% 0.14/0.50 fof(f605,plain,(
% 0.14/0.50 $false|~sQ54_spl),
% 0.14/0.50 inference(forward_subsumption_resolution,[status(thm)],[f598,f64])).
% 0.14/0.50 fof(f606,plain,(
% 0.14/0.50 ~sQ54_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f605])).
% 0.14/0.50 fof(f607,plain,(
% 0.14/0.50 $false|~sQ37_spl|sQ55_spl),
% 0.14/0.50 inference(forward_subsumption_resolution,[status(thm)],[f602,f460])).
% 0.14/0.50 fof(f608,plain,(
% 0.14/0.50 ~sQ37_spl|sQ55_spl),
% 0.14/0.50 inference(contradiction_clause,[status(thm)],[f607])).
% 0.14/0.50 fof(f609,plain,(
% 0.14/0.50 $false),
% 0.14/0.50 inference(sat_refutation,[status(thm)],[f223,f225,f249,f254,f256,f258,f260,f262,f264,f266,f277,f281,f334,f348,f411,f413,f419,f458,f482,f484,f486,f488,f490,f494,f497,f501,f504,f588,f603,f606,f608])).
% 0.14/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.52 % Elapsed time: 0.084453 seconds
% 0.14/0.52 % CPU time: 0.317442 seconds
% 0.14/0.52 % Total memory used: 107.517 MB
% 0.14/0.52 % Net memory used: 107.318 MB
%------------------------------------------------------------------------------