%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET018-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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:11:13 PM UTC 2026
% Result : Unsatisfiable 30.27s 4.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET018-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.34 % Computer : n015.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Mon Sep 21 04:46:05 UTC 2026
% 0.10/0.34 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 30.27/4.27 % Refutation found
% 30.27/4.27 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 30.27/4.27 % SZS output start CNFRefutation for theBenchmark
% 30.27/4.27 fof(f1,axiom,(
% 30.27/4.27 (![X,Y]: (( ~ member(X,Y)| little_set(X) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f5,axiom,(
% 30.27/4.27 (![U,X,Y]: (( ~ member(U,non_ordered_pair(X,Y))| U = X| U = Y ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f6,axiom,(
% 30.27/4.27 (![U,X,Y]: (( member(U,non_ordered_pair(X,Y))| ~ little_set(U)| U != X ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f7,axiom,(
% 30.27/4.27 (![U,X,Y]: (( member(U,non_ordered_pair(X,Y))| ~ little_set(U)| U != Y ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f8,axiom,(
% 30.27/4.27 (![X,Y]: (little_set(non_ordered_pair(X,Y)) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f9,axiom,(
% 30.27/4.27 (![X]: (singleton_set(X) = non_ordered_pair(X,X) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f10,axiom,(
% 30.27/4.27 (![X,Y]: (ordered_pair(X,Y) = non_ordered_pair(singleton_set(X),non_ordered_pair(X,Y)) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f11,axiom,(
% 30.27/4.27 (![X]: (( ~ ordered_pair_predicate(X)| little_set(f2(X)) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f12,axiom,(
% 30.27/4.27 (![X]: (( ~ ordered_pair_predicate(X)| little_set(f3(X)) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f13,axiom,(
% 30.27/4.27 (![X]: (( ~ ordered_pair_predicate(X)| X = ordered_pair(f2(X),f3(X)) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f14,axiom,(
% 30.27/4.27 (![X,Y,Z]: (( ordered_pair_predicate(X)| ~ little_set(Y)| ~ little_set(Z)| X != ordered_pair(Y,Z) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f19,axiom,(
% 30.27/4.27 (![Z,X,U,V]: (( member(Z,first(X))| ~ little_set(U)| ~ little_set(V)| X != ordered_pair(U,V)| ~ member(Z,U) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f68,axiom,(
% 30.27/4.27 (![X,Y]: (( subset(X,Y)| member(f17(X,Y),X) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f69,axiom,(
% 30.27/4.27 (![X,Y]: (( subset(X,Y)| ~ member(f17(X,Y),Y) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f74,axiom,(
% 30.27/4.27 (![Z,X]: (( member(Z,powerset(X))| ~ little_set(Z)| ~ subset(Z,X) ) ))),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f142,hypothesis,(
% 30.27/4.27 little_set(a) ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f143,hypothesis,(
% 30.27/4.27 little_set(b) ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f144,hypothesis,(
% 30.27/4.27 little_set(c) ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f145,hypothesis,(
% 30.27/4.27 little_set(d) ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f146,hypothesis,(
% 30.27/4.27 ordered_pair(a,b) = ordered_pair(c,d) ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f147,negated_conjecture,(
% 30.27/4.27 b != d ),
% 30.27/4.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.27/4.27 fof(f148,plain,(
% 30.27/4.27 ![X]: ((![Y]: ~member(X,Y))|little_set(X))),
% 30.27/4.27 inference(miniscoping,[status(thm)],[f1])).
% 30.27/4.27 fof(f149,plain,(
% 30.27/4.27 ![X0,X1]: (~member(X0,X1)|little_set(X0))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f148])).
% 30.27/4.27 fof(f153,plain,(
% 30.27/4.27 ![U,Y]: ((![X]: (~member(U,non_ordered_pair(X,Y))|U=X))|U=Y)),
% 30.27/4.27 inference(miniscoping,[status(thm)],[f5])).
% 30.27/4.27 fof(f154,plain,(
% 30.27/4.27 ![X0,X1,X2]: (~member(X0,non_ordered_pair(X1,X2))|X0=X1|X0=X2)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f153])).
% 30.27/4.27 fof(f155,plain,(
% 30.27/4.27 ![U,X]: (((![Y]: member(U,non_ordered_pair(X,Y)))|~little_set(U))|~U=X)),
% 30.27/4.27 inference(miniscoping,[status(thm)],[f6])).
% 30.27/4.27 fof(f156,plain,(
% 30.27/4.27 ![X0,X1,X2]: (member(X0,non_ordered_pair(X1,X2))|~little_set(X0)|~X0=X1)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f155])).
% 30.27/4.27 fof(f157,plain,(
% 30.27/4.27 ![U,Y]: (((![X]: member(U,non_ordered_pair(X,Y)))|~little_set(U))|~U=Y)),
% 30.27/4.27 inference(miniscoping,[status(thm)],[f7])).
% 30.27/4.27 fof(f158,plain,(
% 30.27/4.27 ![X0,X1,X2]: (member(X0,non_ordered_pair(X1,X2))|~little_set(X0)|~X0=X2)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f157])).
% 30.27/4.27 fof(f159,plain,(
% 30.27/4.27 ![X0,X1]: (little_set(non_ordered_pair(X0,X1)))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f8])).
% 30.27/4.27 fof(f160,plain,(
% 30.27/4.27 ![X0]: (singleton_set(X0)=non_ordered_pair(X0,X0))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f9])).
% 30.27/4.27 fof(f161,plain,(
% 30.27/4.27 ![X0,X1]: (ordered_pair(X0,X1)=non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f10])).
% 30.27/4.27 fof(f162,plain,(
% 30.27/4.27 ![X0]: (~ordered_pair_predicate(X0)|little_set(f2(X0)))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f11])).
% 30.27/4.27 fof(f163,plain,(
% 30.27/4.27 ![X0]: (~ordered_pair_predicate(X0)|little_set(f3(X0)))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f12])).
% 30.27/4.27 fof(f164,plain,(
% 30.27/4.27 ![X0]: (~ordered_pair_predicate(X0)|X0=ordered_pair(f2(X0),f3(X0)))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f13])).
% 30.27/4.27 fof(f165,plain,(
% 30.27/4.27 ![X0,X1,X2]: (ordered_pair_predicate(X0)|~little_set(X1)|~little_set(X2)|~X0=ordered_pair(X1,X2))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f14])).
% 30.27/4.27 fof(f170,plain,(
% 30.27/4.27 ![Z,U]: ((![X,V]: (((member(Z,first(X))|~little_set(U))|~little_set(V))|~X=ordered_pair(U,V)))|~member(Z,U))),
% 30.27/4.27 inference(miniscoping,[status(thm)],[f19])).
% 30.27/4.27 fof(f171,plain,(
% 30.27/4.27 ![X0,X1,X2,X3]: (member(X0,first(X1))|~little_set(X2)|~little_set(X3)|~X1=ordered_pair(X2,X3)|~member(X0,X2))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f170])).
% 30.27/4.27 fof(f234,plain,(
% 30.27/4.27 ![X0,X1]: (subset(X0,X1)|member(f17(X0,X1),X0))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f68])).
% 30.27/4.27 fof(f235,plain,(
% 30.27/4.27 ![X0,X1]: (subset(X0,X1)|~member(f17(X0,X1),X1))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f69])).
% 30.27/4.27 fof(f240,plain,(
% 30.27/4.27 ![X0,X1]: (member(X0,powerset(X1))|~little_set(X0)|~subset(X0,X1))),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f74])).
% 30.27/4.27 fof(f325,plain,(
% 30.27/4.27 little_set(a)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f142])).
% 30.27/4.27 fof(f326,plain,(
% 30.27/4.27 little_set(b)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f143])).
% 30.27/4.27 fof(f327,plain,(
% 30.27/4.27 little_set(c)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f144])).
% 30.27/4.27 fof(f328,plain,(
% 30.27/4.27 little_set(d)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f145])).
% 30.27/4.27 fof(f329,plain,(
% 30.27/4.27 ordered_pair(a,b)=ordered_pair(c,d)),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f146])).
% 30.27/4.27 fof(f330,plain,(
% 30.27/4.27 ~b=d),
% 30.27/4.27 inference(cnf_transformation,[status(thm)],[f147])).
% 30.27/4.27 fof(f331,plain,(
% 30.27/4.27 ![X0,X1]: (member(X0,non_ordered_pair(X0,X1))|~little_set(X0))),
% 30.27/4.27 inference(destructive_equality_resolution,[status(thm)],[f156])).
% 30.27/4.27 fof(f332,plain,(
% 30.27/4.27 ![X0,X1]: (member(X0,non_ordered_pair(X1,X0))|~little_set(X0))),
% 30.27/4.27 inference(destructive_equality_resolution,[status(thm)],[f158])).
% 30.27/4.27 fof(f333,plain,(
% 30.27/4.27 ![X0,X1]: (ordered_pair_predicate(ordered_pair(X0,X1))|~little_set(X0)|~little_set(X1))),
% 30.27/4.27 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 30.27/4.27 fof(f334,plain,(
% 30.27/4.27 ![X0,X1,X2]: (member(X0,first(ordered_pair(X1,X2)))|~little_set(X1)|~little_set(X2)|~member(X0,X1))),
% 30.27/4.27 inference(destructive_equality_resolution,[status(thm)],[f171])).
% 30.27/4.27 fof(f365,plain,(
% 30.27/4.27 ![X0]: (member(X0,singleton_set(X0))|~little_set(X0))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f160,f331])).
% 30.27/4.28 fof(f366,plain,(
% 30.27/4.28 ![X0,X1]: (~member(X0,singleton_set(X1))|X0=X1|X0=X1)),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f160,f154])).
% 30.27/4.28 fof(f367,plain,(
% 30.27/4.28 ![X0]: (little_set(singleton_set(X0)))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f160,f159])).
% 30.27/4.28 fof(f368,plain,(
% 30.27/4.28 ![X0,X1]: (~member(X0,singleton_set(X1))|X0=X1)),
% 30.27/4.28 inference(duplicate_literals_removal,[status(thm)],[f366])).
% 30.27/4.28 fof(f374,plain,(
% 30.27/4.28 ![X0,X1]: (member(non_ordered_pair(X0,X1),ordered_pair(X0,X1))|~little_set(non_ordered_pair(X0,X1)))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f161,f332])).
% 30.27/4.28 fof(f375,plain,(
% 30.27/4.28 ![X0,X1]: (member(singleton_set(X0),ordered_pair(X0,X1))|~little_set(singleton_set(X0)))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f161,f331])).
% 30.27/4.28 fof(f376,plain,(
% 30.27/4.28 ![X0,X1,X2]: (~member(X0,ordered_pair(X1,X2))|X0=singleton_set(X1)|X0=non_ordered_pair(X1,X2))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f161,f154])).
% 30.27/4.28 fof(f379,plain,(
% 30.27/4.28 ![X0,X1]: (member(non_ordered_pair(X0,X1),ordered_pair(X0,X1)))),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f374,f159])).
% 30.27/4.28 fof(f380,plain,(
% 30.27/4.28 ![X0,X1]: (member(singleton_set(X0),ordered_pair(X0,X1)))),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f375,f367])).
% 30.27/4.28 fof(f982,plain,(
% 30.27/4.28 member(non_ordered_pair(c,d),ordered_pair(a,b))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f329,f379])).
% 30.27/4.28 fof(f983,plain,(
% 30.27/4.28 member(singleton_set(c),ordered_pair(a,b))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f329,f380])).
% 30.27/4.28 fof(f986,plain,(
% 30.27/4.28 ordered_pair_predicate(ordered_pair(a,b))|~little_set(c)|~little_set(d)),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f329,f333])).
% 30.27/4.28 fof(f991,plain,(
% 30.27/4.28 ordered_pair_predicate(ordered_pair(a,b))|~little_set(d)),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f986,f327])).
% 30.27/4.28 fof(f1196,plain,(
% 30.27/4.28 ordered_pair_predicate(ordered_pair(a,b))),
% 30.27/4.28 inference(resolution,[status(thm)],[f991,f328])).
% 30.27/4.28 fof(f1201,plain,(
% 30.27/4.28 ordered_pair(a,b)=ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1196,f164])).
% 30.27/4.28 fof(f1207,plain,(
% 30.27/4.28 member(singleton_set(f2(ordered_pair(a,b))),ordered_pair(a,b))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f1201,f380])).
% 30.27/4.28 fof(f1209,plain,(
% 30.27/4.28 ![X0]: (member(X0,first(ordered_pair(a,b)))|~little_set(f2(ordered_pair(a,b)))|~little_set(f3(ordered_pair(a,b)))|~member(X0,f2(ordered_pair(a,b))))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f1201,f334])).
% 30.27/4.28 fof(f1319,plain,(
% 30.27/4.28 ![X0]: (member(X0,first(ordered_pair(a,b)))|~little_set(f2(ordered_pair(a,b)))|~member(X0,f2(ordered_pair(a,b)))|~ordered_pair_predicate(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1209,f163])).
% 30.27/4.28 fof(f1321,plain,(
% 30.27/4.28 ![X0]: (member(X0,first(ordered_pair(a,b)))|~member(X0,f2(ordered_pair(a,b)))|~ordered_pair_predicate(ordered_pair(a,b)))),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f1319,f162])).
% 30.27/4.28 fof(f1377,plain,(
% 30.27/4.28 ![X0]: (member(X0,first(ordered_pair(a,b)))|~member(X0,f2(ordered_pair(a,b))))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1321,f1196])).
% 30.27/4.28 fof(f1382,plain,(
% 30.27/4.28 ![X0]: (~member(f17(X0,first(ordered_pair(a,b))),f2(ordered_pair(a,b)))|subset(X0,first(ordered_pair(a,b))))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1377,f235])).
% 30.27/4.28 fof(f1566,plain,(
% 30.27/4.28 subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b)))|subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1382,f234])).
% 30.27/4.28 fof(f1567,plain,(
% 30.27/4.28 subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b)))),
% 30.27/4.28 inference(duplicate_literals_removal,[status(thm)],[f1566])).
% 30.27/4.28 fof(f1568,plain,(
% 30.27/4.28 member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b))))|~little_set(f2(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1567,f240])).
% 30.27/4.28 fof(f1664,plain,(
% 30.27/4.28 member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b))))|~ordered_pair_predicate(ordered_pair(a,b))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1568,f162])).
% 30.27/4.28 fof(f1666,plain,(
% 30.27/4.28 member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b))))),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f1664,f1196])).
% 30.27/4.28 fof(f1668,plain,(
% 30.27/4.28 little_set(f2(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f1666,f149])).
% 30.27/4.28 fof(f2092,plain,(
% 30.27/4.28 non_ordered_pair(c,d)=singleton_set(a)|non_ordered_pair(c,d)=non_ordered_pair(a,b)),
% 30.27/4.28 inference(resolution,[status(thm)],[f376,f982])).
% 30.27/4.28 fof(f2095,plain,(
% 30.27/4.28 singleton_set(f2(ordered_pair(a,b)))=singleton_set(a)|singleton_set(f2(ordered_pair(a,b)))=non_ordered_pair(a,b)),
% 30.27/4.28 inference(resolution,[status(thm)],[f376,f1207])).
% 30.27/4.28 fof(f2110,plain,(
% 30.27/4.28 ![X0]: (~member(X0,ordered_pair(a,b))|X0=singleton_set(f2(ordered_pair(a,b)))|X0=non_ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b))))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f1201,f376])).
% 30.27/4.28 fof(f2111,plain,(
% 30.27/4.28 ![X0]: (~member(X0,ordered_pair(a,b))|X0=singleton_set(c)|X0=non_ordered_pair(c,d))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f329,f376])).
% 30.27/4.28 fof(f2179,plain,(
% 30.27/4.28 ![X0]: (~member(X0,non_ordered_pair(a,b))|X0=f2(ordered_pair(a,b))|singleton_set(f2(ordered_pair(a,b)))=singleton_set(a))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f2095,f368])).
% 30.27/4.28 fof(f2248,plain,(
% 30.27/4.28 a=f2(ordered_pair(a,b))|singleton_set(f2(ordered_pair(a,b)))=singleton_set(a)|~little_set(a)),
% 30.27/4.28 inference(resolution,[status(thm)],[f2179,f331])).
% 30.27/4.28 fof(f2251,plain,(
% 30.27/4.28 a=f2(ordered_pair(a,b))|singleton_set(f2(ordered_pair(a,b)))=singleton_set(a)),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f2248,f325])).
% 30.27/4.28 fof(f2263,plain,(
% 30.27/4.28 singleton_set(c)=singleton_set(f2(ordered_pair(a,b)))|singleton_set(c)=non_ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b)))),
% 30.27/4.28 inference(resolution,[status(thm)],[f2110,f983])).
% 30.27/4.28 fof(f2528,plain,(
% 30.27/4.28 member(f2(ordered_pair(a,b)),singleton_set(a))|~little_set(f2(ordered_pair(a,b)))|a=f2(ordered_pair(a,b))),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f2251,f365])).
% 30.27/4.28 fof(f2536,plain,(
% 30.27/4.28 ~little_set(f2(ordered_pair(a,b)))|a=f2(ordered_pair(a,b))),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f2528,f368])).
% 30.27/4.28 fof(f2544,plain,(
% 30.27/4.28 a=f2(ordered_pair(a,b))),
% 30.27/4.28 inference(resolution,[status(thm)],[f2536,f1668])).
% 30.27/4.28 fof(f2630,plain,(
% 30.27/4.28 singleton_set(c)=singleton_set(f2(ordered_pair(a,b)))|singleton_set(c)=non_ordered_pair(a,f3(ordered_pair(a,b)))),
% 30.27/4.28 inference(backward_demodulation,[status(thm)],[f2544,f2263])).
% 30.27/4.28 fof(f2797,plain,(
% 30.27/4.28 singleton_set(c)=singleton_set(a)|singleton_set(c)=non_ordered_pair(a,f3(ordered_pair(a,b)))),
% 30.27/4.28 inference(forward_demodulation,[status(thm)],[f2544,f2630])).
% 30.27/4.28 fof(f4550,plain,(
% 30.27/4.28 member(a,singleton_set(c))|~little_set(a)|singleton_set(c)=singleton_set(a)),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f2797,f331])).
% 30.27/4.28 fof(f4556,plain,(
% 30.27/4.28 member(a,singleton_set(c))|singleton_set(c)=singleton_set(a)),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f4550,f325])).
% 30.27/4.28 fof(f4557,plain,(
% 30.27/4.28 singleton_set(c)=singleton_set(a)|a=c),
% 30.27/4.28 inference(resolution,[status(thm)],[f4556,f368])).
% 30.27/4.28 fof(f4578,plain,(
% 30.27/4.28 member(c,singleton_set(a))|~little_set(c)|a=c),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f4557,f365])).
% 30.27/4.28 fof(f4585,plain,(
% 30.27/4.28 ~little_set(c)|a=c),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f4578,f368])).
% 30.27/4.28 fof(f4663,plain,(
% 30.27/4.28 a=c),
% 30.27/4.28 inference(resolution,[status(thm)],[f4585,f327])).
% 30.27/4.28 fof(f4704,plain,(
% 30.27/4.28 ![X0]: (~member(X0,ordered_pair(a,b))|X0=singleton_set(c)|X0=non_ordered_pair(a,d))),
% 30.27/4.28 inference(backward_demodulation,[status(thm)],[f4663,f2111])).
% 30.27/4.28 fof(f4706,plain,(
% 30.27/4.28 non_ordered_pair(c,d)=singleton_set(a)|non_ordered_pair(a,d)=non_ordered_pair(a,b)),
% 30.27/4.28 inference(backward_demodulation,[status(thm)],[f4663,f2092])).
% 30.27/4.28 fof(f4748,plain,(
% 30.27/4.28 ![X0]: (~member(X0,ordered_pair(a,b))|X0=singleton_set(a)|X0=non_ordered_pair(a,d))),
% 30.27/4.28 inference(forward_demodulation,[status(thm)],[f4663,f4704])).
% 30.27/4.28 fof(f4749,plain,(
% 30.27/4.28 non_ordered_pair(a,d)=singleton_set(a)|non_ordered_pair(a,d)=non_ordered_pair(a,b)),
% 30.27/4.28 inference(forward_demodulation,[status(thm)],[f4663,f4706])).
% 30.27/4.28 fof(f4987,plain,(
% 30.27/4.28 non_ordered_pair(a,b)=singleton_set(a)|non_ordered_pair(a,b)=non_ordered_pair(a,d)),
% 30.27/4.28 inference(resolution,[status(thm)],[f4748,f379])).
% 30.27/4.28 fof(f5019,plain,(
% 30.27/4.28 member(d,non_ordered_pair(a,b))|~little_set(d)|non_ordered_pair(a,d)=singleton_set(a)),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f4749,f332])).
% 30.27/4.28 fof(f5026,plain,(
% 30.27/4.28 member(d,non_ordered_pair(a,b))|non_ordered_pair(a,d)=singleton_set(a)),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f5019,f328])).
% 30.27/4.28 fof(f5027,plain,(
% 30.27/4.28 non_ordered_pair(a,d)=singleton_set(a)|d=a|d=b),
% 30.27/4.28 inference(resolution,[status(thm)],[f5026,f154])).
% 30.27/4.28 fof(f5029,plain,(
% 30.27/4.28 non_ordered_pair(a,d)=singleton_set(a)|d=a),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f5027,f330])).
% 30.27/4.28 fof(f5039,plain,(
% 30.27/4.28 member(d,singleton_set(a))|~little_set(d)|d=a),
% 30.27/4.28 inference(paramodulation,[status(thm)],[f5029,f332])).
% 30.27/4.28 fof(f5046,plain,(
% 30.27/4.28 ~little_set(d)|d=a),
% 30.27/4.28 inference(forward_subsumption_resolution,[status(thm)],[f5039,f368])).
% 30.27/4.28 fof(f5078,plain,(
% 30.27/4.28 d=a),
% 30.27/4.28 inference(resolution,[status(thm)],[f5046,f328])).
% 30.27/4.28 fof(f5119,plain,(
% 30.27/4.28 ~b=a),
% 30.27/4.28 inference(backward_demodulation,[status(thm)],[f5078,f330])).
% 30.27/4.28 fof(f5166,plain,(
% 30.27/4.28 non_ordered_pair(a,b)=singleton_set(a)|non_ordered_pair(a,b)=non_ordered_pair(a,a)),
% 30.27/4.28 inference(backward_demodulation,[status(thm)],[f5078,f4987])).
% 18.58/4.33 fof(f6164,plain,(
% 18.58/4.33 non_ordered_pair(a,b)=singleton_set(a)|non_ordered_pair(a,b)=singleton_set(a)),
% 18.58/4.33 inference(forward_demodulation,[status(thm)],[f160,f5166])).
% 18.58/4.33 fof(f6171,plain,(
% 18.58/4.33 non_ordered_pair(a,b)=singleton_set(a)),
% 18.58/4.33 inference(duplicate_literals_removal,[status(thm)],[f6164])).
% 18.58/4.33 fof(f8371,plain,(
% 18.58/4.33 member(b,singleton_set(a))|~little_set(b)),
% 18.58/4.33 inference(paramodulation,[status(thm)],[f6171,f332])).
% 18.58/4.33 fof(f8387,plain,(
% 18.58/4.33 member(b,singleton_set(a))),
% 18.58/4.33 inference(forward_subsumption_resolution,[status(thm)],[f8371,f326])).
% 18.58/4.33 fof(f8388,plain,(
% 18.58/4.33 b=a),
% 18.58/4.33 inference(resolution,[status(thm)],[f8387,f368])).
% 18.58/4.33 fof(f8390,plain,(
% 18.58/4.33 $false),
% 18.58/4.33 inference(forward_subsumption_resolution,[status(thm)],[f8388,f5119])).
% 18.58/4.33 % SZS output end CNFRefutation for theBenchmark.p
% 18.58/4.35 % Elapsed time: 3.986419 seconds
% 18.58/4.35 % CPU time: 31.292987 seconds
% 18.58/4.35 % Total memory used: 495.494 MB
% 18.58/4.35 % Net memory used: 463.182 MB
%------------------------------------------------------------------------------