%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT394-2 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:03:05 PM UTC 2026
% Result : Unsatisfiable 39.72s 5.58s
% Output : CNFRefutation 39.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 2
% Syntax : Number of formulae : 64 ( 64 unt; 0 def)
% Number of atoms : 64 ( 63 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 167 ( 167 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C,D] : f(f(f(f(A,B),f(B,C)),D),f(B,f(f(B,f(f(A,A),A)),C))) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
f(x0,f(x0,x0)) != f(x1,f(x1,x1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
f(x0,f(x0,x0)) != f(x1,f(x1,x1)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f10,plain,
! [X0,X1,X2,X3] : f(X0,f(f(X0,X1),f(f(f(X0,X1),f(f(f(X2,X0),f(X2,X0)),f(X2,X0))),X3))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(X0,f(f(X0,f(f(f(f(X2,X0),f(X0,X3)),f(f(X2,X0),f(X0,X3))),f(f(X2,X0),f(X0,X3)))),f(f(X0,f(f(X2,X2),X2)),X3)))) = X0,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f12,plain,
! [X0,X1,X2,X3,X4,X5] : f(f(f(X0,f(f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),X3)),X4),f(f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),f(f(f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),f(f(f(f(f(X1,X0),f(X0,X2)),X5),f(f(f(X1,X0),f(X0,X2)),X5)),f(f(f(X1,X0),f(X0,X2)),X5))),X3))) = f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f15,plain,
! [X0,X1,X2] : f(X0,f(f(X0,X1),f(f(f(X2,X0),f(X2,X0)),f(X2,X0)))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f10,f10]) ).
fof(f18,plain,
! [X0,X1,X2] : f(f(X0,X1),f(f(f(X0,X1),f(X1,X2)),X1)) = f(f(X0,X1),f(X1,X2)),
inference(paramodulation,[status(thm)],[f3,f10]) ).
fof(f222,plain,
! [X0,X1] : f(X0,f(f(X0,X1),f(X0,X1))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f11,f10]) ).
fof(f225,plain,
! [X0,X1,X2] : f(f(X0,X0),f(X0,X0)) = f(f(X0,X0),f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2)))),
inference(paramodulation,[status(thm)],[f11,f18]) ).
fof(f316,plain,
! [X0] : f(f(X0,X0),f(X0,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f11,f225]) ).
fof(f341,plain,
! [X0,X1,X2] : f(f(f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2)))),X0) = f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),
inference(paramodulation,[status(thm)],[f11,f316]) ).
fof(f351,plain,
! [X0,X1] : f(X0,f(f(X0,X1),f(X0,f(X0,X0)))) = f(X0,X1),
inference(paramodulation,[status(thm)],[f316,f15]) ).
fof(f363,plain,
! [X0,X1] : f(f(f(X0,X0),f(X0,X0)),f(f(X0,f(f(X0,X0),X1)),f(X0,X0))) = f(f(f(X0,X0),f(X0,X0)),f(f(X0,X0),X1)),
inference(paramodulation,[status(thm)],[f316,f18]) ).
fof(f377,plain,
! [X0,X1] : f(f(X0,X1),f(X0,X0)) = X0,
inference(backward_demodulation,[status(thm)],[f390,f11]) ).
fof(f390,plain,
! [X0,X1,X2] : f(X0,X0) = f(X0,f(f(X0,f(f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),f(f(X1,X0),f(X0,X2)))),f(f(X0,f(f(X1,X1),X1)),X2))),
inference(forward_demodulation,[status(thm)],[f11,f341]) ).
fof(f413,plain,
! [X0,X1] : f(X0,f(f(X0,f(f(X0,X0),X1)),f(X0,X0))) = f(f(f(X0,X0),f(X0,X0)),f(f(X0,X0),X1)),
inference(forward_demodulation,[status(thm)],[f316,f363]) ).
fof(f414,plain,
! [X0,X1] : f(X0,f(f(X0,f(f(X0,X0),X1)),f(X0,X0))) = f(X0,f(f(X0,X0),X1)),
inference(forward_demodulation,[status(thm)],[f316,f413]) ).
fof(f430,plain,
! [X0,X1] : f(X0,X0) = f(X0,f(f(X0,X0),X1)),
inference(backward_demodulation,[status(thm)],[f377,f414]) ).
fof(f464,plain,
! [X0,X1] : f(f(f(X0,X0),X1),X0) = f(X0,X0),
inference(paramodulation,[status(thm)],[f377,f377]) ).
fof(f517,plain,
! [X0,X1,X2] : f(f(f(X0,X1),f(X1,X2)),f(f(X0,X1),f(X1,X2))) = f(f(f(X0,X1),f(X1,X2)),X1),
inference(paramodulation,[status(thm)],[f3,f430]) ).
fof(f523,plain,
! [X0,X1] : f(f(X0,X0),f(X0,X0)) = f(f(X0,X0),f(X0,X1)),
inference(paramodulation,[status(thm)],[f377,f430]) ).
fof(f564,plain,
! [X0,X1] : X0 = f(f(X0,X0),f(X0,X1)),
inference(forward_demodulation,[status(thm)],[f377,f523]) ).
fof(f599,plain,
! [X0,X1] : f(X0,X1) = f(f(f(X0,X1),f(X0,X1)),X0),
inference(paramodulation,[status(thm)],[f377,f564]) ).
fof(f672,plain,
! [X0,X1,X2] : f(X0,f(f(X1,X0),f(X0,X2))) = f(f(f(X1,X0),f(X0,X2)),f(f(X1,X0),f(X0,X2))),
inference(paramodulation,[status(thm)],[f3,f464]) ).
fof(f726,plain,
! [X0,X1,X2] : f(X0,f(f(X1,X0),f(X0,X2))) = f(f(f(X1,X0),f(X0,X2)),X0),
inference(forward_demodulation,[status(thm)],[f517,f672]) ).
fof(f775,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))))) = f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))),
inference(paramodulation,[status(thm)],[f3,f222]) ).
fof(f812,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,X1)) = f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(f(X0,X0),X0)),X2))),
inference(forward_demodulation,[status(thm)],[f3,f775]) ).
fof(f814,plain,
! [X0,X1,X2,X3] : f(f(f(f(X0,X1),f(X1,X2)),X3),f(X1,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f3,f812]) ).
fof(f961,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,f(X1,f(X1,X1)))),X2),f(X1,f(f(X0,X0),X0))) = X1,
inference(paramodulation,[status(thm)],[f351,f3]) ).
fof(f1021,plain,
! [X0,X1] : f(f(X0,X1),f(X1,X1)) = X1,
inference(paramodulation,[status(thm)],[f377,f814]) ).
fof(f1137,plain,
! [X0,X1] : f(f(X0,f(X1,X1)),X1) = f(X1,X1),
inference(paramodulation,[status(thm)],[f1021,f1021]) ).
fof(f1161,plain,
! [X0,X1] : f(f(X0,X1),f(X1,X1)) = f(f(f(f(X0,X1),f(X1,X1)),X1),f(X0,X1)),
inference(paramodulation,[status(thm)],[f1021,f599]) ).
fof(f1170,plain,
! [X0,X1] : f(X0,f(f(X1,X0),f(X1,X0))) = f(X1,X0),
inference(paramodulation,[status(thm)],[f1021,f377]) ).
fof(f1187,plain,
! [X0,X1] : X0 = f(f(f(f(X1,X0),f(X0,X0)),X0),f(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1021,f1161]) ).
fof(f1188,plain,
! [X0,X1] : X0 = f(f(X0,f(f(X1,X0),f(X0,X0))),f(X1,X0)),
inference(forward_demodulation,[status(thm)],[f726,f1187]) ).
fof(f1189,plain,
! [X0,X1] : X0 = f(f(X0,X0),f(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1021,f1188]) ).
fof(f1233,plain,
! [X0,X1,X2,X3,X4] : f(f(f(f(X0,X0),f(X0,X0)),X1),f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4),f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4)),f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4))),X0))) = f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),
inference(paramodulation,[status(thm)],[f464,f12]) ).
fof(f1501,plain,
! [X0,X1,X2,X3,X4] : f(f(X0,X1),f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4),f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4)),f(f(f(X2,f(X0,X0)),f(f(X0,X0),X3)),X4))),X0))) = f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),
inference(forward_demodulation,[status(thm)],[f1021,f1233]) ).
fof(f3450,plain,
! [X0,X1] : f(X0,X0) = f(X0,f(X1,f(X0,X0))),
inference(paramodulation,[status(thm)],[f1189,f1189]) ).
fof(f3564,plain,
! [X0,X1,X2] : f(f(f(f(X0,X1),f(X1,X1)),X2),f(X1,f(f(X0,X0),X0))) = X1,
inference(backward_demodulation,[status(thm)],[f3450,f961]) ).
fof(f3823,plain,
! [X0,X1,X2] : f(f(X0,X1),f(X0,f(f(X2,X2),X2))) = X0,
inference(forward_demodulation,[status(thm)],[f1021,f3564]) ).
fof(f3834,plain,
! [X0,X1,X2] : X0 = f(f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),f(X0,f(f(X0,f(f(X1,X1),X1)),X2))),
inference(paramodulation,[status(thm)],[f3,f1137]) ).
fof(f5083,plain,
! [X0,X1] : f(X0,f(f(X1,X1),X1)) = f(X0,X0),
inference(paramodulation,[status(thm)],[f3823,f599]) ).
fof(f5138,plain,
! [X0,X1,X2] : f(X0,f(f(X1,X1),X1)) = f(X0,f(f(X0,f(f(X1,X1),X1)),X2)),
inference(paramodulation,[status(thm)],[f3823,f564]) ).
fof(f5279,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3))),X0))) = f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),
inference(backward_demodulation,[status(thm)],[f5083,f1501]) ).
fof(f5747,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)))) = f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),
inference(forward_demodulation,[status(thm)],[f430,f5279]) ).
fof(f5748,plain,
! [X0,X1,X2,X3] : f(f(X0,X1),f(X0,X0)) = f(f(X0,X0),f(f(f(X0,X0),f(f(X2,X2),X2)),X3)),
inference(forward_demodulation,[status(thm)],[f3834,f5747]) ).
fof(f5749,plain,
! [X0,X1,X2] : X0 = f(f(X0,X0),f(f(f(X0,X0),f(f(X1,X1),X1)),X2)),
inference(forward_demodulation,[status(thm)],[f377,f5748]) ).
fof(f5751,plain,
! [X0,X1] : X0 = f(f(X0,X0),f(f(X1,X1),X1)),
inference(forward_demodulation,[status(thm)],[f5138,f5749]) ).
fof(f6349,plain,
! [X0,X1] : X0 = f(f(X0,X0),f(X1,f(X1,X1))),
inference(paramodulation,[status(thm)],[f1189,f5751]) ).
fof(f6372,plain,
! [X0,X1] : f(f(f(X0,X0),X0),f(f(f(X1,X1),f(f(X0,X0),X0)),X1)) = f(f(X1,X1),f(f(X0,X0),X0)),
inference(paramodulation,[status(thm)],[f5751,f1170]) ).
fof(f6387,plain,
! [X0,X1] : f(f(f(X0,X0),X0),f(X1,X1)) = f(f(X1,X1),f(f(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f464,f6372]) ).
fof(f6388,plain,
! [X0,X1] : f(f(f(X0,X0),X0),f(X1,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f5751,f6387]) ).
fof(f6581,plain,
! [X0,X1] : f(f(X0,f(X0,X0)),f(f(f(X1,X1),f(X0,f(X0,X0))),X1)) = f(f(X1,X1),f(X0,f(X0,X0))),
inference(paramodulation,[status(thm)],[f6349,f1170]) ).
fof(f6595,plain,
! [X0,X1] : f(f(X0,f(X0,X0)),f(X1,X1)) = f(f(X1,X1),f(X0,f(X0,X0))),
inference(forward_demodulation,[status(thm)],[f464,f6581]) ).
fof(f6596,plain,
! [X0,X1] : f(f(X0,f(X0,X0)),f(X1,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f6349,f6595]) ).
fof(f6651,plain,
! [X0,X1,X2] : f(X0,f(f(f(X1,X1),X1),f(f(X2,X2),X2))) = f(f(X1,X1),X1),
inference(paramodulation,[status(thm)],[f6388,f3823]) ).
fof(f6706,plain,
! [X0,X1] : f(f(X0,f(X0,X0)),X1) = f(X1,X1),
inference(paramodulation,[status(thm)],[f1189,f6596]) ).
fof(f6908,plain,
! [X0,X1,X2] : f(f(f(X0,f(X0,X0)),X1),f(f(f(X2,X2),X2),f(f(X2,X2),X2))) = f(X0,f(X0,X0)),
inference(paramodulation,[status(thm)],[f6706,f3823]) ).
fof(f6982,plain,
! [X0,X1] : f(f(X0,X0),X0) = f(X1,f(X1,X1)),
inference(forward_demodulation,[status(thm)],[f6651,f6908]) ).
fof(f9564,plain,
! [X0,X1] : f(X0,f(X0,X0)) = f(X1,f(X1,X1)),
inference(paramodulation,[status(thm)],[f6349,f6982]) ).
fof(f9664,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f4,f9564]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT394-2 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n003.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 20 23:59:45 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Drodi V4.1.1
% 39.72/5.58 % Refutation found
% 39.72/5.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 39.72/5.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 26.81/6.91 % Elapsed time: 6.241906 seconds
% 26.81/6.91 % CPU time: 29.188654 seconds
% 26.81/6.91 % Total memory used: 416.391 MB
% 26.81/6.91 % Net memory used: 403.583 MB
%------------------------------------------------------------------------------