%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP071-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:35:35 PM UTC 2026
% Result : Unsatisfiable 63.06s 8.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP071-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.49 % Computer : n026.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 19:59:07 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.18/0.51 % Drodi V4.1.1
% 63.06/8.65 % Refutation found
% 63.06/8.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 63.06/8.65 % SZS output start CNFRefutation for theBenchmark
% 63.06/8.65 fof(f1,axiom,(
% 63.06/8.65 (![X,Y,Z,U]: (divide(inverse(divide(X,divide(Y,divide(Z,U)))),divide(divide(U,Z),X)) = Y ))),
% 63.06/8.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 63.06/8.65 fof(f2,axiom,(
% 63.06/8.65 (![X,Y]: (multiply(X,Y) = divide(X,inverse(Y)) ))),
% 63.06/8.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 63.06/8.65 fof(f3,negated_conjecture,(
% 63.06/8.65 ( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)| multiply(multiply(inverse(b2),b2),a2) != a2| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ) ),
% 63.06/8.65 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 63.06/8.65 fof(f4,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,divide(X2,X3)))),divide(divide(X3,X2),X0))=X1)),
% 63.06/8.65 inference(cnf_transformation,[status(thm)],[f1])).
% 63.06/8.65 fof(f5,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(X0,X1)=divide(X0,inverse(X1)))),
% 63.06/8.65 inference(cnf_transformation,[status(thm)],[f2])).
% 63.06/8.65 fof(f6,plain,(
% 63.06/8.65 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|~multiply(multiply(inverse(b2),b2),a2)=a2|~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))),
% 63.06/8.65 inference(cnf_transformation,[status(thm)],[f3])).
% 63.06/8.65 fof(f7,definition,(
% 63.06/8.65 sQ0_spl <=> (multiply(inverse(a1),a1)=multiply(inverse(b1),b1))),
% 63.06/8.65 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 63.06/8.65 fof(f9,plain,(
% 63.06/8.65 ~multiply(inverse(a1),a1)=multiply(inverse(b1),b1)|sQ0_spl),
% 63.06/8.65 inference(component_clause,[status(thm)],[f7])).
% 63.06/8.65 fof(f10,definition,(
% 63.06/8.65 sQ1_spl <=> (multiply(multiply(inverse(b2),b2),a2)=a2)),
% 63.06/8.65 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 63.06/8.65 fof(f12,plain,(
% 63.06/8.65 ~multiply(multiply(inverse(b2),b2),a2)=a2|sQ1_spl),
% 63.06/8.65 inference(component_clause,[status(thm)],[f10])).
% 63.06/8.65 fof(f13,definition,(
% 63.06/8.65 sQ2_spl <=> (multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3)))),
% 63.06/8.65 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 63.06/8.65 fof(f15,plain,(
% 63.06/8.65 ~multiply(multiply(a3,b3),c3)=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 63.06/8.65 inference(component_clause,[status(thm)],[f13])).
% 63.06/8.65 fof(f16,plain,(
% 63.06/8.65 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 63.06/8.65 inference(split_clause,[status(thm)],[f6,f7,f10,f13])).
% 63.06/8.65 fof(f17,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(X1,X2),inverse(divide(divide(X2,X1),divide(X0,divide(X3,X4))))))=divide(X4,X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4,f4])).
% 63.06/8.65 fof(f18,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(X4,X3)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4,f4])).
% 63.06/8.65 fof(f20,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(X2,X3)))),divide(divide(inverse(X3),X2),X0))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f4])).
% 63.06/8.65 fof(f21,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(inverse(X0),divide(X1,divide(X2,X3)))),multiply(divide(X3,X2),X0))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f4])).
% 63.06/8.65 fof(f24,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f17])).
% 63.06/8.65 fof(f27,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(inverse(X1),X2),inverse(divide(multiply(X2,X1),divide(X0,multiply(X3,X4))))))=divide(inverse(X4),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f20,f20])).
% 63.06/8.65 fof(f28,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(divide(inverse(X1),X2),inverse(divide(multiply(X2,X1),divide(X0,divide(X3,X4))))))=divide(X4,X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4,f20])).
% 63.06/8.65 fof(f29,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(inverse(X0),divide(X1,multiply(X2,X3)))),multiply(divide(inverse(X3),X2),X0))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f20])).
% 63.06/8.65 fof(f32,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(X0,divide(X1,multiply(inverse(X2),X3)))),divide(multiply(inverse(X3),X2),X0))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f20])).
% 63.06/8.65 fof(f37,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,multiply(X3,X4)))))=divide(inverse(X4),X3))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f27])).
% 63.06/8.65 fof(f38,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,divide(X3,X4)))))=divide(X4,X3))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f28])).
% 63.06/8.65 fof(f64,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(inverse(X0),X1)),multiply(divide(X2,divide(X3,X4)),X0))=inverse(divide(X2,divide(X1,divide(X4,X3)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4,f21])).
% 63.06/8.65 fof(f74,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(divide(inverse(X0),divide(X1,divide(inverse(X2),X3)))),multiply(multiply(X3,X2),X0))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f21])).
% 63.06/8.65 fof(f76,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(X0,X1)),divide(divide(inverse(X2),divide(X3,X4)),X0))=inverse(divide(inverse(X2),divide(X1,divide(X4,X3)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f21,f20])).
% 63.06/8.65 fof(f108,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(X0),multiply(divide(X1,X2),divide(divide(X2,X1),divide(X0,divide(X3,X4)))))=divide(multiply(divide(X5,X6),divide(divide(X6,X5),divide(X7,divide(X4,X3)))),inverse(X7)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f24,f24])).
% 63.06/8.65 fof(f130,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=divide(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),inverse(X4)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f24,f108])).
% 63.06/8.65 fof(f131,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(X0,X1)=multiply(multiply(divide(X2,X3),divide(divide(X3,X2),divide(X4,divide(X0,X1)))),X4))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f130])).
% 63.06/8.65 fof(f265,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(divide(inverse(X0),divide(X1,multiply(X2,X3)))),multiply(divide(inverse(X3),X2),X0))=multiply(multiply(divide(X4,X5),divide(divide(X5,X4),divide(X6,X1))),X6))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f29,f131])).
% 63.06/8.65 fof(f297,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=multiply(multiply(divide(X1,X2),divide(divide(X2,X1),divide(X3,X0))),X3))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f29,f265])).
% 63.06/8.65 fof(f319,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=multiply(multiply(multiply(X1,X2),divide(divide(inverse(X2),X1),divide(X3,X0))),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f297])).
% 63.06/8.65 fof(f328,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=multiply(multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X3,X0))),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f297])).
% 63.06/8.65 fof(f362,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=inverse(divide(X1,divide(divide(X0,divide(divide(X2,X3),X1)),divide(X3,X2)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4,f18])).
% 63.06/8.65 fof(f612,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=multiply(multiply(multiply(inverse(X1),X2),divide(multiply(inverse(X2),X1),divide(X3,X0))),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f319])).
% 63.06/8.65 fof(f655,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (inverse(X0)=multiply(multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),multiply(X3,X0))),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f328])).
% 63.06/8.65 fof(f723,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=inverse(inverse(divide(X0,divide(X1,divide(inverse(divide(divide(X2,X3),X1)),divide(X3,X2)))))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f18,f362])).
% 63.06/8.65 fof(f738,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=inverse(divide(X1,divide(divide(X0,divide(multiply(X2,X3),X1)),divide(inverse(X3),X2)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f362])).
% 63.06/8.65 fof(f880,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(inverse(X0),divide(X1,divide(inverse(divide(multiply(inverse(X2),X3),divide(X0,X4))),multiply(inverse(X3),X2))))),X4)=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f612,f74])).
% 63.06/8.65 fof(f890,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (multiply(inverse(divide(inverse(X0),divide(X1,divide(inverse(divide(multiply(inverse(X2),X3),divide(X0,inverse(X4)))),multiply(inverse(X3),X2))))),X4)=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f880])).
% 63.06/8.65 fof(f967,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (multiply(inverse(divide(inverse(X0),divide(X1,divide(inverse(divide(multiply(inverse(X2),X3),multiply(X0,X4))),multiply(inverse(X3),X2))))),X4)=X1)),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f890])).
% 63.06/8.65 fof(f1675,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (X0=inverse(divide(X1,divide(divide(X0,divide(multiply(inverse(X2),X3),X1)),multiply(inverse(X3),X2)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f738])).
% 63.06/8.65 fof(f2193,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(inverse(divide(divide(X0,X1),multiply(inverse(X2),X3))),divide(X1,X0)),divide(X4,multiply(inverse(X3),X2))))=inverse(inverse(X4)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f32,f723])).
% 63.06/8.65 fof(f2364,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(inverse(X0)),divide(multiply(inverse(X1),X2),divide(inverse(divide(divide(X3,X4),multiply(inverse(X1),X2))),divide(X4,X3))))=X0)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2193,f32])).
% 63.06/8.65 fof(f2451,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (divide(inverse(inverse(inverse(X0))),divide(multiply(inverse(X1),X2),divide(inverse(divide(divide(X3,X4),multiply(inverse(X1),X2))),divide(X4,X3))))=divide(divide(inverse(divide(divide(X5,X6),multiply(inverse(X7),X8))),divide(X6,X5)),divide(X0,multiply(inverse(X8),X7))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2193,f2364])).
% 63.06/8.65 fof(f2574,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (inverse(X0)=divide(divide(inverse(divide(divide(X1,X2),multiply(inverse(X3),X4))),divide(X2,X1)),divide(X0,multiply(inverse(X4),X3))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f2364,f2451])).
% 63.06/8.65 fof(f2729,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,divide(multiply(inverse(X1),X2),X3)),multiply(inverse(X2),X1)))=inverse(divide(X0,inverse(X3))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2574,f362])).
% 63.06/8.65 fof(f2841,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (inverse(divide(divide(X0,divide(multiply(inverse(X1),X2),X3)),multiply(inverse(X2),X1)))=inverse(multiply(X0,X3)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f2729])).
% 63.06/8.65 fof(f2920,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6,X7]: (divide(inverse(inverse(multiply(X0,X1))),divide(multiply(inverse(X2),X3),divide(inverse(divide(divide(X4,X5),multiply(inverse(X2),X3))),divide(X5,X4))))=divide(divide(X0,divide(multiply(inverse(X6),X7),X1)),multiply(inverse(X7),X6)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2841,f2364])).
% 63.06/8.65 fof(f2963,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (multiply(X0,X1)=divide(divide(X0,divide(multiply(inverse(X2),X3),X1)),multiply(inverse(X3),X2)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f2364,f2920])).
% 63.06/8.65 fof(f2967,plain,(
% 63.06/8.65 ![X0,X1]: (X0=inverse(divide(X1,multiply(X0,X1))))),
% 63.06/8.65 inference(backward_demodulation,[status(thm)],[f2963,f1675])).
% 63.06/8.65 fof(f3014,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6]: (divide(inverse(X0),multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X0,multiply(X3,X4)))))=divide(multiply(inverse(X5),X6),divide(X3,divide(multiply(inverse(X6),X5),X4))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2963,f38])).
% 63.06/8.65 fof(f3049,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(X0),X1)=divide(multiply(inverse(X2),X3),divide(X1,divide(multiply(inverse(X3),X2),X0))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f37,f3014])).
% 63.06/8.65 fof(f3548,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(inverse(X0),inverse(divide(X0,divide(X1,multiply(inverse(X2),X3)))))=divide(multiply(inverse(X2),X3),X1))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f32,f3049])).
% 63.06/8.65 fof(f3632,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (multiply(inverse(X0),divide(X0,divide(X1,multiply(inverse(X2),X3))))=divide(multiply(inverse(X2),X3),X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f3548])).
% 63.06/8.65 fof(f3697,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5,X6]: (multiply(inverse(X0),divide(X0,divide(X1,multiply(X2,X3))))=divide(multiply(inverse(inverse(divide(X2,divide(X4,divide(inverse(divide(divide(X5,X6),X4)),divide(X6,X5)))))),X3),X1))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f723,f3632])).
% 63.06/8.65 fof(f3747,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (multiply(inverse(X0),divide(X0,divide(X1,multiply(X2,X3))))=divide(multiply(X2,X3),X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f723,f3697])).
% 63.06/8.65 fof(f3831,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (inverse(X0)=inverse(divide(divide(X0,divide(X1,multiply(X2,X3))),divide(multiply(X2,X3),X1))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f3747,f2967])).
% 63.06/8.65 fof(f3939,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(X0),divide(multiply(inverse(X1),X2),divide(X0,divide(multiply(inverse(X2),X1),multiply(X3,X4)))))=multiply(X3,X4))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f3831,f32])).
% 63.06/8.65 fof(f4029,plain,(
% 63.06/8.65 ![X0,X1,X2]: (divide(inverse(X0),divide(inverse(multiply(X1,X2)),X0))=multiply(X1,X2))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f3049,f3939])).
% 63.06/8.65 fof(f4048,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4,X5]: (divide(inverse(X0),divide(inverse(X1),X0))=multiply(inverse(divide(inverse(X2),divide(X1,divide(inverse(divide(multiply(inverse(X3),X4),multiply(X2,X5))),multiply(inverse(X4),X3))))),X5))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f967,f4029])).
% 63.06/8.65 fof(f4135,plain,(
% 63.06/8.65 ![X0,X1]: (divide(inverse(X0),divide(inverse(X1),X0))=X1)),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f967,f4048])).
% 63.06/8.65 fof(f4221,plain,(
% 63.06/8.65 ![X0,X1]: (divide(inverse(divide(inverse(X0),X1)),X0)=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4135,f4135])).
% 63.06/8.65 fof(f4376,plain,(
% 63.06/8.65 ![X0,X1]: (divide(X0,X1)=multiply(X0,inverse(X1)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2967,f4221])).
% 63.06/8.65 fof(f4615,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (inverse(inverse(X0))=multiply(multiply(divide(inverse(X1),X2),divide(multiply(X2,X1),divide(X3,X0))),X3))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4376,f655])).
% 63.06/8.65 fof(f4639,plain,(
% 63.06/8.65 ![X0]: (inverse(inverse(X0))=X0)),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f328,f4615])).
% 63.06/8.65 fof(f4949,plain,(
% 63.06/8.65 ![X0,X1]: (inverse(X0)=divide(X1,multiply(X0,X1)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f2967,f4639])).
% 63.06/8.65 fof(f4956,plain,(
% 63.06/8.65 ![X0,X1]: (divide(inverse(X0),divide(X1,X0))=inverse(X1))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4639,f4135])).
% 63.06/8.65 fof(f5093,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(inverse(X0),divide(X0,inverse(X1)))=divide(multiply(X1,X2),X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4949,f3747])).
% 63.06/8.65 fof(f5187,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,X1))=divide(multiply(X1,X2),X2))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f5,f5093])).
% 63.06/8.65 fof(f5708,plain,(
% 63.06/8.65 ![X0,X1,X2]: (divide(multiply(X0,X1),X1)=divide(multiply(X0,X2),X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5187,f5187])).
% 63.06/8.65 fof(f5728,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,X1))=multiply(multiply(X1,inverse(X2)),X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f5187])).
% 63.06/8.65 fof(f5755,plain,(
% 63.06/8.65 ![X0,X1,X2]: (inverse(inverse(X0))=divide(multiply(X0,X1),divide(multiply(X1,X2),X2)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5187,f4949])).
% 63.06/8.65 fof(f5882,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(inverse(X0),multiply(X0,X1))=multiply(divide(X1,X2),X2))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4376,f5728])).
% 63.06/8.65 fof(f5887,plain,(
% 63.06/8.65 ![X0,X1,X2]: (X0=divide(multiply(X0,X1),divide(multiply(X1,X2),X2)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4639,f5755])).
% 63.06/8.65 fof(f5965,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(multiply(X0,inverse(X1)),X1)=divide(multiply(X0,X2),X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5,f5708])).
% 63.06/8.65 fof(f6186,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(divide(X0,X1),X1)=divide(multiply(X0,X2),X2))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4376,f5965])).
% 63.06/8.65 fof(f6318,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(multiply(X0,inverse(X1)),X2)=divide(X0,multiply(inverse(X2),X1)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5887,f2963])).
% 63.06/8.65 fof(f6391,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(divide(X0,X1),X2)=divide(X0,multiply(inverse(X2),X1)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4376,f6318])).
% 63.06/8.65 fof(f6434,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(divide(X0,X1),X1)=multiply(divide(X0,X2),X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6186,f6186])).
% 63.06/8.65 fof(f7804,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(divide(X0,X0),X1)=inverse(inverse(X1)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4949,f6391])).
% 63.06/8.65 fof(f7810,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(divide(X0,X1),inverse(X2))=divide(X0,multiply(X2,X1)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4639,f6391])).
% 63.06/8.65 fof(f7913,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(divide(X0,X0),X1)=X1)),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4639,f7804])).
% 63.06/8.65 fof(f7917,plain,(
% 63.06/8.65 ![X0,X1,X2]: (divide(divide(X0,X1),X2)=divide(X0,multiply(X2,X1)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4376,f7810])).
% 63.06/8.65 fof(f7934,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(inverse(X0),multiply(X0,X1))=X1)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f5882,f7913])).
% 63.06/8.65 fof(f7935,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(divide(X0,X1),X1)=X0)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6434,f7913])).
% 63.06/8.65 fof(f7937,plain,(
% 63.06/8.65 ![X0,X1]: (divide(multiply(X0,X1),X1)=X0)),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6186,f7913])).
% 63.06/8.65 fof(f7939,plain,(
% 63.06/8.65 ![X0,X1]: (divide(divide(X0,X0),X1)=inverse(X1))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f4376,f7913])).
% 63.06/8.65 fof(f7970,plain,(
% 63.06/8.65 ![X0,X1,X2]: (divide(multiply(divide(X0,X0),X1),X1)=divide(X2,X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f7913,f5708])).
% 63.06/8.65 fof(f8004,plain,(
% 63.06/8.65 ![X0,X1]: (divide(X0,X0)=divide(X1,X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7913,f7970])).
% 63.06/8.65 fof(f8057,plain,(
% 63.06/8.65 ![X0,X1]: (inverse(divide(X0,X1))=divide(X1,X0))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f7935,f4949])).
% 63.06/8.65 fof(f8183,plain,(
% 63.06/8.65 ![X0,X1]: (divide(inverse(X0),X1)=inverse(multiply(X1,X0)))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f7937,f4956])).
% 63.06/8.65 fof(f9376,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(divide(multiply(inverse(X0),X1),X1),X0)=divide(X2,X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6391,f8004])).
% 63.06/8.65 fof(f9637,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(inverse(X0),X0)=divide(X1,X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7937,f9376])).
% 63.06/8.65 fof(f10504,plain,(
% 63.06/8.65 ![X0,X1,X2]: (divide(multiply(divide(multiply(inverse(X0),X1),X1),X0),X2)=inverse(X2))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6391,f7939])).
% 63.06/8.65 fof(f10572,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(inverse(divide(inverse(X0),X1)),multiply(inverse(divide(X2,X3)),X0))=inverse(divide(divide(X4,X4),divide(X1,divide(X3,X2)))))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f7939,f64])).
% 63.06/8.65 fof(f10632,plain,(
% 63.06/8.65 ![X0,X1]: (divide(multiply(inverse(X0),X0),X1)=inverse(X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7937,f10504])).
% 63.06/8.65 fof(f10732,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (multiply(divide(inverse(divide(inverse(X0),X1)),X0),divide(X2,X3))=inverse(divide(divide(X4,X4),divide(X1,divide(X3,X2)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f6391,f10572])).
% 63.06/8.65 fof(f10733,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (multiply(X0,divide(X1,X2))=inverse(divide(divide(X3,X3),divide(X0,divide(X2,X1)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4221,f10732])).
% 63.06/8.65 fof(f10734,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=inverse(inverse(divide(X0,divide(X2,X1)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7939,f10733])).
% 63.06/8.65 fof(f10735,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(X0,divide(X1,X2))=divide(X0,divide(X2,X1)))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f4639,f10734])).
% 63.06/8.65 fof(f12540,plain,(
% 63.06/8.65 ![X0,X1,X2]: (multiply(inverse(X0),X0)=multiply(divide(multiply(inverse(X1),X2),X2),X1))),
% 63.06/8.65 inference(paramodulation,[status(thm)],[f6391,f9637])).
% 63.06/8.65 fof(f12620,plain,(
% 63.06/8.65 ![X0,X1]: (multiply(inverse(X0),X0)=multiply(inverse(X1),X1))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7937,f12540])).
% 63.06/8.65 fof(f17864,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (inverse(multiply(divide(divide(inverse(X0),divide(X1,X2)),X3),divide(X3,X4)))=inverse(divide(inverse(X0),divide(X4,divide(X2,X1)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f8183,f76])).
% 63.06/8.65 fof(f17865,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (inverse(divide(divide(divide(inverse(X0),divide(X1,X2)),X3),divide(X4,X3)))=inverse(divide(inverse(X0),divide(X4,divide(X2,X1)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f10735,f17864])).
% 63.06/8.65 fof(f17866,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(divide(X0,X1),divide(divide(inverse(X2),divide(X3,X4)),X1))=inverse(divide(inverse(X2),divide(X0,divide(X4,X3)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f8057,f17865])).
% 63.06/8.65 fof(f17867,plain,(
% 63.06/8.65 ![X0,X1,X2,X3,X4]: (divide(X0,multiply(divide(divide(inverse(X1),divide(X2,X3)),X4),X4))=inverse(divide(inverse(X1),divide(X0,divide(X3,X2)))))),
% 63.06/8.65 inference(forward_demodulation,[status(thm)],[f7917,f17866])).
% 63.06/8.65 fof(f17868,plain,(
% 63.06/8.65 ![X0,X1,X2,X3]: (divide(X0,divide(inverse(X1),divide(X2,X3)))=inverse(divide(inverse(X1),divide(X0,divide(X3,X2)))))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f7935,f17867])).
% 63.06/8.68 fof(f17869,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (divide(X0,inverse(multiply(divide(X1,X2),X3)))=inverse(divide(inverse(X3),divide(X0,divide(X2,X1)))))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f8183,f17868])).
% 63.06/8.68 fof(f17870,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(X1,X2),X3))=inverse(divide(inverse(X3),divide(X0,divide(X2,X1)))))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f5,f17869])).
% 63.06/8.68 fof(f17871,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(X1,X2),X3))=divide(divide(X0,divide(X2,X1)),inverse(X3)))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f8057,f17870])).
% 63.06/8.68 fof(f17872,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(X1,X2),X3))=divide(X0,multiply(inverse(X3),divide(X2,X1))))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f7917,f17871])).
% 63.06/8.68 fof(f17875,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(X1,X2),X3))=multiply(divide(X0,divide(X2,X1)),X3))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f6391,f17872])).
% 63.06/8.68 fof(f17893,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(divide(X1,multiply(inverse(X2),X2)),X3))=multiply(divide(X0,inverse(X1)),X3))),
% 63.06/8.68 inference(paramodulation,[status(thm)],[f10632,f17875])).
% 63.06/8.68 fof(f17943,plain,(
% 63.06/8.68 ![X0,X1,X2,X3]: (multiply(X0,multiply(multiply(divide(X1,X2),X2),X3))=multiply(divide(X0,inverse(X1)),X3))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f6391,f17893])).
% 63.06/8.68 fof(f17944,plain,(
% 63.06/8.68 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(divide(X0,inverse(X1)),X2))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f7935,f17943])).
% 63.06/8.68 fof(f17945,plain,(
% 63.06/8.68 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X0,X1),X2))),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f5,f17944])).
% 63.06/8.68 fof(f19098,plain,(
% 63.06/8.68 ~multiply(a3,multiply(b3,c3))=multiply(a3,multiply(b3,c3))|sQ2_spl),
% 63.06/8.68 inference(backward_demodulation,[status(thm)],[f17945,f15])).
% 63.06/8.68 fof(f19127,plain,(
% 63.06/8.68 $false|sQ2_spl),
% 63.06/8.68 inference(trivial_equality_resolution,[status(thm)],[f19098])).
% 63.06/8.68 fof(f19128,plain,(
% 63.06/8.68 sQ2_spl),
% 63.06/8.68 inference(contradiction_clause,[status(thm)],[f19127])).
% 63.06/8.68 fof(f19158,plain,(
% 63.06/8.68 $false|sQ0_spl),
% 63.06/8.68 inference(forward_subsumption_resolution,[status(thm)],[f9,f12620])).
% 63.06/8.68 fof(f19159,plain,(
% 63.06/8.68 sQ0_spl),
% 63.06/8.68 inference(contradiction_clause,[status(thm)],[f19158])).
% 63.06/8.68 fof(f19160,plain,(
% 63.06/8.68 ~multiply(inverse(b2),multiply(b2,a2))=a2|sQ1_spl),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f17945,f12])).
% 63.06/8.68 fof(f19161,plain,(
% 63.06/8.68 ~a2=a2|sQ1_spl),
% 63.06/8.68 inference(forward_demodulation,[status(thm)],[f7934,f19160])).
% 63.06/8.68 fof(f19162,plain,(
% 63.06/8.68 $false|sQ1_spl),
% 63.06/8.68 inference(trivial_equality_resolution,[status(thm)],[f19161])).
% 63.06/8.68 fof(f19163,plain,(
% 63.06/8.68 sQ1_spl),
% 63.06/8.68 inference(contradiction_clause,[status(thm)],[f19162])).
% 63.06/8.68 fof(f19164,plain,(
% 63.06/8.68 $false),
% 63.06/8.68 inference(sat_refutation,[status(thm)],[f16,f19128,f19159,f19163])).
% 63.06/8.68 % SZS output end CNFRefutation for theBenchmark.p
% 12.05/8.75 % Elapsed time: 8.238987 seconds
% 12.05/8.75 % CPU time: 64.699447 seconds
% 12.05/8.75 % Total memory used: 725.547 MB
% 12.05/8.75 % Net memory used: 718.620 MB
%------------------------------------------------------------------------------