%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG001-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:04 PM UTC 2026
% Result : Unsatisfiable 46.34s 6.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : RNG001-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n016.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 04:14:08 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 46.34/6.42 % Refutation found
% 46.34/6.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 46.34/6.42 % SZS output start CNFRefutation for theBenchmark
% 46.34/6.42 fof(f1,axiom,(
% 46.34/6.42 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f2,axiom,(
% 46.34/6.42 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f3,axiom,(
% 46.34/6.42 (![X]: (sum(additive_identity,X,X) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f4,axiom,(
% 46.34/6.42 (![X]: (sum(X,additive_identity,X) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f5,axiom,(
% 46.34/6.42 (![X,Y]: (product(X,Y,multiply(X,Y)) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f6,axiom,(
% 46.34/6.42 (![X,Y]: (sum(X,Y,add(X,Y)) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f7,axiom,(
% 46.34/6.42 (![X]: (sum(additive_inverse(X),X,additive_identity) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f8,axiom,(
% 46.34/6.42 (![X]: (sum(X,additive_inverse(X),additive_identity) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f9,axiom,(
% 46.34/6.42 (![U,Z,W,Y,V,X]: (ifeq(sum(U,Z,W),true,ifeq(sum(Y,Z,V),true,ifeq(sum(X,Y,U),true,sum(X,V,W),true),true),true) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f11,axiom,(
% 46.34/6.42 (![X,Y,Z]: (ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f15,axiom,(
% 46.34/6.42 (![X,Z,V2,Y,V1,V4,V3]: (ifeq(product(X,Z,V2),true,ifeq(product(X,Y,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(X,V3,V4),true),true),true),true) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f17,axiom,(
% 46.34/6.42 (![Z,X,V2,Y,V1,V4,V3]: (ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(V3,X,V4),true),true),true),true) = true ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f18,axiom,(
% 46.34/6.42 (![X,Y,V,U]: (ifeq2(sum(X,Y,V),true,ifeq2(sum(X,Y,U),true,U,V),V) = V ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f19,axiom,(
% 46.34/6.42 (![X,Y,V,U]: (ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f20,axiom,(
% 46.34/6.42 (![X,W,Z,Y]: (ifeq2(sum(X,W,Z),true,ifeq2(sum(X,Y,Z),true,Y,W),W) = W ))),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f22,negated_conjecture,(
% 46.34/6.42 product(a,additive_identity,additive_identity) != true ),
% 46.34/6.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 46.34/6.42 fof(f23,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f1])).
% 46.34/6.42 fof(f24,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f2])).
% 46.34/6.42 fof(f25,plain,(
% 46.34/6.42 ![X0]: (sum(additive_identity,X0,X0)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f3])).
% 46.34/6.42 fof(f26,plain,(
% 46.34/6.42 ![X0]: (sum(X0,additive_identity,X0)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f4])).
% 46.34/6.42 fof(f27,plain,(
% 46.34/6.42 ![X0,X1]: (product(X0,X1,multiply(X0,X1))=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f5])).
% 46.34/6.42 fof(f28,plain,(
% 46.34/6.42 ![X0,X1]: (sum(X0,X1,add(X0,X1))=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f6])).
% 46.34/6.42 fof(f29,plain,(
% 46.34/6.42 ![X0]: (sum(additive_inverse(X0),X0,additive_identity)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f7])).
% 46.34/6.42 fof(f30,plain,(
% 46.34/6.42 ![X0]: (sum(X0,additive_inverse(X0),additive_identity)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f8])).
% 46.34/6.42 fof(f31,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4,X5]: (ifeq(sum(X0,X1,X2),true,ifeq(sum(X3,X1,X4),true,ifeq(sum(X5,X3,X0),true,sum(X5,X4,X2),true),true),true)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f9])).
% 46.34/6.42 fof(f33,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(sum(X0,X1,X2),true,sum(X1,X0,X2),true)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f11])).
% 46.34/6.42 fof(f37,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4,X5,X6]: (ifeq(product(X0,X1,X2),true,ifeq(product(X0,X3,X4),true,ifeq(sum(X4,X2,X5),true,ifeq(sum(X3,X1,X6),true,product(X0,X6,X5),true),true),true),true)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f15])).
% 46.34/6.42 fof(f39,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4,X5,X6]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X4,X2,X5),true,ifeq(sum(X3,X0,X6),true,product(X6,X1,X5),true),true),true),true)=true)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f17])).
% 46.34/6.42 fof(f40,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq2(sum(X0,X1,X2),true,ifeq2(sum(X0,X1,X3),true,X3,X2),X2)=X2)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f18])).
% 46.34/6.42 fof(f41,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2)=X2)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f19])).
% 46.34/6.42 fof(f42,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq2(sum(X0,X1,X2),true,ifeq2(sum(X0,X3,X2),true,X3,X1),X1)=X1)),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f20])).
% 46.34/6.42 fof(f44,plain,(
% 46.34/6.42 ~product(a,additive_identity,additive_identity)=true),
% 46.34/6.42 inference(cnf_transformation,[status(thm)],[f22])).
% 46.34/6.42 fof(f125,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(additive_inverse(X0),X1,X3),true,ifeq(sum(X3,X2,X4),true,ifeq(true,true,product(additive_identity,X1,X4),true),true),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f29,f39])).
% 46.34/6.42 fof(f132,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(X0,additive_inverse(X1),X3),true,ifeq(sum(X3,X2,X4),true,ifeq(true,true,product(X0,additive_identity,X4),true),true),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f29,f37])).
% 46.34/6.42 fof(f136,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(additive_inverse(X0),X1,X3),true,ifeq(sum(X3,X2,X4),true,product(additive_identity,X1,X4),true),true),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f125])).
% 46.34/6.42 fof(f140,plain,(
% 46.34/6.42 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(X0,additive_inverse(X1),X3),true,ifeq(sum(X3,X2,X4),true,product(X0,additive_identity,X4),true),true),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f132])).
% 46.34/6.42 fof(f249,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(true,true,ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1)),multiply(X0,X1))=multiply(X0,X1))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f41])).
% 46.34/6.42 fof(f251,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,X2,multiply(X0,X1))=multiply(X0,X1))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f249])).
% 46.34/6.42 fof(f466,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(true,true,ifeq(sum(X0,X1,X2),true,ifeq(sum(X3,X0,additive_identity),true,sum(X3,X2,X1),true),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f25,f31])).
% 46.34/6.42 fof(f486,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(sum(X0,X1,X2),true,ifeq(sum(X3,X0,additive_identity),true,sum(X3,X2,X1),true),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f466])).
% 46.34/6.42 fof(f1213,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq(true,true,sum(X0,X1,add(X1,X0)),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f33])).
% 46.34/6.42 fof(f1227,plain,(
% 46.34/6.42 ![X0,X1]: (sum(X0,X1,add(X1,X0))=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f1213])).
% 46.34/6.42 fof(f1240,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,ifeq2(sum(X0,additive_identity,X1),true,X1,X0),X0)=X0)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f26,f40])).
% 46.34/6.42 fof(f1241,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(true,true,ifeq2(sum(X0,X1,X2),true,X2,add(X0,X1)),add(X0,X1))=add(X0,X1))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f40])).
% 46.34/6.42 fof(f1244,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(X0,additive_inverse(X0),X1),true,ifeq2(true,true,additive_identity,X1),X1)=X1)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f30,f40])).
% 46.34/6.42 fof(f1250,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(X0,additive_identity,X1),true,X1,X0)=X0)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1240])).
% 46.34/6.42 fof(f1251,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(sum(X0,X1,X2),true,X2,add(X0,X1))=add(X0,X1))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1241])).
% 46.34/6.42 fof(f1254,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(X0,additive_inverse(X0),X1),true,additive_identity,X1)=X1)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1244])).
% 46.34/6.42 fof(f1258,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,ifeq2(sum(additive_inverse(X0),X1,additive_identity),true,X1,X0),X0)=X0)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f29,f42])).
% 46.34/6.42 fof(f1266,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(X0,X1,X0),true,ifeq2(true,true,additive_identity,X1),X1)=X1)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f26,f42])).
% 46.34/6.42 fof(f1269,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(additive_inverse(X0),X1,additive_identity),true,X1,X0)=X0)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1258])).
% 46.34/6.42 fof(f1277,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(sum(X0,X1,X0),true,additive_identity,X1)=X1)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1266])).
% 46.34/6.42 fof(f1344,plain,(
% 46.34/6.42 ifeq2(true,true,additive_identity,additive_inverse(additive_identity))=additive_inverse(additive_identity)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f30,f1277])).
% 46.34/6.42 fof(f1348,plain,(
% 46.34/6.42 additive_identity=additive_inverse(additive_identity)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1344])).
% 46.34/6.42 fof(f1433,plain,(
% 46.34/6.42 ![X0]: (ifeq2(true,true,add(X0,additive_identity),X0)=X0)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f1250])).
% 46.34/6.42 fof(f1439,plain,(
% 46.34/6.42 ![X0]: (add(X0,additive_identity)=X0)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1433])).
% 46.34/6.42 fof(f1593,plain,(
% 46.34/6.42 ![X0]: (ifeq2(true,true,additive_identity,add(X0,additive_inverse(X0)))=add(X0,additive_inverse(X0)))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f1254])).
% 46.34/6.42 fof(f1597,plain,(
% 46.34/6.42 ![X0]: (additive_identity=add(X0,additive_inverse(X0)))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1593])).
% 46.34/6.42 fof(f1608,plain,(
% 46.34/6.42 ![X0]: (ifeq2(true,true,additive_inverse(additive_inverse(X0)),X0)=X0)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f30,f1269])).
% 46.34/6.42 fof(f1612,plain,(
% 46.34/6.42 ![X0]: (additive_inverse(additive_inverse(X0))=X0)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f1608])).
% 46.34/6.42 fof(f1616,plain,(
% 46.34/6.42 ![X0]: (additive_identity=add(additive_inverse(X0),X0))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1612,f1597])).
% 46.34/6.42 fof(f1969,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(additive_inverse(X0),X1,X3),true,ifeq(true,true,product(additive_identity,X1,add(X3,X2)),true),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f136])).
% 46.34/6.42 fof(f1978,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(additive_inverse(X0),X1,X3),true,product(additive_identity,X1,add(X3,X2)),true),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f1969])).
% 46.34/6.42 fof(f2120,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,product(additive_identity,X1,add(multiply(additive_inverse(X0),X1),X2)),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f1978])).
% 46.34/6.42 fof(f2129,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,product(additive_identity,X1,add(multiply(additive_inverse(X0),X1),X2)),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2120])).
% 46.34/6.42 fof(f2131,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq(true,true,product(additive_identity,X0,add(multiply(additive_inverse(X1),X0),multiply(X1,X0))),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f2129])).
% 46.34/6.42 fof(f2153,plain,(
% 46.34/6.42 ![X0,X1]: (product(additive_identity,X0,add(multiply(additive_inverse(X1),X0),multiply(X1,X0)))=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2131])).
% 46.34/6.42 fof(f2589,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(X0,additive_inverse(X1),X3),true,ifeq(true,true,product(X0,additive_identity,add(X3,X2)),true),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f28,f140])).
% 46.34/6.42 fof(f2600,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(X0,additive_inverse(X1),X3),true,product(X0,additive_identity,add(X3,X2)),true),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2589])).
% 46.34/6.42 fof(f2642,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,product(X0,additive_identity,add(multiply(X0,additive_inverse(X1)),X2)),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f2600])).
% 46.34/6.42 fof(f2643,plain,(
% 46.34/6.42 ![X0,X1,X2,X3]: (ifeq(product(X0,additive_inverse(X1),X2),true,ifeq(product(X0,X1,X3),true,product(X0,additive_identity,add(X3,X2)),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1612,f2600])).
% 46.34/6.42 fof(f2653,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,product(X0,additive_identity,add(multiply(X0,additive_inverse(X1)),X2)),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2642])).
% 46.34/6.42 fof(f2655,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq(true,true,product(X0,additive_identity,add(multiply(X0,additive_inverse(X1)),multiply(X0,X1))),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f2653])).
% 46.34/6.42 fof(f2681,plain,(
% 46.34/6.42 ![X0,X1]: (product(X0,additive_identity,add(multiply(X0,additive_inverse(X1)),multiply(X0,X1)))=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2655])).
% 46.34/6.42 fof(f2767,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(true,true,ifeq(product(X0,X1,X2),true,product(X0,additive_identity,add(X2,multiply(X0,additive_inverse(X1)))),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f27,f2643])).
% 46.34/6.42 fof(f2784,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,product(X0,additive_identity,add(X2,multiply(X0,additive_inverse(X1)))),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f2767])).
% 46.34/6.42 fof(f3679,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,add(multiply(additive_inverse(X0),X1),multiply(X0,X1)),multiply(additive_identity,X1))=multiply(additive_identity,X1))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f2153,f251])).
% 46.34/6.42 fof(f3991,plain,(
% 46.34/6.42 ![X0,X1]: (add(multiply(additive_inverse(X0),X1),multiply(X0,X1))=multiply(additive_identity,X1))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f3679])).
% 46.34/6.42 fof(f4256,plain,(
% 46.34/6.42 ![X0]: (add(multiply(additive_identity,X0),multiply(additive_identity,X0))=multiply(additive_identity,X0))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1348,f3991])).
% 46.34/6.42 fof(f4263,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq(product(X0,X1,multiply(additive_inverse(X0),additive_inverse(X1))),true,product(X0,additive_identity,multiply(additive_identity,additive_inverse(X1))),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f3991,f2784])).
% 46.34/6.42 fof(f4910,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,add(X0,X1),add(X1,X0))=add(X1,X0))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1227,f1251])).
% 46.34/6.42 fof(f5004,plain,(
% 46.34/6.42 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f4910])).
% 46.34/6.42 fof(f5106,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq2(sum(X0,X1,X2),true,X2,add(X1,X0))=add(X0,X1))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f5004,f1251])).
% 46.34/6.42 fof(f6688,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,add(multiply(X0,additive_inverse(X1)),multiply(X0,X1)),multiply(X0,additive_identity))=multiply(X0,additive_identity))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f2681,f251])).
% 46.34/6.42 fof(f7169,plain,(
% 46.34/6.42 ![X0,X1]: (add(multiply(X0,additive_inverse(X1)),multiply(X0,X1))=multiply(X0,additive_identity))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f6688])).
% 46.34/6.42 fof(f7440,plain,(
% 46.34/6.42 ![X0]: (add(multiply(X0,additive_identity),multiply(X0,additive_identity))=multiply(X0,additive_identity))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1348,f7169])).
% 46.34/6.42 fof(f8257,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(sum(X0,X1,X2),true,ifeq(true,true,sum(additive_inverse(X0),X2,X1),true),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f29,f486])).
% 46.34/6.42 fof(f8276,plain,(
% 46.34/6.42 ![X0,X1,X2]: (ifeq(sum(X0,X1,X2),true,sum(additive_inverse(X0),X2,X1),true)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f8257])).
% 46.34/6.42 fof(f8286,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq(true,true,sum(additive_inverse(X0),add(X1,X0),X1),true)=true)),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f1227,f8276])).
% 46.34/6.42 fof(f8308,plain,(
% 46.34/6.42 ![X0,X1]: (sum(additive_inverse(X0),add(X1,X0),X1)=true)),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f24,f8286])).
% 46.34/6.42 fof(f8412,plain,(
% 46.34/6.42 ![X0,X1]: (ifeq2(true,true,X0,add(add(X0,X1),additive_inverse(X1)))=add(additive_inverse(X1),add(X0,X1)))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f8308,f5106])).
% 46.34/6.42 fof(f8535,plain,(
% 46.34/6.42 ![X0,X1]: (X0=add(additive_inverse(X1),add(X0,X1)))),
% 46.34/6.42 inference(forward_demodulation,[status(thm)],[f23,f8412])).
% 46.34/6.42 fof(f8833,plain,(
% 46.34/6.42 ![X0]: (multiply(additive_identity,X0)=add(additive_inverse(multiply(additive_identity,X0)),multiply(additive_identity,X0)))),
% 46.34/6.42 inference(paramodulation,[status(thm)],[f4256,f8535])).
% 46.34/6.42 fof(f8834,plain,(
% 46.34/6.42 ![X0,X1]: (multiply(additive_inverse(X0),X1)=add(additive_inverse(multiply(X0,X1)),multiply(additive_identity,X1)))),
% 27.13/6.58 inference(paramodulation,[status(thm)],[f3991,f8535])).
% 27.13/6.58 fof(f8835,plain,(
% 27.13/6.58 ![X0]: (multiply(X0,additive_identity)=add(additive_inverse(multiply(X0,additive_identity)),multiply(X0,additive_identity)))),
% 27.13/6.58 inference(paramodulation,[status(thm)],[f7440,f8535])).
% 27.13/6.58 fof(f8836,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(X0,additive_inverse(X1))=add(additive_inverse(multiply(X0,X1)),multiply(X0,additive_identity)))),
% 27.13/6.58 inference(paramodulation,[status(thm)],[f7169,f8535])).
% 27.13/6.58 fof(f8931,plain,(
% 27.13/6.58 ![X0,X1]: (ifeq(product(X0,X1,multiply(additive_inverse(X0),additive_inverse(X1))),true,product(X0,additive_identity,additive_identity),true)=true)),
% 27.13/6.58 inference(backward_demodulation,[status(thm)],[f9125,f4263])).
% 27.13/6.58 fof(f9125,plain,(
% 27.13/6.58 ![X0]: (multiply(additive_identity,X0)=additive_identity)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f1616,f8833])).
% 27.13/6.58 fof(f9126,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(additive_inverse(X0),X1)=add(additive_inverse(multiply(X0,X1)),additive_identity))),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f9125,f8834])).
% 27.13/6.58 fof(f9193,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(additive_inverse(X0),X1)=additive_inverse(multiply(X0,X1)))),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f1439,f9126])).
% 27.13/6.58 fof(f9385,plain,(
% 27.13/6.58 ![X0]: (multiply(X0,additive_identity)=additive_identity)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f1616,f8835])).
% 27.13/6.58 fof(f9386,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(X0,additive_inverse(X1))=add(multiply(additive_inverse(X0),X1),multiply(X0,additive_identity)))),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f9193,f8836])).
% 27.13/6.58 fof(f9387,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(X0,additive_inverse(X1))=add(multiply(additive_inverse(X0),X1),additive_identity))),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f9385,f9386])).
% 27.13/6.58 fof(f9404,plain,(
% 27.13/6.58 ![X0,X1]: (multiply(X0,additive_inverse(X1))=multiply(additive_inverse(X0),X1))),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f1439,f9387])).
% 27.13/6.58 fof(f9417,plain,(
% 27.13/6.58 ![X0,X1]: (ifeq(product(X0,X1,multiply(X0,additive_inverse(additive_inverse(X1)))),true,product(X0,additive_identity,additive_identity),true)=true)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f9404,f8931])).
% 27.13/6.58 fof(f9418,plain,(
% 27.13/6.58 ![X0,X1]: (ifeq(product(X0,X1,multiply(X0,X1)),true,product(X0,additive_identity,additive_identity),true)=true)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f1612,f9417])).
% 27.13/6.58 fof(f9419,plain,(
% 27.13/6.58 ![X0]: (ifeq(true,true,product(X0,additive_identity,additive_identity),true)=true)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f27,f9418])).
% 27.13/6.58 fof(f9420,plain,(
% 27.13/6.58 ~true=true),
% 27.13/6.58 inference(backward_demodulation,[status(thm)],[f9427,f44])).
% 27.13/6.58 fof(f9427,plain,(
% 27.13/6.58 ![X0]: (product(X0,additive_identity,additive_identity)=true)),
% 27.13/6.58 inference(forward_demodulation,[status(thm)],[f24,f9419])).
% 27.13/6.58 fof(f10042,plain,(
% 27.13/6.58 $false),
% 27.13/6.58 inference(trivial_equality_resolution,[status(thm)],[f9420])).
% 27.13/6.58 % SZS output end CNFRefutation for theBenchmark.p
% 27.13/6.62 % Elapsed time: 6.139447 seconds
% 27.13/6.62 % CPU time: 47.983182 seconds
% 27.13/6.62 % Total memory used: 446.323 MB
% 27.13/6.62 % Net memory used: 439.312 MB
%------------------------------------------------------------------------------