%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP559-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 : n011.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:49 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP559-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.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:16:40 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.13/0.47 % Refutation found
% 0.13/0.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.47 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.47 fof(f1,axiom,(
% 0.13/0.47 (![A,B,C]: (divide(A,inverse(divide(divide(B,C),divide(A,C)))) = B ))),
% 0.13/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.47 fof(f2,axiom,(
% 0.13/0.47 (![A,B]: (multiply(A,B) = divide(A,inverse(B)) ))),
% 0.13/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.47 fof(f3,negated_conjecture,(
% 0.13/0.47 multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
% 0.13/0.47 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.47 fof(f4,plain,(
% 0.13/0.47 ![X0,X1,X2]: (divide(X0,inverse(divide(divide(X1,X2),divide(X0,X2))))=X1)),
% 0.13/0.47 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.47 fof(f5,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 0.13/0.47 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.47 fof(f6,plain,(
% 0.13/0.47 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 0.13/0.47 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.47 fof(f12,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,divide(divide(X1,X2),divide(X0,X2)))=X1)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f5,f4])).
% 0.13/0.47 fof(f13,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,divide(multiply(X1,X2),divide(X0,inverse(X2))))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f5,f12])).
% 0.13/0.47 fof(f15,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,divide(multiply(X1,X2),multiply(X0,X2)))=X1)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f5,f13])).
% 0.13/0.47 fof(f17,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,multiply(X0,divide(multiply(X1,X2),multiply(X3,X2)))))=X3)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f15,f15])).
% 0.13/0.47 fof(f18,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,multiply(X0,divide(divide(X1,X2),divide(X3,X2)))))=X3)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f12,f15])).
% 0.13/0.47 fof(f19,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(multiply(X1,divide(multiply(X2,X3),multiply(X0,X3))),X2))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f15,f15])).
% 0.13/0.47 fof(f20,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(multiply(X1,divide(divide(X2,X3),divide(X0,X3))),X2))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f12,f15])).
% 0.13/0.47 fof(f21,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(X0,divide(X1,X1))=X0)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f15,f17])).
% 0.13/0.47 fof(f35,plain,(
% 0.13/0.47 ![X0,X1,X2,X3,X4]: (multiply(X0,divide(multiply(X1,divide(X2,multiply(X0,divide(divide(X2,X3),divide(X4,X3))))),X4))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f18,f15])).
% 0.13/0.47 fof(f42,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(X0,divide(X1,X0))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f21,f17])).
% 0.13/0.47 fof(f55,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(inverse(X0),multiply(X1,X0))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f5,f42])).
% 0.13/0.47 fof(f80,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(inverse(divide(X0,X1)),X0)=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f42,f55])).
% 0.13/0.47 fof(f138,plain,(
% 0.13/0.47 ![X0,X1]: (inverse(divide(divide(X0,X0),X1))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f21,f80])).
% 0.13/0.47 fof(f142,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=inverse(divide(divide(multiply(X2,X3),multiply(X0,X3)),X1)))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f80,f19])).
% 0.13/0.47 fof(f148,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(inverse(X0),X1)=inverse(divide(X0,X1)))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f80,f55])).
% 0.13/0.47 fof(f155,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(multiply(inverse(X0),X1),X0)=X1)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f148,f80])).
% 0.13/0.47 fof(f159,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=multiply(inverse(divide(multiply(X2,X3),multiply(X0,X3))),X1))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f148,f142])).
% 0.13/0.47 fof(f161,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(inverse(divide(X0,X0)),X1)=X1)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f148,f138])).
% 0.13/0.47 fof(f199,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=multiply(multiply(inverse(multiply(X2,X3)),multiply(X0,X3)),X1))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f148,f159])).
% 0.13/0.47 fof(f201,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(multiply(inverse(X0),X0),X1)=X1)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f148,f161])).
% 0.13/0.47 fof(f231,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,X1)=divide(divide(X0,X2),divide(inverse(X1),X2)))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f12,f155])).
% 0.13/0.47 fof(f233,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(inverse(X0),X0)=divide(X1,X1))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f21,f155])).
% 0.13/0.47 fof(f246,plain,(
% 0.13/0.47 ![X0,X1,X2]: (X0=divide(divide(X0,X1),divide(multiply(inverse(X2),X2),X1)))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f12,f201])).
% 0.13/0.47 fof(f275,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(X1,X1),X2))=inverse(divide(multiply(X2,X3),multiply(X0,X3))))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f233,f19])).
% 0.13/0.47 fof(f288,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(X1,X1),X2))=multiply(inverse(multiply(X2,X3)),multiply(X0,X3)))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f148,f275])).
% 0.13/0.47 fof(f319,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (divide(multiply(X0,divide(divide(X1,X2),divide(multiply(inverse(X3),X3),X2))),X1)=X0)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f201,f20])).
% 0.13/0.47 fof(f321,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,multiply(multiply(X1,divide(divide(inverse(X2),X3),divide(X0,X3))),X2))=X1)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f5,f20])).
% 0.13/0.47 fof(f339,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,X1)=divide(multiply(X0,divide(divide(X2,X3),divide(inverse(X1),X3))),X2))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f20,f155])).
% 0.13/0.47 fof(f346,plain,(
% 0.13/0.47 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f246,f319])).
% 0.13/0.47 fof(f361,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,X1)=divide(multiply(X0,multiply(X2,X1)),X2))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f231,f339])).
% 0.13/0.47 fof(f406,plain,(
% 0.13/0.47 ![X0,X1]: (divide(X0,X1)=multiply(inverse(X1),X0))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f155,f346])).
% 0.13/0.47 fof(f407,plain,(
% 0.13/0.47 ![X0,X1]: (divide(X0,multiply(X0,X1))=inverse(X1))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f55,f346])).
% 0.13/0.47 fof(f408,plain,(
% 0.13/0.47 ![X0,X1]: (divide(divide(X0,X0),X1)=inverse(X1))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f233,f346])).
% 0.13/0.47 fof(f411,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (divide(X0,divide(multiply(X0,divide(multiply(X1,X2),multiply(X3,X2))),X1))=X3)),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f19,f346])).
% 0.13/0.47 fof(f418,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f346,f42])).
% 0.13/0.47 fof(f427,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(divide(X1,X1),X2))=divide(multiply(X0,X3),multiply(X2,X3)))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f406,f288])).
% 0.13/0.47 fof(f428,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=multiply(divide(multiply(X0,X3),multiply(X2,X3)),X1))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f406,f199])).
% 0.13/0.47 fof(f454,plain,(
% 0.13/0.47 ![X0,X1]: (divide(X0,X1)=inverse(divide(X1,X0)))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f406,f148])).
% 0.13/0.47 fof(f467,plain,(
% 0.13/0.47 ![X0,X1,X2]: (divide(X0,divide(multiply(X0,multiply(X1,inverse(X2))),X1))=X2)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f475,f411])).
% 0.13/0.47 fof(f475,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,inverse(X1))=divide(multiply(X0,X2),multiply(X1,X2)))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f408,f427])).
% 0.13/0.47 fof(f477,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=multiply(multiply(X0,inverse(X2)),X1))),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f475,f428])).
% 0.13/0.47 fof(f509,plain,(
% 0.13/0.47 ![X0,X1]: (divide(X0,multiply(X0,inverse(X1)))=X1)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f361,f467])).
% 0.13/0.47 fof(f510,plain,(
% 0.13/0.47 ![X0]: (inverse(inverse(X0))=X0)),
% 0.13/0.47 inference(forward_demodulation,[status(thm)],[f407,f509])).
% 0.13/0.47 fof(f519,plain,(
% 0.13/0.47 ![X0,X1]: (multiply(X0,inverse(X1))=divide(X0,X1))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f510,f5])).
% 0.13/0.47 fof(f528,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=multiply(divide(X0,X2),X1))),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f519,f477])).
% 0.13/0.47 fof(f582,plain,(
% 0.13/0.47 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=multiply(X0,divide(divide(X1,X3),divide(X2,X3))))),
% 0.13/0.47 inference(paramodulation,[status(thm)],[f42,f35])).
% 0.13/0.47 fof(f614,plain,(
% 0.13/0.47 ![X0,X1,X2]: (multiply(X0,multiply(multiply(X1,divide(inverse(X2),X0)),X2))=X1)),
% 0.13/0.47 inference(backward_demodulation,[status(thm)],[f582,f321])).
% 0.13/0.47 fof(f681,plain,(
% 0.13/0.47 ![X0,X1]: (divide(X0,inverse(X1))=multiply(X1,X0))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f510,f406])).
% 9.24/1.70 fof(f696,plain,(
% 9.24/1.70 ![X0,X1]: (divide(X0,multiply(X1,X0))=inverse(X1))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f418,f407])).
% 9.24/1.70 fof(f823,plain,(
% 9.24/1.70 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X1,X0)))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f5,f454])).
% 9.24/1.70 fof(f826,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(X1,X2))=multiply(divide(X2,X1),X0))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f454,f406])).
% 9.24/1.70 fof(f828,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f454,f5])).
% 9.24/1.70 fof(f833,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X1,divide(X2,X0)))),
% 9.24/1.70 inference(backward_demodulation,[status(thm)],[f826,f528])).
% 9.24/1.70 fof(f842,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,multiply(divide(X1,divide(X0,inverse(X2))),X2))=X1)),
% 9.24/1.70 inference(backward_demodulation,[status(thm)],[f828,f614])).
% 9.24/1.70 fof(f885,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,divide(X1,divide(divide(X0,inverse(X1)),X2)))=X2)),
% 9.24/1.70 inference(forward_demodulation,[status(thm)],[f826,f842])).
% 9.24/1.70 fof(f886,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(divide(divide(X1,inverse(X0)),X2),X1))=X2)),
% 9.24/1.70 inference(forward_demodulation,[status(thm)],[f833,f885])).
% 9.24/1.70 fof(f887,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(divide(multiply(X1,X0),X2),X1))=X2)),
% 9.24/1.70 inference(forward_demodulation,[status(thm)],[f5,f886])).
% 9.24/1.70 fof(f988,plain,(
% 9.24/1.70 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X0,X1)))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f681,f454])).
% 9.24/1.70 fof(f1067,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(inverse(X1),X2))=multiply(X1,multiply(X2,X0)))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f696,f887])).
% 9.24/1.70 fof(f1233,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(inverse(X1),X2))=multiply(multiply(X2,X1),X0))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f823,f681])).
% 9.24/1.70 fof(f1241,plain,(
% 9.24/1.70 ~multiply(b3,multiply(a3,c3))=multiply(a3,multiply(b3,c3))),
% 9.24/1.70 inference(backward_demodulation,[status(thm)],[f1243,f6])).
% 9.24/1.70 fof(f1243,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X1,X0),X2))),
% 9.24/1.70 inference(forward_demodulation,[status(thm)],[f1067,f1233])).
% 9.24/1.70 fof(f1434,plain,(
% 9.24/1.70 ![X0,X1,X2]: (divide(X0,divide(inverse(X1),X2))=multiply(multiply(X1,X2),X0))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f988,f681])).
% 9.24/1.70 fof(f1444,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 9.24/1.70 inference(forward_demodulation,[status(thm)],[f1067,f1434])).
% 9.24/1.70 fof(f2394,plain,(
% 9.24/1.70 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X1,multiply(X0,X2)))),
% 9.24/1.70 inference(paramodulation,[status(thm)],[f1243,f1444])).
% 9.24/1.70 fof(f2424,plain,(
% 9.24/1.70 $false),
% 9.24/1.70 inference(backward_subsumption_resolution,[status(thm)],[f1241,f2394])).
% 9.24/1.70 % SZS output end CNFRefutation for theBenchmark.p
% 9.24/1.70 % Elapsed time: 1.122498 seconds
% 9.24/1.70 % CPU time: 0.462053 seconds
% 9.24/1.70 % Total memory used: 10.874 MB
% 9.24/1.70 % Net memory used: 9.552 MB
%------------------------------------------------------------------------------