%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP772-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:37:18 PM UTC 2026
% Result : Unsatisfiable 5.39s 6.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP772-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/5.49 % Computer : n012.cluster.edu
% 0.04/5.49 % Model : x86_64 x86_64
% 0.04/5.49 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.49 % Memory : 8046.5625MB
% 0.04/5.49 % OS : Linux 6.8.0-71-generic
% 0.04/5.49 % CPULimit : 300
% 0.04/5.49 % WCLimit : 300
% 0.04/5.49 % DateTime : Sun Sep 20 20:39:17 UTC 2026
% 0.04/5.49 % CPUTime :
% 0.04/5.49 % Drodi V4.1.1
% 5.39/6.23 % Refutation found
% 5.39/6.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.39/6.23 % SZS output start CNFRefutation for theBenchmark
% 5.39/6.23 fof(f1,axiom,(
% 5.39/6.23 (![A]: (product(A,one) = A ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f2,axiom,(
% 5.39/6.23 (![A]: (product(one,A) = A ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f3,axiom,(
% 5.39/6.23 (![A,B]: (product(A,difference(A,B)) = B ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f4,axiom,(
% 5.39/6.23 (![A,B]: (difference(A,product(A,B)) = B ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f5,axiom,(
% 5.39/6.23 (![A,B]: (quotient(product(A,B),B) = A ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f6,axiom,(
% 5.39/6.23 (![A,B]: (product(quotient(A,B),B) = A ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f9,axiom,(
% 5.39/6.23 (![A]: (i(A) = difference(A,one) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f10,axiom,(
% 5.39/6.23 (![A]: (j(A) = quotient(one,A) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f19,axiom,(
% 5.39/6.23 (![A,B]: (t(A,B) = quotient(product(A,B),A) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f27,axiom,(
% 5.39/6.23 (![A,B,C,D,E]: (product(a(A,B,C),product(D,E)) = product(product(a(A,B,C),D),E) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f29,axiom,(
% 5.39/6.23 (![A,B,C]: (product(a(A,B,C),difference(C,product(a(C,A,B),C))) = one ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f30,axiom,(
% 5.39/6.23 (![A,B,C]: (a(A,i(B),C) = a(A,j(B),C) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f32,axiom,(
% 5.39/6.23 (![A,B,C]: (a(j(A),B,C) = a(B,C,A) ))),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f33,negated_conjecture,(
% 5.39/6.23 a(x0,x1,x1) != a(x1,x1,x0) ),
% 5.39/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.39/6.23 fof(f34,plain,(
% 5.39/6.23 ![X0]: (product(X0,one)=X0)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f1])).
% 5.39/6.23 fof(f35,plain,(
% 5.39/6.23 ![X0]: (product(one,X0)=X0)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f2])).
% 5.39/6.23 fof(f36,plain,(
% 5.39/6.23 ![X0,X1]: (product(X0,difference(X0,X1))=X1)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f3])).
% 5.39/6.23 fof(f37,plain,(
% 5.39/6.23 ![X0,X1]: (difference(X0,product(X0,X1))=X1)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f4])).
% 5.39/6.23 fof(f38,plain,(
% 5.39/6.23 ![X0,X1]: (quotient(product(X0,X1),X1)=X0)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f5])).
% 5.39/6.23 fof(f39,plain,(
% 5.39/6.23 ![X0,X1]: (product(quotient(X0,X1),X1)=X0)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f6])).
% 5.39/6.23 fof(f42,plain,(
% 5.39/6.23 ![X0]: (i(X0)=difference(X0,one))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f9])).
% 5.39/6.23 fof(f43,plain,(
% 5.39/6.23 ![X0]: (j(X0)=quotient(one,X0))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f10])).
% 5.39/6.23 fof(f52,plain,(
% 5.39/6.23 ![X0,X1]: (t(X0,X1)=quotient(product(X0,X1),X0))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f19])).
% 5.39/6.23 fof(f60,plain,(
% 5.39/6.23 ![X0,X1,X2,X3,X4]: (product(a(X0,X1,X2),product(X3,X4))=product(product(a(X0,X1,X2),X3),X4))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f27])).
% 5.39/6.23 fof(f62,plain,(
% 5.39/6.23 ![X0,X1,X2]: (product(a(X0,X1,X2),difference(X2,product(a(X2,X0,X1),X2)))=one)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f29])).
% 5.39/6.23 fof(f63,plain,(
% 5.39/6.23 ![X0,X1,X2]: (a(X0,i(X1),X2)=a(X0,j(X1),X2))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f30])).
% 5.39/6.23 fof(f65,plain,(
% 5.39/6.23 ![X0,X1,X2]: (a(j(X0),X1,X2)=a(X1,X2,X0))),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f32])).
% 5.39/6.23 fof(f66,plain,(
% 5.39/6.23 ~a(x0,x1,x1)=a(x1,x1,x0)),
% 5.39/6.23 inference(cnf_transformation,[status(thm)],[f33])).
% 5.39/6.23 fof(f75,plain,(
% 5.39/6.23 ![X0]: (quotient(X0,one)=X0)),
% 5.39/6.23 inference(paramodulation,[status(thm)],[f34,f38])).
% 5.39/6.23 fof(f80,plain,(
% 5.39/6.23 ![X0,X1]: (quotient(X0,difference(X1,X0))=X1)),
% 5.39/6.23 inference(paramodulation,[status(thm)],[f36,f38])).
% 5.39/6.23 fof(f89,plain,(
% 5.39/6.23 ![X0,X1]: (t(X0,difference(X0,X1))=quotient(X1,X0))),
% 5.39/6.23 inference(paramodulation,[status(thm)],[f36,f52])).
% 5.39/6.23 fof(f107,plain,(
% 5.39/6.23 ![X0,X1,X2]: (a(j(X0),i(X1),X2)=a(j(X1),X2,X0))),
% 5.39/6.23 inference(paramodulation,[status(thm)],[f65,f63])).
% 5.39/6.23 fof(f109,plain,(
% 5.39/6.23 ![X0,X1,X2]: (a(i(X0),X1,X2)=a(j(X0),X1,X2))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f65,f107])).
% 5.39/6.25 fof(f110,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(i(X0),X1,X2)=a(X1,X2,X0))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f65,f109])).
% 5.39/6.25 fof(f314,plain,(
% 5.39/6.25 ![X0]: (product(X0,i(X0))=one)),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f42,f36])).
% 5.39/6.25 fof(f346,plain,(
% 5.39/6.25 ![X0]: (product(j(X0),X0)=one)),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f43,f39])).
% 5.39/6.25 fof(f358,plain,(
% 5.39/6.25 ![X0]: (difference(j(X0),one)=X0)),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f346,f37])).
% 5.39/6.25 fof(f371,plain,(
% 5.39/6.25 ![X0]: (i(j(X0))=X0)),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f42,f358])).
% 5.39/6.25 fof(f374,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(X0,X1,X2)=a(X1,X2,j(X0)))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f371,f110])).
% 5.39/6.25 fof(f381,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(X0,X1,j(X2))=a(X1,i(X2),j(X0)))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f63,f374])).
% 5.39/6.25 fof(f390,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(X0,X1,X2)=a(X2,i(X0),j(X1)))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f374,f381])).
% 5.39/6.25 fof(f391,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(X0,X1,X2)=a(X1,X2,i(X0)))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f374,f390])).
% 5.39/6.25 fof(f398,plain,(
% 5.39/6.25 ![X0,X1,X2]: (a(X0,j(X1),X2)=a(X2,i(X0),X1))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f65,f391])).
% 5.39/6.25 fof(f2894,plain,(
% 5.39/6.25 ![X0,X1,X2,X3]: (product(a(X0,X1,X2),product(i(a(X0,X1,X2)),X3))=product(one,X3))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f314,f60])).
% 5.39/6.25 fof(f2976,plain,(
% 5.39/6.25 ![X0,X1,X2,X3]: (product(a(X0,X1,X2),product(i(a(X0,X1,X2)),X3))=X3)),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f35,f2894])).
% 5.39/6.25 fof(f4521,plain,(
% 5.39/6.25 ![X0,X1,X2,X3]: (product(a(X0,X1,X2),X3)=difference(i(a(X0,X1,X2)),X3))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f36,f2976])).
% 5.39/6.25 fof(f6561,plain,(
% 5.39/6.25 ![X0,X1,X2,X3]: (quotient(X0,product(a(X1,X2,X3),X0))=i(a(X1,X2,X3)))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f4521,f80])).
% 5.39/6.25 fof(f8266,plain,(
% 5.39/6.25 ![X0,X1,X2]: (quotient(difference(X0,product(a(X0,X1,X2),X0)),one)=i(a(X1,X2,X0)))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f62,f6561])).
% 5.39/6.25 fof(f8321,plain,(
% 5.39/6.25 ![X0,X1,X2]: (difference(X0,product(a(X0,X1,X2),X0))=i(a(X1,X2,X0)))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f75,f8266])).
% 5.39/6.25 fof(f10478,plain,(
% 5.39/6.25 ![X0,X1,X2]: (t(X0,i(a(X1,X2,X0)))=quotient(product(a(X0,X1,X2),X0),X0))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f8321,f89])).
% 5.39/6.25 fof(f10598,plain,(
% 5.39/6.25 ![X0,X1,X2]: (t(X0,i(a(X1,X2,X0)))=a(X0,X1,X2))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f38,f10478])).
% 5.39/6.25 fof(f10611,plain,(
% 5.39/6.25 ![X0,X1,X2]: (t(X0,i(a(X1,X0,X2)))=a(X0,i(X2),X1))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f110,f10598])).
% 5.39/6.25 fof(f10723,plain,(
% 5.39/6.25 ![X0,X1]: (a(X0,X1,X0)=a(X0,i(X0),X1))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f10598,f10611])).
% 5.39/6.25 fof(f10888,plain,(
% 5.39/6.25 ![X0,X1]: (a(X0,X1,X0)=a(X0,j(X1),X0))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f398,f10723])).
% 5.39/6.25 fof(f10963,plain,(
% 5.39/6.25 ![X0,X1]: (a(X0,X1,X0)=a(X0,i(X1),X0))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f63,f10888])).
% 5.39/6.25 fof(f11219,plain,(
% 5.39/6.25 ![X0,X1]: (t(X0,i(a(X0,X1,X0)))=a(X0,X0,i(X1)))),
% 5.39/6.25 inference(paramodulation,[status(thm)],[f10963,f10598])).
% 5.39/6.25 fof(f11295,plain,(
% 5.39/6.25 ![X0,X1]: (a(X0,X0,X1)=a(X0,X0,i(X1)))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f10598,f11219])).
% 5.39/6.25 fof(f11296,plain,(
% 5.39/6.25 ![X0,X1]: (a(X0,X0,X1)=a(X1,X0,X0))),
% 5.39/6.25 inference(forward_demodulation,[status(thm)],[f391,f11295])).
% 5.39/6.25 fof(f11333,plain,(
% 5.39/6.25 ~a(x0,x1,x1)=a(x0,x1,x1)),
% 5.39/6.25 inference(backward_demodulation,[status(thm)],[f11296,f66])).
% 5.39/6.25 fof(f11494,plain,(
% 5.39/6.25 $false),
% 5.39/6.25 inference(trivial_equality_resolution,[status(thm)],[f11333])).
% 5.39/6.25 % SZS output end CNFRefutation for theBenchmark.p
% 5.39/6.28 % Elapsed time: 0.777791 seconds
% 5.39/6.28 % CPU time: 6.093078 seconds
% 5.39/6.28 % Total memory used: 223.933 MB
% 5.39/6.28 % Net memory used: 219.993 MB
%------------------------------------------------------------------------------