%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG007-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 02:05:06 PM UTC 2026
% Result : Unsatisfiable 5.39s 1.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG007-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 04:10:04 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 5.39/1.14 % Refutation found
% 5.39/1.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.39/1.14 % SZS output start CNFRefutation for theBenchmark
% 5.39/1.14 fof(f1,axiom,(
% 5.39/1.14 (![X]: (sum(additive_identity,X,X) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f2,axiom,(
% 5.39/1.14 (![X]: (sum(X,additive_identity,X) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f3,axiom,(
% 5.39/1.14 (![X,Y]: (product(X,Y,multiply(X,Y)) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f4,axiom,(
% 5.39/1.14 (![X,Y]: (sum(X,Y,add(X,Y)) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f5,axiom,(
% 5.39/1.14 (![X]: (sum(additive_inverse(X),X,additive_identity) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f6,axiom,(
% 5.39/1.14 (![X]: (sum(X,additive_inverse(X),additive_identity) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f8,axiom,(
% 5.39/1.14 (![X,Y,U,Z,V,W]: (( ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(X,V,W)| sum(U,Z,W) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f9,axiom,(
% 5.39/1.14 (![X,Y,Z]: (( ~ sum(X,Y,Z)| sum(Y,X,Z) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f10,axiom,(
% 5.39/1.14 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W)| product(X,V,W) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f11,axiom,(
% 5.39/1.14 (![X,Y,U,Z,V,W]: (( ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(X,V,W)| product(U,Z,W) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f12,axiom,(
% 5.39/1.14 (![X,Y,V1,Z,V2,V3,V4]: (( ~ product(X,Y,V1)| ~ product(X,Z,V2)| ~ sum(Y,Z,V3)| ~ product(X,V3,V4)| sum(V1,V2,V4) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f14,axiom,(
% 5.39/1.14 (![Y,X,V1,Z,V2,V3,V4]: (( ~ product(Y,X,V1)| ~ product(Z,X,V2)| ~ sum(Y,Z,V3)| ~ product(V3,X,V4)| sum(V1,V2,V4) ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f16,axiom,(
% 5.39/1.14 (![X,Y,U,V]: (( ~ sum(X,Y,U)| ~ sum(X,Y,V)| U = V ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f17,axiom,(
% 5.39/1.14 (![X,Y,U,V]: (( ~ product(X,Y,U)| ~ product(X,Y,V)| U = V ) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f18,hypothesis,(
% 5.39/1.14 (![X]: (product(X,X,X) ))),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f19,negated_conjecture,(
% 5.39/1.14 ~ sum(a,a,additive_identity) ),
% 5.39/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.39/1.14 fof(f20,plain,(
% 5.39/1.14 ![X0]: (sum(additive_identity,X0,X0))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f1])).
% 5.39/1.14 fof(f21,plain,(
% 5.39/1.14 ![X0]: (sum(X0,additive_identity,X0))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f2])).
% 5.39/1.14 fof(f22,plain,(
% 5.39/1.14 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f3])).
% 5.39/1.14 fof(f23,plain,(
% 5.39/1.14 ![X0,X1]: (sum(X0,X1,add(X0,X1)))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f4])).
% 5.39/1.14 fof(f24,plain,(
% 5.39/1.14 ![X0]: (sum(additive_inverse(X0),X0,additive_identity))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f5])).
% 5.39/1.14 fof(f25,plain,(
% 5.39/1.14 ![X0]: (sum(X0,additive_inverse(X0),additive_identity))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f6])).
% 5.39/1.14 fof(f28,plain,(
% 5.39/1.14 ![U,Z,W]: ((![X,V]: ((![Y]: (~sum(X,Y,U)|~sum(Y,Z,V)))|~sum(X,V,W)))|sum(U,Z,W))),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f8])).
% 5.39/1.14 fof(f29,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5]: (~sum(X0,X1,X2)|~sum(X1,X3,X4)|~sum(X0,X4,X5)|sum(X2,X3,X5))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f28])).
% 5.39/1.14 fof(f30,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~sum(X0,X1,X2)|sum(X1,X0,X2))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f9])).
% 5.39/1.14 fof(f31,plain,(
% 5.39/1.14 ![X,V,W]: ((![U,Z]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(U,Z,W)))|product(X,V,W))),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f10])).
% 5.39/1.14 fof(f32,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X2,X3,X5)|product(X0,X4,X5))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f31])).
% 5.39/1.14 fof(f33,plain,(
% 5.39/1.14 ![U,Z,W]: ((![X,V]: ((![Y]: (~product(X,Y,U)|~product(Y,Z,V)))|~product(X,V,W)))|product(U,Z,W))),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f11])).
% 5.39/1.14 fof(f34,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~product(X1,X3,X4)|~product(X0,X4,X5)|product(X2,X3,X5))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f33])).
% 5.39/1.14 fof(f35,plain,(
% 5.39/1.14 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~product(X,Y,V1)|~product(X,Z,V2))|~sum(Y,Z,V3)))|~product(X,V3,V4)))|sum(V1,V2,V4))),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f12])).
% 5.39/1.14 fof(f36,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X0,X3,X4)|~sum(X1,X3,X5)|~product(X0,X5,X6)|sum(X2,X4,X6))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f35])).
% 5.39/1.14 fof(f39,plain,(
% 5.39/1.14 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~product(Y,X,V1)|~product(Z,X,V2))|~sum(Y,Z,V3)))|~product(V3,X,V4)))|sum(V1,V2,V4))),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f14])).
% 5.39/1.14 fof(f40,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X3,X1,X4)|~sum(X0,X3,X5)|~product(X5,X1,X6)|sum(X2,X4,X6))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f39])).
% 5.39/1.14 fof(f43,plain,(
% 5.39/1.14 ![U,V]: ((![X,Y]: (~sum(X,Y,U)|~sum(X,Y,V)))|U=V)),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f16])).
% 5.39/1.14 fof(f44,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~sum(X0,X1,X3)|X2=X3)),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f43])).
% 5.39/1.14 fof(f45,plain,(
% 5.39/1.14 ![U,V]: ((![X,Y]: (~product(X,Y,U)|~product(X,Y,V)))|U=V)),
% 5.39/1.14 inference(miniscoping,[status(thm)],[f17])).
% 5.39/1.14 fof(f46,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|X2=X3)),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f45])).
% 5.39/1.14 fof(f47,plain,(
% 5.39/1.14 ![X0]: (product(X0,X0,X0))),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f18])).
% 5.39/1.14 fof(f48,plain,(
% 5.39/1.14 ~sum(a,a,additive_identity)),
% 5.39/1.14 inference(cnf_transformation,[status(thm)],[f19])).
% 5.39/1.14 fof(f51,plain,(
% 5.39/1.14 ![X0,X1]: (~sum(additive_identity,X0,X1)|X0=X1)),
% 5.39/1.14 inference(resolution,[status(thm)],[f44,f20])).
% 5.39/1.14 fof(f52,plain,(
% 5.39/1.14 ![X0,X1]: (~sum(X0,additive_identity,X1)|X0=X1)),
% 5.39/1.14 inference(resolution,[status(thm)],[f44,f21])).
% 5.39/1.14 fof(f61,plain,(
% 5.39/1.14 ![X0]: (X0=add(additive_identity,X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f23,f51])).
% 5.39/1.14 fof(f62,plain,(
% 5.39/1.14 ![X0]: (X0=add(X0,additive_identity))),
% 5.39/1.14 inference(resolution,[status(thm)],[f23,f52])).
% 5.39/1.14 fof(f63,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~sum(X3,X2,X4)|sum(add(X3,X0),X1,X4))),
% 5.39/1.14 inference(resolution,[status(thm)],[f23,f29])).
% 5.39/1.14 fof(f65,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X0,X1)=X2)),
% 5.39/1.14 inference(resolution,[status(thm)],[f23,f44])).
% 5.39/1.14 fof(f66,plain,(
% 5.39/1.14 ![X0,X1]: (sum(X0,X1,add(X1,X0)))),
% 5.39/1.14 inference(resolution,[status(thm)],[f23,f30])).
% 5.39/1.14 fof(f81,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(multiply(X3,X0),X1,X4)|product(X3,X2,X4))),
% 5.39/1.14 inference(resolution,[status(thm)],[f32,f22])).
% 5.39/1.14 fof(f82,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|product(X0,X2,X3))),
% 5.39/1.14 inference(resolution,[status(thm)],[f32,f47])).
% 5.39/1.14 fof(f83,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~product(X3,X2,X4)|product(multiply(X3,X0),X1,X4))),
% 5.39/1.14 inference(resolution,[status(thm)],[f34,f22])).
% 5.39/1.14 fof(f97,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X1,X0)=X2)),
% 5.39/1.14 inference(resolution,[status(thm)],[f66,f44])).
% 5.39/1.14 fof(f101,plain,(
% 5.39/1.14 ![X0]: (add(additive_inverse(X0),X0)=additive_identity)),
% 5.39/1.14 inference(resolution,[status(thm)],[f65,f24])).
% 5.39/1.14 fof(f103,plain,(
% 5.39/1.14 ![X0]: (add(X0,additive_inverse(X0))=additive_identity)),
% 5.39/1.14 inference(resolution,[status(thm)],[f65,f25])).
% 5.39/1.14 fof(f105,plain,(
% 5.39/1.14 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f65,f66])).
% 5.39/1.14 fof(f165,plain,(
% 5.39/1.14 ![X0,X1]: (~product(X0,X0,X1)|X0=X1)),
% 5.39/1.14 inference(resolution,[status(thm)],[f46,f47])).
% 5.39/1.14 fof(f166,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X1,X4)|~product(X0,X4,X5)|sum(multiply(X0,X3),X2,X5))),
% 5.39/1.14 inference(resolution,[status(thm)],[f36,f22])).
% 5.39/1.14 fof(f170,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X0,X4)|~product(X4,X1,X5)|sum(multiply(X3,X1),X2,X5))),
% 5.39/1.14 inference(resolution,[status(thm)],[f40,f22])).
% 5.39/1.14 fof(f286,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~sum(X0,additive_identity,X1)|sum(add(X0,additive_inverse(X2)),X2,X1))),
% 5.39/1.14 inference(resolution,[status(thm)],[f63,f24])).
% 5.39/1.14 fof(f289,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~sum(X0,additive_identity,X1)|sum(add(X0,X2),additive_inverse(X2),X1))),
% 5.39/1.14 inference(resolution,[status(thm)],[f63,f25])).
% 5.39/1.14 fof(f303,plain,(
% 5.39/1.14 ![X0]: (X0=multiply(X0,X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f165,f22])).
% 5.39/1.14 fof(f469,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~product(X0,X1,X2)|product(X0,multiply(X0,X1),X2))),
% 5.39/1.14 inference(resolution,[status(thm)],[f82,f22])).
% 5.39/1.14 fof(f471,plain,(
% 5.39/1.14 ![X0,X1]: (product(X0,multiply(X0,X1),multiply(X0,X1)))),
% 5.39/1.14 inference(resolution,[status(thm)],[f469,f22])).
% 5.39/1.14 fof(f474,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~product(multiply(X0,X1),X2,X3)|product(X0,multiply(X1,X2),X3))),
% 5.39/1.14 inference(resolution,[status(thm)],[f81,f22])).
% 5.39/1.14 fof(f476,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~product(X0,multiply(X1,X2),X3)|product(multiply(X0,X1),X2,X3))),
% 5.39/1.14 inference(resolution,[status(thm)],[f83,f22])).
% 5.39/1.14 fof(f814,plain,(
% 5.39/1.14 ![X0,X1]: (sum(add(X0,additive_inverse(X1)),X1,X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f286,f21])).
% 5.39/1.14 fof(f825,plain,(
% 5.39/1.14 ![X0,X1]: (sum(add(X0,X1),additive_inverse(X1),X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f289,f21])).
% 5.39/1.14 fof(f850,plain,(
% 5.39/1.14 ![X0,X1]: (add(X0,add(X1,additive_inverse(X0)))=X1)),
% 5.39/1.14 inference(resolution,[status(thm)],[f814,f97])).
% 5.39/1.14 fof(f852,plain,(
% 5.39/1.14 ![X0,X1]: (add(add(X0,additive_inverse(X1)),X1)=X0)),
% 5.39/1.14 inference(resolution,[status(thm)],[f814,f65])).
% 5.39/1.14 fof(f886,plain,(
% 5.39/1.14 ![X0,X1]: (add(add(X0,X1),additive_inverse(X1))=X0)),
% 5.39/1.14 inference(resolution,[status(thm)],[f825,f65])).
% 5.39/1.14 fof(f903,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X3,X2,X4)|sum(multiply(X3,X0),multiply(X3,X1),X4))),
% 5.39/1.14 inference(resolution,[status(thm)],[f166,f22])).
% 5.39/1.14 fof(f904,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~product(X1,X2,X3)|sum(multiply(X1,X0),X1,X3))),
% 5.39/1.14 inference(resolution,[status(thm)],[f166,f47])).
% 5.39/1.14 fof(f911,plain,(
% 5.39/1.14 ![X0]: (add(X0,additive_identity)=additive_inverse(additive_inverse(X0)))),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f101,f850])).
% 5.39/1.14 fof(f946,plain,(
% 5.39/1.14 ![X0]: (X0=additive_inverse(additive_inverse(X0)))),
% 5.39/1.14 inference(forward_demodulation,[status(thm)],[f62,f911])).
% 5.39/1.14 fof(f992,plain,(
% 5.39/1.14 ![X0,X1]: (add(add(additive_inverse(X0),X1),X0)=X1)),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f105,f852])).
% 5.39/1.14 fof(f1258,plain,(
% 5.39/1.14 ![X0,X1]: (add(add(X0,X1),additive_inverse(X0))=X1)),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f105,f886])).
% 5.39/1.14 fof(f1373,plain,(
% 5.39/1.14 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X2,X3,X4)|sum(multiply(X0,X3),multiply(X1,X3),X4))),
% 5.39/1.14 inference(resolution,[status(thm)],[f170,f22])).
% 5.39/1.14 fof(f1374,plain,(
% 5.39/1.14 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~product(X2,X1,X3)|sum(multiply(X0,X1),X1,X3))),
% 5.39/1.14 inference(resolution,[status(thm)],[f170,f47])).
% 5.39/1.14 fof(f2136,plain,(
% 5.39/1.14 ![X0,X1]: (product(X0,multiply(X1,multiply(X0,X1)),multiply(X0,X1)))),
% 5.39/1.14 inference(resolution,[status(thm)],[f474,f47])).
% 5.39/1.14 fof(f2360,plain,(
% 5.39/1.14 ![X0,X1,X2]: (product(multiply(X0,X1),X2,multiply(X0,multiply(X1,X2))))),
% 5.39/1.14 inference(resolution,[status(thm)],[f476,f22])).
% 5.39/1.14 fof(f3044,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~product(X0,X1,X2)|sum(multiply(X0,additive_identity),multiply(X0,X1),X2))),
% 5.39/1.14 inference(resolution,[status(thm)],[f903,f20])).
% 5.39/1.14 fof(f3063,plain,(
% 5.39/1.14 ![X0,X1]: (~product(X0,additive_identity,X1)|sum(multiply(X0,additive_inverse(X0)),X0,X1))),
% 5.39/1.14 inference(resolution,[status(thm)],[f904,f24])).
% 5.39/1.14 fof(f5021,plain,(
% 5.39/1.14 ![X0,X1,X2]: (~product(X0,X1,X2)|sum(multiply(additive_identity,X1),multiply(X0,X1),X2))),
% 5.39/1.14 inference(resolution,[status(thm)],[f1373,f20])).
% 5.39/1.14 fof(f5049,plain,(
% 5.39/1.14 ![X0,X1]: (~product(additive_identity,X0,X1)|sum(multiply(additive_inverse(X0),X0),X0,X1))),
% 5.39/1.14 inference(resolution,[status(thm)],[f1374,f24])).
% 5.39/1.14 fof(f5985,plain,(
% 5.39/1.14 ![X0]: (sum(multiply(X0,additive_identity),multiply(X0,X0),X0))),
% 5.39/1.14 inference(resolution,[status(thm)],[f3044,f47])).
% 5.39/1.14 fof(f5988,plain,(
% 5.39/1.14 ![X0]: (sum(multiply(X0,additive_identity),X0,X0))),
% 5.39/1.14 inference(forward_demodulation,[status(thm)],[f303,f5985])).
% 5.39/1.14 fof(f6021,plain,(
% 5.39/1.14 ![X0]: (add(X0,multiply(X0,additive_identity))=X0)),
% 5.39/1.14 inference(resolution,[status(thm)],[f5988,f97])).
% 5.39/1.14 fof(f6095,plain,(
% 5.39/1.14 ![X0]: (add(X0,additive_inverse(X0))=multiply(X0,additive_identity))),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f6021,f1258])).
% 5.39/1.14 fof(f6139,plain,(
% 5.39/1.14 ![X0]: (additive_identity=multiply(X0,additive_identity))),
% 5.39/1.14 inference(forward_demodulation,[status(thm)],[f103,f6095])).
% 5.39/1.14 fof(f6158,plain,(
% 5.39/1.14 ![X0]: (product(X0,multiply(X0,additive_identity),additive_identity))),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f6139,f471])).
% 5.39/1.14 fof(f6166,plain,(
% 5.39/1.14 ![X0]: (product(X0,additive_identity,additive_identity))),
% 5.39/1.14 inference(forward_demodulation,[status(thm)],[f6139,f6158])).
% 5.39/1.14 fof(f6585,plain,(
% 5.39/1.14 ![X0]: (sum(multiply(X0,additive_inverse(X0)),X0,additive_identity))),
% 5.39/1.14 inference(resolution,[status(thm)],[f3063,f6166])).
% 5.39/1.14 fof(f6635,plain,(
% 5.39/1.14 ![X0]: (add(X0,multiply(X0,additive_inverse(X0)))=additive_identity)),
% 5.39/1.14 inference(resolution,[status(thm)],[f6585,f97])).
% 5.39/1.14 fof(f6681,plain,(
% 5.39/1.14 ![X0]: (add(additive_identity,X0)=multiply(additive_inverse(X0),additive_inverse(additive_inverse(X0))))),
% 5.39/1.14 inference(paramodulation,[status(thm)],[f6635,f992])).
% 5.39/1.14 fof(f6771,plain,(
% 5.39/1.14 ![X0]: (X0=multiply(additive_inverse(X0),additive_inverse(additive_inverse(X0))))),
% 5.39/1.14 inference(forward_demodulation,[status(thm)],[f61,f6681])).
% 5.39/1.14 fof(f6772,plain,(
% 5.39/1.14 ![X0]: (X0=multiply(additive_inverse(X0),X0))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f946,f6771])).
% 5.39/1.15 fof(f6823,plain,(
% 5.39/1.15 ![X0]: (product(additive_inverse(X0),multiply(X0,multiply(additive_inverse(X0),X0)),X0))),
% 5.39/1.15 inference(paramodulation,[status(thm)],[f6772,f2136])).
% 5.39/1.15 fof(f6840,plain,(
% 5.39/1.15 ![X0]: (product(additive_inverse(X0),multiply(X0,X0),X0))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f6772,f6823])).
% 5.39/1.15 fof(f6841,plain,(
% 5.39/1.15 ![X0]: (product(additive_inverse(X0),X0,X0))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f303,f6840])).
% 5.39/1.15 fof(f7731,plain,(
% 5.39/1.15 ![X0]: (sum(multiply(additive_identity,X0),multiply(additive_inverse(X0),X0),X0))),
% 5.39/1.15 inference(resolution,[status(thm)],[f5021,f6841])).
% 5.39/1.15 fof(f7743,plain,(
% 5.39/1.15 ![X0]: (sum(multiply(additive_identity,X0),X0,X0))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f6772,f7731])).
% 5.39/1.15 fof(f7789,plain,(
% 5.39/1.15 ![X0]: (add(X0,multiply(additive_identity,X0))=X0)),
% 5.39/1.15 inference(resolution,[status(thm)],[f7743,f97])).
% 5.39/1.15 fof(f7885,plain,(
% 5.39/1.15 ![X0]: (add(X0,additive_inverse(X0))=multiply(additive_identity,X0))),
% 5.39/1.15 inference(paramodulation,[status(thm)],[f7789,f1258])).
% 5.39/1.15 fof(f7933,plain,(
% 5.39/1.15 ![X0]: (additive_identity=multiply(additive_identity,X0))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f103,f7885])).
% 5.39/1.15 fof(f7953,plain,(
% 5.39/1.15 ![X0,X1]: (product(multiply(additive_identity,X0),X1,additive_identity))),
% 5.39/1.15 inference(paramodulation,[status(thm)],[f7933,f2360])).
% 5.39/1.15 fof(f7990,plain,(
% 5.39/1.15 ![X0]: (product(additive_identity,X0,additive_identity))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f7933,f7953])).
% 5.39/1.15 fof(f8271,plain,(
% 5.39/1.15 ![X0,X1]: (~product(additive_identity,X0,X1)|sum(X0,X0,X1))),
% 5.39/1.15 inference(forward_demodulation,[status(thm)],[f6772,f5049])).
% 5.39/1.15 fof(f8272,plain,(
% 5.39/1.15 ![X0]: (sum(X0,X0,additive_identity))),
% 5.39/1.15 inference(resolution,[status(thm)],[f8271,f7990])).
% 5.39/1.15 fof(f8300,plain,(
% 5.39/1.15 $false),
% 5.39/1.15 inference(backward_subsumption_resolution,[status(thm)],[f48,f8272])).
% 5.39/1.15 % SZS output end CNFRefutation for theBenchmark.p
% 5.39/1.17 % Elapsed time: 0.780251 seconds
% 5.39/1.17 % CPU time: 5.990872 seconds
% 5.39/1.17 % Total memory used: 66.186 MB
% 5.39/1.17 % Net memory used: 61.654 MB
%------------------------------------------------------------------------------