%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:22:25 PM UTC 2026
% Result : Theorem 0.15s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU359+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:15:25 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.15/0.45 % Refutation found
% 0.15/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.45 fof(f1,axiom,(
% 0.15/0.45 (! [A] :( rel_str(A)=> (! [B,C] :( element(C,the_carrier(A))=> ( ex_sup_of_relstr_set(A,B)=> ( C = join_on_relstr(A,B)<=> ( relstr_set_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,B,D)=> related(A,C,D) ) ) )) ) ) ) )) )),
% 0.15/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f2,axiom,(
% 0.15/0.45 (! [A,B] :( rel_str(A)=> element(join_on_relstr(A,B),the_carrier(A)) ) )),
% 0.15/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f10,axiom,(
% 0.15/0.45 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( ex_sup_of_relstr_set(A,B)<=> (? [C] :( element(C,the_carrier(A))& relstr_set_smaller(A,B,C)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,B,D)=> related(A,C,D) ) ) )) )) )) )),
% 0.15/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f11,conjecture,(
% 0.15/0.45 (! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( ( ( B = join_on_relstr(A,C)& ex_sup_of_relstr_set(A,C) )=> ( relstr_set_smaller(A,C,B)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,C,D)=> related(A,B,D) ) ) )) )& ( ( relstr_set_smaller(A,C,B)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,C,D)=> related(A,B,D) ) ) ))=> ( B = join_on_relstr(A,C)& ex_sup_of_relstr_set(A,C) ) ) ) )) )) )),
% 0.15/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.45 fof(f12,negated_conjecture,(
% 0.15/0.45 ~((! [A] :( ( antisymmetric_relstr(A)& rel_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( ( ( B = join_on_relstr(A,C)& ex_sup_of_relstr_set(A,C) )=> ( relstr_set_smaller(A,C,B)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,C,D)=> related(A,B,D) ) ) )) )& ( ( relstr_set_smaller(A,C,B)& (! [D] :( element(D,the_carrier(A))=> ( relstr_set_smaller(A,C,D)=> related(A,B,D) ) ) ))=> ( B = join_on_relstr(A,C)& ex_sup_of_relstr_set(A,C) ) ) ) )) )) ))),
% 0.15/0.45 inference(negated_conjecture,[status(cth)],[f11])).
% 0.15/0.45 fof(f13,plain,(
% 0.15/0.45 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|(~ex_sup_of_relstr_set(A,B)|(C=join_on_relstr(A,B)<=>(relstr_set_smaller(A,B,C)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))))))),
% 0.15/0.45 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.15/0.45 fof(f14,plain,(
% 0.15/0.45 ![A]: (~rel_str(A)|(![B,C]: (~element(C,the_carrier(A))|(~ex_sup_of_relstr_set(A,B)|((~C=join_on_relstr(A,B)|(relstr_set_smaller(A,B,C)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))&(C=join_on_relstr(A,B)|(~relstr_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D)))))))))))),
% 0.15/0.45 inference(NNF_transformation,[status(thm)],[f13])).
% 0.15/0.45 fof(f15,plain,(
% 0.15/0.45 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|(![B]: (~ex_sup_of_relstr_set(A,B)|((~C=join_on_relstr(A,B)|(relstr_set_smaller(A,B,C)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))&(C=join_on_relstr(A,B)|(~relstr_set_smaller(A,B,C)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D))))))))))))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f14])).
% 0.15/0.45 fof(f16,plain,(
% 0.15/0.45 ![A]: (~rel_str(A)|(![C]: (~element(C,the_carrier(A))|(![B]: (~ex_sup_of_relstr_set(A,B)|((~C=join_on_relstr(A,B)|(relstr_set_smaller(A,B,C)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))&(C=join_on_relstr(A,B)|(~relstr_set_smaller(A,B,C)|(element(sK0_skl(B,C,A),the_carrier(A))&(relstr_set_smaller(A,B,sK0_skl(B,C,A))&~related(A,C,sK0_skl(B,C,A))))))))))))),
% 0.15/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(D,sK0_skl(B,C,A))],[f15])).
% 0.15/0.45 fof(f17,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~ex_sup_of_relstr_set(X0,X2)|~X1=join_on_relstr(X0,X2)|relstr_set_smaller(X0,X2,X1))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f18,plain,(
% 0.15/0.45 ![X0,X1,X2,X3]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~ex_sup_of_relstr_set(X0,X2)|~X1=join_on_relstr(X0,X2)|~element(X3,the_carrier(X0))|~relstr_set_smaller(X0,X2,X3)|related(X0,X1,X3))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f19,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~ex_sup_of_relstr_set(X0,X2)|X1=join_on_relstr(X0,X2)|~relstr_set_smaller(X0,X2,X1)|element(sK0_skl(X2,X1,X0),the_carrier(X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f20,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~ex_sup_of_relstr_set(X0,X2)|X1=join_on_relstr(X0,X2)|~relstr_set_smaller(X0,X2,X1)|relstr_set_smaller(X0,X2,sK0_skl(X2,X1,X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f21,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~element(X1,the_carrier(X0))|~ex_sup_of_relstr_set(X0,X2)|X1=join_on_relstr(X0,X2)|~relstr_set_smaller(X0,X2,X1)|~related(X0,X1,sK0_skl(X2,X1,X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.45 fof(f22,plain,(
% 0.15/0.45 ![A,B]: (~rel_str(A)|element(join_on_relstr(A,B),the_carrier(A)))),
% 0.15/0.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/0.45 fof(f23,plain,(
% 0.15/0.45 ![A]: (~rel_str(A)|(![B]: element(join_on_relstr(A,B),the_carrier(A))))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f22])).
% 0.15/0.45 fof(f24,plain,(
% 0.15/0.45 ![X0,X1]: (~rel_str(X0)|element(join_on_relstr(X0,X1),the_carrier(X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f23])).
% 0.15/0.45 fof(f33,plain,(
% 0.15/0.45 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|(![B]: (ex_sup_of_relstr_set(A,B)<=>(?[C]: ((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))))))),
% 0.15/0.45 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.15/0.45 fof(f34,plain,(
% 0.15/0.45 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|(![B]: ((~ex_sup_of_relstr_set(A,B)|(?[C]: ((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D)))))))&(ex_sup_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D))))))))))),
% 0.15/0.45 inference(NNF_transformation,[status(thm)],[f33])).
% 0.15/0.45 fof(f35,plain,(
% 0.15/0.45 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|((![B]: (~ex_sup_of_relstr_set(A,B)|(?[C]: ((element(C,the_carrier(A))&relstr_set_smaller(A,B,C))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,C,D))))))))&(![B]: (ex_sup_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,B,D)&~related(A,C,D))))))))))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f34])).
% 0.15/0.45 fof(f36,plain,(
% 0.15/0.45 ![A]: ((~antisymmetric_relstr(A)|~rel_str(A))|((![B]: (~ex_sup_of_relstr_set(A,B)|((element(sK4_skl(B,A),the_carrier(A))&relstr_set_smaller(A,B,sK4_skl(B,A)))&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,B,D)|related(A,sK4_skl(B,A),D)))))))&(![B]: (ex_sup_of_relstr_set(A,B)|(![C]: ((~element(C,the_carrier(A))|~relstr_set_smaller(A,B,C))|(element(sK5_skl(C,B,A),the_carrier(A))&(relstr_set_smaller(A,B,sK5_skl(C,B,A))&~related(A,C,sK5_skl(C,B,A))))))))))),
% 0.15/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(C,sK4_skl(B,A)),skolemize(D,sK5_skl(C,B,A))],[f35])).
% 0.15/0.45 fof(f40,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|element(sK5_skl(X2,X1,X0),the_carrier(X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.45 fof(f41,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|relstr_set_smaller(X0,X1,sK5_skl(X2,X1,X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.45 fof(f42,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~antisymmetric_relstr(X0)|~rel_str(X0)|ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|~related(X0,X2,sK5_skl(X2,X1,X0)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.45 fof(f43,plain,(
% 0.15/0.45 (?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (((B=join_on_relstr(A,C)&ex_sup_of_relstr_set(A,C))&(~relstr_set_smaller(A,C,B)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,C,D)&~related(A,B,D))))))|((relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D)))))&(~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C)))))))))),
% 0.15/0.45 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.15/0.45 fof(f44,definition,(
% 0.15/0.45 ![A,B,C]: (sP0_prd(C,B,A)<=>((B=join_on_relstr(A,C)&ex_sup_of_relstr_set(A,C))&(~relstr_set_smaller(A,C,B)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,C,D)&~related(A,B,D)))))))),
% 0.15/0.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.15/0.45 fof(f45,plain,(
% 0.15/0.45 ?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (element(B,the_carrier(A))&(?[C]: (sP0_prd(C,B,A)|((relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D)))))&(~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C))))))))),
% 0.15/0.45 inference(formula_renaming,[status(thm)],[f43,f44])).
% 0.15/0.45 fof(f46,plain,(
% 0.15/0.45 ?[A]: ((antisymmetric_relstr(A)&rel_str(A))&(?[B]: (element(B,the_carrier(A))&((?[C]: sP0_prd(C,B,A))|(?[C]: ((relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D)))))&(~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C))))))))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f45])).
% 0.15/0.45 fof(f47,plain,(
% 0.15/0.45 ((antisymmetric_relstr(sK6_skl)&rel_str(sK6_skl))&(element(sK7_skl,the_carrier(sK6_skl))&(sP0_prd(sK8_skl,sK7_skl,sK6_skl)|((relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)&(![D]: (~element(D,the_carrier(sK6_skl))|(~relstr_set_smaller(sK6_skl,sK9_skl,D)|related(sK6_skl,sK7_skl,D)))))&(~sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~ex_sup_of_relstr_set(sK6_skl,sK9_skl))))))),
% 0.15/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(A,sK6_skl),skolemize(B,sK7_skl),skolemize(C,sK8_skl),skolemize(C,sK9_skl)],[f46])).
% 0.15/0.45 fof(f48,plain,(
% 0.15/0.45 antisymmetric_relstr(sK6_skl)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f49,plain,(
% 0.15/0.45 rel_str(sK6_skl)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f50,plain,(
% 0.15/0.45 element(sK7_skl,the_carrier(sK6_skl))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f51,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f52,plain,(
% 0.15/0.45 ![X0]: (sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(X0,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,X0)|related(sK6_skl,sK7_skl,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f53,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~ex_sup_of_relstr_set(sK6_skl,sK9_skl)),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/0.45 fof(f54,plain,(
% 0.15/0.45 ![A,B,C]: ((~sP0_prd(C,B,A)|((B=join_on_relstr(A,C)&ex_sup_of_relstr_set(A,C))&(~relstr_set_smaller(A,C,B)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,C,D)&~related(A,B,D)))))))&(sP0_prd(C,B,A)|((~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C))|(relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D))))))))),
% 0.15/0.45 inference(NNF_transformation,[status(thm)],[f44])).
% 0.15/0.45 fof(f55,plain,(
% 0.15/0.45 (![A,B,C]: (~sP0_prd(C,B,A)|((B=join_on_relstr(A,C)&ex_sup_of_relstr_set(A,C))&(~relstr_set_smaller(A,C,B)|(?[D]: (element(D,the_carrier(A))&(relstr_set_smaller(A,C,D)&~related(A,B,D))))))))&(![A,B,C]: (sP0_prd(C,B,A)|((~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C))|(relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D))))))))),
% 0.15/0.45 inference(miniscoping,[status(thm)],[f54])).
% 0.15/0.45 fof(f56,plain,(
% 0.15/0.45 (![A,B,C]: (~sP0_prd(C,B,A)|((B=join_on_relstr(A,C)&ex_sup_of_relstr_set(A,C))&(~relstr_set_smaller(A,C,B)|(element(sK10_skl(C,B,A),the_carrier(A))&(relstr_set_smaller(A,C,sK10_skl(C,B,A))&~related(A,B,sK10_skl(C,B,A))))))))&(![A,B,C]: (sP0_prd(C,B,A)|((~B=join_on_relstr(A,C)|~ex_sup_of_relstr_set(A,C))|(relstr_set_smaller(A,C,B)&(![D]: (~element(D,the_carrier(A))|(~relstr_set_smaller(A,C,D)|related(A,B,D))))))))),
% 0.15/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(D,sK10_skl(C,B,A))],[f55])).
% 0.15/0.45 fof(f57,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|X1=join_on_relstr(X2,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/0.45 fof(f58,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|ex_sup_of_relstr_set(X2,X0))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/0.45 fof(f59,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~relstr_set_smaller(X2,X0,X1)|element(sK10_skl(X0,X1,X2),the_carrier(X2)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/0.45 fof(f60,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~relstr_set_smaller(X2,X0,X1)|relstr_set_smaller(X2,X0,sK10_skl(X0,X1,X2)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/0.45 fof(f61,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~relstr_set_smaller(X2,X0,X1)|~related(X2,X1,sK10_skl(X0,X1,X2)))),
% 0.15/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.15/0.45 fof(f64,plain,(
% 0.15/0.45 ![X0,X1]: (~rel_str(X0)|~element(join_on_relstr(X0,X1),the_carrier(X0))|~ex_sup_of_relstr_set(X0,X1)|relstr_set_smaller(X0,X1,join_on_relstr(X0,X1)))),
% 0.15/0.45 inference(destructive_equality_resolution,[status(thm)],[f17])).
% 0.15/0.45 fof(f65,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~element(join_on_relstr(X0,X1),the_carrier(X0))|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|related(X0,join_on_relstr(X0,X1),X2))),
% 0.15/0.45 inference(destructive_equality_resolution,[status(thm)],[f18])).
% 0.15/0.45 fof(f68,plain,(
% 0.15/0.45 ![X0,X1,X2]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|~element(X2,the_carrier(X0))|~relstr_set_smaller(X0,X1,X2)|related(X0,join_on_relstr(X0,X1),X2))),
% 0.15/0.45 inference(backward_subsumption_resolution,[status(thm)],[f65,f24])).
% 0.15/0.45 fof(f69,plain,(
% 0.15/0.45 ![X0,X1]: (~rel_str(X0)|~ex_sup_of_relstr_set(X0,X1)|relstr_set_smaller(X0,X1,join_on_relstr(X0,X1)))),
% 0.15/0.45 inference(backward_subsumption_resolution,[status(thm)],[f64,f24])).
% 0.15/0.45 fof(f76,plain,(
% 0.15/0.45 ![X0]: (~rel_str(sK6_skl)|~ex_sup_of_relstr_set(sK6_skl,X0)|sK7_skl=join_on_relstr(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|relstr_set_smaller(sK6_skl,X0,sK0_skl(X0,sK7_skl,sK6_skl)))),
% 0.15/0.45 inference(resolution,[status(thm)],[f20,f50])).
% 0.15/0.45 fof(f77,plain,(
% 0.15/0.45 ![X0]: (~ex_sup_of_relstr_set(sK6_skl,X0)|sK7_skl=join_on_relstr(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|relstr_set_smaller(sK6_skl,X0,sK0_skl(X0,sK7_skl,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f76,f49])).
% 0.15/0.45 fof(f83,plain,(
% 0.15/0.45 ![X0]: (sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK0_skl(X0,sK7_skl,sK6_skl),the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(X0,sK7_skl,sK6_skl))|~rel_str(sK6_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~ex_sup_of_relstr_set(sK6_skl,X0)|sK7_skl=join_on_relstr(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl))),
% 0.15/0.45 inference(resolution,[status(thm)],[f52,f21])).
% 0.15/0.45 fof(f87,plain,(
% 0.15/0.45 ![X0]: (sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(X0,sK7_skl,sK6_skl))|~rel_str(sK6_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~ex_sup_of_relstr_set(sK6_skl,X0)|sK7_skl=join_on_relstr(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f83,f19])).
% 0.15/0.45 fof(f111,plain,(
% 0.15/0.45 ![X0]: (~antisymmetric_relstr(sK6_skl)|~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl)))),
% 0.15/0.45 inference(resolution,[status(thm)],[f40,f50])).
% 0.15/0.45 fof(f114,plain,(
% 0.15/0.45 ![X0]: (~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f111,f48])).
% 0.15/0.45 fof(f118,plain,(
% 0.15/0.45 ![X0]: (~antisymmetric_relstr(sK6_skl)|~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|relstr_set_smaller(sK6_skl,X0,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(resolution,[status(thm)],[f41,f50])).
% 0.15/0.45 fof(f121,plain,(
% 0.15/0.45 ![X0]: (~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|relstr_set_smaller(sK6_skl,X0,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f118,f48])).
% 0.15/0.45 fof(f122,plain,(
% 0.15/0.45 ![X0]: (~antisymmetric_relstr(sK6_skl)|~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~element(sK7_skl,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(resolution,[status(thm)],[f42,f52])).
% 0.15/0.45 fof(f123,plain,(
% 0.15/0.45 ![X0]: (~rel_str(sK6_skl)|ex_sup_of_relstr_set(sK6_skl,X0)|~element(sK7_skl,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f122,f48])).
% 0.15/0.45 fof(f137,plain,(
% 0.15/0.45 ~ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(sK9_skl,sK7_skl,sK6_skl))|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f77,f51])).
% 0.15/0.45 fof(f138,plain,(
% 0.15/0.45 ~ex_sup_of_relstr_set(sK6_skl,sK9_skl)|relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(sK9_skl,sK7_skl,sK6_skl))|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f137,f53])).
% 0.15/0.45 fof(f140,plain,(
% 0.15/0.45 ![X0]: (sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(X0,sK7_skl,sK6_skl))|~element(sK7_skl,the_carrier(sK6_skl))|~ex_sup_of_relstr_set(sK6_skl,X0)|sK7_skl=join_on_relstr(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f87,f49])).
% 0.15/0.45 fof(f143,plain,(
% 0.15/0.45 ![X0]: (ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|relstr_set_smaller(sK6_skl,X0,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f121,f49])).
% 0.15/0.45 fof(f144,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,sK9_skl,sK6_skl))|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f143,f51])).
% 0.15/0.45 fof(f145,plain,(
% 0.15/0.45 ![X0]: (ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f114,f49])).
% 0.15/0.45 fof(f146,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|element(sK5_skl(sK7_skl,sK9_skl,sK6_skl),the_carrier(sK6_skl))|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f145,f51])).
% 0.15/0.45 fof(f147,plain,(
% 0.15/0.45 ![X0]: (ex_sup_of_relstr_set(sK6_skl,X0)|~element(sK7_skl,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,X0,sK7_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK5_skl(sK7_skl,X0,sK6_skl),the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,X0,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f123,f49])).
% 0.15/0.45 fof(f152,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|ex_sup_of_relstr_set(sK6_skl,sK9_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,sK9_skl,sK6_skl))),
% 0.15/0.45 inference(resolution,[status(thm)],[f146,f147])).
% 0.15/0.45 fof(f161,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,sK9_skl,sK6_skl))),
% 0.15/0.45 inference(duplicate_literals_removal,[status(thm)],[f152])).
% 0.15/0.45 fof(f162,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,sK9_skl,sK6_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f161,f50])).
% 0.15/0.45 fof(f177,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(backward_subsumption_resolution,[status(thm)],[f144,f178])).
% 0.15/0.45 fof(f178,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK5_skl(sK7_skl,sK9_skl,sK6_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f162,f51])).
% 0.15/0.45 fof(f179,plain,(
% 0.15/0.45 relstr_set_smaller(sK6_skl,sK9_skl,sK0_skl(sK9_skl,sK7_skl,sK6_skl))|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(backward_subsumption_resolution,[status(thm)],[f138,f177])).
% 0.15/0.45 fof(f183,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~sK7_skl=join_on_relstr(sK6_skl,sK9_skl)),
% 0.15/0.45 inference(backward_subsumption_resolution,[status(thm)],[f53,f177])).
% 0.15/0.45 fof(f200,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f179,f140])).
% 0.15/0.45 fof(f204,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~element(sK7_skl,the_carrier(sK6_skl))|~ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)),
% 0.15/0.45 inference(duplicate_literals_removal,[status(thm)],[f200])).
% 0.15/0.45 fof(f205,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~ex_sup_of_relstr_set(sK6_skl,sK9_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f204,f50])).
% 0.15/0.45 fof(f272,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|~relstr_set_smaller(sK6_skl,sK9_skl,sK7_skl)),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f205,f177])).
% 0.15/0.45 fof(f273,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)|sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f272,f51])).
% 0.15/0.45 fof(f274,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)|sK7_skl=join_on_relstr(sK6_skl,sK9_skl)),
% 0.15/0.45 inference(duplicate_literals_removal,[status(thm)],[f273])).
% 0.15/0.45 fof(f275,plain,(
% 0.15/0.45 sP0_prd(sK8_skl,sK7_skl,sK6_skl)),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f274,f183])).
% 0.15/0.45 fof(f281,plain,(
% 0.15/0.45 sK7_skl=join_on_relstr(sK6_skl,sK8_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f275,f57])).
% 0.15/0.45 fof(f282,plain,(
% 0.15/0.45 ex_sup_of_relstr_set(sK6_skl,sK8_skl)),
% 0.15/0.45 inference(resolution,[status(thm)],[f275,f58])).
% 0.15/0.45 fof(f283,plain,(
% 0.15/0.45 ~rel_str(sK6_skl)|relstr_set_smaller(sK6_skl,sK8_skl,join_on_relstr(sK6_skl,sK8_skl))),
% 0.15/0.45 inference(resolution,[status(thm)],[f282,f69])).
% 0.15/0.45 fof(f287,plain,(
% 0.15/0.45 relstr_set_smaller(sK6_skl,sK8_skl,join_on_relstr(sK6_skl,sK8_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f283,f49])).
% 0.15/0.45 fof(f308,plain,(
% 0.15/0.45 relstr_set_smaller(sK6_skl,sK8_skl,sK7_skl)),
% 0.15/0.45 inference(forward_demodulation,[status(thm)],[f281,f287])).
% 0.15/0.45 fof(f315,plain,(
% 0.15/0.45 ~sP0_prd(sK8_skl,sK7_skl,sK6_skl)|relstr_set_smaller(sK6_skl,sK8_skl,sK10_skl(sK8_skl,sK7_skl,sK6_skl))),
% 0.15/0.45 inference(resolution,[status(thm)],[f308,f60])).
% 0.15/0.45 fof(f316,plain,(
% 0.15/0.45 ~sP0_prd(sK8_skl,sK7_skl,sK6_skl)|element(sK10_skl(sK8_skl,sK7_skl,sK6_skl),the_carrier(sK6_skl))),
% 0.15/0.45 inference(resolution,[status(thm)],[f308,f59])).
% 0.15/0.45 fof(f320,plain,(
% 0.15/0.45 relstr_set_smaller(sK6_skl,sK8_skl,sK10_skl(sK8_skl,sK7_skl,sK6_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f315,f275])).
% 0.15/0.45 fof(f321,plain,(
% 0.15/0.45 element(sK10_skl(sK8_skl,sK7_skl,sK6_skl),the_carrier(sK6_skl))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f316,f275])).
% 0.15/0.45 fof(f324,plain,(
% 0.15/0.45 ![X0]: (~rel_str(sK6_skl)|~ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK10_skl(sK8_skl,sK7_skl,sK6_skl))|related(sK6_skl,join_on_relstr(sK6_skl,X0),sK10_skl(sK8_skl,sK7_skl,sK6_skl)))),
% 0.15/0.45 inference(resolution,[status(thm)],[f321,f68])).
% 0.15/0.45 fof(f331,plain,(
% 0.15/0.45 ![X0]: (~ex_sup_of_relstr_set(sK6_skl,X0)|~relstr_set_smaller(sK6_skl,X0,sK10_skl(sK8_skl,sK7_skl,sK6_skl))|related(sK6_skl,join_on_relstr(sK6_skl,X0),sK10_skl(sK8_skl,sK7_skl,sK6_skl)))),
% 0.15/0.45 inference(forward_subsumption_resolution,[status(thm)],[f324,f49])).
% 0.15/0.45 fof(f387,plain,(
% 0.15/0.45 ~ex_sup_of_relstr_set(sK6_skl,sK8_skl)|related(sK6_skl,join_on_relstr(sK6_skl,sK8_skl),sK10_skl(sK8_skl,sK7_skl,sK6_skl))),
% 0.15/0.47 inference(resolution,[status(thm)],[f331,f320])).
% 0.15/0.47 fof(f388,plain,(
% 0.15/0.47 ~ex_sup_of_relstr_set(sK6_skl,sK8_skl)|related(sK6_skl,sK7_skl,sK10_skl(sK8_skl,sK7_skl,sK6_skl))),
% 0.15/0.47 inference(forward_demodulation,[status(thm)],[f281,f387])).
% 0.15/0.47 fof(f389,plain,(
% 0.15/0.47 related(sK6_skl,sK7_skl,sK10_skl(sK8_skl,sK7_skl,sK6_skl))),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f388,f282])).
% 0.15/0.47 fof(f394,plain,(
% 0.15/0.47 ~sP0_prd(sK8_skl,sK7_skl,sK6_skl)|~relstr_set_smaller(sK6_skl,sK8_skl,sK7_skl)),
% 0.15/0.47 inference(resolution,[status(thm)],[f389,f61])).
% 0.15/0.47 fof(f395,plain,(
% 0.15/0.47 ~relstr_set_smaller(sK6_skl,sK8_skl,sK7_skl)),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f394,f275])).
% 0.15/0.47 fof(f396,plain,(
% 0.15/0.47 $false),
% 0.15/0.47 inference(forward_subsumption_resolution,[status(thm)],[f395,f308])).
% 0.15/0.47 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.49 % Elapsed time: 0.109934 seconds
% 0.15/0.49 % CPU time: 0.353153 seconds
% 0.15/0.49 % Total memory used: 54.554 MB
% 0.15/0.49 % Net memory used: 54.303 MB
%------------------------------------------------------------------------------