%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWX190-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 03:13:23 PM UTC 2026
% Result : Unsatisfiable 15.41s 2.59s
% Output : CNFRefutation 13.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 36 ( 36 unt; 0 def)
% Number of atoms : 36 ( 35 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-2 aty)
% Number of variables : 44 ( 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f15,axiom,
! [Y] : fail(Y,n(z)) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [Y] : d(n(Y)) = n(z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [F,G] : d(x(F,G)) = x(d(F),d(G)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,axiom,
d(x2) = n(s(z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [X4,E] : opt(x(n(s(X4)),E)) = fail(n(s(X4)),E),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [E] : opt(x(n(z),E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X] : prop4(X) = eq2(opt(d(X)),opt(d(opt(X)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [X,Y,Z] : eq2(x(X,Y),n(Z)) = bfalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [X] : eq3(X,X) = btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
! [X] : eq3(prop4(X),bfalse) != btrue,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,plain,
! [X0] : fail(X0,n(z)) = X0,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f134,plain,
! [X0] : d(n(X0)) = n(z),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f135,plain,
! [X0,X1] : d(x(X0,X1)) = x(d(X0),d(X1)),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f137,plain,
d(x2) = n(s(z)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f142,plain,
! [X0,X1] : opt(x(n(s(X0)),X1)) = fail(n(s(X0)),X1),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f143,plain,
! [X0] : opt(x(n(z),X0)) = X0,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f154,plain,
! [X0] : prop4(X0) = eq2(opt(d(X0)),opt(d(opt(X0)))),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f169,plain,
! [X0,X1,X2] : eq2(x(X0,X1),n(X2)) = bfalse,
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f183,plain,
! [X0] : eq3(X0,X0) = btrue,
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f184,plain,
! [X0] : eq3(prop4(X0),bfalse) != btrue,
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f248,plain,
! [X0] : prop4(x(n(z),X0)) = eq2(opt(d(x(n(z),X0))),opt(d(X0))),
inference(paramodulation,[status(thm)],[f143,f154]) ).
fof(f393,plain,
! [X0,X1] : eq2(x(X0,X1),d(x2)) = bfalse,
inference(paramodulation,[status(thm)],[f137,f169]) ).
fof(f1276,plain,
! [X0,X1] : d(x(n(X0),X1)) = x(n(z),d(X1)),
inference(paramodulation,[status(thm)],[f134,f135]) ).
fof(f1278,plain,
! [X0,X1] : d(x(X0,n(X1))) = x(d(X0),n(z)),
inference(paramodulation,[status(thm)],[f134,f135]) ).
fof(f1291,plain,
! [X0,X1] : eq2(d(x(X0,X1)),d(x2)) = bfalse,
inference(paramodulation,[status(thm)],[f135,f393]) ).
fof(f2113,plain,
! [X0] : opt(x(d(x2),X0)) = fail(n(s(z)),X0),
inference(paramodulation,[status(thm)],[f137,f142]) ).
fof(f2124,plain,
! [X0] : opt(x(d(x2),X0)) = fail(d(x2),X0),
inference(forward_demodulation,[status(thm)],[f137,f2113]) ).
fof(f17086,plain,
! [X0,X1] : opt(d(x(n(X0),X1))) = d(X1),
inference(paramodulation,[status(thm)],[f1276,f143]) ).
fof(f17257,plain,
! [X0] : prop4(x(n(z),X0)) = eq2(d(X0),opt(d(X0))),
inference(backward_demodulation,[status(thm)],[f17086,f248]) ).
fof(f18582,plain,
! [X0] : opt(d(x(x2,n(X0)))) = fail(d(x2),n(z)),
inference(paramodulation,[status(thm)],[f1278,f2124]) ).
fof(f18744,plain,
! [X0] : opt(d(x(x2,n(X0)))) = d(x2),
inference(forward_demodulation,[status(thm)],[f105,f18582]) ).
fof(f18782,plain,
! [X0] : prop4(x(n(z),x(x2,n(X0)))) = eq2(d(x(x2,n(X0))),d(x2)),
inference(paramodulation,[status(thm)],[f18744,f17257]) ).
fof(f18817,plain,
! [X0] : prop4(x(n(z),x(x2,n(X0)))) = bfalse,
inference(forward_demodulation,[status(thm)],[f1291,f18782]) ).
fof(f20198,plain,
eq3(bfalse,bfalse) != btrue,
inference(paramodulation,[status(thm)],[f18817,f184]) ).
fof(f20205,plain,
btrue != btrue,
inference(forward_demodulation,[status(thm)],[f183,f20198]) ).
fof(f20206,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f20205]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX190-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.44 % Computer : n005.cluster.edu
% 0.15/0.44 % Model : x86_64 x86_64
% 0.15/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.44 % Memory : 8046.5625MB
% 0.15/0.44 % OS : Linux 6.8.0-71-generic
% 0.15/0.44 % CPULimit : 300
% 0.15/0.44 % WCLimit : 300
% 0.15/0.44 % DateTime : Mon Sep 21 10:31:04 UTC 2026
% 0.15/0.44 % CPUTime :
% 0.15/0.46 % Drodi V4.1.1
% 15.41/2.59 % Refutation found
% 15.41/2.59 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 15.41/2.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.01/2.75 % Elapsed time: 2.293165 seconds
% 2.01/2.75 % CPU time: 17.351003 seconds
% 2.01/2.75 % Total memory used: 380.412 MB
% 2.01/2.75 % Net memory used: 375.767 MB
%------------------------------------------------------------------------------