%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP447-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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 12:36:38 PM UTC 2026
% Result : Unsatisfiable 0.22s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP447-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n003.cluster.edu
% 0.18/0.49 % Model : x86_64 x86_64
% 0.18/0.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49 % Memory : 8046.5625MB
% 0.18/0.49 % OS : Linux 6.8.0-71-generic
% 0.18/0.49 % CPULimit : 300
% 0.18/0.49 % WCLimit : 300
% 0.18/0.49 % DateTime : Sun Sep 20 20:15:00 UTC 2026
% 0.18/0.50 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 0.22/0.60 % Refutation found
% 0.22/0.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.60 fof(f1,axiom,(
% 0.22/0.60 (![A,B,C]: (divide(A,divide(divide(divide(divide(A,A),B),C),divide(divide(divide(A,A),A),C))) = B ))),
% 0.22/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.60 fof(f2,axiom,(
% 0.22/0.60 (![A,B,C]: (multiply(A,B) = divide(A,divide(divide(C,C),B)) ))),
% 0.22/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.60 fof(f3,axiom,(
% 0.22/0.60 (![A,B]: (inverse(A) = divide(divide(B,B),A) ))),
% 0.22/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.60 fof(f4,negated_conjecture,(
% 0.22/0.60 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.22/0.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.60 fof(f5,plain,(
% 0.22/0.60 ![X0,X1,X2]: (divide(X0,divide(divide(divide(divide(X0,X0),X1),X2),divide(divide(divide(X0,X0),X0),X2)))=X1)),
% 0.22/0.60 inference(cnf_transformation,[status(thm)],[f1])).
% 0.22/0.60 fof(f6,plain,(
% 0.22/0.60 ![X0,X1,X2]: (multiply(X0,X1)=divide(X0,divide(divide(X2,X2),X1)))),
% 0.22/0.60 inference(cnf_transformation,[status(thm)],[f2])).
% 0.22/0.60 fof(f7,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(divide(X1,X1),X0))),
% 0.22/0.60 inference(cnf_transformation,[status(thm)],[f3])).
% 0.22/0.60 fof(f8,plain,(
% 0.22/0.60 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.22/0.60 inference(cnf_transformation,[status(thm)],[f4])).
% 0.22/0.60 fof(f14,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f7,f6])).
% 0.22/0.60 fof(f15,plain,(
% 0.22/0.60 ![X0,X1,X2]: (divide(X0,divide(divide(divide(divide(X0,X0),X1),X2),divide(inverse(X0),X2)))=X1)),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f7,f5])).
% 0.22/0.60 fof(f16,plain,(
% 0.22/0.60 ![X0,X1,X2]: (divide(X0,divide(divide(inverse(X1),X2),divide(inverse(X0),X2)))=X1)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f7,f15])).
% 0.22/0.60 fof(f17,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(inverse(X0))=multiply(divide(X1,X1),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f14,f7])).
% 0.22/0.60 fof(f18,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(inverse(divide(X1,X1)),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f7,f7])).
% 0.22/0.60 fof(f19,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(multiply(inverse(X1),X1),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f14,f7])).
% 0.22/0.60 fof(f21,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(inverse(X0))=multiply(inverse(divide(X1,X1)),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f7,f17])).
% 0.22/0.60 fof(f22,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(inverse(X0))=multiply(multiply(inverse(X1),X1),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f14,f17])).
% 0.22/0.60 fof(f25,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(inverse(X0))=multiply(inverse(multiply(inverse(X1),X1)),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f19,f17])).
% 0.22/0.60 fof(f26,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(inverse(multiply(inverse(X1),X1)),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f19,f7])).
% 0.22/0.60 fof(f30,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(inverse(inverse(divide(X1,X1))),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f21,f19])).
% 0.22/0.60 fof(f37,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(X0)=divide(inverse(inverse(multiply(inverse(X1),X1))),X0))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f26,f7])).
% 0.22/0.60 fof(f122,plain,(
% 0.22/0.60 ![X0,X1,X2]: (inverse(divide(divide(inverse(X0),X1),divide(inverse(inverse(divide(X2,X2))),X1)))=X0)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f18,f16])).
% 0.22/0.60 fof(f129,plain,(
% 0.22/0.60 ![X0,X1]: (divide(X0,inverse(divide(inverse(X0),inverse(X1))))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f7,f16])).
% 0.22/0.60 fof(f135,plain,(
% 0.22/0.60 ![X0,X1,X2,X3]: (divide(X0,divide(X1,divide(inverse(X0),divide(divide(inverse(X1),X2),divide(inverse(inverse(X3)),X2)))))=X3)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f16,f16])).
% 0.22/0.60 fof(f136,plain,(
% 0.22/0.60 ![X0,X1,X2]: (divide(X0,divide(multiply(inverse(X1),X2),divide(inverse(X0),inverse(X2))))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f14,f16])).
% 0.22/0.60 fof(f142,plain,(
% 0.22/0.60 ![X0,X1,X2,X3]: (divide(X0,divide(divide(inverse(X1),divide(divide(inverse(X2),X3),divide(inverse(inverse(X0)),X3))),X2))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f16,f16])).
% 0.22/0.60 fof(f151,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(divide(divide(inverse(X0),X1),inverse(X1)))=X0)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f30,f122])).
% 0.22/0.60 fof(f152,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(multiply(divide(inverse(X0),X1),X1))=X0)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f14,f151])).
% 0.22/0.60 fof(f165,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,divide(inverse(X0),inverse(X1)))=X1)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f14,f129])).
% 0.22/0.60 fof(f166,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,multiply(inverse(X0),X1))=X1)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f14,f165])).
% 0.22/0.60 fof(f167,plain,(
% 0.22/0.60 ![X0,X1,X2]: (divide(X0,divide(multiply(inverse(X1),X2),multiply(inverse(X0),X2)))=X1)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f14,f136])).
% 0.22/0.60 fof(f193,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),X1)))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f22,f166])).
% 0.22/0.60 fof(f205,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f166,f166])).
% 0.22/0.60 fof(f227,plain,(
% 0.22/0.60 ![X0]: (inverse(inverse(inverse(inverse(X0))))=X0)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f25,f193])).
% 0.22/0.60 fof(f256,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(inverse(inverse(inverse(X0))),multiply(X0,X1))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f227,f166])).
% 0.22/0.60 fof(f264,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(X1))))=divide(X0,X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f227,f14])).
% 0.22/0.60 fof(f265,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f205,f256])).
% 0.22/0.60 fof(f296,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(multiply(inverse(X0),X0))=divide(X1,X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f18,f152])).
% 0.22/0.60 fof(f346,plain,(
% 0.22/0.60 ![X0,X1]: (divide(X0,X0)=divide(X1,X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f296,f296])).
% 0.22/0.60 fof(f351,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(multiply(X0,inverse(inverse(inverse(X0)))))=divide(X1,X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f227,f296])).
% 0.22/0.60 fof(f373,plain,(
% 0.22/0.60 ![X0,X1,X2]: (multiply(X0,multiply(inverse(X1),X1))=divide(X0,divide(X2,X2)))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f296,f14])).
% 0.22/0.60 fof(f389,plain,(
% 0.22/0.60 ![X0,X1]: (inverse(divide(X0,X0))=divide(X1,X1))),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f264,f351])).
% 0.22/0.60 fof(f414,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(inverse(X0),X0)=divide(X1,X1))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f14,f346])).
% 0.22/0.60 fof(f502,plain,(
% 0.22/0.60 ![X0,X1,X2]: (multiply(X0,divide(X1,X1))=divide(X0,divide(X2,X2)))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f389,f14])).
% 0.22/0.60 fof(f565,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,divide(X1,X1))=X0)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f414,f166])).
% 0.22/0.60 fof(f595,plain,(
% 0.22/0.60 ![X0,X1]: (X0=divide(X0,divide(X1,X1)))),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f565,f502])).
% 0.22/0.60 fof(f598,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,multiply(inverse(X1),X1))=X0)),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f595,f373])).
% 0.22/0.60 fof(f600,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,divide(X1,X1))=inverse(inverse(X0)))),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f205,f565])).
% 0.22/0.60 fof(f606,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,inverse(inverse(inverse(multiply(inverse(X1),X1)))))=X0)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f37,f565])).
% 0.22/0.60 fof(f652,plain,(
% 0.22/0.60 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f669,f264])).
% 0.22/0.60 fof(f667,plain,(
% 0.22/0.60 ![X0,X1,X2,X3]: (divide(X0,divide(divide(inverse(X1),divide(divide(inverse(X2),X3),divide(X0,X3))),X2))=X1)),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f669,f142])).
% 0.22/0.60 fof(f668,plain,(
% 0.22/0.60 ![X0,X1,X2,X3]: (divide(X0,divide(X1,divide(inverse(X0),divide(divide(inverse(X1),X2),divide(X3,X2)))))=X3)),
% 0.22/0.60 inference(backward_demodulation,[status(thm)],[f669,f135])).
% 0.22/0.60 fof(f669,plain,(
% 0.22/0.60 ![X0]: (X0=inverse(inverse(X0)))),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f565,f600])).
% 0.22/0.60 fof(f674,plain,(
% 0.22/0.60 ![X0,X1]: (divide(X0,multiply(inverse(X1),X1))=X0)),
% 0.22/0.60 inference(forward_demodulation,[status(thm)],[f264,f606])).
% 0.22/0.60 fof(f791,plain,(
% 0.22/0.60 ![X0,X1,X2,X3,X4]: (divide(X0,divide(divide(inverse(X1),divide(divide(inverse(X2),divide(multiply(inverse(X3),X4),multiply(inverse(X0),X4))),X3)),X2))=X1)),
% 0.22/0.60 inference(paramodulation,[status(thm)],[f167,f667])).
% 0.22/0.60 fof(f911,plain,(
% 0.22/0.61 ![X0,X1,X2]: (divide(X0,divide(X1,divide(inverse(X0),multiply(inverse(X2),X2))))=inverse(X1))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f414,f668])).
% 0.22/0.61 fof(f980,plain,(
% 0.22/0.61 ![X0,X1]: (divide(X0,divide(X1,inverse(X0)))=inverse(X1))),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f674,f911])).
% 0.22/0.61 fof(f982,plain,(
% 0.22/0.61 ![X0,X1]: (divide(X0,multiply(X1,X0))=inverse(X1))),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f14,f980])).
% 0.22/0.61 fof(f1345,plain,(
% 0.22/0.61 ![X0,X1]: (divide(multiply(X0,X1),X1)=inverse(inverse(X0)))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f265,f982])).
% 0.22/0.61 fof(f1363,plain,(
% 0.22/0.61 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f669,f1345])).
% 0.22/0.61 fof(f1377,plain,(
% 0.22/0.61 ![X0,X1]: (multiply(multiply(X0,inverse(X1)),X1)=X0)),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f14,f1363])).
% 0.22/0.61 fof(f1395,plain,(
% 0.22/0.61 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f652,f1377])).
% 0.22/0.61 fof(f1426,plain,(
% 0.22/0.61 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f1395,f982])).
% 0.22/0.61 fof(f1448,plain,(
% 0.22/0.61 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X1,X0)))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f14,f1426])).
% 0.22/0.61 fof(f1453,plain,(
% 0.22/0.61 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f1426,f652])).
% 0.22/0.61 fof(f1473,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (divide(X0,divide(divide(inverse(X1),divide(inverse(multiply(divide(multiply(inverse(X2),X3),multiply(inverse(X0),X3)),X4)),X2)),X4))=X1)),
% 0.22/0.61 inference(backward_demodulation,[status(thm)],[f1448,f791])).
% 0.22/0.61 fof(f1516,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(X1,divide(inverse(X2),divide(inverse(multiply(divide(multiply(inverse(X3),X4),multiply(inverse(X0),X4)),X1)),X3))))=X2)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f1453,f1473])).
% 0.22/0.61 fof(f1517,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,divide(divide(inverse(multiply(divide(multiply(inverse(X2),X3),multiply(inverse(X0),X3)),X1)),X2),inverse(X4))))=X4)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f1453,f1516])).
% 0.22/0.61 fof(f1518,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,multiply(divide(inverse(multiply(divide(multiply(inverse(X2),X3),multiply(inverse(X0),X3)),X1)),X2),X4)))=X4)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f14,f1517])).
% 0.22/0.61 fof(f1519,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,multiply(inverse(multiply(X2,multiply(divide(multiply(inverse(X2),X3),multiply(inverse(X0),X3)),X1))),X4)))=X4)),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f1448,f1518])).
% 0.22/0.61 fof(f1663,plain,(
% 0.22/0.61 ![X0,X1,X2,X3]: (multiply(X0,X1)=multiply(X2,multiply(divide(multiply(inverse(X2),X3),multiply(inverse(X0),X3)),X1)))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f598,f1519])).
% 0.22/0.61 fof(f1665,plain,(
% 0.22/0.61 ![X0,X1,X2,X3,X4]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X3,multiply(divide(multiply(inverse(X3),X4),multiply(inverse(X0),X4)),X1)),X2))),
% 0.22/0.61 inference(paramodulation,[status(thm)],[f265,f1519])).
% 0.22/0.61 fof(f1748,plain,(
% 0.22/0.61 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))),
% 0.22/0.61 inference(backward_demodulation,[status(thm)],[f1768,f8])).
% 0.22/0.61 fof(f1768,plain,(
% 0.22/0.61 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 0.22/0.61 inference(forward_demodulation,[status(thm)],[f1663,f1665])).
% 0.22/0.61 fof(f1895,plain,(
% 0.22/0.61 $false),
% 0.22/0.61 inference(trivial_equality_resolution,[status(thm)],[f1748])).
% 0.22/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.65 % Elapsed time: 0.118670 seconds
% 0.22/0.65 % CPU time: 0.604905 seconds
% 0.22/0.65 % Total memory used: 15.629 MB
% 0.22/0.65 % Net memory used: 15.149 MB
%------------------------------------------------------------------------------