%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG128-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:25 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG128-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n006.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 04:22:12 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.36 % Drodi V4.1.1
% 0.14/0.42 % Refutation found
% 0.14/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.42 fof(f1,axiom,(
% 0.14/0.42 (![A,B,C]: (add(A,add(B,C)) = add(add(A,B),C) ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f2,axiom,(
% 0.14/0.42 (![A,B]: (add(A,B) = add(B,A) ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f3,axiom,(
% 0.14/0.42 (![A,B]: (mult(A,B) = mult(B,A) ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f4,axiom,(
% 0.14/0.42 (![A,B,C]: (mult(A,add(B,C)) = add(mult(A,B),mult(A,C)) ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f5,axiom,(
% 0.14/0.42 (![A]: (add(zero,A) = A ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f6,axiom,(
% 0.14/0.42 (![A]: (mult(A,unit) = A ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f7,axiom,(
% 0.14/0.42 (![A]: (add(unit,add(A,mult(A,A))) = A ))),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f8,negated_conjecture,(
% 0.14/0.42 add(x0,x1) != mult(x0,x1) ),
% 0.14/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.42 fof(f9,plain,(
% 0.14/0.42 ![X0,X1,X2]: (add(X0,add(X1,X2))=add(add(X0,X1),X2))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/0.42 fof(f10,plain,(
% 0.14/0.42 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.14/0.42 fof(f11,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,X1)=mult(X1,X0))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f3])).
% 0.14/0.42 fof(f12,plain,(
% 0.14/0.42 ![X0,X1,X2]: (mult(X0,add(X1,X2))=add(mult(X0,X1),mult(X0,X2)))),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.14/0.42 fof(f13,plain,(
% 0.14/0.42 ![X0]: (add(zero,X0)=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.42 fof(f14,plain,(
% 0.14/0.42 ![X0]: (mult(X0,unit)=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.14/0.42 fof(f15,plain,(
% 0.14/0.42 ![X0]: (add(unit,add(X0,mult(X0,X0)))=X0)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.42 fof(f16,plain,(
% 0.14/0.42 ~add(x0,x1)=mult(x0,x1)),
% 0.14/0.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.42 fof(f17,definition,(
% 0.14/0.42 sF0_fnc=add(x0,x1)),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.14/0.42 fof(f18,definition,(
% 0.14/0.42 sF1_fnc=mult(x0,x1)),
% 0.14/0.42 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.14/0.42 fof(f19,plain,(
% 0.14/0.42 ~sF0_fnc=sF1_fnc),
% 0.14/0.42 inference(definition_folding,[],[f16,f18,f17])).
% 0.14/0.42 fof(f20,plain,(
% 0.14/0.42 ![X0]: (X0=add(X0,zero))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f13,f10])).
% 0.14/0.42 fof(f28,plain,(
% 0.14/0.42 ![X0,X1,X2]: (add(X0,add(X1,X2))=add(X2,add(X0,X1)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f10,f9])).
% 0.14/0.42 fof(f48,plain,(
% 0.14/0.42 ![X0]: (X0=mult(unit,X0))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f14,f11])).
% 0.14/0.42 fof(f62,plain,(
% 0.14/0.42 ![X0,X1,X2]: (mult(X0,add(X1,X2))=add(mult(X0,X2),mult(X0,X1)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f10,f12])).
% 0.14/0.42 fof(f66,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,add(unit,X1))=add(X0,mult(X0,X1)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f14,f12])).
% 0.14/0.42 fof(f71,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,add(X1,unit))=add(mult(X0,X1),X0))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f14,f12])).
% 0.14/0.42 fof(f81,plain,(
% 0.14/0.42 add(unit,add(unit,unit))=unit),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f48,f15])).
% 0.14/0.42 fof(f93,plain,(
% 0.14/0.42 ![X0,X1,X2]: (add(add(X0,X1),X2)=add(X1,add(X2,X0)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f10,f28])).
% 0.14/0.42 fof(f100,plain,(
% 0.14/0.42 ![X0]: (add(X0,sF0_fnc)=add(x1,add(X0,x0)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f17,f28])).
% 0.14/0.42 fof(f107,plain,(
% 0.14/0.42 ![X0]: (add(X0,add(mult(X0,X0),unit))=X0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f15,f28])).
% 0.14/0.42 fof(f162,plain,(
% 0.14/0.42 add(mult(zero,zero),unit)=zero),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f13,f107])).
% 0.14/0.42 fof(f164,plain,(
% 0.14/0.42 ![X0]: (add(X0,add(unit,mult(X0,X0)))=X0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f10,f107])).
% 0.14/0.42 fof(f180,plain,(
% 0.14/0.42 ![X0]: (add(mult(zero,zero),add(unit,X0))=add(X0,zero))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f162,f28])).
% 0.14/0.42 fof(f185,plain,(
% 0.14/0.42 ![X0]: (add(mult(zero,zero),add(unit,X0))=X0)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f20,f180])).
% 0.14/0.42 fof(f191,plain,(
% 0.14/0.42 ![X0]: (add(unit,add(mult(X0,X0),X0))=X0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f28,f164])).
% 0.14/0.42 fof(f374,plain,(
% 0.14/0.42 add(zero,sF0_fnc)=add(x1,x0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f13,f100])).
% 0.14/0.42 fof(f386,plain,(
% 0.14/0.42 sF0_fnc=add(x1,x0)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f13,f374])).
% 0.14/0.42 fof(f568,plain,(
% 0.14/0.42 add(mult(zero,zero),unit)=add(unit,unit)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f81,f185])).
% 0.14/0.42 fof(f594,plain,(
% 0.14/0.42 zero=add(unit,unit)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f162,f568])).
% 0.14/0.42 fof(f615,plain,(
% 0.14/0.42 add(mult(zero,zero),zero)=unit),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f594,f185])).
% 0.14/0.42 fof(f622,plain,(
% 0.14/0.42 mult(zero,zero)=unit),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f20,f615])).
% 0.14/0.42 fof(f791,plain,(
% 0.14/0.42 ![X0]: (mult(X0,unit)=add(X0,mult(X0,add(unit,mult(unit,unit)))))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f164,f66])).
% 0.14/0.42 fof(f823,plain,(
% 0.14/0.42 ![X0]: (X0=add(X0,mult(X0,add(unit,mult(unit,unit)))))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f14,f791])).
% 0.14/0.42 fof(f824,plain,(
% 0.14/0.42 ![X0]: (X0=add(X0,mult(X0,add(unit,unit))))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f48,f823])).
% 0.14/0.42 fof(f825,plain,(
% 0.14/0.42 ![X0]: (X0=add(X0,mult(X0,zero)))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f594,f824])).
% 0.14/0.42 fof(f841,plain,(
% 0.14/0.42 zero=add(zero,unit)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f622,f825])).
% 0.14/0.42 fof(f862,plain,(
% 0.14/0.42 zero=unit),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f13,f841])).
% 0.14/0.42 fof(f876,plain,(
% 0.14/0.42 ![X0]: (add(zero,add(mult(X0,X0),X0))=X0)),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f862,f191])).
% 0.14/0.42 fof(f881,plain,(
% 0.14/0.42 ![X0]: (mult(X0,zero)=X0)),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f862,f14])).
% 0.14/0.42 fof(f888,plain,(
% 0.14/0.42 ![X0]: (add(mult(X0,X0),X0)=X0)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f13,f876])).
% 0.14/0.42 fof(f909,plain,(
% 0.14/0.42 ![X0]: (X0=add(X0,X0))),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f881,f825])).
% 0.14/0.42 fof(f947,plain,(
% 0.14/0.42 ![X0,X1]: (add(X0,X1)=add(X1,add(add(X0,X1),X0)))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f93,f909])).
% 0.14/0.42 fof(f963,plain,(
% 0.14/0.42 add(x0,sF0_fnc)=add(x1,x0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f909,f100])).
% 0.14/0.42 fof(f972,plain,(
% 0.14/0.42 ![X0,X1]: (add(X0,X1)=add(X1,add(X1,add(X0,X0))))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f93,f947])).
% 0.14/0.42 fof(f973,plain,(
% 0.14/0.42 ![X0,X1]: (add(X0,X1)=add(X1,add(X1,X0)))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f909,f972])).
% 0.14/0.42 fof(f982,plain,(
% 0.14/0.42 add(x0,sF0_fnc)=sF0_fnc),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f386,f963])).
% 0.14/0.42 fof(f1118,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,add(X1,zero))=add(mult(X0,X1),X0))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f862,f71])).
% 0.14/0.42 fof(f1119,plain,(
% 0.14/0.42 ![X0]: (mult(X0,X0)=X0)),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f1120,f888])).
% 0.14/0.42 fof(f1120,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,X1)=add(mult(X0,X1),X0))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f20,f1118])).
% 0.14/0.42 fof(f1163,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,add(X0,X1))=add(mult(X0,X1),X0))),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f1119,f62])).
% 0.14/0.42 fof(f1168,plain,(
% 0.14/0.42 ![X0,X1]: (mult(X0,add(X0,X1))=mult(X0,X1))),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f1120,f1163])).
% 0.14/0.42 fof(f1278,plain,(
% 0.14/0.42 add(sF0_fnc,x0)=add(x0,sF0_fnc)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f982,f973])).
% 0.14/0.42 fof(f1350,plain,(
% 0.14/0.42 add(sF0_fnc,x0)=sF0_fnc),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f982,f1278])).
% 0.14/0.42 fof(f1724,plain,(
% 0.14/0.42 mult(sF0_fnc,sF0_fnc)=mult(sF0_fnc,x0)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f1350,f1168])).
% 0.14/0.42 fof(f1744,plain,(
% 0.14/0.42 mult(x0,sF0_fnc)=mult(x0,x1)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f17,f1168])).
% 0.14/0.42 fof(f1773,plain,(
% 0.14/0.42 sF0_fnc=mult(sF0_fnc,x0)),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f1119,f1724])).
% 0.14/0.42 fof(f1779,plain,(
% 0.14/0.42 mult(x0,sF0_fnc)=sF1_fnc),
% 0.14/0.42 inference(forward_demodulation,[status(thm)],[f18,f1744])).
% 0.14/0.42 fof(f1799,plain,(
% 0.14/0.42 sF0_fnc=mult(x0,sF0_fnc)),
% 0.14/0.42 inference(paramodulation,[status(thm)],[f11,f1773])).
% 0.14/0.42 fof(f1890,plain,(
% 0.14/0.42 sF0_fnc=sF1_fnc),
% 0.14/0.42 inference(backward_demodulation,[status(thm)],[f1799,f1779])).
% 0.14/0.42 fof(f1904,plain,(
% 0.14/0.42 $false),
% 0.14/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1890,f19])).
% 0.14/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.082644 seconds
% 0.14/0.44 % CPU time: 0.406224 seconds
% 0.14/0.44 % Total memory used: 8.788 MB
% 0.14/0.44 % Net memory used: 8.661 MB
%------------------------------------------------------------------------------