%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM172-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:44 PM UTC 2026
% Result : Unsatisfiable 4.08s 1.38s
% Output : CNFRefutation 1.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 20
% Syntax : Number of formulae : 90 ( 26 unt; 0 def)
% Number of atoms : 176 ( 46 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 154 ( 68 ~; 86 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-2 aty)
% Number of variables : 128 ( 128 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,U] :
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X] : subclass(X,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X,Y] :
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : unordered_pair(X,X) = singleton(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U,V,X,Y] :
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U,X,V,Y] :
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [Z,X,Y] :
( ordered_pair(first(Z),second(Z)) = Z
| ~ member(Z,cross_product(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [Z,X,Y] :
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [Z,X,Y] :
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [Z,X] :
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [Z,X] :
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X,Y] : complement(intersection(complement(X),complement(Y))) = union(X,Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [X] : union(X,singleton(X)) = successor(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [X,Y] :
( member(ordered_pair(X,Y),successor_relation)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
| successor(X) != Y ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
! [X] :
( member(regular(X),X)
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
! [X] :
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
member(x,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f160,negated_conjecture,
successor(x) = x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,plain,
! [Y,U] :
( member(U,Y)
| ! [X] :
( ~ member(U,X)
| ~ subclass(X,Y) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f162,plain,
! [X0,X1,X2] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f165,plain,
! [X0] : subclass(X0,universal_class),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f169,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,unordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f170,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,unordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
! [X] :
( ! [Y] : member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f172,plain,
! [X0,X1] :
( member(X0,unordered_pair(X0,X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f176,plain,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f180,plain,
! [V,Y] :
( member(V,Y)
| ! [U,X] : ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f181,plain,
! [X0,X1,X2,X3] :
( member(X1,X3)
| ~ member(ordered_pair(X0,X1),cross_product(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f180]) ).
fof(f182,plain,
! [X0,X1,X2,X3] :
( member(ordered_pair(X0,X2),cross_product(X1,X3))
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f183,plain,
! [Z] :
( ordered_pair(first(Z),second(Z)) = Z
| ! [X,Y] : ~ member(Z,cross_product(X,Y)) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f184,plain,
! [X0,X1,X2] :
( ordered_pair(first(X0),second(X0)) = X0
| ~ member(X0,cross_product(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f190,plain,
! [Z,Y] :
( member(Z,Y)
| ! [X] : ~ member(Z,intersection(X,Y)) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f191,plain,
! [X0,X1,X2] :
( member(X0,X2)
| ~ member(X0,intersection(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f190]) ).
fof(f192,plain,
! [X0,X1,X2] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f193,plain,
! [X0,X1] :
( ~ member(X0,X1)
| ~ member(X0,complement(X1)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f194,plain,
! [X0,X1] :
( member(X0,X1)
| member(X0,complement(X1))
| ~ member(X0,universal_class) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f195,plain,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f212,plain,
! [X0] : union(X0,singleton(X0)) = successor(X0),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f213,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f215,plain,
! [X0,X1] :
( member(ordered_pair(X0,X1),successor_relation)
| ~ member(ordered_pair(X0,X1),cross_product(universal_class,universal_class))
| successor(X0) != X1 ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f235,plain,
! [X0] :
( member(regular(X0),X0)
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f236,plain,
! [X0] :
( intersection(X0,regular(X0)) = null_class
| X0 = null_class ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f348,plain,
member(x,universal_class),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f349,plain,
successor(x) = x,
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f353,plain,
! [X0] :
( member(ordered_pair(X0,successor(X0)),successor_relation)
| ~ member(ordered_pair(X0,successor(X0)),cross_product(universal_class,universal_class)) ),
inference(destructive_equality_resolution,[status(thm)],[f215]) ).
fof(f359,plain,
( member(ordered_pair(x,successor(x)),successor_relation)
| ~ member(ordered_pair(x,x),cross_product(universal_class,universal_class)) ),
inference(paramodulation,[status(thm)],[f349,f353]) ).
fof(f360,plain,
( member(ordered_pair(x,x),successor_relation)
| ~ member(ordered_pair(x,x),cross_product(universal_class,universal_class)) ),
inference(forward_demodulation,[status(thm)],[f349,f359]) ).
fof(f362,plain,
! [X0,X1] :
( member(X0,universal_class)
| ~ member(X0,X1) ),
inference(resolution,[status(thm)],[f165,f162]) ).
fof(f383,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f176,f170]) ).
fof(f384,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f383]) ).
fof(f386,plain,
! [X0] :
( member(X0,singleton(X0))
| ~ member(X0,universal_class) ),
inference(paramodulation,[status(thm)],[f176,f172]) ).
fof(f389,plain,
! [X0] :
( singleton(X0) = null_class
| regular(singleton(X0)) = X0 ),
inference(resolution,[status(thm)],[f384,f235]) ).
fof(f398,plain,
! [X0] :
( complement(X0) = null_class
| ~ member(regular(complement(X0)),X0) ),
inference(resolution,[status(thm)],[f193,f235]) ).
fof(f402,plain,
! [X0] :
( member(X0,cross_product(universal_class,universal_class))
| ~ member(X0,successor_relation) ),
inference(resolution,[status(thm)],[f213,f162]) ).
fof(f451,plain,
! [X0] :
( singleton(X0) = null_class
| intersection(singleton(X0),X0) = null_class
| singleton(X0) = null_class ),
inference(paramodulation,[status(thm)],[f389,f236]) ).
fof(f453,plain,
! [X0] :
( intersection(singleton(X0),X0) = null_class
| singleton(X0) = null_class ),
inference(duplicate_literals_removal,[status(thm)],[f451]) ).
fof(f458,plain,
( member(ordered_pair(x,x),successor_relation)
| ~ member(x,universal_class)
| ~ member(x,universal_class) ),
inference(resolution,[status(thm)],[f182,f360]) ).
fof(f462,plain,
( member(ordered_pair(x,x),successor_relation)
| ~ member(x,universal_class) ),
inference(duplicate_literals_removal,[status(thm)],[f458]) ).
fof(f463,plain,
member(ordered_pair(x,x),successor_relation),
inference(forward_subsumption_resolution,[status(thm)],[f462,f348]) ).
fof(f662,plain,
! [X0] :
( ~ member(regular(complement(universal_class)),X0)
| complement(universal_class) = null_class ),
inference(resolution,[status(thm)],[f398,f362]) ).
fof(f715,plain,
! [X0,X1] :
( singleton(X1) = null_class
| member(X0,null_class)
| ~ member(X0,X1)
| ~ member(X0,singleton(X1)) ),
inference(paramodulation,[status(thm)],[f453,f192]) ).
fof(f908,plain,
member(ordered_pair(x,x),cross_product(universal_class,universal_class)),
inference(resolution,[status(thm)],[f402,f463]) ).
fof(f939,plain,
ordered_pair(first(ordered_pair(x,x)),second(ordered_pair(x,x))) = ordered_pair(x,x),
inference(resolution,[status(thm)],[f908,f184]) ).
fof(f950,plain,
! [X0,X1] :
( member(second(ordered_pair(x,x)),X1)
| ~ member(ordered_pair(x,x),cross_product(X0,X1)) ),
inference(paramodulation,[status(thm)],[f939,f181]) ).
fof(f978,plain,
! [X0,X1] :
( ~ member(x,X0)
| ~ member(x,X1)
| member(second(ordered_pair(x,x)),X0) ),
inference(resolution,[status(thm)],[f950,f182]) ).
fof(f982,plain,
! [X0] :
( ~ member(x,X0)
| member(second(ordered_pair(x,x)),X0) ),
inference(resolution,[status(thm)],[f978,f348]) ).
fof(f1005,plain,
! [X0] :
( member(x,X0)
| ~ member(x,universal_class)
| member(second(ordered_pair(x,x)),complement(X0)) ),
inference(resolution,[status(thm)],[f982,f194]) ).
fof(f1008,plain,
( ~ member(x,universal_class)
| member(second(ordered_pair(x,x)),singleton(x)) ),
inference(resolution,[status(thm)],[f982,f386]) ).
fof(f1015,plain,
! [X0] :
( member(x,X0)
| member(second(ordered_pair(x,x)),complement(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1005,f348]) ).
fof(f1016,plain,
member(second(ordered_pair(x,x)),singleton(x)),
inference(forward_subsumption_resolution,[status(thm)],[f1008,f348]) ).
fof(f1019,plain,
second(ordered_pair(x,x)) = x,
inference(resolution,[status(thm)],[f1016,f384]) ).
fof(f1020,plain,
member(x,singleton(x)),
inference(backward_demodulation,[status(thm)],[f1019,f1016]) ).
fof(f1031,plain,
! [X0] :
( member(x,X0)
| member(x,complement(X0)) ),
inference(backward_demodulation,[status(thm)],[f1019,f1015]) ).
fof(f1068,plain,
! [X0,X1] :
( member(x,intersection(complement(X0),complement(X1)))
| member(x,union(X0,X1)) ),
inference(paramodulation,[status(thm)],[f195,f1031]) ).
fof(f1179,plain,
! [X0,X1] :
( member(x,complement(X1))
| member(x,union(X0,X1)) ),
inference(resolution,[status(thm)],[f1068,f191]) ).
fof(f1198,plain,
! [X0] :
( member(x,complement(singleton(X0)))
| member(x,successor(X0)) ),
inference(paramodulation,[status(thm)],[f212,f1179]) ).
fof(f1210,plain,
! [X0] :
( ~ member(x,singleton(X0))
| member(x,successor(X0)) ),
inference(resolution,[status(thm)],[f1198,f193]) ).
fof(f1215,plain,
( ~ member(x,singleton(x))
| member(x,x) ),
inference(paramodulation,[status(thm)],[f349,f1210]) ).
fof(f1217,plain,
member(x,x),
inference(forward_subsumption_resolution,[status(thm)],[f1215,f1020]) ).
fof(f1897,plain,
( complement(universal_class) = null_class
| complement(universal_class) = null_class ),
inference(resolution,[status(thm)],[f662,f235]) ).
fof(f1937,plain,
complement(universal_class) = null_class,
inference(duplicate_literals_removal,[status(thm)],[f1897]) ).
fof(f1956,plain,
! [X0] :
( ~ member(X0,universal_class)
| ~ member(X0,null_class) ),
inference(paramodulation,[status(thm)],[f1937,f193]) ).
fof(f1958,plain,
! [X0,X1] :
( singleton(X1) = null_class
| ~ member(X0,X1)
| ~ member(X0,singleton(X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f715,f1960]) ).
fof(f1960,plain,
! [X0] : ~ member(X0,null_class),
inference(forward_subsumption_resolution,[status(thm)],[f1956,f362]) ).
fof(f2651,plain,
( singleton(x) = null_class
| ~ member(x,x) ),
inference(resolution,[status(thm)],[f1958,f1020]) ).
fof(f2674,plain,
member(x,null_class),
inference(backward_demodulation,[status(thm)],[f2717,f1020]) ).
fof(f2717,plain,
singleton(x) = null_class,
inference(forward_subsumption_resolution,[status(thm)],[f2651,f1217]) ).
fof(f2739,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2674,f1960]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM172-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.65 % Computer : n004.cluster.edu
% 0.19/0.65 % Model : x86_64 x86_64
% 0.19/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.65 % Memory : 8046.5625MB
% 0.19/0.65 % OS : Linux 6.8.0-71-generic
% 0.19/0.65 % CPULimit : 300
% 0.19/0.65 % WCLimit : 300
% 0.19/0.65 % DateTime : Mon Sep 21 02:09:36 UTC 2026
% 0.19/0.66 % CPUTime :
% 0.19/0.68 % Drodi V4.1.1
% 4.08/1.38 % Refutation found
% 4.08/1.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.08/1.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.43/1.41 % Elapsed time: 0.743212 seconds
% 1.43/1.41 % CPU time: 4.812094 seconds
% 1.43/1.41 % Total memory used: 228.238 MB
% 1.43/1.41 % Net memory used: 220.095 MB
%------------------------------------------------------------------------------