%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM010-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 01:38:31 PM UTC 2026
% Result : Unsatisfiable 73.63s 9.80s
% Output : CNFRefutation 48.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of formulae : 105 ( 29 unt; 0 def)
% Number of atoms : 245 ( 61 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 238 ( 98 ~; 140 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 104 ( 104 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y] :
( little_set(X)
| ~ member(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y] :
( X = Y
| little_set(f1(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y] :
( X = Y
| member(f1(X,Y),Y)
| member(f1(X,Y),X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [U,X,Y] :
( U = Y
| U = X
| ~ member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [U,X,Y] :
( U != X
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X,Y] : little_set(non_ordered_pair(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : singleton_set(X) = non_ordered_pair(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [Z] : ~ member(Z,empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,axiom,
little_set(infinity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
member(empty_set,infinity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [X] :
( member(successor(X),infinity)
| ~ member(X,infinity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,axiom,
! [X] :
( member(f24(X),X)
| X = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [X] :
( member(f26(X),X)
| X = empty_set
| ~ little_set(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f166,axiom,
! [Z,Xs] :
( member(Z,Xs)
| member(f43(Z,Xs),Xs)
| ~ member(empty_set,Xs)
| ~ little_set(Xs)
| ~ member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,axiom,
! [Z,Xs] :
( member(Z,Xs)
| ~ member(successor(f43(Z,Xs)),Xs)
| ~ member(empty_set,Xs)
| ~ little_set(Xs)
| ~ member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,axiom,
! [Z] :
( little_set(f44(Z))
| ~ little_set(Z)
| member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,axiom,
! [Z] :
( member(empty_set,f44(Z))
| ~ little_set(Z)
| member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,axiom,
! [Z,Xk] :
( member(successor(Xk),f44(Z))
| ~ member(Xk,f44(Z))
| ~ little_set(Z)
| member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,axiom,
! [Z] :
( ~ member(Z,f44(Z))
| member(Z,natural_numbers) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f220,hypothesis,
member(f74,natural_numbers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f221,negated_conjecture,
~ member(successor(f74),natural_numbers),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f222,plain,
! [X] :
( little_set(X)
| ! [Y] : ~ member(X,Y) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f223,plain,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
! [X0,X1] :
( X0 = X1
| little_set(f1(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f225,plain,
! [X0,X1] :
( X0 = X1
| member(f1(X0,X1),X1)
| member(f1(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f227,plain,
! [U,Y] :
( U = Y
| ! [X] :
( U = X
| ~ member(U,non_ordered_pair(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f228,plain,
! [X0,X1,X2] :
( X0 = X2
| X0 = X1
| ~ member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f227]) ).
fof(f229,plain,
! [U,X] :
( U != X
| ~ little_set(U)
| ! [Y] : member(U,non_ordered_pair(X,Y)) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f230,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ little_set(X0)
| member(X0,non_ordered_pair(X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f233,plain,
! [X0,X1] : little_set(non_ordered_pair(X0,X1)),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f234,plain,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f296,plain,
! [X0] : ~ member(X0,empty_set),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f298,plain,
little_set(infinity),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f299,plain,
member(empty_set,infinity),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f300,plain,
! [X0] :
( member(successor(X0),infinity)
| ~ member(X0,infinity) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f342,plain,
! [X0] :
( member(f24(X0),X0)
| X0 = empty_set ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f345,plain,
! [X0] :
( member(f26(X0),X0)
| X0 = empty_set
| ~ little_set(X0) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f432,plain,
! [X0,X1] :
( member(X0,X1)
| member(f43(X0,X1),X1)
| ~ member(empty_set,X1)
| ~ little_set(X1)
| ~ member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f166]) ).
fof(f433,plain,
! [X0,X1] :
( member(X0,X1)
| ~ member(successor(f43(X0,X1)),X1)
| ~ member(empty_set,X1)
| ~ little_set(X1)
| ~ member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f434,plain,
! [X0] :
( little_set(f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f168]) ).
fof(f435,plain,
! [X0] :
( member(empty_set,f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f436,plain,
! [X0,X1] :
( member(successor(X1),f44(X0))
| ~ member(X1,f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f170]) ).
fof(f437,plain,
! [X0] :
( ~ member(X0,f44(X0))
| member(X0,natural_numbers) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f488,plain,
member(f74,natural_numbers),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f489,plain,
~ member(successor(f74),natural_numbers),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f490,plain,
! [X0,X1] :
( ~ little_set(X0)
| member(X0,non_ordered_pair(X0,X1)) ),
inference(destructive_equality_resolution,[status(thm)],[f230]) ).
fof(f509,plain,
! [X0] :
( X0 = empty_set
| member(f1(X0,empty_set),X0) ),
inference(resolution,[status(thm)],[f225,f296]) ).
fof(f513,plain,
! [X0] :
( ~ little_set(X0)
| member(X0,singleton_set(X0)) ),
inference(paramodulation,[status(thm)],[f234,f490]) ).
fof(f514,plain,
! [X0,X1] :
( X0 = X1
| X0 = X1
| ~ member(X0,singleton_set(X1)) ),
inference(paramodulation,[status(thm)],[f234,f228]) ).
fof(f515,plain,
! [X0] : little_set(singleton_set(X0)),
inference(paramodulation,[status(thm)],[f234,f233]) ).
fof(f516,plain,
! [X0,X1] :
( X0 = X1
| ~ member(X0,singleton_set(X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f514]) ).
fof(f541,plain,
! [X0] :
( f24(singleton_set(X0)) = X0
| singleton_set(X0) = empty_set ),
inference(resolution,[status(thm)],[f342,f516]) ).
fof(f659,plain,
! [X0] :
( f1(singleton_set(X0),empty_set) = X0
| singleton_set(X0) = empty_set ),
inference(resolution,[status(thm)],[f509,f516]) ).
fof(f685,plain,
! [X0] :
( f24(singleton_set(X0)) = X0
| ~ little_set(X0)
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f541,f513]) ).
fof(f691,plain,
! [X0] :
( f24(singleton_set(X0)) = X0
| ~ little_set(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f685,f296]) ).
fof(f716,plain,
! [X0,X1] :
( ~ member(X0,X1)
| f24(singleton_set(X0)) = X0 ),
inference(resolution,[status(thm)],[f691,f223]) ).
fof(f783,plain,
! [X0] :
( f24(singleton_set(successor(X0))) = successor(X0)
| ~ member(X0,infinity) ),
inference(resolution,[status(thm)],[f300,f716]) ).
fof(f813,plain,
! [X0] :
( f26(singleton_set(X0)) = X0
| singleton_set(X0) = empty_set
| ~ little_set(singleton_set(X0)) ),
inference(resolution,[status(thm)],[f345,f516]) ).
fof(f821,plain,
! [X0] :
( f26(singleton_set(X0)) = X0
| singleton_set(X0) = empty_set ),
inference(forward_subsumption_resolution,[status(thm)],[f813,f515]) ).
fof(f838,plain,
! [X0] :
( f26(singleton_set(X0)) = X0
| ~ little_set(X0)
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f821,f513]) ).
fof(f845,plain,
! [X0] :
( f26(singleton_set(X0)) = X0
| ~ little_set(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f296]) ).
fof(f896,plain,
! [X0,X1] :
( ~ member(X0,X1)
| f26(singleton_set(X0)) = X0 ),
inference(resolution,[status(thm)],[f845,f223]) ).
fof(f925,plain,
! [X0] :
( ~ member(X0,infinity)
| f26(singleton_set(successor(X0))) = successor(X0) ),
inference(resolution,[status(thm)],[f896,f300]) ).
fof(f1555,plain,
! [X0] :
( f1(singleton_set(X0),empty_set) = X0
| ~ little_set(X0)
| member(X0,empty_set) ),
inference(paramodulation,[status(thm)],[f659,f513]) ).
fof(f1563,plain,
! [X0] :
( f1(singleton_set(X0),empty_set) = X0
| ~ little_set(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1555,f296]) ).
fof(f1619,plain,
! [X0,X1] :
( ~ member(X0,X1)
| f1(singleton_set(X0),empty_set) = X0 ),
inference(resolution,[status(thm)],[f1563,f223]) ).
fof(f1683,plain,
! [X0] :
( X0 = empty_set
| f1(singleton_set(f24(X0)),empty_set) = f24(X0) ),
inference(resolution,[status(thm)],[f1619,f342]) ).
fof(f2192,plain,
! [X0] :
( member(f74,X0)
| member(f43(f74,X0),X0)
| ~ member(empty_set,X0)
| ~ little_set(X0) ),
inference(resolution,[status(thm)],[f432,f488]) ).
fof(f2201,plain,
! [X0] :
( member(f74,X0)
| ~ member(successor(f43(f74,X0)),X0)
| ~ member(empty_set,X0)
| ~ little_set(X0) ),
inference(resolution,[status(thm)],[f433,f488]) ).
fof(f2205,plain,
( member(f74,infinity)
| member(f43(f74,infinity),infinity)
| ~ little_set(infinity) ),
inference(resolution,[status(thm)],[f2192,f299]) ).
fof(f2227,plain,
( member(f74,infinity)
| member(f43(f74,infinity),infinity) ),
inference(forward_subsumption_resolution,[status(thm)],[f2205,f298]) ).
fof(f2236,plain,
( ~ member(f43(f74,infinity),infinity)
| member(f74,infinity)
| ~ member(empty_set,infinity)
| ~ little_set(infinity) ),
inference(resolution,[status(thm)],[f2201,f300]) ).
fof(f2250,plain,
( ~ member(f43(f74,infinity),infinity)
| member(f74,infinity)
| ~ member(empty_set,infinity) ),
inference(forward_subsumption_resolution,[status(thm)],[f2236,f298]) ).
fof(f2251,plain,
member(f74,infinity),
inference(backward_subsumption_resolution,[status(thm)],[f2227,f2252]) ).
fof(f2252,plain,
( ~ member(f43(f74,infinity),infinity)
| member(f74,infinity) ),
inference(forward_subsumption_resolution,[status(thm)],[f2250,f299]) ).
fof(f2312,plain,
! [X0] :
( member(f74,f44(X0))
| ~ member(empty_set,f44(X0))
| ~ little_set(f44(X0))
| ~ member(f43(f74,f44(X0)),f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(resolution,[status(thm)],[f436,f2201]) ).
fof(f2313,plain,
! [X0] :
( member(successor(X0),natural_numbers)
| ~ member(X0,f44(successor(X0)))
| ~ little_set(successor(X0))
| member(successor(X0),natural_numbers) ),
inference(resolution,[status(thm)],[f436,f437]) ).
fof(f2317,plain,
! [X0] :
( member(f74,f44(X0))
| ~ member(empty_set,f44(X0))
| ~ little_set(f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(forward_subsumption_resolution,[status(thm)],[f2312,f2192]) ).
fof(f2318,plain,
! [X0] :
( ~ member(X0,f44(successor(X0)))
| ~ little_set(successor(X0))
| member(successor(X0),natural_numbers) ),
inference(duplicate_literals_removal,[status(thm)],[f2313]) ).
fof(f3024,plain,
! [X0] :
( member(f74,f44(X0))
| ~ member(empty_set,f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(forward_subsumption_resolution,[status(thm)],[f2317,f434]) ).
fof(f3025,plain,
! [X0] :
( ~ little_set(X0)
| member(X0,natural_numbers)
| member(f74,f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(resolution,[status(thm)],[f3024,f435]) ).
fof(f3026,plain,
! [X0] :
( member(f74,f44(X0))
| ~ little_set(X0)
| member(X0,natural_numbers) ),
inference(duplicate_literals_removal,[status(thm)],[f3025]) ).
fof(f3228,plain,
f24(singleton_set(successor(f74))) = successor(f74),
inference(resolution,[status(thm)],[f783,f2251]) ).
fof(f3679,plain,
f26(singleton_set(successor(f74))) = successor(f74),
inference(resolution,[status(thm)],[f925,f2251]) ).
fof(f4491,plain,
! [X0] :
( X0 = empty_set
| singleton_set(f24(X0)) = empty_set
| little_set(f24(X0)) ),
inference(paramodulation,[status(thm)],[f1683,f224]) ).
fof(f4609,plain,
( singleton_set(successor(f74)) = empty_set
| singleton_set(f24(singleton_set(successor(f74)))) = empty_set
| little_set(successor(f74)) ),
inference(paramodulation,[status(thm)],[f3228,f4491]) ).
fof(f4622,plain,
( singleton_set(successor(f74)) = empty_set
| singleton_set(successor(f74)) = empty_set
| little_set(successor(f74)) ),
inference(forward_demodulation,[status(thm)],[f3228,f4609]) ).
fof(f4623,plain,
( singleton_set(successor(f74)) = empty_set
| little_set(successor(f74)) ),
inference(duplicate_literals_removal,[status(thm)],[f4622]) ).
fof(f20605,plain,
( singleton_set(successor(f74)) = empty_set
| ~ member(f74,f44(successor(f74)))
| member(successor(f74),natural_numbers) ),
inference(resolution,[status(thm)],[f2318,f4623]) ).
fof(f20610,plain,
( singleton_set(successor(f74)) = empty_set
| ~ member(f74,f44(successor(f74))) ),
inference(forward_subsumption_resolution,[status(thm)],[f20605,f489]) ).
fof(f20628,plain,
( ~ little_set(successor(f74))
| member(successor(f74),natural_numbers)
| singleton_set(successor(f74)) = empty_set ),
inference(resolution,[status(thm)],[f20610,f3026]) ).
fof(f20633,plain,
( ~ little_set(successor(f74))
| singleton_set(successor(f74)) = empty_set ),
inference(forward_subsumption_resolution,[status(thm)],[f20628,f489]) ).
fof(f20643,plain,
f26(empty_set) = successor(f74),
inference(backward_demodulation,[status(thm)],[f20648,f3679]) ).
fof(f20647,plain,
f24(empty_set) = successor(f74),
inference(backward_demodulation,[status(thm)],[f20648,f3228]) ).
fof(f20648,plain,
singleton_set(successor(f74)) = empty_set,
inference(forward_subsumption_resolution,[status(thm)],[f20633,f4623]) ).
fof(f20705,plain,
( ~ little_set(successor(f74))
| member(successor(f74),empty_set) ),
inference(paramodulation,[status(thm)],[f20648,f513]) ).
fof(f20790,plain,
~ little_set(successor(f74)),
inference(forward_subsumption_resolution,[status(thm)],[f20705,f296]) ).
fof(f20807,plain,
( member(f26(empty_set),infinity)
| ~ member(f74,infinity) ),
inference(paramodulation,[status(thm)],[f20643,f300]) ).
fof(f20822,plain,
member(f26(empty_set),infinity),
inference(forward_subsumption_resolution,[status(thm)],[f20807,f2251]) ).
fof(f20905,plain,
~ little_set(f26(empty_set)),
inference(forward_demodulation,[status(thm)],[f20643,f20790]) ).
fof(f20908,plain,
! [X0] : ~ member(f26(empty_set),X0),
inference(resolution,[status(thm)],[f20905,f223]) ).
fof(f20965,plain,
! [X0] : ~ member(f24(empty_set),X0),
inference(backward_demodulation,[status(thm)],[f20970,f20908]) ).
fof(f20970,plain,
f24(empty_set) = f26(empty_set),
inference(forward_demodulation,[status(thm)],[f20643,f20647]) ).
fof(f21207,plain,
member(f24(empty_set),infinity),
inference(forward_demodulation,[status(thm)],[f20970,f20822]) ).
fof(f21208,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f21207,f20965]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM010-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 01:58:33 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.13/0.39 % Drodi V4.1.1
% 73.63/9.80 % Refutation found
% 73.63/9.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 73.63/9.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 48.94/9.87 % Elapsed time: 9.485605 seconds
% 48.94/9.87 % CPU time: 74.738436 seconds
% 48.94/9.87 % Total memory used: 563.427 MB
% 48.94/9.87 % Net memory used: 511.402 MB
%------------------------------------------------------------------------------