%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV235+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:50:17 PM UTC 2026
% Result : Theorem 41.58s 5.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV235+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 08:37:52 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 41.58/5.70 % Refutation found
% 41.58/5.70 % SZS status Theorem for theBenchmark: Theorem is valid
% 41.58/5.70 % SZS output start CNFRefutation for theBenchmark
% 41.58/5.70 fof(f1,axiom,(
% 41.58/5.70 (! [X1,X2] : xor(X1,X2) = xor(X2,X1) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f3,axiom,(
% 41.58/5.70 (! [X1,X2] : decrypt(X1,crypt(X1,X2)) = X2 )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f4,axiom,(
% 41.58/5.70 (! [X1] : xor(X1,id) = X1 )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f5,axiom,(
% 41.58/5.70 (! [X1] : xor(X1,X1) = id )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f7,axiom,(
% 41.58/5.70 (! [Xtype,Xk1,Xkek1] :( ( p(crypt(xor(km,Xtype),Xk1))& p(Xtype)& p(crypt(xor(km,exp),Xkek1)) )=> p(crypt(xor(Xkek1,Xtype),Xk1)) ) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f8,axiom,(
% 41.58/5.70 (! [Xk,Xtype] :( ( p(Xk)& p(Xtype) )=> p(crypt(xor(km,xor(kp,Xtype)),Xk)) ) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f10,axiom,(
% 41.58/5.70 (! [Xk1,Xtype,Xk2] :( ( p(Xk1)& p(crypt(xor(km,xor(Xtype,kp)),Xk2))& p(Xtype) )=> p(crypt(xor(km,Xtype),xor(Xk2,Xk1))) ) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f12,axiom,(
% 41.58/5.70 (! [X1,Xk1] :( ( p(X1)& p(crypt(xor(km,data),Xk1)) )=> p(decrypt(Xk1,X1)) ) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f16,axiom,(
% 41.58/5.70 (! [X1,X2] :( ( p(X2)& p(X1) )=> p(crypt(X1,X2)) ) )),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f19,axiom,(
% 41.58/5.70 p(data) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f20,axiom,(
% 41.58/5.70 p(id) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f21,axiom,(
% 41.58/5.70 p(pin) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f22,axiom,(
% 41.58/5.70 p(crypt(xor(km,pin),pp)) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f27,axiom,(
% 41.58/5.70 p(exp) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f28,axiom,(
% 41.58/5.70 p(a) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f29,conjecture,(
% 41.58/5.70 p(crypt(pp,a)) ),
% 41.58/5.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 41.58/5.70 fof(f30,negated_conjecture,(
% 41.58/5.70 ~(p(crypt(pp,a)) )),
% 41.58/5.70 inference(negated_conjecture,[status(cth)],[f29])).
% 41.58/5.70 fof(f31,plain,(
% 41.58/5.70 ![X0,X1]: (xor(X0,X1)=xor(X1,X0))),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f1])).
% 41.58/5.70 fof(f33,plain,(
% 41.58/5.70 ![X0,X1]: (decrypt(X0,crypt(X0,X1))=X1)),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f3])).
% 41.58/5.70 fof(f34,plain,(
% 41.58/5.70 ![X0]: (xor(X0,id)=X0)),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f4])).
% 41.58/5.70 fof(f35,plain,(
% 41.58/5.70 ![X0]: (xor(X0,X0)=id)),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f5])).
% 41.58/5.70 fof(f38,plain,(
% 41.58/5.70 ![Xtype,Xk1,Xkek1]: (((~p(crypt(xor(km,Xtype),Xk1))|~p(Xtype))|~p(crypt(xor(km,exp),Xkek1)))|p(crypt(xor(Xkek1,Xtype),Xk1)))),
% 41.58/5.70 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 41.58/5.70 fof(f39,plain,(
% 41.58/5.70 ![X0,X1,X2]: (~p(crypt(xor(km,X0),X1))|~p(X0)|~p(crypt(xor(km,exp),X2))|p(crypt(xor(X2,X0),X1)))),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f38])).
% 41.58/5.70 fof(f40,plain,(
% 41.58/5.70 ![Xk,Xtype]: ((~p(Xk)|~p(Xtype))|p(crypt(xor(km,xor(kp,Xtype)),Xk)))),
% 41.58/5.70 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 41.58/5.70 fof(f41,plain,(
% 41.58/5.70 ![X0,X1]: (~p(X0)|~p(X1)|p(crypt(xor(km,xor(kp,X1)),X0)))),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f40])).
% 41.58/5.70 fof(f44,plain,(
% 41.58/5.70 ![Xk1,Xtype,Xk2]: (((~p(Xk1)|~p(crypt(xor(km,xor(Xtype,kp)),Xk2)))|~p(Xtype))|p(crypt(xor(km,Xtype),xor(Xk2,Xk1))))),
% 41.58/5.70 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 41.58/5.70 fof(f45,plain,(
% 41.58/5.70 ![X0,X1,X2]: (~p(X0)|~p(crypt(xor(km,xor(X1,kp)),X2))|~p(X1)|p(crypt(xor(km,X1),xor(X2,X0))))),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f44])).
% 41.58/5.70 fof(f48,plain,(
% 41.58/5.70 ![X1,Xk1]: ((~p(X1)|~p(crypt(xor(km,data),Xk1)))|p(decrypt(Xk1,X1)))),
% 41.58/5.70 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 41.58/5.70 fof(f49,plain,(
% 41.58/5.70 ![X0,X1]: (~p(X0)|~p(crypt(xor(km,data),X1))|p(decrypt(X1,X0)))),
% 41.58/5.70 inference(cnf_transformation,[status(thm)],[f48])).
% 41.58/5.70 fof(f58,plain,(
% 41.58/5.70 ![X1,X2]: ((~p(X2)|~p(X1))|p(crypt(X1,X2)))),
% 41.58/5.70 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 41.58/5.70 fof(f59,plain,(
% 41.58/5.70 ![X0,X1]: (~p(X0)|~p(X1)|p(crypt(X1,X0)))),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f58])).
% 41.58/5.73 fof(f62,plain,(
% 41.58/5.73 p(data)),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f19])).
% 41.58/5.73 fof(f63,plain,(
% 41.58/5.73 p(id)),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f20])).
% 41.58/5.73 fof(f64,plain,(
% 41.58/5.73 p(pin)),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f21])).
% 41.58/5.73 fof(f65,plain,(
% 41.58/5.73 p(crypt(xor(km,pin),pp))),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f22])).
% 41.58/5.73 fof(f70,plain,(
% 41.58/5.73 p(exp)),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f27])).
% 41.58/5.73 fof(f71,plain,(
% 41.58/5.73 p(a)),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f28])).
% 41.58/5.73 fof(f72,plain,(
% 41.58/5.73 ~p(crypt(pp,a))),
% 41.58/5.73 inference(cnf_transformation,[status(thm)],[f30])).
% 41.58/5.73 fof(f102,plain,(
% 41.58/5.73 ![X0]: (X0=xor(id,X0))),
% 41.58/5.73 inference(paramodulation,[status(thm)],[f34,f31])).
% 41.58/5.73 fof(f677,plain,(
% 41.58/5.73 ![X0,X1]: (~p(X0)|~p(X1)|p(crypt(xor(km,xor(X1,kp)),X0)))),
% 41.58/5.73 inference(paramodulation,[status(thm)],[f31,f41])).
% 41.58/5.73 fof(f2220,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(X1)|~p(X2)|~p(X1)|p(crypt(xor(km,X1),xor(X0,X2))))),
% 41.58/5.73 inference(resolution,[status(thm)],[f677,f45])).
% 41.58/5.73 fof(f2241,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(X1)|~p(X2)|p(crypt(xor(km,X1),xor(X0,X2))))),
% 41.58/5.73 inference(duplicate_literals_removal,[status(thm)],[f2220])).
% 41.58/5.73 fof(f2397,plain,(
% 41.58/5.73 ![X0,X1]: (~p(id)|~p(X0)|~p(X1)|p(crypt(xor(km,X0),X1)))),
% 41.58/5.73 inference(paramodulation,[status(thm)],[f102,f2241])).
% 41.58/5.73 fof(f2412,plain,(
% 41.58/5.73 ![X0,X1]: (~p(X0)|~p(X1)|~p(X0)|p(crypt(xor(km,X1),id)))),
% 41.58/5.73 inference(paramodulation,[status(thm)],[f35,f2241])).
% 41.58/5.73 fof(f2421,plain,(
% 41.58/5.73 ![X0,X1]: (~p(X0)|~p(X1)|p(crypt(xor(km,X0),X1)))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2397,f63])).
% 41.58/5.73 fof(f2423,plain,(
% 41.58/5.73 ![X0,X1]: (~p(X0)|~p(X1)|p(crypt(xor(km,X1),id)))),
% 41.58/5.73 inference(duplicate_literals_removal,[status(thm)],[f2412])).
% 41.58/5.73 fof(f2424,plain,(
% 41.58/5.73 ![X0,X1]: (~p(data)|~p(X0)|~p(X1)|p(decrypt(X0,X1)))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2421,f49])).
% 41.58/5.73 fof(f2447,plain,(
% 41.58/5.73 ![X0,X1]: (~p(X0)|~p(X1)|p(decrypt(X0,X1)))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2424,f62])).
% 41.58/5.73 fof(f2451,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(X1)|~p(X2)|p(crypt(decrypt(X0,X1),X2)))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2447,f59])).
% 41.58/5.73 fof(f2469,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(exp)|~p(crypt(xor(km,X1),X2))|~p(X1)|p(crypt(xor(id,X1),X2)))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2423,f39])).
% 41.58/5.73 fof(f2492,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(exp)|~p(crypt(xor(km,X1),X2))|~p(X1)|p(crypt(X1,X2)))),
% 41.58/5.73 inference(forward_demodulation,[status(thm)],[f102,f2469])).
% 41.58/5.73 fof(f2493,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(crypt(xor(km,X1),X2))|~p(X1)|p(crypt(X1,X2)))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2492,f70])).
% 41.58/5.73 fof(f2595,plain,(
% 41.58/5.73 ![X0,X1,X2]: (~p(X0)|~p(crypt(X0,X1))|~p(X2)|p(crypt(X1,X2)))),
% 41.58/5.73 inference(paramodulation,[status(thm)],[f33,f2451])).
% 41.58/5.73 fof(f2605,plain,(
% 41.58/5.73 ![X0]: (~p(X0)|~p(crypt(X0,pp))|~p(a))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2595,f72])).
% 41.58/5.73 fof(f2608,plain,(
% 41.58/5.73 ![X0]: (~p(X0)|~p(crypt(X0,pp)))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2605,f71])).
% 41.58/5.73 fof(f2851,plain,(
% 41.58/5.73 ![X0]: (~p(X0)|~p(pin)|p(crypt(pin,pp)))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2493,f65])).
% 41.58/5.73 fof(f2885,plain,(
% 41.58/5.73 ![X0]: (~p(X0)|p(crypt(pin,pp)))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2851,f64])).
% 41.58/5.73 fof(f2904,plain,(
% 41.58/5.73 ![X0]: (~p(X0)|~p(pin))),
% 41.58/5.73 inference(resolution,[status(thm)],[f2885,f2608])).
% 41.58/5.73 fof(f2908,plain,(
% 41.58/5.73 ![X0]: (~p(X0))),
% 41.58/5.73 inference(forward_subsumption_resolution,[status(thm)],[f2904,f64])).
% 41.58/5.73 fof(f2909,plain,(
% 41.58/5.73 $false),
% 41.58/5.73 inference(backward_subsumption_resolution,[status(thm)],[f70,f2908])).
% 41.58/5.73 % SZS output end CNFRefutation for theBenchmark.p
% 15.03/5.76 % Elapsed time: 5.385710 seconds
% 15.03/5.76 % CPU time: 42.388803 seconds
% 15.03/5.76 % Total memory used: 267.687 MB
% 15.03/5.76 % Net memory used: 227.347 MB
%------------------------------------------------------------------------------