%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM154-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 01:38:42 PM UTC 2026
% Result : Unsatisfiable 18.44s 3.19s
% Output : CNFRefutation 18.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of formulae : 70 ( 30 unt; 0 def)
% Number of atoms : 119 ( 26 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 95 ( 46 ~; 49 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 89 ( 89 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,X] :
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [Z,X,Y] :
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,Y] : complement(intersection(complement(X),complement(Y))) = union(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [X,Y] : intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))) = symmetric_difference(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X] : union(X,singleton(X)) = successor(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
! [X] :
( member(null_class,X)
| ~ inductive(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,axiom,
inductive(omega),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
successor(x) = null_class,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f161,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f164,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f172,plain,
! [Y] :
( ! [X] : member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f173,plain,
! [X0,X1] :
( member(X0,unordered_pair(X1,X0))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f172]) ).
fof(f175,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f187,plain,
! [Z,X] :
( member(Z,X)
| ! [Y] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f188,plain,
! [X0,X1,X2] :
( member(X0,X1)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f189,plain,
! [Z,Y] :
( member(Z,Y)
| ! [X] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f190,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f192,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f193,plain,
! [X0,X1] :
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f194,plain,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f195,plain,
! [X0,X1] : intersection(complement(intersection(X0,X1)),complement(intersection(complement(X0),complement(X1)))) = symmetric_difference(X0,X1),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f211,plain,
! [X0] : union(X0,singleton(X0)) = successor(X0),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f215,plain,
! [X0] :
( member(null_class,X0)
| ~ inductive(X0) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f218,plain,
inductive(omega),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f234,plain,
! [X0] :
( member(regular(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f347,plain,
successor(x) = null_class,
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f368,plain,
member(null_class,omega),
inference(resolution,[status(thm)],[f215,f218]) ).
fof(f369,plain,
! [X0] :
( member(null_class,X0)
| ~ subclass(omega,X0) ),
inference(resolution,[status(thm)],[f368,f161]) ).
fof(f395,plain,
! [X0,X1] :
( member(regular(X0),X1)
| ~ subclass(X0,X1)
| X0 = null_class ),
inference(resolution,[status(thm)],[f234,f161]) ).
fof(f399,plain,
! [X0,X1] :
( intersection(X0,X1) = null_class
| member(regular(intersection(X0,X1)),X0) ),
inference(resolution,[status(thm)],[f188,f234]) ).
fof(f417,plain,
! [X0] :
( complement(X0) = null_class
| ~ member(regular(complement(X0)),X0) ),
inference(resolution,[status(thm)],[f192,f234]) ).
fof(f428,plain,
! [X0,X1,X2] :
( member(X0,intersection(complement(X1),complement(X2)))
| member(X0,union(X1,X2))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f194,f193]) ).
fof(f437,plain,
! [X0,X1] : intersection(complement(intersection(X0,X1)),union(X0,X1)) = symmetric_difference(X0,X1),
inference(forward_demodulation,[status(thm)],[f194,f195]) ).
fof(f443,plain,
! [X0] : intersection(complement(intersection(X0,singleton(X0))),successor(X0)) = symmetric_difference(X0,singleton(X0)),
inference(paramodulation,[status(thm)],[f211,f437]) ).
fof(f501,plain,
member(null_class,universal_class),
inference(resolution,[status(thm)],[f369,f164]) ).
fof(f504,plain,
! [X0] : member(null_class,unordered_pair(X0,null_class)),
inference(resolution,[status(thm)],[f501,f173]) ).
fof(f511,plain,
member(null_class,singleton(null_class)),
inference(paramodulation,[status(thm)],[f175,f504]) ).
fof(f1426,plain,
! [X0] :
( member(regular(X0),universal_class)
| X0 = null_class ),
inference(resolution,[status(thm)],[f395,f164]) ).
fof(f1483,plain,
( complement(universal_class) = null_class
| complement(universal_class) = null_class ),
inference(resolution,[status(thm)],[f417,f1426]) ).
fof(f1491,plain,
complement(universal_class) = null_class,
inference(duplicate_literals_removal,[status(thm)],[f1483]) ).
fof(f1502,plain,
! [X0] :
( ~ member(X0,universal_class)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f1491,f192]) ).
fof(f2356,plain,
! [X0] :
( ~ member(regular(intersection(null_class,X0)),universal_class)
| intersection(null_class,X0) = null_class ),
inference(resolution,[status(thm)],[f399,f1502]) ).
fof(f2434,plain,
! [X0] : intersection(null_class,X0) = null_class,
inference(forward_subsumption_resolution,[status(thm)],[f2356,f1426]) ).
fof(f2495,plain,
intersection(complement(null_class),successor(null_class)) = symmetric_difference(null_class,singleton(null_class)),
inference(paramodulation,[status(thm)],[f2434,f443]) ).
fof(f2500,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f2434,f190]) ).
fof(f2579,plain,
! [X0] :
( member(X0,complement(null_class))
| ~ member(X0,symmetric_difference(null_class,singleton(null_class))) ),
inference(paramodulation,[status(thm)],[f2495,f188]) ).
fof(f2584,plain,
! [X0] :
( ~ member(X0,null_class)
| ~ member(X0,symmetric_difference(null_class,singleton(null_class))) ),
inference(resolution,[status(thm)],[f2579,f192]) ).
fof(f2749,plain,
! [X0] : ~ member(X0,null_class),
inference(backward_subsumption_resolution,[status(thm)],[f2584,f2500]) ).
fof(f4395,plain,
! [X0,X1] :
( member(X0,intersection(complement(X1),complement(singleton(X1))))
| member(X0,successor(X1))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f211,f428]) ).
fof(f4514,plain,
! [X0] :
( member(X0,intersection(complement(x),complement(singleton(x))))
| member(X0,null_class)
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f347,f4395]) ).
fof(f4527,plain,
! [X0] :
( member(X0,intersection(complement(x),complement(singleton(x))))
| ~ member(X0,universal_class) ),
inference(forward_subsumption_resolution,[status(thm)],[f4514,f2749]) ).
fof(f4644,plain,
! [X0] :
( member(X0,complement(singleton(x)))
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f4527,f190]) ).
fof(f4645,plain,
! [X0] :
( member(X0,complement(x))
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f4527,f188]) ).
fof(f4658,plain,
! [X0] :
( ~ member(X0,x)
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f4645,f192]) ).
fof(f4694,plain,
( x = null_class
| ~ member(regular(x),universal_class) ),
inference(resolution,[status(thm)],[f4658,f234]) ).
fof(f4697,plain,
x = null_class,
inference(forward_subsumption_resolution,[status(thm)],[f4694,f1426]) ).
fof(f4858,plain,
member(null_class,singleton(x)),
inference(backward_demodulation,[status(thm)],[f4697,f511]) ).
fof(f4864,plain,
member(x,universal_class),
inference(backward_demodulation,[status(thm)],[f4697,f501]) ).
fof(f4952,plain,
member(x,singleton(x)),
inference(forward_demodulation,[status(thm)],[f4697,f4858]) ).
fof(f6847,plain,
! [X0] :
( ~ member(X0,singleton(x))
| ~ member(X0,universal_class) ),
inference(resolution,[status(thm)],[f4644,f192]) ).
fof(f6918,plain,
~ member(x,universal_class),
inference(resolution,[status(thm)],[f6847,f4952]) ).
fof(f6925,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6918,f4864]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM154-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 % Computer : n001.cluster.edu
% 0.18/0.46 % Model : x86_64 x86_64
% 0.18/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.46 % Memory : 8046.5625MB
% 0.18/0.46 % OS : Linux 6.8.0-71-generic
% 0.18/0.46 % CPULimit : 300
% 0.18/0.46 % WCLimit : 300
% 0.18/0.46 % DateTime : Mon Sep 21 02:13:59 UTC 2026
% 0.18/0.47 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 18.44/3.19 % Refutation found
% 18.44/3.19 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 18.44/3.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.22/3.27 % Elapsed time: 2.788106 seconds
% 12.22/3.27 % CPU time: 21.523114 seconds
% 12.22/3.27 % Total memory used: 318.678 MB
% 12.22/3.27 % Net memory used: 301.608 MB
%------------------------------------------------------------------------------