%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU192+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 : n011.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:21:57 PM UTC 2026
% Result : Theorem 0.82s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU192+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.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 05:56:41 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.82/0.67 % Refutation found
% 0.82/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.82/0.67 % SZS output start CNFRefutation for theBenchmark
% 0.82/0.67 fof(f4,axiom,(
% 0.82/0.67 (! [A] :( relation(A)=> (! [B,C] :( relation(C)=> ( C = relation_dom_restriction(A,B)<=> (! [D,E] :( in(ordered_pair(D,E),C)<=> ( in(D,B)& in(ordered_pair(D,E),A) ) ) )) ) )) )),
% 0.82/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.82/0.67 fof(f5,axiom,(
% 0.82/0.67 (! [A] :( relation(A)=> (! [B] :( B = relation_dom(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(C,D),A) )) )) )) )),
% 0.82/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.82/0.67 fof(f12,axiom,(
% 0.82/0.67 (! [A,B] :( relation(A)=> relation(relation_dom_restriction(A,B)) ) )),
% 0.82/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.82/0.67 fof(f30,conjecture,(
% 0.82/0.67 (! [A,B,C] :( relation(C)=> ( in(A,relation_dom(relation_dom_restriction(C,B)))<=> ( in(A,B)& in(A,relation_dom(C)) ) ) ) )),
% 0.82/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.82/0.67 fof(f31,negated_conjecture,(
% 0.82/0.67 ~((! [A,B,C] :( relation(C)=> ( in(A,relation_dom(relation_dom_restriction(C,B)))<=> ( in(A,B)& in(A,relation_dom(C)) ) ) ) ))),
% 0.82/0.67 inference(negated_conjecture,[status(cth)],[f30])).
% 0.82/0.67 fof(f38,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![B,C]: (~relation(C)|(C=relation_dom_restriction(A,B)<=>(![D,E]: (in(ordered_pair(D,E),C)<=>(in(D,B)&in(ordered_pair(D,E),A))))))))),
% 0.82/0.67 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.82/0.67 fof(f39,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![B,C]: (~relation(C)|((~C=relation_dom_restriction(A,B)|(![D,E]: ((~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A))))))&(C=relation_dom_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))))))))),
% 0.82/0.67 inference(NNF_transformation,[status(thm)],[f38])).
% 0.82/0.67 fof(f40,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![C]: (~relation(C)|((![B]: (~C=relation_dom_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))))))&(![B]: (C=relation_dom_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))&(in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A)))))))))))),
% 0.82/0.67 inference(miniscoping,[status(thm)],[f39])).
% 0.82/0.67 fof(f41,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![C]: (~relation(C)|((![B]: (~C=relation_dom_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(D,B)&in(ordered_pair(D,E),A))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(D,B)|~in(ordered_pair(D,E),A)))))))&(![B]: (C=relation_dom_restriction(A,B)|((~in(ordered_pair(sK0_skl(B,C,A),sK1_skl(B,C,A)),C)|(~in(sK0_skl(B,C,A),B)|~in(ordered_pair(sK0_skl(B,C,A),sK1_skl(B,C,A)),A)))&(in(ordered_pair(sK0_skl(B,C,A),sK1_skl(B,C,A)),C)|(in(sK0_skl(B,C,A),B)&in(ordered_pair(sK0_skl(B,C,A),sK1_skl(B,C,A)),A))))))))))),
% 0.82/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(D,sK0_skl(B,C,A)),skolemize(E,sK1_skl(B,C,A))],[f40])).
% 0.82/0.67 fof(f42,plain,(
% 0.82/0.67 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_dom_restriction(X0,X2)|~in(ordered_pair(X3,X4),X1)|in(X3,X2))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f41])).
% 0.82/0.67 fof(f43,plain,(
% 0.82/0.67 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_dom_restriction(X0,X2)|~in(ordered_pair(X3,X4),X1)|in(ordered_pair(X3,X4),X0))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f41])).
% 0.82/0.67 fof(f44,plain,(
% 0.82/0.67 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_dom_restriction(X0,X2)|in(ordered_pair(X3,X4),X1)|~in(X3,X2)|~in(ordered_pair(X3,X4),X0))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f41])).
% 0.82/0.67 fof(f48,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![B]: (B=relation_dom(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(C,D),A)))))))),
% 0.82/0.67 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.82/0.67 fof(f49,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![B]: ((~B=relation_dom(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(C,D),A)))&(in(C,B)|(![D]: ~in(ordered_pair(C,D),A))))))&(B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 0.82/0.67 inference(NNF_transformation,[status(thm)],[f48])).
% 0.82/0.67 fof(f50,plain,(
% 0.82/0.67 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(C,D),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))&(in(C,B)|(?[D]: in(ordered_pair(C,D),A)))))))))),
% 0.82/0.67 inference(miniscoping,[status(thm)],[f49])).
% 0.82/0.67 fof(f51,plain,(
% 0.82/0.67 ![A]: (~relation(A)|((![B]: (~B=relation_dom(A)|((![C]: (~in(C,B)|in(ordered_pair(C,sK2_skl(C,B,A)),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(C,D),A)))))))&(![B]: (B=relation_dom(A)|((~in(sK3_skl(B,A),B)|(![D]: ~in(ordered_pair(sK3_skl(B,A),D),A)))&(in(sK3_skl(B,A),B)|in(ordered_pair(sK3_skl(B,A),sK4_skl(B,A)),A)))))))),
% 0.82/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl]),skolemize(D,sK2_skl(C,B,A)),skolemize(C,sK3_skl(B,A)),skolemize(D,sK4_skl(B,A))],[f50])).
% 0.82/0.67 fof(f52,plain,(
% 0.82/0.67 ![X0,X1,X2]: (~relation(X0)|~X1=relation_dom(X0)|~in(X2,X1)|in(ordered_pair(X2,sK2_skl(X2,X1,X0)),X0))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f51])).
% 0.82/0.67 fof(f53,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_dom(X0)|in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f51])).
% 0.82/0.67 fof(f57,plain,(
% 0.82/0.67 ![A,B]: (~relation(A)|relation(relation_dom_restriction(A,B)))),
% 0.82/0.67 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.82/0.67 fof(f58,plain,(
% 0.82/0.67 ![A]: (~relation(A)|(![B]: relation(relation_dom_restriction(A,B))))),
% 0.82/0.67 inference(miniscoping,[status(thm)],[f57])).
% 0.82/0.67 fof(f59,plain,(
% 0.82/0.67 ![X0,X1]: (~relation(X0)|relation(relation_dom_restriction(X0,X1)))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f58])).
% 0.82/0.67 fof(f92,plain,(
% 0.82/0.67 (?[A,B,C]: (relation(C)&(in(A,relation_dom(relation_dom_restriction(C,B)))<~>(in(A,B)&in(A,relation_dom(C))))))),
% 0.82/0.67 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.82/0.67 fof(f93,plain,(
% 0.82/0.67 ?[A,B,C]: (relation(C)&((in(A,relation_dom(relation_dom_restriction(C,B)))|(in(A,B)&in(A,relation_dom(C))))&(~in(A,relation_dom(relation_dom_restriction(C,B)))|(~in(A,B)|~in(A,relation_dom(C))))))),
% 0.82/0.67 inference(NNF_transformation,[status(thm)],[f92])).
% 0.82/0.67 fof(f94,plain,(
% 0.82/0.67 ?[C]: (relation(C)&(?[A,B]: ((in(A,relation_dom(relation_dom_restriction(C,B)))|(in(A,B)&in(A,relation_dom(C))))&(~in(A,relation_dom(relation_dom_restriction(C,B)))|(~in(A,B)|~in(A,relation_dom(C)))))))),
% 0.82/0.67 inference(miniscoping,[status(thm)],[f93])).
% 0.82/0.67 fof(f95,plain,(
% 0.82/0.67 (relation(sK10_skl)&((in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|(in(sK11_skl,sK12_skl)&in(sK11_skl,relation_dom(sK10_skl))))&(~in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|(~in(sK11_skl,sK12_skl)|~in(sK11_skl,relation_dom(sK10_skl))))))),
% 0.82/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(C,sK10_skl),skolemize(A,sK11_skl),skolemize(B,sK12_skl)],[f94])).
% 0.82/0.67 fof(f96,plain,(
% 0.82/0.67 relation(sK10_skl)),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f95])).
% 0.82/0.67 fof(f97,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|in(sK11_skl,sK12_skl)),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f95])).
% 0.82/0.67 fof(f98,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f95])).
% 0.82/0.67 fof(f99,plain,(
% 0.82/0.67 ~in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|~in(sK11_skl,sK12_skl)|~in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(cnf_transformation,[status(thm)],[f95])).
% 0.82/0.67 fof(f103,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_dom_restriction(X0,X1))|~in(ordered_pair(X2,X3),relation_dom_restriction(X0,X1))|in(X2,X1))),
% 0.82/0.67 inference(destructive_equality_resolution,[status(thm)],[f42])).
% 0.82/0.67 fof(f104,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_dom_restriction(X0,X1))|~in(ordered_pair(X2,X3),relation_dom_restriction(X0,X1))|in(ordered_pair(X2,X3),X0))),
% 0.82/0.67 inference(destructive_equality_resolution,[status(thm)],[f43])).
% 0.82/0.67 fof(f105,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_dom_restriction(X0,X1))|in(ordered_pair(X2,X3),relation_dom_restriction(X0,X1))|~in(X2,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.82/0.67 inference(destructive_equality_resolution,[status(thm)],[f44])).
% 0.82/0.67 fof(f106,plain,(
% 0.82/0.67 ![X0,X1]: (~relation(X0)|~in(X1,relation_dom(X0))|in(ordered_pair(X1,sK2_skl(X1,relation_dom(X0),X0)),X0))),
% 0.82/0.67 inference(destructive_equality_resolution,[status(thm)],[f52])).
% 0.82/0.67 fof(f107,plain,(
% 0.82/0.67 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_dom(X0))|~in(ordered_pair(X1,X2),X0))),
% 0.82/0.67 inference(destructive_equality_resolution,[status(thm)],[f53])).
% 0.82/0.67 fof(f112,plain,(
% 0.82/0.67 ![X0]: (relation(relation_dom_restriction(sK10_skl,X0)))),
% 0.82/0.67 inference(resolution,[status(thm)],[f59,f96])).
% 0.82/0.67 fof(f116,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~in(ordered_pair(X1,X2),relation_dom_restriction(X0,X3))|in(X1,X3))),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f103,f59])).
% 0.82/0.67 fof(f117,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|~in(ordered_pair(X1,X2),relation_dom_restriction(X0,X3))|in(ordered_pair(X1,X2),X0))),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f104,f59])).
% 0.82/0.67 fof(f135,plain,(
% 0.82/0.67 ![X0,X1,X2,X3]: (~relation(X0)|in(ordered_pair(X1,X2),relation_dom_restriction(X0,X3))|~in(X1,X3)|~in(ordered_pair(X1,X2),X0))),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f105,f59])).
% 0.82/0.67 fof(f208,plain,(
% 0.82/0.67 ~relation(relation_dom_restriction(sK10_skl,sK12_skl))|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),relation_dom_restriction(sK10_skl,sK12_skl))|in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(resolution,[status(thm)],[f106,f98])).
% 0.82/0.67 fof(f209,plain,(
% 0.82/0.67 ~relation(relation_dom_restriction(sK10_skl,sK12_skl))|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),relation_dom_restriction(sK10_skl,sK12_skl))|in(sK11_skl,sK12_skl)),
% 0.82/0.67 inference(resolution,[status(thm)],[f106,f97])).
% 0.82/0.67 fof(f211,plain,(
% 0.82/0.67 in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),relation_dom_restriction(sK10_skl,sK12_skl))|in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f208,f112])).
% 0.82/0.67 fof(f212,plain,(
% 0.82/0.67 in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),relation_dom_restriction(sK10_skl,sK12_skl))|in(sK11_skl,sK12_skl)),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f209,f112])).
% 0.82/0.67 fof(f257,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(sK10_skl))|~relation(sK10_skl)|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),sK10_skl)),
% 0.82/0.67 inference(resolution,[status(thm)],[f211,f117])).
% 0.82/0.67 fof(f264,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(sK10_skl))|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),sK10_skl)),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f257,f96])).
% 0.82/0.67 fof(f350,plain,(
% 0.82/0.67 in(sK11_skl,sK12_skl)|~relation(sK10_skl)|in(sK11_skl,sK12_skl)),
% 0.82/0.67 inference(resolution,[status(thm)],[f212,f116])).
% 0.82/0.67 fof(f357,plain,(
% 0.82/0.67 in(sK11_skl,sK12_skl)|~relation(sK10_skl)),
% 0.82/0.67 inference(duplicate_literals_removal,[status(thm)],[f350])).
% 0.82/0.67 fof(f358,plain,(
% 0.82/0.67 in(sK11_skl,sK12_skl)),
% 0.82/0.67 inference(forward_subsumption_resolution,[status(thm)],[f357,f96])).
% 0.82/0.67 fof(f360,plain,(
% 0.82/0.67 ~in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))|~in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(backward_subsumption_resolution,[status(thm)],[f99,f358])).
% 0.82/0.67 fof(f1537,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(sK10_skl))|~relation(sK10_skl)|in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.67 inference(resolution,[status(thm)],[f264,f107])).
% 0.82/0.67 fof(f1542,plain,(
% 0.82/0.67 in(sK11_skl,relation_dom(sK10_skl))|~relation(sK10_skl)),
% 0.82/0.67 inference(duplicate_literals_removal,[status(thm)],[f1537])).
% 0.82/0.67 fof(f1543,plain,(
% 0.82/0.68 in(sK11_skl,relation_dom(sK10_skl))),
% 0.82/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1542,f96])).
% 0.82/0.68 fof(f1544,plain,(
% 0.82/0.68 ~in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))),
% 0.82/0.68 inference(backward_subsumption_resolution,[status(thm)],[f360,f1543])).
% 0.82/0.68 fof(f1545,plain,(
% 0.82/0.68 ~relation(sK10_skl)|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(sK10_skl),sK10_skl)),sK10_skl)),
% 0.82/0.68 inference(resolution,[status(thm)],[f1543,f106])).
% 0.82/0.68 fof(f1549,plain,(
% 0.82/0.68 in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(sK10_skl),sK10_skl)),sK10_skl)),
% 0.82/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1545,f96])).
% 0.82/0.68 fof(f1551,plain,(
% 0.82/0.68 ![X0]: (~relation(sK10_skl)|in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(sK10_skl),sK10_skl)),relation_dom_restriction(sK10_skl,X0))|~in(sK11_skl,X0))),
% 0.82/0.68 inference(resolution,[status(thm)],[f1549,f135])).
% 0.82/0.68 fof(f1556,plain,(
% 0.82/0.68 ![X0]: (in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(sK10_skl),sK10_skl)),relation_dom_restriction(sK10_skl,X0))|~in(sK11_skl,X0))),
% 0.82/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1551,f96])).
% 0.82/0.68 fof(f2060,plain,(
% 0.82/0.68 in(ordered_pair(sK11_skl,sK2_skl(sK11_skl,relation_dom(sK10_skl),sK10_skl)),relation_dom_restriction(sK10_skl,sK12_skl))),
% 0.82/0.68 inference(resolution,[status(thm)],[f1556,f358])).
% 0.82/0.68 fof(f2065,plain,(
% 0.82/0.68 ~relation(relation_dom_restriction(sK10_skl,sK12_skl))|in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))),
% 0.82/0.68 inference(resolution,[status(thm)],[f2060,f107])).
% 0.82/0.68 fof(f2070,plain,(
% 0.82/0.68 in(sK11_skl,relation_dom(relation_dom_restriction(sK10_skl,sK12_skl)))),
% 0.82/0.68 inference(forward_subsumption_resolution,[status(thm)],[f2065,f112])).
% 0.82/0.68 fof(f2098,plain,(
% 0.82/0.68 $false),
% 0.82/0.68 inference(forward_subsumption_resolution,[status(thm)],[f2070,f1544])).
% 0.82/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.54/0.69 % Elapsed time: 0.307156 seconds
% 0.54/0.69 % CPU time: 2.152792 seconds
% 0.54/0.69 % Total memory used: 147.776 MB
% 0.54/0.69 % Net memory used: 144.851 MB
%------------------------------------------------------------------------------