%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU197+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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.27s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU197+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n013.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 05:56:37 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.27/0.84 % Refutation found
% 0.27/0.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/0.84 % SZS output start CNFRefutation for theBenchmark
% 0.27/0.84 fof(f4,axiom,(
% 0.27/0.84 (! [A,B] :( relation(B)=> (! [C] :( relation(C)=> ( C = relation_rng_restriction(A,B)<=> (! [D,E] :( in(ordered_pair(D,E),C)<=> ( in(E,A)& in(ordered_pair(D,E),B) ) ) )) ) )) )),
% 0.27/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.84 fof(f5,axiom,(
% 0.27/0.84 (! [A] :( relation(A)=> (! [B] :( B = relation_rng(A)<=> (! [C] :( in(C,B)<=> (? [D] : in(ordered_pair(D,C),A) )) )) )) )),
% 0.27/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.84 fof(f12,axiom,(
% 0.27/0.84 (! [A,B] :( relation(B)=> relation(relation_rng_restriction(A,B)) ) )),
% 0.27/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.84 fof(f26,conjecture,(
% 0.27/0.84 (! [A,B,C] :( relation(C)=> ( in(A,relation_rng(relation_rng_restriction(B,C)))<=> ( in(A,B)& in(A,relation_rng(C)) ) ) ) )),
% 0.27/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.84 fof(f27,negated_conjecture,(
% 0.27/0.84 ~((! [A,B,C] :( relation(C)=> ( in(A,relation_rng(relation_rng_restriction(B,C)))<=> ( in(A,B)& in(A,relation_rng(C)) ) ) ) ))),
% 0.27/0.84 inference(negated_conjecture,[status(cth)],[f26])).
% 0.27/0.84 fof(f38,plain,(
% 0.27/0.84 ![A,B]: (~relation(B)|(![C]: (~relation(C)|(C=relation_rng_restriction(A,B)<=>(![D,E]: (in(ordered_pair(D,E),C)<=>(in(E,A)&in(ordered_pair(D,E),B))))))))),
% 0.27/0.84 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.27/0.84 fof(f39,plain,(
% 0.27/0.84 ![A,B]: (~relation(B)|(![C]: (~relation(C)|((~C=relation_rng_restriction(A,B)|(![D,E]: ((~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B))))))&(C=relation_rng_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))))))))),
% 0.27/0.84 inference(NNF_transformation,[status(thm)],[f38])).
% 0.27/0.84 fof(f40,plain,(
% 0.27/0.84 ![B]: (~relation(B)|(![C]: (~relation(C)|((![A]: (~C=relation_rng_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))))))&(![A]: (C=relation_rng_restriction(A,B)|(?[D,E]: ((~in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))&(in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B)))))))))))),
% 0.27/0.84 inference(miniscoping,[status(thm)],[f39])).
% 0.27/0.84 fof(f41,plain,(
% 0.27/0.84 ![B]: (~relation(B)|(![C]: (~relation(C)|((![A]: (~C=relation_rng_restriction(A,B)|((![D,E]: (~in(ordered_pair(D,E),C)|(in(E,A)&in(ordered_pair(D,E),B))))&(![D,E]: (in(ordered_pair(D,E),C)|(~in(E,A)|~in(ordered_pair(D,E),B)))))))&(![A]: (C=relation_rng_restriction(A,B)|((~in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),C)|(~in(sK1_skl(A,C,B),A)|~in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),B)))&(in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),C)|(in(sK1_skl(A,C,B),A)&in(ordered_pair(sK0_skl(A,C,B),sK1_skl(A,C,B)),B))))))))))),
% 0.27/0.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(D,sK0_skl(A,C,B)),skolemize(E,sK1_skl(A,C,B))],[f40])).
% 0.27/0.84 fof(f42,plain,(
% 0.27/0.84 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_rng_restriction(X2,X0)|~in(ordered_pair(X3,X4),X1)|in(X4,X2))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f41])).
% 0.27/0.84 fof(f43,plain,(
% 0.27/0.84 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_rng_restriction(X2,X0)|~in(ordered_pair(X3,X4),X1)|in(ordered_pair(X3,X4),X0))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f41])).
% 0.27/0.84 fof(f44,plain,(
% 0.27/0.84 ![X0,X1,X2,X3,X4]: (~relation(X0)|~relation(X1)|~X1=relation_rng_restriction(X2,X0)|in(ordered_pair(X3,X4),X1)|~in(X4,X2)|~in(ordered_pair(X3,X4),X0))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f41])).
% 0.27/0.84 fof(f48,plain,(
% 0.27/0.84 ![A]: (~relation(A)|(![B]: (B=relation_rng(A)<=>(![C]: (in(C,B)<=>(?[D]: in(ordered_pair(D,C),A)))))))),
% 0.27/0.84 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.27/0.84 fof(f49,plain,(
% 0.27/0.84 ![A]: (~relation(A)|(![B]: ((~B=relation_rng(A)|(![C]: ((~in(C,B)|(?[D]: in(ordered_pair(D,C),A)))&(in(C,B)|(![D]: ~in(ordered_pair(D,C),A))))))&(B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 0.27/0.84 inference(NNF_transformation,[status(thm)],[f48])).
% 0.27/0.84 fof(f50,plain,(
% 0.27/0.84 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|(?[D]: in(ordered_pair(D,C),A))))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|(?[C]: ((~in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))&(in(C,B)|(?[D]: in(ordered_pair(D,C),A)))))))))),
% 0.27/0.84 inference(miniscoping,[status(thm)],[f49])).
% 0.27/0.84 fof(f51,plain,(
% 0.27/0.84 ![A]: (~relation(A)|((![B]: (~B=relation_rng(A)|((![C]: (~in(C,B)|in(ordered_pair(sK2_skl(C,B,A),C),A)))&(![C]: (in(C,B)|(![D]: ~in(ordered_pair(D,C),A)))))))&(![B]: (B=relation_rng(A)|((~in(sK3_skl(B,A),B)|(![D]: ~in(ordered_pair(D,sK3_skl(B,A)),A)))&(in(sK3_skl(B,A),B)|in(ordered_pair(sK4_skl(B,A),sK3_skl(B,A)),A)))))))),
% 0.27/0.84 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.27/0.84 fof(f52,plain,(
% 0.27/0.84 ![X0,X1,X2]: (~relation(X0)|~X1=relation_rng(X0)|~in(X2,X1)|in(ordered_pair(sK2_skl(X2,X1,X0),X2),X0))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f51])).
% 0.27/0.84 fof(f53,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~X1=relation_rng(X0)|in(X2,X1)|~in(ordered_pair(X3,X2),X0))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f51])).
% 0.27/0.84 fof(f57,plain,(
% 0.27/0.84 ![A,B]: (~relation(B)|relation(relation_rng_restriction(A,B)))),
% 0.27/0.84 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.27/0.84 fof(f58,plain,(
% 0.27/0.84 ![B]: (~relation(B)|(![A]: relation(relation_rng_restriction(A,B))))),
% 0.27/0.84 inference(miniscoping,[status(thm)],[f57])).
% 0.27/0.84 fof(f59,plain,(
% 0.27/0.84 ![X0,X1]: (~relation(X0)|relation(relation_rng_restriction(X1,X0)))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f58])).
% 0.27/0.84 fof(f83,plain,(
% 0.27/0.84 (?[A,B,C]: (relation(C)&(in(A,relation_rng(relation_rng_restriction(B,C)))<~>(in(A,B)&in(A,relation_rng(C))))))),
% 0.27/0.84 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.27/0.84 fof(f84,plain,(
% 0.27/0.84 ?[A,B,C]: (relation(C)&((in(A,relation_rng(relation_rng_restriction(B,C)))|(in(A,B)&in(A,relation_rng(C))))&(~in(A,relation_rng(relation_rng_restriction(B,C)))|(~in(A,B)|~in(A,relation_rng(C))))))),
% 0.27/0.84 inference(NNF_transformation,[status(thm)],[f83])).
% 0.27/0.84 fof(f85,plain,(
% 0.27/0.84 ?[C]: (relation(C)&(?[A,B]: ((in(A,relation_rng(relation_rng_restriction(B,C)))|(in(A,B)&in(A,relation_rng(C))))&(~in(A,relation_rng(relation_rng_restriction(B,C)))|(~in(A,B)|~in(A,relation_rng(C)))))))),
% 0.27/0.84 inference(miniscoping,[status(thm)],[f84])).
% 0.27/0.84 fof(f86,plain,(
% 0.27/0.84 (relation(sK10_skl)&((in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|(in(sK11_skl,sK12_skl)&in(sK11_skl,relation_rng(sK10_skl))))&(~in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|(~in(sK11_skl,sK12_skl)|~in(sK11_skl,relation_rng(sK10_skl))))))),
% 0.27/0.84 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)],[f85])).
% 0.27/0.84 fof(f87,plain,(
% 0.27/0.84 relation(sK10_skl)),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f86])).
% 0.27/0.84 fof(f88,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|in(sK11_skl,sK12_skl)),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f86])).
% 0.27/0.84 fof(f89,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f86])).
% 0.27/0.84 fof(f90,plain,(
% 0.27/0.84 ~in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|~in(sK11_skl,sK12_skl)|~in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(cnf_transformation,[status(thm)],[f86])).
% 0.27/0.84 fof(f103,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_rng_restriction(X1,X0))|~in(ordered_pair(X2,X3),relation_rng_restriction(X1,X0))|in(X3,X1))),
% 0.27/0.84 inference(destructive_equality_resolution,[status(thm)],[f42])).
% 0.27/0.84 fof(f104,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_rng_restriction(X1,X0))|~in(ordered_pair(X2,X3),relation_rng_restriction(X1,X0))|in(ordered_pair(X2,X3),X0))),
% 0.27/0.84 inference(destructive_equality_resolution,[status(thm)],[f43])).
% 0.27/0.84 fof(f105,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~relation(relation_rng_restriction(X1,X0))|in(ordered_pair(X2,X3),relation_rng_restriction(X1,X0))|~in(X3,X1)|~in(ordered_pair(X2,X3),X0))),
% 0.27/0.84 inference(destructive_equality_resolution,[status(thm)],[f44])).
% 0.27/0.84 fof(f106,plain,(
% 0.27/0.84 ![X0,X1]: (~relation(X0)|~in(X1,relation_rng(X0))|in(ordered_pair(sK2_skl(X1,relation_rng(X0),X0),X1),X0))),
% 0.27/0.84 inference(destructive_equality_resolution,[status(thm)],[f52])).
% 0.27/0.84 fof(f107,plain,(
% 0.27/0.84 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_rng(X0))|~in(ordered_pair(X2,X1),X0))),
% 0.27/0.84 inference(destructive_equality_resolution,[status(thm)],[f53])).
% 0.27/0.84 fof(f112,plain,(
% 0.27/0.84 ![X0]: (relation(relation_rng_restriction(X0,sK10_skl)))),
% 0.27/0.84 inference(resolution,[status(thm)],[f59,f87])).
% 0.27/0.84 fof(f116,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~in(ordered_pair(X1,X2),relation_rng_restriction(X3,X0))|in(X2,X3))),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f103,f59])).
% 0.27/0.84 fof(f117,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|~in(ordered_pair(X1,X2),relation_rng_restriction(X3,X0))|in(ordered_pair(X1,X2),X0))),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f104,f59])).
% 0.27/0.84 fof(f135,plain,(
% 0.27/0.84 ![X0,X1,X2,X3]: (~relation(X0)|in(ordered_pair(X1,X2),relation_rng_restriction(X3,X0))|~in(X2,X3)|~in(ordered_pair(X1,X2),X0))),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f105,f59])).
% 0.27/0.84 fof(f208,plain,(
% 0.27/0.84 ~relation(relation_rng_restriction(sK12_skl,sK10_skl))|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),relation_rng_restriction(sK12_skl,sK10_skl))|in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(resolution,[status(thm)],[f106,f89])).
% 0.27/0.84 fof(f209,plain,(
% 0.27/0.84 ~relation(relation_rng_restriction(sK12_skl,sK10_skl))|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),relation_rng_restriction(sK12_skl,sK10_skl))|in(sK11_skl,sK12_skl)),
% 0.27/0.84 inference(resolution,[status(thm)],[f106,f88])).
% 0.27/0.84 fof(f211,plain,(
% 0.27/0.84 in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),relation_rng_restriction(sK12_skl,sK10_skl))|in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f208,f112])).
% 0.27/0.84 fof(f212,plain,(
% 0.27/0.84 in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),relation_rng_restriction(sK12_skl,sK10_skl))|in(sK11_skl,sK12_skl)),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f209,f112])).
% 0.27/0.84 fof(f257,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(sK10_skl))|~relation(sK10_skl)|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),sK10_skl)),
% 0.27/0.84 inference(resolution,[status(thm)],[f211,f117])).
% 0.27/0.84 fof(f264,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(sK10_skl))|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)),relation_rng_restriction(sK12_skl,sK10_skl)),sK11_skl),sK10_skl)),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f257,f87])).
% 0.27/0.84 fof(f350,plain,(
% 0.27/0.84 in(sK11_skl,sK12_skl)|~relation(sK10_skl)|in(sK11_skl,sK12_skl)),
% 0.27/0.84 inference(resolution,[status(thm)],[f212,f116])).
% 0.27/0.84 fof(f357,plain,(
% 0.27/0.84 in(sK11_skl,sK12_skl)|~relation(sK10_skl)),
% 0.27/0.84 inference(duplicate_literals_removal,[status(thm)],[f350])).
% 0.27/0.84 fof(f358,plain,(
% 0.27/0.84 in(sK11_skl,sK12_skl)),
% 0.27/0.84 inference(forward_subsumption_resolution,[status(thm)],[f357,f87])).
% 0.27/0.84 fof(f360,plain,(
% 0.27/0.84 ~in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))|~in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(backward_subsumption_resolution,[status(thm)],[f90,f358])).
% 0.27/0.84 fof(f1510,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(sK10_skl))|~relation(sK10_skl)|in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.84 inference(resolution,[status(thm)],[f264,f107])).
% 0.27/0.84 fof(f1515,plain,(
% 0.27/0.84 in(sK11_skl,relation_rng(sK10_skl))|~relation(sK10_skl)),
% 0.27/0.84 inference(duplicate_literals_removal,[status(thm)],[f1510])).
% 0.27/0.84 fof(f1516,plain,(
% 0.27/0.86 in(sK11_skl,relation_rng(sK10_skl))),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f1515,f87])).
% 0.27/0.86 fof(f1517,plain,(
% 0.27/0.86 ~in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))),
% 0.27/0.86 inference(backward_subsumption_resolution,[status(thm)],[f360,f1516])).
% 0.27/0.86 fof(f1518,plain,(
% 0.27/0.86 ~relation(sK10_skl)|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(sK10_skl),sK10_skl),sK11_skl),sK10_skl)),
% 0.27/0.86 inference(resolution,[status(thm)],[f1516,f106])).
% 0.27/0.86 fof(f1522,plain,(
% 0.27/0.86 in(ordered_pair(sK2_skl(sK11_skl,relation_rng(sK10_skl),sK10_skl),sK11_skl),sK10_skl)),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f1518,f87])).
% 0.27/0.86 fof(f1524,plain,(
% 0.27/0.86 ![X0]: (~relation(sK10_skl)|in(ordered_pair(sK2_skl(sK11_skl,relation_rng(sK10_skl),sK10_skl),sK11_skl),relation_rng_restriction(X0,sK10_skl))|~in(sK11_skl,X0))),
% 0.27/0.86 inference(resolution,[status(thm)],[f1522,f135])).
% 0.27/0.86 fof(f1529,plain,(
% 0.27/0.86 ![X0]: (in(ordered_pair(sK2_skl(sK11_skl,relation_rng(sK10_skl),sK10_skl),sK11_skl),relation_rng_restriction(X0,sK10_skl))|~in(sK11_skl,X0))),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f1524,f87])).
% 0.27/0.86 fof(f2054,plain,(
% 0.27/0.86 in(ordered_pair(sK2_skl(sK11_skl,relation_rng(sK10_skl),sK10_skl),sK11_skl),relation_rng_restriction(sK12_skl,sK10_skl))),
% 0.27/0.86 inference(resolution,[status(thm)],[f1529,f358])).
% 0.27/0.86 fof(f2059,plain,(
% 0.27/0.86 ~relation(relation_rng_restriction(sK12_skl,sK10_skl))|in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))),
% 0.27/0.86 inference(resolution,[status(thm)],[f2054,f107])).
% 0.27/0.86 fof(f2064,plain,(
% 0.27/0.86 in(sK11_skl,relation_rng(relation_rng_restriction(sK12_skl,sK10_skl)))),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f2059,f112])).
% 0.27/0.86 fof(f2092,plain,(
% 0.27/0.86 $false),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f2064,f1517])).
% 0.27/0.86 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.88 % Elapsed time: 0.441657 seconds
% 0.27/0.88 % CPU time: 3.122918 seconds
% 0.27/0.88 % Total memory used: 149.534 MB
% 0.27/0.88 % Net memory used: 146.176 MB
%------------------------------------------------------------------------------