%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET980+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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 02:12:56 PM UTC 2026
% Result : Theorem 0.84s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SET980+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n010.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 05:46:10 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.84/0.88 % Refutation found
% 0.84/0.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.84/0.88 % SZS output start CNFRefutation for theBenchmark
% 0.84/0.88 fof(f1,axiom,(
% 0.84/0.88 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f3,axiom,(
% 0.84/0.88 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f7,axiom,(
% 0.84/0.88 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f10,axiom,(
% 0.84/0.88 (! [A,B] :( cartesian_product2(A,B) = empty_set<=> ( A = empty_set| B = empty_set ) ) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f11,conjecture,(
% 0.84/0.88 (! [A,B,C,D] :( cartesian_product2(A,B) = cartesian_product2(C,D)=> ( A = empty_set| B = empty_set| ( A = C& B = D ) ) ) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f12,negated_conjecture,(
% 0.84/0.88 ~((! [A,B,C,D] :( cartesian_product2(A,B) = cartesian_product2(C,D)=> ( A = empty_set| B = empty_set| ( A = C& B = D ) ) ) ))),
% 0.84/0.88 inference(negated_conjecture,[status(cth)],[f11])).
% 0.84/0.88 fof(f13,axiom,(
% 0.84/0.88 (! [A,B] :( (! [C] :( in(C,A)<=> in(C,B) ))=> A = B ) )),
% 0.84/0.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.84/0.88 fof(f14,plain,(
% 0.84/0.88 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.84/0.88 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.84/0.88 fof(f15,plain,(
% 0.84/0.88 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f14])).
% 0.84/0.88 fof(f17,plain,(
% 0.84/0.88 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 0.84/0.88 inference(NNF_transformation,[status(thm)],[f3])).
% 0.84/0.88 fof(f18,plain,(
% 0.84/0.88 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 0.84/0.88 inference(miniscoping,[status(thm)],[f17])).
% 0.84/0.88 fof(f19,plain,(
% 0.84/0.88 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK0_skl(A),A)))),
% 0.84/0.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f18])).
% 0.84/0.88 fof(f20,plain,(
% 0.84/0.88 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f19])).
% 0.84/0.88 fof(f21,plain,(
% 0.84/0.88 ![X0]: (X0=empty_set|in(sK0_skl(X0),X0))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f19])).
% 0.84/0.88 fof(f25,plain,(
% 0.84/0.88 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.84/0.88 inference(NNF_transformation,[status(thm)],[f7])).
% 0.84/0.88 fof(f26,plain,(
% 0.84/0.88 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 0.84/0.88 inference(miniscoping,[status(thm)],[f25])).
% 0.84/0.88 fof(f27,plain,(
% 0.84/0.88 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X0,X2))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f26])).
% 0.84/0.88 fof(f28,plain,(
% 0.84/0.88 ![X0,X1,X2,X3]: (~in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|in(X1,X3))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f26])).
% 0.84/0.88 fof(f29,plain,(
% 0.84/0.88 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f26])).
% 0.84/0.88 fof(f34,plain,(
% 0.84/0.88 ![A,B]: ((~cartesian_product2(A,B)=empty_set|(A=empty_set|B=empty_set))&(cartesian_product2(A,B)=empty_set|(~A=empty_set&~B=empty_set)))),
% 0.84/0.88 inference(NNF_transformation,[status(thm)],[f10])).
% 0.84/0.88 fof(f35,plain,(
% 0.84/0.88 (![A,B]: (~cartesian_product2(A,B)=empty_set|(A=empty_set|B=empty_set)))&(![A,B]: (cartesian_product2(A,B)=empty_set|(~A=empty_set&~B=empty_set)))),
% 0.84/0.88 inference(miniscoping,[status(thm)],[f34])).
% 0.84/0.88 fof(f36,plain,(
% 0.84/0.88 ![X0,X1]: (~cartesian_product2(X0,X1)=empty_set|X0=empty_set|X1=empty_set)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f35])).
% 0.84/0.88 fof(f37,plain,(
% 0.84/0.88 ![X0,X1]: (cartesian_product2(X0,X1)=empty_set|~X0=empty_set)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f35])).
% 0.84/0.88 fof(f38,plain,(
% 0.84/0.88 ![X0,X1]: (cartesian_product2(X0,X1)=empty_set|~X1=empty_set)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f35])).
% 0.84/0.88 fof(f39,plain,(
% 0.84/0.88 (?[A,B,C,D]: (cartesian_product2(A,B)=cartesian_product2(C,D)&((~A=empty_set&~B=empty_set)&(~A=C|~B=D))))),
% 0.84/0.88 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.84/0.88 fof(f40,plain,(
% 0.84/0.88 (cartesian_product2(sK3_skl,sK4_skl)=cartesian_product2(sK5_skl,sK6_skl)&((~sK3_skl=empty_set&~sK4_skl=empty_set)&(~sK3_skl=sK5_skl|~sK4_skl=sK6_skl)))),
% 0.84/0.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(A,sK3_skl),skolemize(B,sK4_skl),skolemize(C,sK5_skl),skolemize(D,sK6_skl)],[f39])).
% 0.84/0.88 fof(f41,plain,(
% 0.84/0.88 cartesian_product2(sK3_skl,sK4_skl)=cartesian_product2(sK5_skl,sK6_skl)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f40])).
% 0.84/0.88 fof(f42,plain,(
% 0.84/0.88 ~sK3_skl=empty_set),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f40])).
% 0.84/0.88 fof(f43,plain,(
% 0.84/0.88 ~sK4_skl=empty_set),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f40])).
% 0.84/0.88 fof(f44,plain,(
% 0.84/0.88 ~sK3_skl=sK5_skl|~sK4_skl=sK6_skl),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f40])).
% 0.84/0.88 fof(f45,plain,(
% 0.84/0.88 ![A,B]: ((?[C]: (in(C,A)<~>in(C,B)))|A=B)),
% 0.84/0.88 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.84/0.88 fof(f46,plain,(
% 0.84/0.88 ![A,B]: ((?[C]: ((in(C,A)|in(C,B))&(~in(C,A)|~in(C,B))))|A=B)),
% 0.84/0.88 inference(NNF_transformation,[status(thm)],[f45])).
% 0.84/0.88 fof(f47,plain,(
% 0.84/0.88 ![A,B]: (((in(sK7_skl(B,A),A)|in(sK7_skl(B,A),B))&(~in(sK7_skl(B,A),A)|~in(sK7_skl(B,A),B)))|A=B)),
% 0.84/0.88 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(C,sK7_skl(B,A))],[f46])).
% 0.84/0.88 fof(f48,plain,(
% 0.84/0.88 ![X0,X1]: (in(sK7_skl(X0,X1),X1)|in(sK7_skl(X0,X1),X0)|X1=X0)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f47])).
% 0.84/0.88 fof(f49,plain,(
% 0.84/0.88 ![X0,X1]: (~in(sK7_skl(X0,X1),X1)|~in(sK7_skl(X0,X1),X0)|X1=X0)),
% 0.84/0.88 inference(cnf_transformation,[status(thm)],[f47])).
% 0.84/0.88 fof(f50,definition,(
% 0.84/0.88 sQ0_spl <=> (sK3_skl=sK5_skl)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f51,plain,(
% 0.84/0.88 sK3_skl=sK5_skl|~sQ0_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f50])).
% 0.84/0.88 fof(f53,definition,(
% 0.84/0.88 sQ1_spl <=> (sK4_skl=sK6_skl)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f56,plain,(
% 0.84/0.88 ~sQ0_spl|~sQ1_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f44,f50,f53])).
% 0.84/0.88 fof(f57,plain,(
% 0.84/0.88 ![X0]: (~in(X0,empty_set))),
% 0.84/0.88 inference(destructive_equality_resolution,[status(thm)],[f20])).
% 0.84/0.88 fof(f58,plain,(
% 0.84/0.88 ![X0]: (cartesian_product2(empty_set,X0)=empty_set)),
% 0.84/0.88 inference(destructive_equality_resolution,[status(thm)],[f37])).
% 0.84/0.88 fof(f59,plain,(
% 0.84/0.88 ![X0]: (cartesian_product2(X0,empty_set)=empty_set)),
% 0.84/0.88 inference(destructive_equality_resolution,[status(thm)],[f38])).
% 0.84/0.88 fof(f62,plain,(
% 0.84/0.88 ![X0]: (empty_set=empty_set|X0=empty_set)),
% 0.84/0.88 inference(resolution,[status(thm)],[f36,f58])).
% 0.84/0.88 fof(f65,plain,(
% 0.84/0.88 ~cartesian_product2(sK5_skl,sK6_skl)=empty_set|sK3_skl=empty_set|sK4_skl=empty_set),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f36])).
% 0.84/0.88 fof(f67,definition,(
% 0.84/0.88 sQ2_spl <=> (empty_set=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f70,definition,(
% 0.84/0.88 ![X0]: (sQ3_spl <=> (X0=empty_set))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f71,plain,(
% 0.84/0.88 ![X0]: (X0=empty_set|~sQ3_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f70])).
% 0.84/0.88 fof(f73,plain,(
% 0.84/0.88 sQ2_spl|sQ3_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f62,f67,f70])).
% 0.84/0.88 fof(f76,definition,(
% 0.84/0.88 sQ4_spl <=> (cartesian_product2(sK5_skl,sK6_skl)=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f78,plain,(
% 0.84/0.88 ~cartesian_product2(sK5_skl,sK6_skl)=empty_set|sQ4_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f76])).
% 0.84/0.88 fof(f79,definition,(
% 0.84/0.88 sQ5_spl <=> (sK3_skl=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f80,plain,(
% 0.84/0.88 sK3_skl=empty_set|~sQ5_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f79])).
% 0.84/0.88 fof(f82,definition,(
% 0.84/0.88 sQ6_spl <=> (sK4_skl=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f83,plain,(
% 0.84/0.88 sK4_skl=empty_set|~sQ6_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f82])).
% 0.84/0.88 fof(f85,plain,(
% 0.84/0.88 ~sQ4_spl|sQ5_spl|sQ6_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f65,f76,f79,f82])).
% 0.84/0.88 fof(f87,plain,(
% 0.84/0.88 $false|~sQ6_spl),
% 0.84/0.88 inference(forward_subsumption_resolution,[status(thm)],[f83,f43])).
% 0.84/0.88 fof(f88,plain,(
% 0.84/0.88 ~sQ6_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f87])).
% 0.84/0.88 fof(f132,plain,(
% 0.84/0.88 ![X0,X1]: (~in(ordered_pair(X0,X1),cartesian_product2(sK5_skl,sK6_skl))|in(X0,sK3_skl))),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f27])).
% 0.84/0.88 fof(f135,plain,(
% 0.84/0.88 ![X0,X1]: (~in(ordered_pair(X0,X1),cartesian_product2(sK5_skl,sK6_skl))|in(X1,sK4_skl))),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f28])).
% 0.84/0.88 fof(f138,plain,(
% 0.84/0.88 ![X0]: (in(sK7_skl(X0,empty_set),X0)|empty_set=X0)),
% 0.84/0.88 inference(resolution,[status(thm)],[f48,f57])).
% 0.84/0.88 fof(f141,plain,(
% 0.84/0.88 ![X0]: (in(sK7_skl(empty_set,X0),X0)|X0=empty_set)),
% 0.84/0.88 inference(resolution,[status(thm)],[f48,f57])).
% 0.84/0.88 fof(f148,plain,(
% 0.84/0.88 ![X0,X1,X2]: (in(ordered_pair(X0,sK7_skl(empty_set,X1)),cartesian_product2(X2,X1))|~in(X0,X2)|X1=empty_set)),
% 0.84/0.88 inference(resolution,[status(thm)],[f29,f141])).
% 0.84/0.88 fof(f149,plain,(
% 0.84/0.88 ![X0,X1,X2]: (in(ordered_pair(X0,sK7_skl(X1,empty_set)),cartesian_product2(X2,X1))|~in(X0,X2)|empty_set=X1)),
% 0.84/0.88 inference(resolution,[status(thm)],[f29,f138])).
% 0.84/0.88 fof(f154,plain,(
% 0.84/0.88 ![X0,X1,X2]: (in(ordered_pair(X0,sK0_skl(X1)),cartesian_product2(X2,X1))|~in(X0,X2)|X1=empty_set)),
% 0.84/0.88 inference(resolution,[status(thm)],[f29,f21])).
% 0.84/0.88 fof(f190,plain,(
% 0.84/0.88 ![X0,X1]: (in(ordered_pair(sK0_skl(X0),sK7_skl(empty_set,X1)),cartesian_product2(X0,X1))|X1=empty_set|X0=empty_set)),
% 0.84/0.88 inference(resolution,[status(thm)],[f148,f21])).
% 0.84/0.88 fof(f198,plain,(
% 0.84/0.88 sK6_skl=empty_set|sK5_skl=empty_set|in(sK7_skl(empty_set,sK6_skl),sK4_skl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f190,f135])).
% 0.84/0.88 fof(f199,plain,(
% 0.84/0.88 sK6_skl=empty_set|sK5_skl=empty_set|in(sK0_skl(sK5_skl),sK3_skl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f190,f132])).
% 0.84/0.88 fof(f207,plain,(
% 0.84/0.88 in(ordered_pair(sK0_skl(sK3_skl),sK7_skl(empty_set,sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|sK4_skl=empty_set|sK3_skl=empty_set),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f190])).
% 0.84/0.88 fof(f209,definition,(
% 0.84/0.88 sQ8_spl <=> (sK6_skl=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f210,plain,(
% 0.84/0.88 sK6_skl=empty_set|~sQ8_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f209])).
% 0.84/0.88 fof(f212,definition,(
% 0.84/0.88 sQ9_spl <=> (sK5_skl=empty_set)),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f213,plain,(
% 0.84/0.88 sK5_skl=empty_set|~sQ9_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f212])).
% 0.84/0.88 fof(f215,definition,(
% 0.84/0.88 sQ10_spl <=> (in(sK7_skl(empty_set,sK6_skl),sK4_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f216,plain,(
% 0.84/0.88 in(sK7_skl(empty_set,sK6_skl),sK4_skl)|~sQ10_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f215])).
% 0.84/0.88 fof(f218,plain,(
% 0.84/0.88 sQ8_spl|sQ9_spl|sQ10_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f198,f209,f212,f215])).
% 0.84/0.88 fof(f219,definition,(
% 0.84/0.88 sQ11_spl <=> (in(sK0_skl(sK5_skl),sK3_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f220,plain,(
% 0.84/0.88 in(sK0_skl(sK5_skl),sK3_skl)|~sQ11_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f219])).
% 0.84/0.88 fof(f222,plain,(
% 0.84/0.88 sQ8_spl|sQ9_spl|sQ11_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f199,f209,f212,f219])).
% 0.84/0.88 fof(f223,definition,(
% 0.84/0.88 ![X0]: (sQ12_spl <=> (X0=empty_set|in(sK7_skl(empty_set,X0),X0)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f224,plain,(
% 0.84/0.88 ![X0]: (X0=empty_set|in(sK7_skl(empty_set,X0),X0)|~sQ12_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f223])).
% 0.84/0.88 fof(f227,definition,(
% 0.84/0.88 ![X1]: (sQ13_spl <=> (X1=empty_set|in(sK0_skl(X1),X1)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f228,plain,(
% 0.84/0.88 ![X0]: (X0=empty_set|in(sK0_skl(X0),X0)|~sQ13_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f227])).
% 0.84/0.88 fof(f235,definition,(
% 0.84/0.88 sQ15_spl <=> (in(ordered_pair(sK0_skl(sK3_skl),sK7_skl(empty_set,sK4_skl)),cartesian_product2(sK5_skl,sK6_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f236,plain,(
% 0.84/0.88 in(ordered_pair(sK0_skl(sK3_skl),sK7_skl(empty_set,sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~sQ15_spl),
% 0.84/0.88 inference(component_clause,[status(thm)],[f235])).
% 0.84/0.88 fof(f238,plain,(
% 0.84/0.88 sQ15_spl|sQ6_spl|sQ5_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f207,f235,f82,f79])).
% 0.84/0.88 fof(f243,plain,(
% 0.84/0.88 $false|~sQ3_spl),
% 0.84/0.88 inference(backward_subsumption_resolution,[status(thm)],[f43,f71])).
% 0.84/0.88 fof(f245,plain,(
% 0.84/0.88 ~sQ3_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f243])).
% 0.84/0.88 fof(f250,plain,(
% 0.84/0.88 $false|~sQ5_spl),
% 0.84/0.88 inference(forward_subsumption_resolution,[status(thm)],[f80,f42])).
% 0.84/0.88 fof(f251,plain,(
% 0.84/0.88 ~sQ5_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f250])).
% 0.84/0.88 fof(f255,plain,(
% 0.84/0.88 ~cartesian_product2(empty_set,sK6_skl)=empty_set|~sQ9_spl|sQ4_spl),
% 0.84/0.88 inference(forward_demodulation,[status(thm)],[f213,f78])).
% 0.84/0.88 fof(f256,plain,(
% 0.84/0.88 ~empty_set=empty_set|~sQ9_spl|sQ4_spl),
% 0.84/0.88 inference(forward_demodulation,[status(thm)],[f58,f255])).
% 0.84/0.88 fof(f257,plain,(
% 0.84/0.88 $false|~sQ9_spl|sQ4_spl),
% 0.84/0.88 inference(trivial_equality_resolution,[status(thm)],[f256])).
% 0.84/0.88 fof(f258,plain,(
% 0.84/0.88 ~sQ9_spl|sQ4_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f257])).
% 0.84/0.88 fof(f260,plain,(
% 0.84/0.88 ~cartesian_product2(sK5_skl,empty_set)=empty_set|~sQ8_spl|sQ4_spl),
% 0.84/0.88 inference(forward_demodulation,[status(thm)],[f210,f78])).
% 0.84/0.88 fof(f261,plain,(
% 0.84/0.88 ~empty_set=empty_set|~sQ8_spl|sQ4_spl),
% 0.84/0.88 inference(forward_demodulation,[status(thm)],[f59,f260])).
% 0.84/0.88 fof(f262,plain,(
% 0.84/0.88 $false|~sQ8_spl|sQ4_spl),
% 0.84/0.88 inference(trivial_equality_resolution,[status(thm)],[f261])).
% 0.84/0.88 fof(f263,plain,(
% 0.84/0.88 ~sQ8_spl|sQ4_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f262])).
% 0.84/0.88 fof(f324,definition,(
% 0.84/0.88 ![X0,X1]: (sQ17_spl <=> (~in(X0,X1)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f325,plain,(
% 0.84/0.88 ![X0,X1]: (~in(X0,X1)|~sQ17_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f324])).
% 0.84/0.88 fof(f329,plain,(
% 0.84/0.88 in(sK0_skl(sK3_skl),sK3_skl)|~sQ15_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f236,f132])).
% 0.84/0.88 fof(f330,plain,(
% 0.84/0.88 in(sK7_skl(empty_set,sK4_skl),sK4_skl)|~sQ15_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f236,f135])).
% 0.84/0.88 fof(f331,plain,(
% 0.84/0.88 in(sK7_skl(empty_set,sK4_skl),sK6_skl)|~sQ15_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f236,f28])).
% 0.84/0.88 fof(f332,plain,(
% 0.84/0.88 in(sK0_skl(sK3_skl),sK5_skl)|~sQ15_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f236,f27])).
% 0.84/0.88 fof(f339,plain,(
% 0.84/0.88 ![X0,X1]: (in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(X1,sK3_skl))|~in(X0,X1)|~sQ15_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f329,f29])).
% 0.84/0.88 fof(f343,plain,(
% 0.84/0.88 ![X0,X1]: (in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(X1,sK5_skl))|~in(X0,X1)|~sQ15_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f332,f29])).
% 0.84/0.88 fof(f345,plain,(
% 0.84/0.88 ~in(sK7_skl(empty_set,sK4_skl),empty_set)|sK4_skl=empty_set|~sQ15_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f330,f49])).
% 0.84/0.88 fof(f350,definition,(
% 0.84/0.88 sQ18_spl <=> (in(sK7_skl(empty_set,sK4_skl),empty_set))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f353,plain,(
% 0.84/0.88 ~sQ18_spl|sQ6_spl|~sQ15_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f345,f350,f82,f235])).
% 0.84/0.88 fof(f356,plain,(
% 0.84/0.88 ![X0,X1]: (in(ordered_pair(X0,sK7_skl(empty_set,sK4_skl)),cartesian_product2(X1,sK6_skl))|~in(X0,X1)|~sQ15_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f331,f29])).
% 0.84/0.88 fof(f358,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK5_skl)|sK6_skl=empty_set|in(X0,sK3_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f148,f132])).
% 0.84/0.88 fof(f360,plain,(
% 0.84/0.88 ![X0,X1,X2]: (~in(X0,X1)|X2=empty_set|in(sK7_skl(empty_set,X2),X2))),
% 0.84/0.88 inference(resolution,[status(thm)],[f148,f28])).
% 0.84/0.88 fof(f366,plain,(
% 0.84/0.88 ![X0]: (in(ordered_pair(X0,sK7_skl(empty_set,sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)|sK4_skl=empty_set)),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f148])).
% 0.84/0.88 fof(f369,definition,(
% 0.84/0.88 ![X0]: (sQ19_spl <=> (~in(X0,sK5_skl)|in(X0,sK3_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f370,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK5_skl)|in(X0,sK3_skl)|~sQ19_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f369])).
% 0.84/0.88 fof(f372,plain,(
% 0.84/0.88 sQ19_spl|sQ8_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f358,f369,f209])).
% 0.84/0.88 fof(f373,definition,(
% 0.84/0.88 ![X0]: (sQ20_spl <=> (~in(X0,sK5_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f374,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK5_skl)|~sQ20_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f373])).
% 0.84/0.88 fof(f377,plain,(
% 0.84/0.88 sQ17_spl|sQ12_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f360,f324,f223])).
% 0.84/0.88 fof(f378,definition,(
% 0.84/0.88 ![X0,X1]: (sQ21_spl <=> (~in(X0,X1)|in(X0,X1)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f382,definition,(
% 0.84/0.88 ![X0]: (sQ22_spl <=> (in(ordered_pair(X0,sK7_skl(empty_set,sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f385,plain,(
% 0.84/0.88 sQ22_spl|sQ6_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f366,f382,f82])).
% 0.84/0.88 fof(f391,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK5_skl)|empty_set=sK6_skl|in(sK7_skl(sK6_skl,empty_set),sK4_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f149,f135])).
% 0.84/0.88 fof(f392,plain,(
% 0.84/0.88 ![X0,X1,X2]: (~in(X0,X1)|empty_set=X2|in(sK7_skl(X2,empty_set),X2))),
% 0.84/0.88 inference(resolution,[status(thm)],[f149,f28])).
% 0.84/0.88 fof(f398,plain,(
% 0.84/0.88 ![X0]: (in(ordered_pair(X0,sK7_skl(sK4_skl,empty_set)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)|empty_set=sK4_skl)),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f149])).
% 0.84/0.88 fof(f402,definition,(
% 0.84/0.88 sQ24_spl <=> (in(sK7_skl(sK6_skl,empty_set),sK4_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f405,plain,(
% 0.84/0.88 sQ20_spl|sQ8_spl|sQ24_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f391,f373,f209,f402])).
% 0.84/0.88 fof(f406,definition,(
% 0.84/0.88 ![X2]: (sQ25_spl <=> (empty_set=X2|in(sK7_skl(X2,empty_set),X2)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f407,plain,(
% 0.84/0.88 ![X0]: (empty_set=X0|in(sK7_skl(X0,empty_set),X0)|~sQ25_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f406])).
% 0.84/0.88 fof(f409,plain,(
% 0.84/0.88 sQ17_spl|sQ25_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f392,f324,f406])).
% 0.84/0.88 fof(f411,definition,(
% 0.84/0.88 ![X0]: (sQ26_spl <=> (in(ordered_pair(X0,sK7_skl(sK4_skl,empty_set)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f414,plain,(
% 0.84/0.88 sQ26_spl|sQ6_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f398,f411,f82])).
% 0.84/0.88 fof(f416,plain,(
% 0.84/0.88 $false|~sQ20_spl|~sQ15_spl),
% 0.84/0.88 inference(backward_subsumption_resolution,[status(thm)],[f332,f374])).
% 0.84/0.88 fof(f417,plain,(
% 0.84/0.88 $false|~sQ17_spl|~sQ15_spl),
% 0.84/0.88 inference(backward_subsumption_resolution,[status(thm)],[f236,f325])).
% 0.84/0.88 fof(f463,plain,(
% 0.84/0.88 ~sQ20_spl|~sQ15_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f416])).
% 0.84/0.88 fof(f464,plain,(
% 0.84/0.88 ~sQ17_spl|~sQ15_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f417])).
% 0.84/0.88 fof(f471,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK5_skl)|~in(sK3_skl,X0)|~sQ19_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f370,f15])).
% 0.84/0.88 fof(f472,plain,(
% 0.84/0.88 ![X0]: (~in(sK7_skl(X0,sK3_skl),X0)|sK3_skl=X0|~in(sK7_skl(X0,sK3_skl),sK5_skl)|~sQ19_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f49,f370])).
% 0.84/0.88 fof(f474,plain,(
% 0.84/0.88 ![X0,X1]: (in(ordered_pair(X0,X1),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)|~in(X1,sK4_skl))),
% 0.84/0.88 inference(paramodulation,[status(thm)],[f41,f29])).
% 0.84/0.88 fof(f477,plain,(
% 0.84/0.88 ![X0,X1,X2,X3]: (in(X0,X1)|~in(X2,X3)|~in(X0,X1))),
% 0.84/0.88 inference(resolution,[status(thm)],[f28,f29])).
% 0.84/0.88 fof(f481,plain,(
% 0.84/0.88 sQ21_spl|sQ17_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f477,f378,f324])).
% 0.84/0.88 fof(f492,plain,(
% 0.84/0.88 ~in(sK3_skl,sK5_skl)|~in(sK3_skl,sK5_skl)|~sQ19_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f471,f370])).
% 0.84/0.88 fof(f493,definition,(
% 0.84/0.88 sQ28_spl <=> (in(sK3_skl,sK5_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f496,plain,(
% 0.84/0.88 ~sQ28_spl|~sQ19_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f492,f493,f369])).
% 0.84/0.88 fof(f501,plain,(
% 0.84/0.88 ![X0,X1]: (in(X0,sK4_skl)|~in(X1,sK5_skl)|~in(X0,sK6_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f135,f29])).
% 0.84/0.88 fof(f502,definition,(
% 0.84/0.88 ![X0]: (sQ29_spl <=> (in(X0,sK4_skl)|~in(X0,sK6_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f503,plain,(
% 0.84/0.88 ![X0]: (in(X0,sK4_skl)|~in(X0,sK6_skl)|~sQ29_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f502])).
% 0.84/0.88 fof(f505,plain,(
% 0.84/0.88 sQ29_spl|sQ20_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f501,f502,f373])).
% 0.84/0.88 fof(f506,plain,(
% 0.84/0.88 ![X0,X1]: (~in(X0,sK3_skl)|~in(X1,sK4_skl)|in(X1,sK4_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f474,f135])).
% 0.84/0.88 fof(f507,plain,(
% 0.84/0.88 ![X0,X1]: (~in(X0,sK3_skl)|~in(X1,sK4_skl)|in(X0,sK3_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f474,f132])).
% 0.84/0.88 fof(f508,plain,(
% 0.84/0.88 ![X0,X1]: (~in(X0,sK3_skl)|~in(X1,sK4_skl)|in(X1,sK6_skl))),
% 0.84/0.88 inference(resolution,[status(thm)],[f474,f28])).
% 0.84/0.88 fof(f510,definition,(
% 0.84/0.88 ![X0]: (sQ30_spl <=> (~in(X0,sK3_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f511,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK3_skl)|~sQ30_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f510])).
% 0.84/0.88 fof(f513,definition,(
% 0.84/0.88 ![X1]: (sQ31_spl <=> (~in(X1,sK4_skl)|in(X1,sK4_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f516,plain,(
% 0.84/0.88 sQ30_spl|sQ31_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f506,f510,f513])).
% 0.84/0.88 fof(f517,definition,(
% 0.84/0.88 ![X0]: (sQ32_spl <=> (~in(X0,sK3_skl)|in(X0,sK3_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f520,definition,(
% 0.84/0.88 ![X1]: (sQ33_spl <=> (~in(X1,sK4_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f521,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK4_skl)|~sQ33_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f520])).
% 0.84/0.88 fof(f523,plain,(
% 0.84/0.88 sQ32_spl|sQ33_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f507,f517,f520])).
% 0.84/0.88 fof(f524,definition,(
% 0.84/0.88 ![X1]: (sQ34_spl <=> (~in(X1,sK4_skl)|in(X1,sK6_skl)))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f525,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK4_skl)|in(X0,sK6_skl)|~sQ34_spl)),
% 0.84/0.88 inference(component_clause,[status(thm)],[f524])).
% 0.84/0.88 fof(f527,plain,(
% 0.84/0.88 sQ30_spl|sQ34_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f508,f510,f524])).
% 0.84/0.88 fof(f529,plain,(
% 0.84/0.88 $false|~sQ30_spl|~sQ11_spl),
% 0.84/0.88 inference(backward_subsumption_resolution,[status(thm)],[f220,f511])).
% 0.84/0.88 fof(f533,plain,(
% 0.84/0.88 ~sQ30_spl|~sQ11_spl),
% 0.84/0.88 inference(contradiction_clause,[status(thm)],[f529])).
% 0.84/0.88 fof(f536,plain,(
% 0.84/0.88 ![X0]: (~in(sK7_skl(X0,sK4_skl),sK6_skl)|~in(sK7_skl(X0,sK4_skl),X0)|sK4_skl=X0|~sQ29_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f503,f49])).
% 0.84/0.88 fof(f538,plain,(
% 0.84/0.88 ![X0]: (~in(X0,sK6_skl)|~in(sK4_skl,X0)|~sQ29_spl)),
% 0.84/0.88 inference(resolution,[status(thm)],[f503,f15])).
% 0.84/0.88 fof(f546,plain,(
% 0.84/0.88 in(sK7_skl(empty_set,sK6_skl),sK6_skl)|~sQ34_spl|~sQ10_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f525,f216])).
% 0.84/0.88 fof(f549,plain,(
% 0.84/0.88 in(sK7_skl(sK4_skl,empty_set),sK6_skl)|empty_set=sK4_skl|~sQ34_spl|~sQ25_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f525,f407])).
% 0.84/0.88 fof(f550,plain,(
% 0.84/0.88 in(sK0_skl(sK4_skl),sK6_skl)|sK4_skl=empty_set|~sQ34_spl|~sQ13_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f525,f228])).
% 0.84/0.88 fof(f552,definition,(
% 0.84/0.88 sQ37_spl <=> (in(sK7_skl(sK4_skl,empty_set),sK6_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f555,plain,(
% 0.84/0.88 sQ37_spl|sQ6_spl|~sQ34_spl|~sQ25_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f549,f552,f82,f524,f406])).
% 0.84/0.88 fof(f556,definition,(
% 0.84/0.88 sQ38_spl <=> (in(sK0_skl(sK4_skl),sK6_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f559,plain,(
% 0.84/0.88 sQ38_spl|sQ6_spl|~sQ34_spl|~sQ13_spl),
% 0.84/0.88 inference(split_clause,[status(thm)],[f550,f556,f82,f524,f227])).
% 0.84/0.88 fof(f566,plain,(
% 0.84/0.88 ~in(sK4_skl,sK6_skl)|~in(sK4_skl,sK6_skl)|~sQ29_spl),
% 0.84/0.88 inference(resolution,[status(thm)],[f538,f503])).
% 0.84/0.88 fof(f568,definition,(
% 0.84/0.88 sQ39_spl <=> (in(sK4_skl,sK6_skl))),
% 0.84/0.88 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.84/0.88 fof(f571,plain,(
% 0.84/0.88 ~sQ39_spl|~sQ29_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f566,f568,f502])).
% 0.84/0.89 fof(f572,plain,(
% 0.84/0.89 ~in(sK7_skl(empty_set,sK6_skl),empty_set)|sK6_skl=empty_set|~sQ34_spl|~sQ10_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f546,f49])).
% 0.84/0.89 fof(f574,definition,(
% 0.84/0.89 sQ40_spl <=> (in(sK7_skl(empty_set,sK6_skl),empty_set))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f577,plain,(
% 0.84/0.89 ~sQ40_spl|sQ8_spl|~sQ34_spl|~sQ10_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f572,f574,f209,f524,f215])).
% 0.84/0.89 fof(f605,plain,(
% 0.84/0.89 ![X0,X1]: (~in(X0,sK3_skl)|~in(X1,sK4_skl)|in(X0,sK5_skl))),
% 0.84/0.89 inference(resolution,[status(thm)],[f474,f27])).
% 0.84/0.89 fof(f608,definition,(
% 0.84/0.89 ![X0]: (sQ43_spl <=> (~in(X0,sK3_skl)|in(X0,sK5_skl)))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f609,plain,(
% 0.84/0.89 ![X0]: (~in(X0,sK3_skl)|in(X0,sK5_skl)|~sQ43_spl)),
% 0.84/0.89 inference(component_clause,[status(thm)],[f608])).
% 0.84/0.89 fof(f611,plain,(
% 0.84/0.89 sQ43_spl|sQ33_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f605,f608,f520])).
% 0.84/0.89 fof(f613,plain,(
% 0.84/0.89 $false|~sQ33_spl|~sQ10_spl),
% 0.84/0.89 inference(backward_subsumption_resolution,[status(thm)],[f216,f521])).
% 0.84/0.89 fof(f618,plain,(
% 0.84/0.89 ~sQ33_spl|~sQ10_spl),
% 0.84/0.89 inference(contradiction_clause,[status(thm)],[f613])).
% 0.84/0.89 fof(f619,plain,(
% 0.84/0.89 in(sK7_skl(sK3_skl,empty_set),sK5_skl)|empty_set=sK3_skl|~sQ43_spl|~sQ25_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f609,f407])).
% 0.84/0.89 fof(f628,definition,(
% 0.84/0.89 sQ44_spl <=> (in(sK7_skl(sK3_skl,empty_set),sK5_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f631,plain,(
% 0.84/0.89 sQ44_spl|sQ5_spl|~sQ43_spl|~sQ25_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f619,f628,f79,f608,f406])).
% 0.84/0.89 fof(f640,definition,(
% 0.84/0.89 sQ47_spl <=> (in(sK0_skl(sK3_skl),sK5_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f682,plain,(
% 0.84/0.89 sK4_skl=empty_set|in(sK7_skl(empty_set,sK4_skl),sK6_skl)|~sQ12_spl|~sQ34_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f224,f525])).
% 0.84/0.89 fof(f683,plain,(
% 0.84/0.89 sK3_skl=empty_set|in(sK7_skl(empty_set,sK3_skl),sK5_skl)|~sQ12_spl|~sQ43_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f224,f609])).
% 0.84/0.89 fof(f687,definition,(
% 0.84/0.89 sQ48_spl <=> (in(sK7_skl(empty_set,sK4_skl),sK6_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f690,plain,(
% 0.84/0.89 sQ6_spl|sQ48_spl|~sQ12_spl|~sQ34_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f682,f82,f687,f223,f524])).
% 0.84/0.89 fof(f691,definition,(
% 0.84/0.89 sQ49_spl <=> (in(sK7_skl(empty_set,sK3_skl),sK5_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f692,plain,(
% 0.84/0.89 in(sK7_skl(empty_set,sK3_skl),sK5_skl)|~sQ49_spl),
% 0.84/0.89 inference(component_clause,[status(thm)],[f691])).
% 0.84/0.89 fof(f694,plain,(
% 0.84/0.89 sQ5_spl|sQ49_spl|~sQ12_spl|~sQ43_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f683,f79,f691,f223,f608])).
% 0.84/0.89 fof(f707,plain,(
% 0.84/0.89 ![X0,X1]: (~in(X0,X1)|in(sK0_skl(sK3_skl),sK5_skl)|~sQ15_spl)),
% 0.84/0.89 inference(resolution,[status(thm)],[f343,f28])).
% 0.84/0.89 fof(f710,plain,(
% 0.84/0.89 sQ17_spl|sQ47_spl|~sQ15_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f707,f324,f640,f235])).
% 0.84/0.89 fof(f767,plain,(
% 0.84/0.89 ![X0]: (~in(X0,sK5_skl)|sK6_skl=empty_set|in(sK0_skl(sK6_skl),sK4_skl))),
% 0.84/0.89 inference(resolution,[status(thm)],[f154,f135])).
% 0.84/0.89 fof(f770,plain,(
% 0.84/0.89 ![X0,X1,X2]: (~in(X0,X1)|X2=empty_set|in(sK0_skl(X2),X2))),
% 0.84/0.89 inference(resolution,[status(thm)],[f154,f28])).
% 0.84/0.89 fof(f774,plain,(
% 0.84/0.89 ![X0]: (in(ordered_pair(X0,sK0_skl(sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)|sK4_skl=empty_set)),
% 0.84/0.89 inference(paramodulation,[status(thm)],[f41,f154])).
% 0.84/0.89 fof(f777,definition,(
% 0.84/0.89 sQ50_spl <=> (in(sK0_skl(sK6_skl),sK4_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f780,plain,(
% 0.84/0.89 sQ20_spl|sQ8_spl|sQ50_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f767,f373,f209,f777])).
% 0.84/0.89 fof(f783,plain,(
% 0.84/0.89 sQ17_spl|sQ13_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f770,f324,f227])).
% 0.84/0.89 fof(f784,definition,(
% 0.84/0.89 ![X0]: (sQ51_spl <=> (in(ordered_pair(X0,sK0_skl(sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK3_skl)))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f787,plain,(
% 0.84/0.89 sQ51_spl|sQ6_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f774,f784,f82])).
% 0.84/0.89 fof(f800,plain,(
% 0.84/0.89 ![X0,X1]: (~in(X0,X1)|in(sK0_skl(sK3_skl),sK3_skl)|~sQ15_spl)),
% 0.84/0.89 inference(resolution,[status(thm)],[f339,f28])).
% 0.84/0.89 fof(f805,definition,(
% 0.84/0.89 sQ53_spl <=> (in(sK0_skl(sK3_skl),sK3_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f808,plain,(
% 0.84/0.89 sQ17_spl|sQ53_spl|~sQ15_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f800,f324,f805,f235])).
% 0.84/0.89 fof(f811,plain,(
% 0.84/0.89 ![X0]: (~in(X0,sK5_skl)|in(sK7_skl(empty_set,sK4_skl),sK4_skl)|~sQ15_spl)),
% 0.84/0.89 inference(resolution,[status(thm)],[f356,f135])).
% 0.84/0.89 fof(f819,definition,(
% 0.84/0.89 sQ54_spl <=> (in(sK7_skl(empty_set,sK4_skl),sK4_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f822,plain,(
% 0.84/0.89 sQ20_spl|sQ54_spl|~sQ15_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f811,f373,f819,f235])).
% 0.84/0.89 fof(f841,plain,(
% 0.84/0.89 ~in(sK7_skl(empty_set,sK3_skl),empty_set)|sK3_skl=empty_set|~sQ19_spl|~sQ49_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f472,f692])).
% 0.84/0.89 fof(f842,plain,(
% 0.84/0.89 ~in(sK7_skl(sK5_skl,sK3_skl),sK5_skl)|sK3_skl=sK5_skl|in(sK7_skl(sK5_skl,sK3_skl),sK3_skl)|sK3_skl=sK5_skl|~sQ19_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f472,f48])).
% 0.84/0.89 fof(f847,definition,(
% 0.84/0.89 sQ56_spl <=> (in(sK7_skl(empty_set,sK3_skl),empty_set))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f850,plain,(
% 0.84/0.89 ~sQ56_spl|sQ5_spl|~sQ19_spl|~sQ49_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f841,f847,f79,f369,f691])).
% 0.84/0.89 fof(f851,definition,(
% 0.84/0.89 sQ57_spl <=> (in(sK7_skl(sK5_skl,sK3_skl),sK5_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f853,plain,(
% 0.84/0.89 ~in(sK7_skl(sK5_skl,sK3_skl),sK5_skl)|sQ57_spl),
% 0.84/0.89 inference(component_clause,[status(thm)],[f851])).
% 0.84/0.89 fof(f854,definition,(
% 0.84/0.89 sQ58_spl <=> (in(sK7_skl(sK5_skl,sK3_skl),sK3_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f855,plain,(
% 0.84/0.89 in(sK7_skl(sK5_skl,sK3_skl),sK3_skl)|~sQ58_spl),
% 0.84/0.89 inference(component_clause,[status(thm)],[f854])).
% 0.84/0.89 fof(f857,plain,(
% 0.84/0.89 ~sQ57_spl|sQ0_spl|sQ58_spl|~sQ19_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f842,f851,f50,f854,f369])).
% 0.84/0.89 fof(f874,plain,(
% 0.84/0.89 ~in(sK7_skl(sK5_skl,sK3_skl),sK5_skl)|sK3_skl=sK5_skl|~sQ58_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f855,f49])).
% 0.84/0.89 fof(f875,plain,(
% 0.84/0.89 in(sK7_skl(sK5_skl,sK3_skl),sK5_skl)|~sQ58_spl|~sQ43_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f855,f609])).
% 0.84/0.89 fof(f879,plain,(
% 0.84/0.89 ~sQ57_spl|sQ0_spl|~sQ58_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f874,f851,f50,f854])).
% 0.84/0.89 fof(f880,plain,(
% 0.84/0.89 in(sK7_skl(sK5_skl,sK3_skl),sK3_skl)|sK3_skl=sK5_skl|sQ57_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f853,f48])).
% 0.84/0.89 fof(f881,plain,(
% 0.84/0.89 sQ58_spl|sQ0_spl|sQ57_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f880,f854,f50,f851])).
% 0.84/0.89 fof(f882,plain,(
% 0.84/0.89 $false|sQ57_spl|~sQ58_spl|~sQ43_spl),
% 0.84/0.89 inference(forward_subsumption_resolution,[status(thm)],[f875,f853])).
% 0.84/0.89 fof(f883,plain,(
% 0.84/0.89 sQ57_spl|~sQ58_spl|~sQ43_spl),
% 0.84/0.89 inference(contradiction_clause,[status(thm)],[f882])).
% 0.84/0.89 fof(f888,plain,(
% 0.84/0.89 ![X0,X1]: (in(ordered_pair(X0,sK0_skl(sK3_skl)),cartesian_product2(X1,sK5_skl))|~in(X0,X1)|~sQ0_spl|~sQ15_spl)),
% 0.84/0.89 inference(backward_demodulation,[status(thm)],[f51,f339])).
% 0.84/0.89 fof(f894,plain,(
% 0.84/0.89 in(sK7_skl(empty_set,sK5_skl),sK5_skl)|~sQ0_spl|~sQ49_spl),
% 0.84/0.89 inference(backward_demodulation,[status(thm)],[f51,f692])).
% 0.84/0.89 fof(f897,plain,(
% 0.84/0.89 ![X0,X1]: (in(ordered_pair(X0,X1),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK5_skl)|~in(X1,sK4_skl)|~sQ0_spl)),
% 0.84/0.89 inference(backward_demodulation,[status(thm)],[f51,f474])).
% 0.84/0.89 fof(f910,plain,(
% 0.84/0.89 cartesian_product2(sK5_skl,sK4_skl)=cartesian_product2(sK5_skl,sK6_skl)|~sQ0_spl),
% 0.84/0.89 inference(backward_demodulation,[status(thm)],[f51,f41])).
% 0.84/0.89 fof(f947,plain,(
% 0.84/0.89 ![X0,X1]: (in(ordered_pair(X0,sK0_skl(sK5_skl)),cartesian_product2(X1,sK5_skl))|~in(X0,X1)|~sQ0_spl|~sQ15_spl)),
% 0.84/0.89 inference(forward_demodulation,[status(thm)],[f51,f888])).
% 0.84/0.89 fof(f971,plain,(
% 0.84/0.89 ~in(sK7_skl(empty_set,sK5_skl),empty_set)|sK5_skl=empty_set|~sQ0_spl|~sQ49_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f894,f49])).
% 0.84/0.89 fof(f975,definition,(
% 0.84/0.89 sQ61_spl <=> (in(sK7_skl(empty_set,sK5_skl),empty_set))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f978,plain,(
% 0.84/0.89 ~sQ61_spl|sQ9_spl|~sQ0_spl|~sQ49_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f971,f975,f212,f50,f691])).
% 0.84/0.89 fof(f984,plain,(
% 0.84/0.89 ![X0]: (in(ordered_pair(X0,sK7_skl(sK4_skl,empty_set)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK5_skl)|empty_set=sK4_skl|~sQ0_spl)),
% 0.84/0.89 inference(paramodulation,[status(thm)],[f910,f149])).
% 0.84/0.89 fof(f985,plain,(
% 0.84/0.89 ![X0]: (in(ordered_pair(X0,sK0_skl(sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK5_skl)|sK4_skl=empty_set|~sQ0_spl)),
% 0.84/0.89 inference(paramodulation,[status(thm)],[f910,f154])).
% 0.84/0.89 fof(f990,definition,(
% 0.84/0.89 ![X0]: (sQ62_spl <=> (in(ordered_pair(X0,sK7_skl(sK4_skl,empty_set)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK5_skl)))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f993,plain,(
% 0.84/0.89 sQ62_spl|sQ6_spl|~sQ0_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f984,f990,f82,f50])).
% 0.84/0.89 fof(f994,definition,(
% 0.84/0.89 ![X0]: (sQ63_spl <=> (in(ordered_pair(X0,sK0_skl(sK4_skl)),cartesian_product2(sK5_skl,sK6_skl))|~in(X0,sK5_skl)))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f997,plain,(
% 0.84/0.89 sQ63_spl|sQ6_spl|~sQ0_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f985,f994,f82,f50])).
% 0.84/0.89 fof(f1006,plain,(
% 0.84/0.89 ![X0,X1]: (~in(X0,sK5_skl)|~in(X1,sK4_skl)|in(X0,sK5_skl)|~sQ0_spl)),
% 0.84/0.89 inference(resolution,[status(thm)],[f897,f27])).
% 0.84/0.89 fof(f1012,definition,(
% 0.84/0.89 ![X0]: (sQ64_spl <=> (~in(X0,sK5_skl)|in(X0,sK5_skl)))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f1015,plain,(
% 0.84/0.89 sQ64_spl|sQ33_spl|~sQ0_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f1006,f1012,f520,f50])).
% 0.84/0.89 fof(f1025,plain,(
% 0.84/0.89 ![X0,X1]: (~in(X0,X1)|in(sK0_skl(sK5_skl),sK5_skl)|~sQ0_spl|~sQ15_spl)),
% 0.84/0.89 inference(resolution,[status(thm)],[f947,f28])).
% 0.84/0.89 fof(f1030,definition,(
% 0.84/0.89 sQ65_spl <=> (in(sK0_skl(sK5_skl),sK5_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f1033,plain,(
% 0.84/0.89 sQ17_spl|sQ65_spl|~sQ0_spl|~sQ15_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f1025,f324,f1030,f50,f235])).
% 0.84/0.89 fof(f1035,plain,(
% 0.84/0.89 ~in(sK7_skl(sK6_skl,sK4_skl),sK6_skl)|sK4_skl=sK6_skl|in(sK7_skl(sK6_skl,sK4_skl),sK4_skl)|sK4_skl=sK6_skl|~sQ29_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f536,f48])).
% 0.84/0.89 fof(f1037,definition,(
% 0.84/0.89 sQ66_spl <=> (in(sK7_skl(sK6_skl,sK4_skl),sK6_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f1039,plain,(
% 0.84/0.89 ~in(sK7_skl(sK6_skl,sK4_skl),sK6_skl)|sQ66_spl),
% 0.84/0.89 inference(component_clause,[status(thm)],[f1037])).
% 0.84/0.89 fof(f1040,definition,(
% 0.84/0.89 sQ67_spl <=> (in(sK7_skl(sK6_skl,sK4_skl),sK4_skl))),
% 0.84/0.89 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.84/0.89 fof(f1041,plain,(
% 0.84/0.89 in(sK7_skl(sK6_skl,sK4_skl),sK4_skl)|~sQ67_spl),
% 0.84/0.89 inference(component_clause,[status(thm)],[f1040])).
% 0.84/0.89 fof(f1043,plain,(
% 0.84/0.89 ~sQ66_spl|sQ1_spl|sQ67_spl|~sQ29_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f1035,f1037,f53,f1040,f502])).
% 0.84/0.89 fof(f1044,plain,(
% 0.84/0.89 in(sK7_skl(sK6_skl,sK4_skl),sK4_skl)|sK4_skl=sK6_skl|sQ66_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f1039,f48])).
% 0.84/0.89 fof(f1045,plain,(
% 0.84/0.89 sQ67_spl|sQ1_spl|sQ66_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f1044,f1040,f53,f1037])).
% 0.84/0.89 fof(f1046,plain,(
% 0.84/0.89 ~in(sK7_skl(sK6_skl,sK4_skl),sK6_skl)|sK4_skl=sK6_skl|~sQ67_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f1041,f49])).
% 0.84/0.89 fof(f1047,plain,(
% 0.84/0.89 in(sK7_skl(sK6_skl,sK4_skl),sK6_skl)|~sQ67_spl|~sQ34_spl),
% 0.84/0.89 inference(resolution,[status(thm)],[f1041,f525])).
% 0.84/0.89 fof(f1051,plain,(
% 0.84/0.89 ~sQ66_spl|sQ1_spl|~sQ67_spl),
% 0.84/0.89 inference(split_clause,[status(thm)],[f1046,f1037,f53,f1040])).
% 0.84/0.89 fof(f1052,plain,(
% 0.84/0.89 $false|~sQ67_spl|~sQ34_spl|sQ66_spl),
% 0.84/0.89 inference(forward_subsumption_resolution,[status(thm)],[f1039,f1047])).
% 0.84/0.89 fof(f1053,plain,(
% 0.84/0.89 ~sQ67_spl|~sQ34_spl|sQ66_spl),
% 0.84/0.89 inference(contradiction_clause,[status(thm)],[f1052])).
% 0.84/0.89 fof(f1054,plain,(
% 0.84/0.89 $false),
% 0.84/0.89 inference(sat_refutation,[status(thm)],[f56,f73,f85,f88,f218,f222,f238,f245,f251,f258,f263,f353,f372,f377,f385,f405,f409,f414,f463,f464,f481,f496,f505,f516,f523,f527,f533,f555,f559,f571,f577,f611,f618,f631,f690,f694,f710,f780,f783,f787,f808,f822,f850,f857,f879,f881,f883,f978,f993,f997,f1015,f1033,f1043,f1045,f1051,f1053])).
% 0.84/0.89 % SZS output end CNFRefutation for theBenchmark.p
% 1.98/0.90 % Elapsed time: 0.459980 seconds
% 1.98/0.90 % CPU time: 3.228745 seconds
% 1.98/0.90 % Total memory used: 131.728 MB
% 1.98/0.90 % Net memory used: 126.232 MB
%------------------------------------------------------------------------------