%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET018-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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:08:54 PM UTC 2026
% Result : Unsatisfiable 284.88s 36.32s
% Output : CNFRefutation 136.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 21
% Syntax : Number of formulae : 115 ( 41 unt; 0 def)
% Number of atoms : 235 ( 80 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 213 ( 93 ~; 120 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 114 ( 114 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( little_set(X)
| ~ member(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [U,X,Y] :
( U != X
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [U,X,Y] :
( U != Y
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : little_set(non_ordered_pair(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : singleton_set(X) = non_ordered_pair(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : ordered_pair(X,Y) = non_ordered_pair(singleton_set(X),non_ordered_pair(X,Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X] :
( little_set(f2(X))
| ~ ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] :
( little_set(f3(X))
| ~ ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] :
( X = ordered_pair(f2(X),f3(X))
| ~ ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [X,Y,Z] :
( X != ordered_pair(Y,Z)
| ~ little_set(Z)
| ~ little_set(Y)
| ordered_pair_predicate(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [Z,X,U,V] :
( ~ member(Z,U)
| X != ordered_pair(U,V)
| ~ little_set(V)
| ~ little_set(U)
| member(Z,first(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [X,Y] :
( member(f17(X,Y),X)
| subset(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [X,Y] :
( ~ member(f17(X,Y),Y)
| subset(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [Z,X] :
( ~ subset(Z,X)
| ~ little_set(Z)
| member(Z,powerset(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,hypothesis,
little_set(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,hypothesis,
little_set(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,hypothesis,
little_set(c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,hypothesis,
little_set(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,hypothesis,
ordered_pair(a,b) = ordered_pair(c,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,negated_conjecture,
b != d,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,plain,
! [X] :
( little_set(X)
| ! [Y] : ~ member(X,Y) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f149,plain,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f153,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,non_ordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f154,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f155,plain,
! [U,X] :
( U != X
| ~ little_set(U)
| ! [Y] : member(U,non_ordered_pair(X,Y)) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f156,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [U,Y] :
( U != Y
| ~ little_set(U)
| ! [X] : member(U,non_ordered_pair(X,Y)) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f158,plain,
! [X0,X1,X2] :
( X0 != X2
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f160,plain,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f161,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f162,plain,
! [X0] :
( little_set(f2(X0))
| ~ ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f163,plain,
! [X0] :
( little_set(f3(X0))
| ~ ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f164,plain,
! [X0] :
( X0 = ordered_pair(f2(X0),f3(X0))
| ~ ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f165,plain,
! [X0,X1,X2] :
( X0 != ordered_pair(X1,X2)
| ~ little_set(X2)
| ~ little_set(X1)
| ordered_pair_predicate(X0) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f170,plain,
! [Z,U] :
( ~ member(Z,U)
| ! [X,V] :
( X != ordered_pair(U,V)
| ~ little_set(V)
| ~ little_set(U)
| member(Z,first(X)) ) ),
inference(miniscoping,[status(thm)],[f19]) ).
fof(f171,plain,
! [X0,X1,X2,X3] :
( ~ member(X0,X2)
| X1 != ordered_pair(X2,X3)
| ~ little_set(X3)
| ~ little_set(X2)
| member(X0,first(X1)) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f234,plain,
! [X0,X1] :
( member(f17(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f235,plain,
! [X0,X1] :
( ~ member(f17(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f240,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| ~ little_set(X0)
| member(X0,powerset(X1)) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f325,plain,
little_set(a),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f326,plain,
little_set(b),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f327,plain,
little_set(c),
inference(cnf_transformation,[status(thm)],[f144]) ).
fof(f328,plain,
little_set(d),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f329,plain,
ordered_pair(a,b) = ordered_pair(c,d),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f330,plain,
b != d,
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f331,plain,
! [X0,X1] :
( ~ little_set(X0)
| member(X0,non_ordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f156]) ).
fof(f332,plain,
! [X0,X1] :
( ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X0)) ),
inference(destructive_equality_resolution,[status(thm)],[f158]) ).
fof(f333,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| ordered_pair_predicate(ordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f165]) ).
fof(f334,plain,
! [X0,X1,X2] :
( ~ member(X0,X1)
| ~ little_set(X2)
| ~ little_set(X1)
| member(X0,first(ordered_pair(X1,X2))) ),
inference(destructive_equality_resolution,[status(thm)],[f171]) ).
fof(f348,plain,
! [X0] : little_set(singleton_set(X0)),
inference(paramodulation,[status(thm)],[f160,f159]) ).
fof(f378,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton_set(X1)) ),
inference(paramodulation,[status(thm)],[f160,f154]) ).
fof(f379,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton_set(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f378]) ).
fof(f382,plain,
! [X0] :
( ~ little_set(X0)
| member(X0,singleton_set(X0)) ),
inference(paramodulation,[status(thm)],[f160,f331]) ).
fof(f426,plain,
! [X0,X1] :
( ~ little_set(non_ordered_pair(X0,X1))
| member(non_ordered_pair(X0,X1),ordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f161,f332]) ).
fof(f427,plain,
! [X0,X1] :
( ~ little_set(singleton_set(X0))
| member(singleton_set(X0),ordered_pair(X0,X1)) ),
inference(paramodulation,[status(thm)],[f161,f331]) ).
fof(f428,plain,
! [X0,X1,X2] :
( X0 = non_ordered_pair(X1,X2)
| X0 = singleton_set(X1)
| ~ member(X0,ordered_pair(X1,X2)) ),
inference(paramodulation,[status(thm)],[f161,f154]) ).
fof(f431,plain,
! [X0,X1] : member(non_ordered_pair(X0,X1),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f426,f159]) ).
fof(f432,plain,
! [X0,X1] : member(singleton_set(X0),ordered_pair(X0,X1)),
inference(forward_subsumption_resolution,[status(thm)],[f427,f348]) ).
fof(f737,plain,
( ~ little_set(d)
| ~ little_set(c)
| ordered_pair_predicate(ordered_pair(a,b)) ),
inference(paramodulation,[status(thm)],[f329,f333]) ).
fof(f738,plain,
member(non_ordered_pair(c,d),ordered_pair(a,b)),
inference(paramodulation,[status(thm)],[f329,f431]) ).
fof(f739,plain,
member(singleton_set(c),ordered_pair(a,b)),
inference(paramodulation,[status(thm)],[f329,f432]) ).
fof(f744,plain,
( ~ little_set(d)
| ordered_pair_predicate(ordered_pair(a,b)) ),
inference(forward_subsumption_resolution,[status(thm)],[f737,f327]) ).
fof(f795,plain,
ordered_pair_predicate(ordered_pair(a,b)),
inference(forward_subsumption_resolution,[status(thm)],[f744,f328]) ).
fof(f796,plain,
ordered_pair(a,b) = ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b))),
inference(resolution,[status(thm)],[f795,f164]) ).
fof(f799,plain,
! [X0] :
( ~ member(X0,f2(ordered_pair(a,b)))
| ~ little_set(f3(ordered_pair(a,b)))
| ~ little_set(f2(ordered_pair(a,b)))
| member(X0,first(ordered_pair(a,b))) ),
inference(paramodulation,[status(thm)],[f796,f334]) ).
fof(f802,plain,
member(singleton_set(f2(ordered_pair(a,b))),ordered_pair(a,b)),
inference(paramodulation,[status(thm)],[f796,f432]) ).
fof(f836,plain,
! [X0] :
( ~ ordered_pair_predicate(ordered_pair(a,b))
| ~ member(X0,f2(ordered_pair(a,b)))
| ~ little_set(f2(ordered_pair(a,b)))
| member(X0,first(ordered_pair(a,b))) ),
inference(resolution,[status(thm)],[f799,f163]) ).
fof(f838,plain,
! [X0] :
( ~ ordered_pair_predicate(ordered_pair(a,b))
| ~ member(X0,f2(ordered_pair(a,b)))
| member(X0,first(ordered_pair(a,b))) ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f162]) ).
fof(f839,plain,
! [X0] :
( ~ member(X0,f2(ordered_pair(a,b)))
| member(X0,first(ordered_pair(a,b))) ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f795]) ).
fof(f840,plain,
! [X0] :
( subset(X0,first(ordered_pair(a,b)))
| ~ member(f17(X0,first(ordered_pair(a,b))),f2(ordered_pair(a,b))) ),
inference(resolution,[status(thm)],[f839,f235]) ).
fof(f1010,plain,
( subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b)))
| subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b))) ),
inference(resolution,[status(thm)],[f840,f234]) ).
fof(f1011,plain,
subset(f2(ordered_pair(a,b)),first(ordered_pair(a,b))),
inference(duplicate_literals_removal,[status(thm)],[f1010]) ).
fof(f1012,plain,
( ~ little_set(f2(ordered_pair(a,b)))
| member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b)))) ),
inference(resolution,[status(thm)],[f1011,f240]) ).
fof(f1015,plain,
( ~ ordered_pair_predicate(ordered_pair(a,b))
| member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b)))) ),
inference(resolution,[status(thm)],[f1012,f162]) ).
fof(f1017,plain,
member(f2(ordered_pair(a,b)),powerset(first(ordered_pair(a,b)))),
inference(forward_subsumption_resolution,[status(thm)],[f1015,f795]) ).
fof(f1021,plain,
little_set(f2(ordered_pair(a,b))),
inference(resolution,[status(thm)],[f1017,f149]) ).
fof(f6525,plain,
( singleton_set(f2(ordered_pair(a,b))) = non_ordered_pair(a,b)
| singleton_set(f2(ordered_pair(a,b))) = singleton_set(a) ),
inference(resolution,[status(thm)],[f428,f802]) ).
fof(f6554,plain,
! [X0] :
( X0 = non_ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b)))
| X0 = singleton_set(f2(ordered_pair(a,b)))
| ~ member(X0,ordered_pair(a,b)) ),
inference(paramodulation,[status(thm)],[f796,f428]) ).
fof(f6676,plain,
! [X0] :
( singleton_set(f2(ordered_pair(a,b))) = singleton_set(a)
| X0 = f2(ordered_pair(a,b))
| ~ member(X0,non_ordered_pair(a,b)) ),
inference(paramodulation,[status(thm)],[f6525,f379]) ).
fof(f6731,plain,
( ~ little_set(a)
| singleton_set(f2(ordered_pair(a,b))) = singleton_set(a)
| a = f2(ordered_pair(a,b)) ),
inference(resolution,[status(thm)],[f6676,f331]) ).
fof(f6734,plain,
( singleton_set(f2(ordered_pair(a,b))) = singleton_set(a)
| a = f2(ordered_pair(a,b)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6731,f325]) ).
fof(f6887,plain,
( a = f2(ordered_pair(a,b))
| ~ little_set(f2(ordered_pair(a,b)))
| member(f2(ordered_pair(a,b)),singleton_set(a)) ),
inference(paramodulation,[status(thm)],[f6734,f382]) ).
fof(f6907,plain,
( a = f2(ordered_pair(a,b))
| ~ little_set(f2(ordered_pair(a,b))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6887,f379]) ).
fof(f7102,plain,
a = f2(ordered_pair(a,b)),
inference(forward_subsumption_resolution,[status(thm)],[f6907,f1021]) ).
fof(f7185,plain,
! [X0] :
( X0 = non_ordered_pair(f2(ordered_pair(a,b)),f3(ordered_pair(a,b)))
| X0 = singleton_set(a)
| ~ member(X0,ordered_pair(a,b)) ),
inference(forward_demodulation,[status(thm)],[f7102,f6554]) ).
fof(f7186,plain,
! [X0] :
( X0 = non_ordered_pair(a,f3(ordered_pair(a,b)))
| X0 = singleton_set(a)
| ~ member(X0,ordered_pair(a,b)) ),
inference(forward_demodulation,[status(thm)],[f7102,f7185]) ).
fof(f7200,plain,
( singleton_set(c) = non_ordered_pair(a,f3(ordered_pair(a,b)))
| singleton_set(c) = singleton_set(a) ),
inference(resolution,[status(thm)],[f7186,f739]) ).
fof(f8169,plain,
( singleton_set(c) = singleton_set(a)
| ~ little_set(a)
| member(a,singleton_set(c)) ),
inference(paramodulation,[status(thm)],[f7200,f331]) ).
fof(f8176,plain,
( singleton_set(c) = singleton_set(a)
| member(a,singleton_set(c)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8169,f325]) ).
fof(f8177,plain,
( a = c
| singleton_set(c) = singleton_set(a) ),
inference(resolution,[status(thm)],[f8176,f379]) ).
fof(f8211,plain,
( a = c
| ~ little_set(c)
| member(c,singleton_set(a)) ),
inference(paramodulation,[status(thm)],[f8177,f382]) ).
fof(f8227,plain,
( a = c
| ~ little_set(c) ),
inference(forward_subsumption_resolution,[status(thm)],[f8211,f379]) ).
fof(f8235,plain,
member(non_ordered_pair(a,d),ordered_pair(a,b)),
inference(backward_demodulation,[status(thm)],[f8240,f738]) ).
fof(f8238,plain,
ordered_pair(a,b) = ordered_pair(a,d),
inference(backward_demodulation,[status(thm)],[f8240,f329]) ).
fof(f8240,plain,
a = c,
inference(forward_subsumption_resolution,[status(thm)],[f8227,f327]) ).
fof(f8266,plain,
( non_ordered_pair(a,d) = non_ordered_pair(a,b)
| non_ordered_pair(a,d) = singleton_set(a) ),
inference(resolution,[status(thm)],[f8235,f428]) ).
fof(f9556,plain,
( non_ordered_pair(a,d) = singleton_set(a)
| ~ little_set(d)
| member(d,non_ordered_pair(a,b)) ),
inference(paramodulation,[status(thm)],[f8266,f332]) ).
fof(f9564,plain,
( non_ordered_pair(a,d) = singleton_set(a)
| member(d,non_ordered_pair(a,b)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9556,f328]) ).
fof(f9565,plain,
( d = b
| d = a
| non_ordered_pair(a,d) = singleton_set(a) ),
inference(resolution,[status(thm)],[f9564,f154]) ).
fof(f9567,plain,
( d = a
| non_ordered_pair(a,d) = singleton_set(a) ),
inference(forward_subsumption_resolution,[status(thm)],[f9565,f330]) ).
fof(f9580,plain,
( d = a
| ~ little_set(d)
| member(d,singleton_set(a)) ),
inference(paramodulation,[status(thm)],[f9567,f332]) ).
fof(f9593,plain,
( d = a
| ~ little_set(d) ),
inference(forward_subsumption_resolution,[status(thm)],[f9580,f379]) ).
fof(f9605,plain,
ordered_pair(a,b) = ordered_pair(a,a),
inference(backward_demodulation,[status(thm)],[f9612,f8238]) ).
fof(f9611,plain,
b != a,
inference(backward_demodulation,[status(thm)],[f9612,f330]) ).
fof(f9612,plain,
d = a,
inference(forward_subsumption_resolution,[status(thm)],[f9593,f328]) ).
fof(f9738,plain,
member(non_ordered_pair(a,b),ordered_pair(a,a)),
inference(paramodulation,[status(thm)],[f9605,f431]) ).
fof(f10058,plain,
( non_ordered_pair(a,b) = non_ordered_pair(a,a)
| non_ordered_pair(a,b) = singleton_set(a) ),
inference(resolution,[status(thm)],[f9738,f428]) ).
fof(f10061,plain,
( non_ordered_pair(a,b) = singleton_set(a)
| non_ordered_pair(a,b) = singleton_set(a) ),
inference(forward_demodulation,[status(thm)],[f160,f10058]) ).
fof(f10062,plain,
non_ordered_pair(a,b) = singleton_set(a),
inference(duplicate_literals_removal,[status(thm)],[f10061]) ).
fof(f10072,plain,
( ~ little_set(b)
| member(b,singleton_set(a)) ),
inference(paramodulation,[status(thm)],[f10062,f332]) ).
fof(f10094,plain,
member(b,singleton_set(a)),
inference(forward_subsumption_resolution,[status(thm)],[f10072,f326]) ).
fof(f10103,plain,
b = a,
inference(resolution,[status(thm)],[f10094,f379]) ).
fof(f10105,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10103,f9611]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET018-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.36 % Computer : n020.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 04:43:47 UTC 2026
% 0.14/0.37 % CPUTime :
% 0.14/0.39 % Drodi V4.1.1
% 284.88/36.32 % Refutation found
% 284.88/36.32 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 284.88/36.32 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 136.80/36.50 % Elapsed time: 36.110297 seconds
% 136.80/36.50 % CPU time: 286.019562 seconds
% 136.80/36.50 % Total memory used: 967.520 MB
% 136.80/36.50 % Net memory used: 885.530 MB
%------------------------------------------------------------------------------