%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP480-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 12:36:41 PM UTC 2026
% Result : Unsatisfiable 25.79s 3.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP480-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.52 % Computer : n014.cluster.edu
% 0.09/0.52 % Model : x86_64 x86_64
% 0.09/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.52 % Memory : 8046.5625MB
% 0.09/0.52 % OS : Linux 6.8.0-71-generic
% 0.09/0.52 % CPULimit : 300
% 0.09/0.52 % WCLimit : 300
% 0.09/0.52 % DateTime : Sun Sep 20 20:14:21 UTC 2026
% 0.09/0.52 % CPUTime :
% 0.09/0.53 % Drodi V4.1.1
% 25.79/3.83 % Refutation found
% 25.79/3.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 25.79/3.83 % SZS output start CNFRefutation for theBenchmark
% 25.79/3.83 fof(f1,axiom,(
% 25.79/3.83 (![A,B,C,D]: (divide(inverse(divide(divide(divide(A,A),B),divide(C,divide(B,D)))),D) = C ))),
% 25.79/3.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 25.79/3.83 fof(f2,axiom,(
% 25.79/3.83 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 25.79/3.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 25.79/3.83 fof(f3,negated_conjecture,(
% 25.79/3.83 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 25.79/3.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 25.79/3.83 fof(f4,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(inverse(divide(divide(divide(X0,X0),X1),divide(X2,divide(X1,X3)))),X3)=X2)),
% 25.79/3.83 inference(cnf_transformation,[status(thm)],[f1])).
% 25.79/3.83 fof(f5,plain,(
% 25.79/3.83 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 25.79/3.83 inference(cnf_transformation,[status(thm)],[f2])).
% 25.79/3.83 fof(f6,plain,(
% 25.79/3.83 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 25.79/3.83 inference(cnf_transformation,[status(thm)],[f3])).
% 25.79/3.83 fof(f12,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (multiply(inverse(divide(divide(divide(X0,X0),X1),divide(X2,divide(X1,inverse(X3))))),X3)=X2)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f4])).
% 25.79/3.83 fof(f13,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(inverse(divide(multiply(divide(X0,X0),X1),divide(X2,divide(inverse(X1),X3)))),X3)=X2)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f4])).
% 25.79/3.83 fof(f15,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X0),X1),X2)),X3)=inverse(divide(divide(divide(X4,X4),X5),divide(X2,divide(X5,divide(X1,X3))))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f4,f4])).
% 25.79/3.83 fof(f16,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(divide(divide(X0,X0),inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4))))),divide(X5,X3))),X4)=X5)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f4,f4])).
% 25.79/3.83 fof(f19,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (multiply(inverse(divide(divide(divide(X0,X0),X1),divide(X2,multiply(X1,X3)))),X3)=X2)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f12])).
% 25.79/3.83 fof(f20,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(divide(X0,X0),divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),divide(X5,X3))),X4)=X5)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f16])).
% 25.79/3.83 fof(f30,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(divide(multiply(divide(X0,X0),X1),X2)),X3)=inverse(divide(multiply(divide(X4,X4),X5),divide(X2,divide(inverse(X5),divide(inverse(X1),X3))))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f13,f13])).
% 25.79/3.83 fof(f126,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(divide(inverse(divide(divide(divide(X0,X0),X1),X2)),X3),divide(X1,X3))=X2)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f15,f4])).
% 25.79/3.83 fof(f169,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(divide(divide(X0,X0),X1),X2)),X3),divide(X1,inverse(X3)))=X2)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f126])).
% 25.79/3.83 fof(f194,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(divide(divide(X0,X0),X1),X2)),X3),multiply(X1,X3))=X2)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f169])).
% 25.79/3.83 fof(f211,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(inverse(multiply(divide(divide(X0,X0),X1),X2)),X3),multiply(X1,X3))=inverse(X2))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f194])).
% 25.79/3.83 fof(f212,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(X0,X1)),X2),multiply(divide(X3,inverse(divide(divide(divide(X4,X4),X3),X0))),X2))=X1)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f126,f194])).
% 25.79/3.83 fof(f213,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(inverse(divide(multiply(divide(X0,X0),X1),X2)),X3),multiply(inverse(X1),X3))=X2)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f194])).
% 25.79/3.83 fof(f228,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(X0,X1)),X2),multiply(multiply(X3,divide(divide(divide(X4,X4),X3),X0)),X2))=X1)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f212])).
% 25.79/3.83 fof(f546,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(inverse(multiply(multiply(divide(X0,X0),X1),X2)),X3),multiply(inverse(X1),X3))=inverse(X2))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f211])).
% 25.79/3.83 fof(f1055,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5,X6]: (X0=inverse(divide(multiply(divide(X1,X1),X2),divide(divide(X0,X3),divide(inverse(X2),divide(inverse(divide(divide(divide(X4,X4),X5),divide(X3,divide(X5,X6)))),X6))))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f20,f30])).
% 25.79/3.83 fof(f1191,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X1),X2),divide(divide(X0,X3),divide(inverse(X2),X3)))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f4,f1055])).
% 25.79/3.83 fof(f1310,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X1),X2),divide(multiply(X0,X3),divide(inverse(X2),inverse(X3))))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f1191])).
% 25.79/3.83 fof(f1336,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(X0,X1),multiply(inverse(X2),X1))=divide(divide(X0,X3),divide(inverse(X2),X3)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1191,f213])).
% 25.79/3.83 fof(f1350,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(divide(X1,X1),X2),divide(divide(X3,X4),divide(inverse(X2),X4))))=divide(X0,X3))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1191,f5])).
% 25.79/3.83 fof(f1357,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(divide(X1,X1),X2),divide(multiply(X0,X3),multiply(inverse(X2),X3)))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f1310])).
% 25.79/3.83 fof(f1365,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=inverse(divide(multiply(multiply(inverse(X1),X1),X2),divide(multiply(X0,X3),multiply(inverse(X2),X3)))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f5,f1357])).
% 25.79/3.83 fof(f1412,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(divide(X1,X1),X2),divide(multiply(X3,X4),multiply(inverse(X2),X4))))=divide(X0,X3))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1357,f5])).
% 25.79/3.83 fof(f1439,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5,X6]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(divide(X0,X3),divide(inverse(divide(multiply(divide(X4,X4),X5),divide(multiply(X2,X6),multiply(inverse(X5),X6)))),X3)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1357,f1336])).
% 25.79/3.83 fof(f1630,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(divide(X0,X3),divide(X2,X3)))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f1357,f1439])).
% 25.79/3.83 fof(f1958,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(divide(X0,X1),divide(X2,X1))=divide(divide(X0,X3),divide(X2,X3)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1630,f1630])).
% 25.79/3.83 fof(f1973,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(multiply(X0,X3),multiply(X2,X3)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1630,f1630])).
% 25.79/3.83 fof(f2083,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (divide(multiply(inverse(divide(multiply(divide(X0,X0),X1),multiply(X2,X1))),X3),multiply(X4,X3))=divide(X2,X4))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1630,f194])).
% 25.79/3.83 fof(f20513,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (multiply(X0,X1)=divide(X0,multiply(X2,divide(divide(divide(X3,X3),X2),multiply(divide(X4,X4),X1)))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f228,f2083])).
% 25.79/3.83 fof(f21084,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5,X6]: (divide(multiply(inverse(multiply(multiply(divide(X0,X0),X1),X2)),X3),multiply(inverse(X1),X3))=multiply(X4,divide(divide(divide(X5,X5),X4),multiply(divide(X6,X6),X2))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f20513,f213])).
% 25.79/3.83 fof(f21468,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (inverse(X0)=multiply(X1,divide(divide(divide(X2,X2),X1),multiply(divide(X3,X3),X0))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f546,f21084])).
% 25.79/3.83 fof(f21635,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5,X6]: (inverse(divide(multiply(divide(X0,X0),X1),divide(multiply(X2,X3),multiply(inverse(X1),X3))))=multiply(X4,divide(divide(divide(X5,X5),X4),divide(divide(X6,X6),X2))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1412,f21468])).
% 25.79/3.83 fof(f21812,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=multiply(X1,divide(divide(divide(X2,X2),X1),divide(divide(X3,X3),X0))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f1357,f21635])).
% 25.79/3.83 fof(f21894,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (X0=multiply(X0,divide(divide(divide(X1,X1),X2),divide(divide(X3,X3),X2))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1958,f21812])).
% 25.79/3.83 fof(f23335,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4,X5]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(multiply(X0,divide(divide(divide(X3,X3),X4),divide(divide(X5,X5),X4))),X2))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f21894,f1973])).
% 25.79/3.83 fof(f23497,plain,(
% 25.79/3.83 ![X0,X1,X2]: (divide(multiply(X0,X1),multiply(X2,X1))=divide(X0,X2))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f21894,f23335])).
% 25.79/3.83 fof(f23522,plain,(
% 25.79/3.83 ![X0,X1,X2]: (X0=inverse(divide(multiply(multiply(inverse(X1),X1),X2),divide(X0,inverse(X2)))))),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f23497,f1365])).
% 25.79/3.83 fof(f23523,plain,(
% 25.79/3.83 ![X0,X1,X2]: (X0=inverse(divide(multiply(divide(X1,X1),X2),divide(X0,inverse(X2)))))),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f23497,f1357])).
% 25.79/3.83 fof(f23747,plain,(
% 25.79/3.83 ![X0,X1,X2]: (X0=inverse(divide(multiply(multiply(inverse(X1),X1),X2),multiply(X0,X2))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f23522])).
% 25.79/3.83 fof(f23748,plain,(
% 25.79/3.83 ![X0,X1]: (X0=inverse(divide(multiply(inverse(X1),X1),X0)))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f23497,f23747])).
% 25.79/3.83 fof(f23749,plain,(
% 25.79/3.83 ![X0,X1,X2]: (X0=inverse(divide(multiply(divide(X1,X1),X2),multiply(X0,X2))))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f23523])).
% 25.79/3.83 fof(f23750,plain,(
% 25.79/3.83 ![X0,X1]: (X0=inverse(divide(divide(X1,X1),X0)))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f23497,f23749])).
% 25.79/3.83 fof(f23948,plain,(
% 25.79/3.83 ![X0,X1]: (multiply(X0,X1)=inverse(divide(inverse(X1),X0)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f23497,f23748])).
% 25.79/3.83 fof(f25138,plain,(
% 25.79/3.83 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(divide(X1,X1),X2),divide(divide(X3,X4),divide(inverse(X2),X4))))=inverse(divide(X3,X0)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f1191,f23948])).
% 25.79/3.83 fof(f25233,plain,(
% 25.79/3.83 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f1350,f25138])).
% 25.79/3.83 fof(f25286,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (multiply(divide(divide(X0,multiply(X1,X2)),divide(divide(X3,X3),X1)),X2)=X0)),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f25233,f19])).
% 25.79/3.83 fof(f25290,plain,(
% 25.79/3.83 ![X0,X1,X2,X3]: (divide(divide(divide(X0,divide(X1,X2)),divide(divide(X3,X3),X1)),X2)=X0)),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f25233,f4])).
% 25.79/3.83 fof(f25296,plain,(
% 25.79/3.83 ![X0,X1]: (X0=divide(X0,divide(X1,X1)))),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f25233,f23750])).
% 25.79/3.83 fof(f25358,plain,(
% 25.79/3.83 ![X0,X1,X2]: (X0=multiply(X0,divide(divide(X1,X1),divide(X2,X2))))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f25296,f21894])).
% 25.79/3.83 fof(f25385,plain,(
% 25.79/3.83 ![X0,X1]: (divide(divide(X0,X0),X1)=inverse(X1))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f25296,f25233])).
% 25.79/3.83 fof(f25427,plain,(
% 25.79/3.83 ![X0,X1]: (X0=multiply(X0,divide(X1,X1)))),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f25296,f25358])).
% 25.79/3.83 fof(f26059,plain,(
% 25.79/3.83 ![X0,X1,X2]: (divide(divide(divide(X0,divide(X1,X2)),inverse(X1)),X2)=X0)),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f25385,f25290])).
% 25.79/3.83 fof(f26116,plain,(
% 25.79/3.83 ![X0,X1,X2]: (divide(multiply(divide(X0,divide(X1,X2)),X1),X2)=X0)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f26059])).
% 25.79/3.83 fof(f26190,plain,(
% 25.79/3.83 ![X0,X1,X2]: (divide(divide(X0,divide(divide(X1,X1),X2)),X2)=X0)),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f25427,f26116])).
% 25.79/3.83 fof(f26229,plain,(
% 25.79/3.83 ![X0,X1]: (divide(divide(X0,inverse(X1)),X1)=X0)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f25385,f26190])).
% 25.79/3.83 fof(f26230,plain,(
% 25.79/3.83 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f26229])).
% 25.79/3.83 fof(f26682,plain,(
% 25.79/3.83 ![X0,X1,X2]: (multiply(divide(divide(X0,multiply(X1,X2)),inverse(X1)),X2)=X0)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f25385,f25286])).
% 25.79/3.83 fof(f26683,plain,(
% 25.79/3.83 ![X0,X1,X2]: (multiply(multiply(divide(X0,multiply(X1,X2)),X1),X2)=X0)),
% 25.79/3.83 inference(forward_demodulation,[status(thm)],[f5,f26682])).
% 25.79/3.83 fof(f26691,plain,(
% 25.79/3.83 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 25.79/3.83 inference(paramodulation,[status(thm)],[f26230,f26683])).
% 25.79/3.83 fof(f30284,plain,(
% 25.79/3.83 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 25.79/3.83 inference(backward_demodulation,[status(thm)],[f26691,f6])).
% 25.79/3.83 fof(f30311,plain,(
% 25.79/3.83 $false),
% 25.79/3.83 inference(trivial_equality_resolution,[status(thm)],[f30284])).
% 25.79/3.83 % SZS output end CNFRefutation for theBenchmark.p
% 10.14/12.35 % Elapsed time: 11.823351 seconds
% 10.14/12.35 % CPU time: 91.765791 seconds
% 10.14/12.35 % Total memory used: 53.139 GB
% 10.14/12.35 % Net memory used: 53.137 GB
%------------------------------------------------------------------------------