%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG005-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 11:49:26 AM UTC 2026
% Result : Unsatisfiable 8.08s 1.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG005-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n020.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 12:53:19 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 8.08/1.64 % Refutation found
% 8.08/1.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 8.08/1.64 % SZS output start CNFRefutation for theBenchmark
% 8.08/1.64 fof(f1,axiom,(
% 8.08/1.64 (![X,Y]: (difference(X,difference(Y,X)) = X ))),
% 8.08/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.08/1.64 fof(f2,axiom,(
% 8.08/1.64 (![X,Y]: (difference(X,difference(X,Y)) = difference(Y,difference(Y,X)) ))),
% 8.08/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.08/1.64 fof(f3,axiom,(
% 8.08/1.64 (![X,Y,Z]: (difference(difference(X,Y),Z) = difference(difference(X,Z),difference(Y,Z)) ))),
% 8.08/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.08/1.64 fof(f4,axiom,(
% 8.08/1.64 (![X,Y]: (multiply(X,Y) = difference(X,difference(X,Y)) ))),
% 8.08/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.08/1.64 fof(f5,negated_conjecture,(
% 8.08/1.64 multiply(multiply(a,b),c) != multiply(a,multiply(b,c)) ),
% 8.08/1.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.08/1.64 fof(f6,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X1,X0))=X0)),
% 8.08/1.64 inference(cnf_transformation,[status(thm)],[f1])).
% 8.08/1.64 fof(f7,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X0,X1))=difference(X1,difference(X1,X0)))),
% 8.08/1.64 inference(cnf_transformation,[status(thm)],[f2])).
% 8.08/1.64 fof(f8,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),X2)=difference(difference(X0,X2),difference(X1,X2)))),
% 8.08/1.64 inference(cnf_transformation,[status(thm)],[f3])).
% 8.08/1.64 fof(f9,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(X0,X1)=difference(X0,difference(X0,X1)))),
% 8.08/1.64 inference(cnf_transformation,[status(thm)],[f4])).
% 8.08/1.64 fof(f10,plain,(
% 8.08/1.64 ~multiply(multiply(a,b),c)=multiply(a,multiply(b,c))),
% 8.08/1.64 inference(cnf_transformation,[status(thm)],[f5])).
% 8.08/1.64 fof(f16,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X0,X1))=multiply(X1,X0))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f9,f7])).
% 8.08/1.64 fof(f17,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(X0,difference(X0,X1))=difference(X0,multiply(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f9])).
% 8.08/1.64 fof(f212,plain,(
% 8.08/1.64 ![X0]: (multiply(X0,X0)=X0)),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f6])).
% 8.08/1.64 fof(f217,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),X1)=difference(X0,X1))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f6,f6])).
% 8.08/1.64 fof(f219,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),multiply(X0,X1))=difference(X0,X1))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f6])).
% 8.08/1.64 fof(f222,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X0)=multiply(difference(X1,X0),X0))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f6,f16])).
% 8.08/1.64 fof(f223,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(X0,difference(X1,X0))=difference(X0,X0))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f6,f9])).
% 8.08/1.64 fof(f258,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X1),difference(X1,X0))=difference(X1,difference(X1,X0)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f217])).
% 8.08/1.64 fof(f262,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(difference(X0,X1),X1)=difference(difference(X0,X1),difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f217,f9])).
% 8.08/1.64 fof(f266,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X1),difference(X1,X0))=multiply(X0,X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f16,f258])).
% 8.08/1.64 fof(f269,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X0)=difference(difference(X1,X0),difference(X1,X0)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f222,f262])).
% 8.08/1.64 fof(f270,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X0)=difference(difference(X1,X1),X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f269])).
% 8.08/1.64 fof(f348,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(difference(X0,X1),multiply(X1,X0))=difference(difference(X0,X1),difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f223])).
% 8.08/1.64 fof(f360,plain,(
% 8.08/1.64 ![X0,X1]: (multiply(difference(X0,X1),multiply(X1,X0))=difference(difference(X0,X0),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f348])).
% 8.08/1.64 fof(f402,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,difference(X1,X0)),difference(X1,X0))=multiply(X0,difference(X1,X0)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f217,f266])).
% 8.08/1.64 fof(f409,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(difference(X0,X1),X0),multiply(X0,X1))=multiply(difference(X0,X1),X0))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f266])).
% 8.08/1.64 fof(f415,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X1),multiply(X0,X1))=multiply(difference(X1,X0),multiply(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f266,f16])).
% 8.08/1.64 fof(f427,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X1,X0))=multiply(X0,difference(X1,X0)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f223,f402])).
% 8.08/1.64 fof(f428,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),X0)=multiply(X0,difference(X1,X0)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f427])).
% 8.08/1.64 fof(f429,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),X0)=difference(X0,X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f223,f428])).
% 8.08/1.64 fof(f448,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X1),multiply(X0,X1))=difference(difference(X1,X1),X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f360,f415])).
% 8.08/1.64 fof(f454,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X0,X1))=difference(difference(X0,X1),difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f429,f429])).
% 8.08/1.64 fof(f455,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X1,X1))=difference(difference(X1,X1),difference(X1,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f270,f429])).
% 8.08/1.64 fof(f462,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X1),X1)=difference(X1,X1))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f429])).
% 8.08/1.64 fof(f472,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),difference(X0,X0))=multiply(X0,difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f429,f16])).
% 8.08/1.64 fof(f474,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X0,X1))=difference(difference(X0,X0),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f454])).
% 8.08/1.64 fof(f475,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X1,X1))=difference(difference(X1,X1),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f474,f455])).
% 8.08/1.64 fof(f476,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X1,X1))=difference(X1,X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f429,f475])).
% 8.08/1.64 fof(f539,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),multiply(X1,X0))=difference(multiply(X1,X0),multiply(X1,X0)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f462,f429])).
% 8.08/1.64 fof(f558,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),multiply(X1,X0))=difference(difference(X0,X0),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f448,f539])).
% 8.08/1.64 fof(f574,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X2,X0))=difference(X0,difference(X1,difference(X2,X0))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f6,f8])).
% 8.08/1.64 fof(f575,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X0,X2))=difference(multiply(X2,X0),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f8])).
% 8.08/1.64 fof(f576,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X0,X2))=difference(multiply(X0,X2),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f8])).
% 8.08/1.64 fof(f579,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),X1)=difference(difference(X0,X1),difference(X1,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f429,f8])).
% 8.08/1.64 fof(f583,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,multiply(X1,X2)),X2)=difference(difference(X0,X2),difference(X2,X2)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f462,f8])).
% 8.08/1.64 fof(f602,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(difference(X0,X2),X1))=multiply(difference(X2,X1),difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f8,f16])).
% 8.08/1.64 fof(f603,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(difference(X0,X1),difference(X2,X1))=difference(difference(X0,X1),difference(difference(X0,X2),X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f8,f9])).
% 8.08/1.64 fof(f620,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X1,difference(X0,X0)))=multiply(X0,difference(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f574,f472])).
% 8.08/1.64 fof(f624,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),X1)=difference(difference(X0,X1),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f579])).
% 8.08/1.64 fof(f625,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),X1)=difference(X0,X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f217,f624])).
% 8.08/1.64 fof(f629,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,multiply(X1,X2)),X2)=difference(difference(X0,X2),X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f583])).
% 8.08/1.64 fof(f630,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,multiply(X1,X2)),X2)=difference(X0,X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f217,f629])).
% 8.08/1.64 fof(f647,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X0,X1)),X2)=multiply(difference(X1,X2),difference(X0,X2)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f602])).
% 8.08/1.64 fof(f651,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=multiply(difference(X0,X2),difference(X1,X2)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f16,f647])).
% 8.08/1.64 fof(f652,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=difference(difference(X0,X2),difference(difference(X0,X1),X2)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f651,f603])).
% 8.08/1.64 fof(f653,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=difference(difference(X0,difference(X0,X1)),X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f8,f652])).
% 8.08/1.64 fof(f654,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=difference(multiply(X1,X0),X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f16,f653])).
% 8.08/1.64 fof(f751,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),multiply(difference(X1,X1),X0))=difference(difference(X1,X1),X0))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f270,f219])).
% 8.08/1.64 fof(f760,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(difference(X0,X0),X1),multiply(X1,X1))=difference(X1,X1))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f270,f219])).
% 8.08/1.64 fof(f797,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),difference(X1,X1))=difference(difference(X1,X1),X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f558,f751])).
% 8.08/1.64 fof(f826,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X0)=difference(difference(X0,X0),X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f476,f797])).
% 8.08/1.64 fof(f842,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X0),multiply(X1,X1))=difference(X1,X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f826,f760])).
% 8.08/1.64 fof(f843,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X0)=difference(X1,X1))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f826,f842])).
% 8.08/1.64 fof(f913,plain,(
% 8.08/1.64 ![X0,X1]: (difference(multiply(X0,X0),difference(X1,X1))=multiply(X0,X0))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f843,f266])).
% 8.08/1.64 fof(f936,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X1,X1))=multiply(X0,X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f212,f913])).
% 8.08/1.64 fof(f943,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X1)=multiply(X0,difference(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f945,f620])).
% 8.08/1.64 fof(f945,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,difference(X1,X1))=X0)),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f212,f936])).
% 8.08/1.64 fof(f985,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X1)=difference(X0,multiply(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f943,f17])).
% 8.08/1.64 fof(f1584,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),difference(difference(X0,X1),X0))=difference(multiply(difference(X0,X1),X0),difference(X2,difference(X0,X0))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f429,f576])).
% 8.08/1.64 fof(f1672,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),difference(X0,X0))=difference(multiply(difference(X0,X1),X0),difference(X2,difference(X0,X0))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f429,f1584])).
% 8.08/1.64 fof(f1673,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),X2)=difference(multiply(difference(X0,X1),X0),difference(X2,difference(X0,X0))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f945,f1672])).
% 8.08/1.64 fof(f1676,plain,(
% 8.08/1.64 ![X0,X1]: (difference(difference(X0,X1),multiply(X0,X1))=multiply(difference(X0,X1),X0))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f1678,f409])).
% 8.08/1.64 fof(f1678,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),X2)=difference(multiply(difference(X0,X1),X0),X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f945,f1673])).
% 8.08/1.64 fof(f1742,plain,(
% 8.08/1.64 ![X0,X1]: (difference(X0,X1)=multiply(difference(X0,X1),X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f219,f1676])).
% 8.08/1.64 fof(f1755,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(difference(X0,X1),X2),multiply(X0,X1))=multiply(difference(X0,X1),difference(X2,multiply(X0,X1))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f219,f651])).
% 8.08/1.64 fof(f1766,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),difference(X2,X0))=multiply(X0,difference(X1,difference(X2,X0))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f6,f651])).
% 8.08/1.64 fof(f1767,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),difference(X0,X2))=multiply(multiply(X2,X0),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f16,f651])).
% 8.08/1.64 fof(f1768,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),difference(X0,X2))=multiply(multiply(X0,X2),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f651])).
% 8.08/1.64 fof(f1775,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,difference(X1,X2)),X2)=multiply(difference(X0,X2),difference(X1,X2)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f217,f651])).
% 8.08/1.64 fof(f1819,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,difference(X1,X2)),X2)=difference(multiply(X0,X1),X2))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f651,f1775])).
% 8.08/1.64 fof(f1878,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),multiply(X0,X2))=multiply(difference(X0,X2),difference(X1,multiply(X0,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f985,f651])).
% 8.08/1.64 fof(f1901,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(difference(X0,X1),X2),multiply(X0,X1))=difference(multiply(X0,X2),multiply(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f1878,f1755])).
% 8.08/1.64 fof(f2838,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(multiply(X0,X1),X2),difference(X0,X1))=difference(multiply(X0,X1),difference(X2,difference(difference(X0,X1),multiply(X0,X1)))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f219,f574])).
% 8.08/1.64 fof(f2865,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),difference(X0,X1))=difference(multiply(X1,X0),difference(X1,difference(X2,difference(X0,X1)))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f574,f575])).
% 8.08/1.64 fof(f2873,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X2,X0))=multiply(difference(X0,X1),difference(X0,difference(X1,difference(X2,X0)))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f574,f943])).
% 8.08/1.64 fof(f2933,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(multiply(X0,X1),X2),difference(X0,X1))=difference(multiply(X0,X1),difference(X2,difference(X0,X1))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f219,f2838])).
% 8.08/1.64 fof(f2934,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(multiply(X0,X1),X2),difference(X0,X1))=difference(difference(X0,X2),difference(X0,X1)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f576,f2933])).
% 8.08/1.64 fof(f2993,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(X0,difference(X1,difference(X2,X0)))=multiply(difference(X0,X1),difference(X0,difference(X1,difference(X2,X0)))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f574,f2873])).
% 8.08/1.64 fof(f3758,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=difference(multiply(X1,X0),difference(multiply(X0,X1),X2)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f654])).
% 8.08/1.64 fof(f6852,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),X1)=multiply(difference(X0,X1),difference(X0,difference(X1,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f625,f1742])).
% 8.08/1.64 fof(f6864,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X2)),difference(X0,X1))=multiply(X1,difference(X0,difference(X1,X2))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f625,f16])).
% 8.08/1.64 fof(f6918,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(X0,difference(X1,difference(X2,X0)))=difference(X0,X1))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f6919,f2993])).
% 8.08/1.64 fof(f6919,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(X0,X1)=multiply(difference(X0,X1),difference(X0,difference(X1,X2))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f625,f6852])).
% 8.08/1.64 fof(f6938,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=difference(multiply(X0,X1),difference(X0,difference(X2,difference(X1,X0)))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f6864,f2865])).
% 8.08/1.64 fof(f6941,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X2,X0))=difference(X0,X1))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f6918,f574])).
% 8.08/1.64 fof(f6989,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=multiply(multiply(X0,X2),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f6991,f1768])).
% 8.08/1.64 fof(f6990,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=multiply(multiply(X2,X0),difference(X1,difference(X0,X2))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f6991,f1767])).
% 8.08/1.64 fof(f6991,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=difference(multiply(X0,X1),difference(X0,X2)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f6918,f6938])).
% 8.08/1.64 fof(f7342,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(X0,difference(X1,X0))=difference(X0,multiply(X2,difference(X1,X0))))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f630,f6941])).
% 8.08/1.64 fof(f7393,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),difference(X2,X0))=difference(X0,difference(X0,X1)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f9,f6941])).
% 8.08/1.64 fof(f7409,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(difference(multiply(X0,X1),X2),difference(X0,X1))=difference(multiply(X0,X1),X2))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f219,f6941])).
% 8.08/1.64 fof(f7509,plain,(
% 8.08/1.64 ![X0,X1,X2]: (X0=difference(X0,multiply(X1,difference(X2,X0))))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f6,f7342])).
% 8.08/1.64 fof(f7551,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,X1)=multiply(X1,difference(X0,difference(X2,X1))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f7552,f1766])).
% 8.08/1.64 fof(f7552,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),difference(X2,X0))=multiply(X1,X0))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f16,f7393])).
% 8.08/1.64 fof(f7562,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=difference(difference(X0,X2),difference(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f7409,f2934])).
% 8.08/1.64 fof(f7629,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=difference(multiply(X0,X1),difference(X2,difference(X0,X1))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f7562,f576])).
% 8.08/1.64 fof(f7971,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(multiply(X0,X1),difference(X2,difference(X0,X1)))=difference(multiply(X0,X1),difference(multiply(X0,X1),X2)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f7629,f9])).
% 8.08/1.64 fof(f8112,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=difference(multiply(X0,X2),difference(multiply(X0,X2),X1)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f6989,f7971])).
% 8.08/1.64 fof(f8118,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(multiply(X2,X1),difference(X0,difference(X1,X2))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8123,f6990])).
% 8.08/1.64 fof(f8123,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,difference(X0,X2)))=multiply(X1,multiply(X0,X2)))),
% 8.08/1.64 inference(forward_demodulation,[status(thm)],[f16,f8112])).
% 8.08/1.64 fof(f8526,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,difference(X1,X2)),X2)=multiply(X0,difference(X1,X2)))),
% 8.08/1.64 inference(paramodulation,[status(thm)],[f7509,f6])).
% 8.08/1.64 fof(f8549,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,X2))=difference(multiply(X0,X1),X2))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8526,f1819])).
% 8.08/1.64 fof(f8557,plain,(
% 8.08/1.64 ![X0,X1,X2]: (difference(multiply(X0,X1),X2)=multiply(X1,difference(X0,X2)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8549,f654])).
% 8.08/1.64 fof(f8583,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(difference(X0,X1),difference(X2,multiply(X0,X1)))=difference(multiply(X0,X2),multiply(X0,X1)))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8549,f1901])).
% 8.08/1.64 fof(f8654,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X1,difference(X0,difference(multiply(X0,X1),X2))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8549,f3758])).
% 8.08/1.64 fof(f8674,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(X0,difference(X1,multiply(X0,X2)))=multiply(difference(X0,X2),difference(X1,multiply(X0,X2))))),
% 8.08/1.64 inference(backward_demodulation,[status(thm)],[f8549,f1878])).
% 8.08/1.64 fof(f8813,plain,(
% 8.08/1.64 ![X0,X1,X2]: (multiply(difference(X0,X1),difference(X2,multiply(X0,X1)))=multiply(X2,difference(X0,multiply(X0,X1))))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f8557,f8583])).
% 8.08/1.66 fof(f8814,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(difference(X0,X1),difference(X2,multiply(X0,X1)))=multiply(X2,difference(X0,X1)))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f985,f8813])).
% 8.08/1.66 fof(f8914,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X1,difference(X0,multiply(X1,difference(X0,X2)))))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f8557,f8654])).
% 8.08/1.66 fof(f8930,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,difference(X1,difference(X0,X2))))),
% 8.08/1.66 inference(backward_demodulation,[status(thm)],[f8933,f8914])).
% 8.08/1.66 fof(f8933,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(X0,difference(X1,multiply(X0,X2)))=multiply(X1,difference(X0,X2)))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f8814,f8674])).
% 8.08/1.66 fof(f9150,plain,(
% 8.08/1.66 ~multiply(b,multiply(a,c))=multiply(a,multiply(b,c))),
% 8.08/1.66 inference(backward_demodulation,[status(thm)],[f9188,f10])).
% 8.08/1.66 fof(f9175,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X1,multiply(X2,difference(X0,difference(X1,X2)))))),
% 8.08/1.66 inference(backward_demodulation,[status(thm)],[f9188,f8118])).
% 8.08/1.66 fof(f9188,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X1,multiply(X0,X2)))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f8123,f8930])).
% 8.08/1.66 fof(f9286,plain,(
% 8.08/1.66 ![X0,X1,X2]: (multiply(X0,multiply(X1,X2))=multiply(X1,multiply(X0,X2)))),
% 8.08/1.66 inference(forward_demodulation,[status(thm)],[f7551,f9175])).
% 8.08/1.66 fof(f9287,plain,(
% 8.08/1.66 $false),
% 8.08/1.66 inference(backward_subsumption_resolution,[status(thm)],[f9150,f9286])).
% 8.08/1.66 % SZS output end CNFRefutation for theBenchmark.p
% 8.08/1.70 % Elapsed time: 1.227359 seconds
% 8.08/1.70 % CPU time: 9.186648 seconds
% 8.08/1.70 % Total memory used: 76.518 MB
% 8.08/1.70 % Net memory used: 74.331 MB
%------------------------------------------------------------------------------