%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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:46:56 PM UTC 2026
% Result : Theorem 0.14s 0.45s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 16
% Syntax : Number of formulae : 119 ( 27 unt; 0 def)
% Number of atoms : 503 ( 120 equ)
% Maximal formula atoms : 11 ( 4 avg)
% Number of connectives : 760 ( 376 ~; 338 |; 37 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 7 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-2 aty)
% Number of variables : 294 ( 294 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [E1,E2] :
( ( knows(inverse(E2))
& knows(encrypt(E1,E2)) )
=> knows(E1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [E1,E2] :
( ( knows(E2)
& knows(symmetric_encrypt(E1,E2)) )
=> knows(E1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [E,K] :
( ( knows(K)
& knows(sign(E,inverse(K))) )
=> knows(E) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [E1,E2] :
( ( knows(E2)
& knows(E1) )
=> ( knows(sign(E1,E2))
& knows(extract(E1,E2))
& knows(symmetric_decrypt(E1,E2))
& knows(decrypt(E1,E2))
& knows(symmetric_encrypt(E1,E2))
& knows(encrypt(E1,E2))
& knows(concatenate(E1,E2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [E1,E2] :
( knows(concatenate(E1,E2))
=> ( knows(E2)
& knows(E1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [E] :
( knows(E)
=> ( knows(hash(E))
& knows(tail(E))
& knows(head(E)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [E,K] : decrypt(encrypt(E,K),inverse(K)) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [E,K] : extract(sign(E,inverse(K)),K) = E,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X,Y] : head(concatenate(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] : tail(concatenate(X,Y)) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [X] : first(X) = head(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [X] : second(X) = head(tail(X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X,Y] :
( ( knows(Y)
& knows(X) )
=> knows(mac(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( knows(k_a)
& knows(inverse(k_a))
& knows(k_ca) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [Init_1,Init_2,Init_3,Resp_1,Resp_2] :
( ( ( second(extract(Init_3,Init_2)) = Init_2
& knows(Init_3)
& knows(Init_2)
& knows(Init_1) )
=> knows(concatenate(encrypt(sign(concatenate(kgen(Init_2),concatenate(Init_1,eol)),inverse(k_s)),Init_2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) )
& ( ( second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))) = n
& first(extract(Resp_2,k_ca)) = s
& knows(Resp_2)
& knows(Resp_1) )
=> knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))))) )
& knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,conjecture,
knows(secret),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
~ knows(secret),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
! [E1,E2] :
( knows(E1)
| ~ knows(inverse(E2))
| ~ knows(encrypt(E1,E2)) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f22,plain,
! [E1] :
( knows(E1)
| ! [E2] :
( ~ knows(inverse(E2))
| ~ knows(encrypt(E1,E2)) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f23,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(inverse(X1))
| ~ knows(encrypt(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [E1,E2] :
( knows(E1)
| ~ knows(E2)
| ~ knows(symmetric_encrypt(E1,E2)) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f25,plain,
! [E1] :
( knows(E1)
| ! [E2] :
( ~ knows(E2)
| ~ knows(symmetric_encrypt(E1,E2)) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f26,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(X1)
| ~ knows(symmetric_encrypt(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f27,plain,
! [E,K] :
( knows(E)
| ~ knows(K)
| ~ knows(sign(E,inverse(K))) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
! [E] :
( knows(E)
| ! [K] :
( ~ knows(K)
| ~ knows(sign(E,inverse(K))) ) ),
inference(miniscoping,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(X1)
| ~ knows(sign(X0,inverse(X1))) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f30,plain,
! [E1,E2] :
( ( knows(sign(E1,E2))
& knows(extract(E1,E2))
& knows(symmetric_decrypt(E1,E2))
& knows(decrypt(E1,E2))
& knows(symmetric_encrypt(E1,E2))
& knows(encrypt(E1,E2))
& knows(concatenate(E1,E2)) )
| ~ knows(E2)
| ~ knows(E1) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
! [X0,X1] :
( knows(concatenate(X0,X1))
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f32,plain,
! [X0,X1] :
( knows(encrypt(X0,X1))
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f36,plain,
! [X0,X1] :
( knows(extract(X0,X1))
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f37,plain,
! [X0,X1] :
( knows(sign(X0,X1))
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f38,plain,
! [E1,E2] :
( ( knows(E2)
& knows(E1) )
| ~ knows(concatenate(E1,E2)) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f39,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(concatenate(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f40,plain,
! [X0,X1] :
( knows(X1)
| ~ knows(concatenate(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f41,plain,
! [E] :
( ( knows(hash(E))
& knows(tail(E))
& knows(head(E)) )
| ~ knows(E) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f42,plain,
! [X0] :
( knows(head(X0))
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f45,plain,
! [X0,X1] : decrypt(encrypt(X0,X1),inverse(X1)) = X0,
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f47,plain,
! [X0,X1] : extract(sign(X0,inverse(X1)),X1) = X0,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f48,plain,
! [X0,X1] : head(concatenate(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f49,plain,
! [X0,X1] : tail(concatenate(X0,X1)) = X1,
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f50,plain,
! [X0] : first(X0) = head(X0),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f51,plain,
! [X0] : second(X0) = head(tail(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f54,plain,
! [X,Y] :
( knows(mac(X,Y))
| ~ knows(Y)
| ~ knows(X) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f55,plain,
! [X0,X1] :
( knows(mac(X0,X1))
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f56,plain,
knows(k_ca),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f57,plain,
knows(inverse(k_a)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f58,plain,
knows(k_a),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f59,plain,
! [Init_1,Init_2,Init_3,Resp_1,Resp_2] :
( ( knows(concatenate(encrypt(sign(concatenate(kgen(Init_2),concatenate(Init_1,eol)),inverse(k_s)),Init_2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| second(extract(Init_3,Init_2)) != Init_2
| ~ knows(Init_3)
| ~ knows(Init_2)
| ~ knows(Init_1) )
& ( knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))))
| second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))) != n
| first(extract(Resp_2,k_ca)) != s
| ~ knows(Resp_2)
| ~ knows(Resp_1) )
& knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f60,plain,
( ! [Init_1,Init_2] :
( knows(concatenate(encrypt(sign(concatenate(kgen(Init_2),concatenate(Init_1,eol)),inverse(k_s)),Init_2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| ! [Init_3] :
( second(extract(Init_3,Init_2)) != Init_2
| ~ knows(Init_3)
| ~ knows(Init_2)
| ~ knows(Init_1) ) )
& ! [Resp_1,Resp_2] :
( knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))))
| second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))) != n
| first(extract(Resp_2,k_ca)) != s
| ~ knows(Resp_2)
| ~ knows(Resp_1) )
& knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))) ),
inference(miniscoping,[status(thm)],[f59]) ).
fof(f61,plain,
knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,first(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))))
| second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))) != n
| first(extract(X1,k_ca)) != s
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f63,plain,
! [X0,X1,X2] :
( knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f64,plain,
~ knows(secret),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f68,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,first(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))))
| second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))) != n
| head(extract(X1,k_ca)) != s
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f50,f62]) ).
fof(f69,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))))
| second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))) != n
| head(extract(X1,k_ca)) != s
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f50,f68]) ).
fof(f72,plain,
! [X0,X1] : second(concatenate(X0,X1)) = head(X1),
inference(paramodulation,[status(thm)],[f49,f51]) ).
fof(f76,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca))))))
| second(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca)))) != n
| head(X1) != s
| ~ knows(sign(X1,inverse(k_ca)))
| ~ knows(X0) ),
inference(paramodulation,[status(thm)],[f47,f69]) ).
fof(f77,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca))))))
| second(extract(decrypt(X0,inverse(k_c)),second(X1))) != n
| head(X1) != s
| ~ knows(sign(X1,inverse(k_ca)))
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f47,f76]) ).
fof(f78,plain,
! [X0,X1] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(X1)))))
| second(extract(decrypt(X0,inverse(k_c)),second(X1))) != n
| head(X1) != s
| ~ knows(sign(X1,inverse(k_ca)))
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f47,f77]) ).
fof(f95,plain,
knows(concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))),
inference(resolution,[status(thm)],[f61,f40]) ).
fof(f96,plain,
knows(n),
inference(resolution,[status(thm)],[f61,f39]) ).
fof(f97,plain,
knows(sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))),
inference(resolution,[status(thm)],[f95,f40]) ).
fof(f98,plain,
knows(k_c),
inference(resolution,[status(thm)],[f95,f39]) ).
fof(f99,plain,
! [X0,X1,X2] :
( knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f63,f40]) ).
fof(f100,plain,
! [X0,X1,X2] :
( knows(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f63,f39]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))
| second(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol))))) != n
| head(concatenate(s,concatenate(k_s,eol))) != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f99,f78]) ).
fof(f103,plain,
! [X0,X1,X2] :
( knows(concatenate(s,concatenate(k_s,eol)))
| ~ knows(k_ca)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f99,f29]) ).
fof(f104,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))
| second(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol))))) != n
| s != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f48,f102]) ).
fof(f105,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))
| second(extract(decrypt(X3,inverse(k_c)),head(concatenate(k_s,eol)))) != n
| s != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f72,f104]) ).
fof(f106,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| s != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f48,f105]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),head(concatenate(k_s,eol))))))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| s != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f72,f106]) ).
fof(f108,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),k_s))))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| s != s
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f48,f107]) ).
fof(f109,plain,
! [X0,X1,X2,X3] :
( knows(symmetric_encrypt(secret,head(extract(decrypt(X3,inverse(k_c)),k_s))))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(trivial_equality_resolution,[status(thm)],[f108]) ).
fof(f110,plain,
! [X0,X1,X2] :
( knows(concatenate(s,concatenate(k_s,eol)))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f103,f56]) ).
fof(f111,plain,
! [X0,X1,X2,X3] :
( knows(secret)
| ~ knows(head(extract(decrypt(X3,inverse(k_c)),k_s)))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f109,f26]) ).
fof(f113,plain,
! [X0,X1,X2,X3] :
( ~ knows(head(extract(decrypt(X3,inverse(k_c)),k_s)))
| second(extract(decrypt(X3,inverse(k_c)),k_s)) != n
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f111,f64]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( ~ knows(head(extract(X3,k_s)))
| second(extract(decrypt(encrypt(X3,k_c),inverse(k_c)),k_s)) != n
| ~ knows(encrypt(X3,k_c))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(paramodulation,[status(thm)],[f45,f113]) ).
fof(f117,plain,
! [X0,X1,X2,X3] :
( ~ knows(head(extract(X3,k_s)))
| second(extract(X3,k_s)) != n
| ~ knows(encrypt(X3,k_c))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f45,f116]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ knows(k_c)
| ~ knows(X3)
| ~ knows(head(extract(X3,k_s)))
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f117,f32]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ knows(X3)
| ~ knows(head(extract(X3,k_s)))
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f118,f98]) ).
fof(f120,plain,
! [X0,X1,X2,X3] :
( ~ knows(extract(X3,k_s))
| ~ knows(X3)
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f119,f42]) ).
fof(f123,plain,
! [X0,X1,X2,X3] :
( ~ knows(k_s)
| ~ knows(X3)
| ~ knows(X3)
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f120,f36]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( ~ knows(k_s)
| ~ knows(X3)
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f123]) ).
fof(f140,plain,
( knows(concatenate(c,concatenate(k_c,eol)))
| ~ knows(k_c) ),
inference(resolution,[status(thm)],[f97,f29]) ).
fof(f141,plain,
knows(concatenate(c,concatenate(k_c,eol))),
inference(forward_subsumption_resolution,[status(thm)],[f140,f98]) ).
fof(f147,plain,
! [X0,X1,X2] :
( knows(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)))
| ~ knows(inverse(X1))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f100,f23]) ).
fof(f171,plain,
! [X0,X1,X2] :
( knows(concatenate(k_s,eol))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f110,f40]) ).
fof(f174,plain,
! [X0,X1,X2] :
( knows(k_s)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f171,f39]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ knows(X3)
| second(extract(X3,k_s)) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f125,f174]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ~ knows(sign(X3,inverse(k_s)))
| second(X3) != n
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(paramodulation,[status(thm)],[f47,f175]) ).
fof(f178,plain,
! [X0,X1] :
( knows(sign(concatenate(kgen(k_a),concatenate(X0,eol)),inverse(k_s)))
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(k_a)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f147,f57]) ).
fof(f179,plain,
! [X0,X1] :
( knows(sign(concatenate(kgen(k_a),concatenate(X0,eol)),inverse(k_s)))
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f58]) ).
fof(f180,plain,
! [X0,X1,X2,X3,X4] :
( second(concatenate(kgen(k_a),concatenate(X0,eol))) != n
| second(extract(X4,X3)) != X3
| ~ knows(X4)
| ~ knows(X3)
| ~ knows(X2)
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f179,f176]) ).
fof(f182,plain,
! [X0,X1,X2,X3,X4] :
( head(concatenate(X0,eol)) != n
| second(extract(X4,X3)) != X3
| ~ knows(X4)
| ~ knows(X3)
| ~ knows(X2)
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f72,f180]) ).
fof(f183,plain,
! [X0,X1,X2,X3,X4] :
( X0 != n
| second(extract(X4,X3)) != X3
| ~ knows(X4)
| ~ knows(X3)
| ~ knows(X2)
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_demodulation,[status(thm)],[f48,f182]) ).
fof(f184,plain,
! [X1,X2,X3,X4] :
( second(extract(X4,X3)) != X3
| ~ knows(X4)
| ~ knows(X3)
| ~ knows(X2)
| second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(n) ),
inference(destructive_equality_resolution,[status(thm)],[f183]) ).
fof(f185,plain,
! [X0,X1,X2,X3] :
( second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| second(extract(X0,k_a)) != k_a
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f184,f96]) ).
fof(f186,plain,
! [X0,X1,X2,X3] :
( second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| second(X0) != k_a
| ~ knows(sign(X0,inverse(k_a))) ),
inference(paramodulation,[status(thm)],[f47,f185]) ).
fof(f187,plain,
! [X0,X1,X2,X3] :
( ~ knows(inverse(k_a))
| ~ knows(X0)
| second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| second(X0) != k_a ),
inference(resolution,[status(thm)],[f186,f37]) ).
fof(f188,plain,
! [X0,X1,X2,X3] :
( ~ knows(X0)
| second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| second(X0) != k_a ),
inference(forward_subsumption_resolution,[status(thm)],[f187,f57]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4] :
( ~ knows(concatenate(X4,X0))
| second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| head(X0) != k_a ),
inference(paramodulation,[status(thm)],[f72,f188]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4] :
( ~ knows(X0)
| ~ knows(X4)
| second(extract(X3,X2)) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(X1)
| head(X0) != k_a ),
inference(resolution,[status(thm)],[f189,f31]) ).
fof(f236,plain,
! [X0,X1,X2,X3,X4] :
( ~ knows(concatenate(k_a,X4))
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f210,f48]) ).
fof(f240,plain,
! [X0,X1,X2,X3,X4] :
( ~ knows(X4)
| ~ knows(k_a)
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f236,f31]) ).
fof(f241,plain,
! [X0,X1,X2] :
( ~ knows(inverse(X1))
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f147,f244]) ).
fof(f244,plain,
! [X0,X1,X2,X3,X4] :
( ~ knows(X4)
| ~ knows(X3)
| second(extract(X2,X1)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f240,f58]) ).
fof(f245,plain,
! [X0,X1] :
( second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(k_a)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f241,f57]) ).
fof(f246,plain,
! [X0,X1] :
( second(extract(X1,k_a)) != k_a
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f245,f58]) ).
fof(f247,plain,
! [X0,X1] :
( second(X1) != k_a
| ~ knows(sign(X1,inverse(k_a)))
| ~ knows(X0) ),
inference(paramodulation,[status(thm)],[f47,f246]) ).
fof(f248,plain,
! [X0,X1] :
( ~ knows(inverse(k_a))
| ~ knows(X1)
| second(X1) != k_a
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f247,f37]) ).
fof(f249,plain,
! [X0,X1] :
( ~ knows(X1)
| second(X1) != k_a
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f248,f57]) ).
fof(f250,plain,
! [X0,X1,X2] :
( ~ knows(concatenate(X2,X1))
| head(X1) != k_a
| ~ knows(X0) ),
inference(paramodulation,[status(thm)],[f72,f249]) ).
fof(f268,plain,
! [X0,X1,X2] :
( ~ knows(X1)
| ~ knows(X2)
| head(X1) != k_a
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f250,f31]) ).
fof(f301,plain,
! [X0,X1,X2] :
( ~ knows(concatenate(k_a,X2))
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f268,f48]) ).
fof(f305,plain,
! [X0,X1,X2] :
( ~ knows(X2)
| ~ knows(k_a)
| ~ knows(X1)
| ~ knows(X0) ),
inference(resolution,[status(thm)],[f301,f31]) ).
fof(f311,plain,
! [X0,X1] :
( ~ knows(X1)
| ~ knows(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f55,f319]) ).
fof(f319,plain,
! [X0,X1,X2] :
( ~ knows(X2)
| ~ knows(X1)
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f305,f58]) ).
fof(f320,plain,
! [X0,X1] : ~ knows(concatenate(X0,X1)),
inference(backward_subsumption_resolution,[status(thm)],[f40,f311]) ).
fof(f329,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f141,f320]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n006.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:35:12 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 0.14/0.45 % Refutation found
% 0.14/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.48 % Elapsed time: 0.108243 seconds
% 0.14/0.48 % CPU time: 0.537415 seconds
% 0.14/0.48 % Total memory used: 73.870 MB
% 0.14/0.48 % Net memory used: 72.544 MB
%------------------------------------------------------------------------------