%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:16 PM UTC 2026
% Result : Theorem 4.86s 1.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.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:34:51 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 4.86/1.52 % Refutation found
% 4.86/1.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.86/1.52 % SZS output start CNFRefutation for theBenchmark
% 4.86/1.52 fof(f1,axiom,(
% 4.86/1.52 (! [E1,E2] :( ( knows(encrypt(E1,E2))& knows(inverse(E2)) )=> knows(E1) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f2,axiom,(
% 4.86/1.52 (! [E1,E2] :( ( knows(symmetric_encrypt(E1,E2))& knows(E2) )=> knows(E1) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f3,axiom,(
% 4.86/1.52 (! [E,K] :( ( knows(sign(E,inverse(K)))& knows(K) )=> knows(E) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f4,axiom,(
% 4.86/1.52 (! [E1,E2] :( ( knows(E1)& knows(E2) )=> ( knows(concatenate(E1,E2))& knows(encrypt(E1,E2))& knows(symmetric_encrypt(E1,E2))& knows(decrypt(E1,E2))& knows(symmetric_decrypt(E1,E2))& knows(extract(E1,E2))& knows(sign(E1,E2)) ) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f5,axiom,(
% 4.86/1.52 (! [E1,E2] :( knows(concatenate(E1,E2))=> ( knows(E1)& knows(E2) ) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f6,axiom,(
% 4.86/1.52 (! [E] :( knows(E)=> ( knows(head(E))& knows(tail(E))& knows(hash(E)) ) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f7,axiom,(
% 4.86/1.52 (! [E,K] : decrypt(encrypt(E,K),inverse(K)) = E )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f9,axiom,(
% 4.86/1.52 (! [E,K] : extract(sign(E,inverse(K)),K) = E )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f10,axiom,(
% 4.86/1.52 (! [X,Y] : head(concatenate(X,Y)) = X )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f11,axiom,(
% 4.86/1.52 (! [X,Y] : tail(concatenate(X,Y)) = Y )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f12,axiom,(
% 4.86/1.52 (! [X] : first(X) = head(X) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f13,axiom,(
% 4.86/1.52 (! [X] : second(X) = head(tail(X)) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f14,axiom,(
% 4.86/1.52 (! [X] : third(X) = head(tail(tail(X))) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f17,axiom,(
% 4.86/1.52 ( knows(k_ca)& knows(inverse(k_a))& knows(k_a) ) ),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f18,axiom,(
% 4.86/1.52 (! [Init_1,Init_2,Init_3,Resp_1,Resp_2] :( knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))& ( ( knows(Resp_1)& knows(Resp_2)& first(extract(Resp_2,k_ca)) = s& second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))) = n )=> knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))))) )& ( ( knows(Init_1)& knows(Init_2)& knows(Init_3)& second(extract(Init_3,Init_2)) = 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)))) ) ) )),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f19,conjecture,(
% 4.86/1.52 knows(secret) ),
% 4.86/1.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.86/1.52 fof(f20,negated_conjecture,(
% 4.86/1.52 ~(knows(secret) )),
% 4.86/1.52 inference(negated_conjecture,[status(cth)],[f19])).
% 4.86/1.52 fof(f21,plain,(
% 4.86/1.52 ![E1,E2]: ((~knows(encrypt(E1,E2))|~knows(inverse(E2)))|knows(E1))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 4.86/1.52 fof(f22,plain,(
% 4.86/1.52 ![E1]: ((![E2]: (~knows(encrypt(E1,E2))|~knows(inverse(E2))))|knows(E1))),
% 4.86/1.52 inference(miniscoping,[status(thm)],[f21])).
% 4.86/1.52 fof(f23,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(encrypt(X0,X1))|~knows(inverse(X1))|knows(X0))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f22])).
% 4.86/1.52 fof(f24,plain,(
% 4.86/1.52 ![E1,E2]: ((~knows(symmetric_encrypt(E1,E2))|~knows(E2))|knows(E1))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 4.86/1.52 fof(f25,plain,(
% 4.86/1.52 ![E1]: ((![E2]: (~knows(symmetric_encrypt(E1,E2))|~knows(E2)))|knows(E1))),
% 4.86/1.52 inference(miniscoping,[status(thm)],[f24])).
% 4.86/1.52 fof(f26,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(symmetric_encrypt(X0,X1))|~knows(X1)|knows(X0))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f25])).
% 4.86/1.52 fof(f27,plain,(
% 4.86/1.52 ![E,K]: ((~knows(sign(E,inverse(K)))|~knows(K))|knows(E))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 4.86/1.52 fof(f28,plain,(
% 4.86/1.52 ![E]: ((![K]: (~knows(sign(E,inverse(K)))|~knows(K)))|knows(E))),
% 4.86/1.52 inference(miniscoping,[status(thm)],[f27])).
% 4.86/1.52 fof(f29,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(sign(X0,inverse(X1)))|~knows(X1)|knows(X0))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f28])).
% 4.86/1.52 fof(f30,plain,(
% 4.86/1.52 ![E1,E2]: ((~knows(E1)|~knows(E2))|((((((knows(concatenate(E1,E2))&knows(encrypt(E1,E2)))&knows(symmetric_encrypt(E1,E2)))&knows(decrypt(E1,E2)))&knows(symmetric_decrypt(E1,E2)))&knows(extract(E1,E2)))&knows(sign(E1,E2))))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 4.86/1.52 fof(f31,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|knows(concatenate(X0,X1)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f30])).
% 4.86/1.52 fof(f32,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|knows(encrypt(X0,X1)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f30])).
% 4.86/1.52 fof(f36,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|knows(extract(X0,X1)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f30])).
% 4.86/1.52 fof(f37,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|knows(sign(X0,X1)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f30])).
% 4.86/1.52 fof(f38,plain,(
% 4.86/1.52 ![E1,E2]: (~knows(concatenate(E1,E2))|(knows(E1)&knows(E2)))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 4.86/1.52 fof(f39,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(concatenate(X0,X1))|knows(X0))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f38])).
% 4.86/1.52 fof(f40,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(concatenate(X0,X1))|knows(X1))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f38])).
% 4.86/1.52 fof(f41,plain,(
% 4.86/1.52 ![E]: (~knows(E)|((knows(head(E))&knows(tail(E)))&knows(hash(E))))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 4.86/1.52 fof(f42,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|knows(head(X0)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f41])).
% 4.86/1.52 fof(f43,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|knows(tail(X0)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f41])).
% 4.86/1.52 fof(f45,plain,(
% 4.86/1.52 ![X0,X1]: (decrypt(encrypt(X0,X1),inverse(X1))=X0)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f7])).
% 4.86/1.52 fof(f47,plain,(
% 4.86/1.52 ![X0,X1]: (extract(sign(X0,inverse(X1)),X1)=X0)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f9])).
% 4.86/1.52 fof(f48,plain,(
% 4.86/1.52 ![X0,X1]: (head(concatenate(X0,X1))=X0)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f10])).
% 4.86/1.52 fof(f49,plain,(
% 4.86/1.52 ![X0,X1]: (tail(concatenate(X0,X1))=X1)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f11])).
% 4.86/1.52 fof(f50,plain,(
% 4.86/1.52 ![X0]: (first(X0)=head(X0))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f12])).
% 4.86/1.52 fof(f51,plain,(
% 4.86/1.52 ![X0]: (second(X0)=head(tail(X0)))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f13])).
% 4.86/1.52 fof(f52,plain,(
% 4.86/1.52 ![X0]: (third(X0)=head(tail(tail(X0))))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f14])).
% 4.86/1.52 fof(f56,plain,(
% 4.86/1.52 knows(k_ca)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f17])).
% 4.86/1.52 fof(f57,plain,(
% 4.86/1.52 knows(inverse(k_a))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f17])).
% 4.86/1.52 fof(f58,plain,(
% 4.86/1.52 knows(k_a)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f17])).
% 4.86/1.52 fof(f59,plain,(
% 4.86/1.52 ![Init_1,Init_2,Init_3,Resp_1,Resp_2]: ((knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))&((((~knows(Resp_1)|~knows(Resp_2))|~first(extract(Resp_2,k_ca))=s)|~second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))=n)|knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))))))&((((~knows(Init_1)|~knows(Init_2))|~knows(Init_3))|~second(extract(Init_3,Init_2))=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))))))),
% 4.86/1.52 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 4.86/1.52 fof(f60,plain,(
% 4.86/1.52 (knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))&(![Resp_1,Resp_2]: ((((~knows(Resp_1)|~knows(Resp_2))|~first(extract(Resp_2,k_ca))=s)|~second(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca))))=n)|knows(symmetric_encrypt(secret,first(extract(decrypt(Resp_1,inverse(k_c)),second(extract(Resp_2,k_ca)))))))))&(![Init_1,Init_2]: ((![Init_3]: (((~knows(Init_1)|~knows(Init_2))|~knows(Init_3))|~second(extract(Init_3,Init_2))=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))))))),
% 4.86/1.52 inference(miniscoping,[status(thm)],[f59])).
% 4.86/1.52 fof(f61,plain,(
% 4.86/1.52 knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f60])).
% 4.86/1.52 fof(f62,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|~first(extract(X1,k_ca))=s|~second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))=n|knows(symmetric_encrypt(secret,first(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))))))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f60])).
% 4.86/1.52 fof(f63,plain,(
% 4.86/1.52 ![X0,X1,X2]: (~knows(X0)|~knows(X1)|~knows(X2)|~second(extract(X2,X1))=X1|knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))))),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f60])).
% 4.86/1.52 fof(f64,plain,(
% 4.86/1.52 ~knows(secret)),
% 4.86/1.52 inference(cnf_transformation,[status(thm)],[f20])).
% 4.86/1.52 fof(f65,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|~first(extract(X1,k_ca))=s|~second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))))))),
% 4.86/1.52 inference(backward_demodulation,[status(thm)],[f50,f62])).
% 4.86/1.52 fof(f66,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|~head(extract(X1,k_ca))=s|~second(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(X1,k_ca)))))))),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f50,f65])).
% 4.86/1.52 fof(f67,plain,(
% 4.86/1.52 ![X0]: (~knows(encrypt(X0,k_a))|knows(X0))),
% 4.86/1.52 inference(resolution,[status(thm)],[f57,f23])).
% 4.86/1.52 fof(f70,plain,(
% 4.86/1.52 ![X0,X1]: (second(concatenate(X0,X1))=head(X1))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f49,f51])).
% 4.86/1.52 fof(f71,plain,(
% 4.86/1.52 ![X0]: (~knows(tail(X0))|knows(second(X0)))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f51,f42])).
% 4.86/1.52 fof(f72,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(sign(X1,inverse(k_ca)))|~head(X1)=s|~second(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca)))))))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f47,f66])).
% 4.86/1.52 fof(f73,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(sign(X1,inverse(k_ca)))|~head(X1)=s|~second(extract(decrypt(X0,inverse(k_c)),second(X1)))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(extract(sign(X1,inverse(k_ca)),k_ca)))))))),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f47,f72])).
% 4.86/1.52 fof(f74,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(sign(X1,inverse(k_ca)))|~head(X1)=s|~second(extract(decrypt(X0,inverse(k_c)),second(X1)))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(X1))))))),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f47,f73])).
% 4.86/1.52 fof(f75,plain,(
% 4.86/1.52 ![X0]: (third(X0)=second(tail(X0)))),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f51,f52])).
% 4.86/1.52 fof(f76,plain,(
% 4.86/1.52 ![X0,X1]: (third(concatenate(X0,X1))=second(X1))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f49,f75])).
% 4.86/1.52 fof(f79,definition,(
% 4.86/1.52 ![X0]: (sQ0_spl <=> (~knows(X0)))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f80,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~sQ0_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f79])).
% 4.86/1.52 fof(f88,definition,(
% 4.86/1.52 sQ2_spl <=> (knows(k_a))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f90,plain,(
% 4.86/1.52 ~knows(k_a)|sQ2_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f88])).
% 4.86/1.52 fof(f97,plain,(
% 4.86/1.52 ![X0]: (~knows(tail(tail(X0)))|knows(third(X0)))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f75,f71])).
% 4.86/1.52 fof(f123,definition,(
% 4.86/1.52 sQ8_spl <=> (knows(secret))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f124,plain,(
% 4.86/1.52 knows(secret)|~sQ8_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f123])).
% 4.86/1.52 fof(f133,plain,(
% 4.86/1.52 $false|~sQ8_spl),
% 4.86/1.52 inference(forward_subsumption_resolution,[status(thm)],[f124,f64])).
% 4.86/1.52 fof(f134,plain,(
% 4.86/1.52 ~sQ8_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f133])).
% 4.86/1.52 fof(f149,definition,(
% 4.86/1.52 sQ10_spl <=> (knows(k_c))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f151,plain,(
% 4.86/1.52 ~knows(k_c)|sQ10_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f149])).
% 4.86/1.52 fof(f208,plain,(
% 4.86/1.52 $false|~sQ0_spl),
% 4.86/1.52 inference(backward_subsumption_resolution,[status(thm)],[f57,f80])).
% 4.86/1.52 fof(f211,plain,(
% 4.86/1.52 ~sQ0_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f208])).
% 4.86/1.52 fof(f254,plain,(
% 4.86/1.52 knows(concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))),
% 4.86/1.52 inference(resolution,[status(thm)],[f40,f61])).
% 4.86/1.52 fof(f255,plain,(
% 4.86/1.52 knows(n)),
% 4.86/1.52 inference(resolution,[status(thm)],[f39,f61])).
% 4.86/1.52 fof(f259,plain,(
% 4.86/1.52 ![X0,X1,X2]: (~knows(X0)|~knows(X1)|~knows(X2)|~second(extract(X2,X1))=X1|knows(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1)))),
% 4.86/1.52 inference(resolution,[status(thm)],[f63,f39])).
% 4.86/1.52 fof(f260,plain,(
% 4.86/1.52 ![X0,X1,X2]: (~knows(X0)|~knows(X1)|~knows(X2)|~second(extract(X2,X1))=X1|knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))),
% 4.86/1.52 inference(resolution,[status(thm)],[f63,f40])).
% 4.86/1.52 fof(f261,definition,(
% 4.86/1.52 ![X1,X2]: (sQ14_spl <=> (~knows(X1)|~knows(X2)|~second(extract(X2,X1))=X1))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f262,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(X1)|~second(extract(X1,X0))=X0|~sQ14_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f261])).
% 4.86/1.52 fof(f264,definition,(
% 4.86/1.52 sQ15_spl <=> (knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f265,plain,(
% 4.86/1.52 knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))|~sQ15_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f264])).
% 4.86/1.52 fof(f267,plain,(
% 4.86/1.52 sQ0_spl|sQ14_spl|sQ15_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f260,f79,f261,f264])).
% 4.86/1.52 fof(f327,plain,(
% 4.86/1.52 ![X0]: (knows(third(X0))|~knows(tail(X0)))),
% 4.86/1.52 inference(resolution,[status(thm)],[f97,f43])).
% 4.86/1.52 fof(f331,plain,(
% 4.86/1.52 ![X0,X1]: (knows(second(X0))|~knows(tail(concatenate(X1,X0))))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f76,f327])).
% 4.86/1.52 fof(f332,plain,(
% 4.86/1.52 ![X0]: (knows(second(X0))|~knows(X0))),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f49,f331])).
% 4.86/1.52 fof(f336,plain,(
% 4.86/1.52 ![X0,X1]: (knows(head(X0))|~knows(concatenate(X1,X0)))),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f70,f332])).
% 4.86/1.52 fof(f338,plain,(
% 4.86/1.52 knows(head(concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))),
% 4.86/1.52 inference(resolution,[status(thm)],[f336,f61])).
% 4.86/1.52 fof(f343,plain,(
% 4.86/1.52 knows(k_c)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f338])).
% 4.86/1.52 fof(f344,plain,(
% 4.86/1.52 $false|sQ10_spl),
% 4.86/1.52 inference(forward_subsumption_resolution,[status(thm)],[f343,f151])).
% 4.86/1.52 fof(f345,plain,(
% 4.86/1.52 sQ10_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f344])).
% 4.86/1.52 fof(f417,plain,(
% 4.86/1.52 knows(sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))),
% 4.86/1.52 inference(resolution,[status(thm)],[f254,f40])).
% 4.86/1.52 fof(f556,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)),X0))=X0|~sQ14_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f417,f262])).
% 4.86/1.52 fof(f1733,plain,(
% 4.86/1.52 ~second(extract(sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)),k_c))=k_c|~sQ14_spl),
% 4.86/1.52 inference(resolution,[status(thm)],[f556,f343])).
% 4.86/1.52 fof(f1755,plain,(
% 4.86/1.52 ~second(concatenate(c,concatenate(k_c,eol)))=k_c|~sQ14_spl),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f47,f1733])).
% 4.86/1.52 fof(f1756,plain,(
% 4.86/1.52 ~head(concatenate(k_c,eol))=k_c|~sQ14_spl),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f70,f1755])).
% 4.86/1.52 fof(f1757,plain,(
% 4.86/1.52 ~k_c=k_c|~sQ14_spl),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f1756])).
% 4.86/1.52 fof(f1758,plain,(
% 4.86/1.52 $false|~sQ14_spl),
% 4.86/1.52 inference(trivial_equality_resolution,[status(thm)],[f1757])).
% 4.86/1.52 fof(f1759,plain,(
% 4.86/1.52 ~sQ14_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f1758])).
% 4.86/1.52 fof(f1760,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~head(concatenate(s,concatenate(k_s,eol)))=s|~second(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))|~sQ15_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f265,f74])).
% 4.86/1.52 fof(f1761,plain,(
% 4.86/1.52 ~knows(k_ca)|knows(concatenate(s,concatenate(k_s,eol)))|~sQ15_spl),
% 4.86/1.52 inference(resolution,[status(thm)],[f265,f29])).
% 4.86/1.52 fof(f1762,definition,(
% 4.86/1.52 ![X0]: (sQ39_spl <=> (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1763,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))|~sQ39_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1762])).
% 4.86/1.52 fof(f1765,definition,(
% 4.86/1.52 sQ40_spl <=> (head(concatenate(s,concatenate(k_s,eol)))=s)),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1767,plain,(
% 4.86/1.52 ~head(concatenate(s,concatenate(k_s,eol)))=s|sQ40_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1765])).
% 4.86/1.52 fof(f1768,plain,(
% 4.86/1.52 sQ39_spl|~sQ40_spl|~sQ15_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1760,f1762,f1765,f264])).
% 4.86/1.52 fof(f1769,definition,(
% 4.86/1.52 sQ41_spl <=> (knows(k_ca))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1771,plain,(
% 4.86/1.52 ~knows(k_ca)|sQ41_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1769])).
% 4.86/1.52 fof(f1772,definition,(
% 4.86/1.52 sQ42_spl <=> (knows(concatenate(s,concatenate(k_s,eol))))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1773,plain,(
% 4.86/1.52 knows(concatenate(s,concatenate(k_s,eol)))|~sQ42_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1772])).
% 4.86/1.52 fof(f1775,plain,(
% 4.86/1.52 ~sQ41_spl|sQ42_spl|~sQ15_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1761,f1769,f1772,f264])).
% 4.86/1.52 fof(f1776,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),head(concatenate(k_s,eol))))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))|~sQ39_spl)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f70,f1763])).
% 4.86/1.52 fof(f1777,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),k_s))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),second(concatenate(s,concatenate(k_s,eol)))))))|~sQ39_spl)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f1776])).
% 4.86/1.52 fof(f1778,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),k_s))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),head(concatenate(k_s,eol))))))|~sQ39_spl)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f70,f1777])).
% 4.86/1.52 fof(f1779,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(decrypt(X0,inverse(k_c)),k_s))=n|knows(symmetric_encrypt(secret,head(extract(decrypt(X0,inverse(k_c)),k_s))))|~sQ39_spl)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f1778])).
% 4.86/1.52 fof(f1780,plain,(
% 4.86/1.52 $false|sQ41_spl),
% 4.86/1.52 inference(forward_subsumption_resolution,[status(thm)],[f1771,f56])).
% 4.86/1.52 fof(f1781,plain,(
% 4.86/1.52 sQ41_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f1780])).
% 4.86/1.52 fof(f1784,plain,(
% 4.86/1.52 knows(head(concatenate(k_s,eol)))|~sQ42_spl),
% 4.86/1.52 inference(resolution,[status(thm)],[f1773,f336])).
% 4.86/1.52 fof(f1789,plain,(
% 4.86/1.52 knows(k_s)|~sQ42_spl),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f1784])).
% 4.86/1.52 fof(f1801,plain,(
% 4.86/1.52 $false|sQ2_spl),
% 4.86/1.52 inference(forward_subsumption_resolution,[status(thm)],[f90,f58])).
% 4.86/1.52 fof(f1802,plain,(
% 4.86/1.52 sQ2_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f1801])).
% 4.86/1.52 fof(f1810,plain,(
% 4.86/1.52 ![X0,X1]: (~knows(X0)|~knows(k_a)|~knows(X1)|~second(extract(X1,k_a))=k_a|knows(sign(concatenate(kgen(k_a),concatenate(X0,eol)),inverse(k_s))))),
% 4.86/1.52 inference(resolution,[status(thm)],[f259,f67])).
% 4.86/1.52 fof(f1812,definition,(
% 4.86/1.52 ![X0]: (sQ43_spl <=> (~knows(X0)|knows(sign(concatenate(kgen(k_a),concatenate(X0,eol)),inverse(k_s)))))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1813,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|knows(sign(concatenate(kgen(k_a),concatenate(X0,eol)),inverse(k_s)))|~sQ43_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1812])).
% 4.86/1.52 fof(f1815,definition,(
% 4.86/1.52 ![X1]: (sQ44_spl <=> (~knows(X1)|~second(extract(X1,k_a))=k_a))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1816,plain,(
% 4.86/1.52 ![X0]: (~knows(X0)|~second(extract(X0,k_a))=k_a|~sQ44_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1815])).
% 4.86/1.52 fof(f1818,plain,(
% 4.86/1.52 sQ43_spl|~sQ2_spl|sQ44_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1810,f1812,f88,f1815])).
% 4.86/1.52 fof(f1820,plain,(
% 4.86/1.52 ![X0]: (~knows(encrypt(X0,k_c))|~second(extract(decrypt(encrypt(X0,k_c),inverse(k_c)),k_s))=n|knows(symmetric_encrypt(secret,head(extract(X0,k_s))))|~sQ39_spl)),
% 4.86/1.52 inference(paramodulation,[status(thm)],[f45,f1779])).
% 4.86/1.52 fof(f1825,plain,(
% 4.86/1.52 ![X0]: (~knows(encrypt(X0,k_c))|~second(extract(X0,k_s))=n|knows(symmetric_encrypt(secret,head(extract(X0,k_s))))|~sQ39_spl)),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f45,f1820])).
% 4.86/1.52 fof(f1826,plain,(
% 4.86/1.52 ~s=s|sQ40_spl),
% 4.86/1.52 inference(forward_demodulation,[status(thm)],[f48,f1767])).
% 4.86/1.52 fof(f1827,plain,(
% 4.86/1.52 $false|sQ40_spl),
% 4.86/1.52 inference(trivial_equality_resolution,[status(thm)],[f1826])).
% 4.86/1.52 fof(f1828,plain,(
% 4.86/1.52 sQ40_spl),
% 4.86/1.52 inference(contradiction_clause,[status(thm)],[f1827])).
% 4.86/1.52 fof(f1829,plain,(
% 4.86/1.52 ![X0]: (~knows(encrypt(X0,k_c))|~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))|knows(secret)|~sQ39_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f1825,f26])).
% 4.86/1.52 fof(f1831,definition,(
% 4.86/1.52 ![X0]: (sQ46_spl <=> (~knows(encrypt(X0,k_c))|~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1832,plain,(
% 4.86/1.52 ![X0]: (~knows(encrypt(X0,k_c))|~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))|~sQ46_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1831])).
% 4.86/1.52 fof(f1834,plain,(
% 4.86/1.52 sQ46_spl|sQ8_spl|~sQ39_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1829,f1831,f123,f1762])).
% 4.86/1.52 fof(f1837,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))|~knows(X0)|~knows(k_c)|~sQ46_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f1832,f32])).
% 4.86/1.52 fof(f1845,definition,(
% 4.86/1.52 ![X0]: (sQ49_spl <=> (~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))|~knows(X0)))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1846,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(head(extract(X0,k_s)))|~knows(X0)|~sQ49_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1845])).
% 4.86/1.52 fof(f1848,plain,(
% 4.86/1.52 sQ49_spl|~sQ10_spl|~sQ46_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1837,f1845,f149,f1831])).
% 4.86/1.52 fof(f1860,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(X0)|~knows(extract(X0,k_s))|~sQ49_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f1846,f42])).
% 4.86/1.52 fof(f1863,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(X0)|~knows(X0)|~knows(k_s)|~sQ49_spl)),
% 4.86/1.52 inference(resolution,[status(thm)],[f1860,f36])).
% 4.86/1.52 fof(f1865,definition,(
% 4.86/1.52 ![X0]: (sQ50_spl <=> (~second(extract(X0,k_s))=n|~knows(X0)|~knows(X0)))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1866,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(X0)|~knows(X0)|~sQ50_spl)),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1865])).
% 4.86/1.52 fof(f1868,definition,(
% 4.86/1.52 sQ51_spl <=> (knows(k_s))),
% 4.86/1.52 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 4.86/1.52 fof(f1870,plain,(
% 4.86/1.52 ~knows(k_s)|sQ51_spl),
% 4.86/1.52 inference(component_clause,[status(thm)],[f1868])).
% 4.86/1.52 fof(f1871,plain,(
% 4.86/1.52 sQ50_spl|~sQ51_spl|~sQ49_spl),
% 4.86/1.52 inference(split_clause,[status(thm)],[f1863,f1865,f1868,f1845])).
% 4.86/1.52 fof(f1873,plain,(
% 4.86/1.52 ![X0]: (~second(extract(X0,k_s))=n|~knows(X0)|~sQ50_spl)),
% 4.86/1.55 inference(duplicate_literals_removal,[status(thm)],[f1866])).
% 4.86/1.55 fof(f1874,plain,(
% 4.86/1.55 ![X0]: (~second(X0)=n|~knows(sign(X0,inverse(k_s)))|~sQ50_spl)),
% 4.86/1.55 inference(paramodulation,[status(thm)],[f47,f1873])).
% 4.86/1.55 fof(f1880,plain,(
% 4.86/1.55 $false|~sQ42_spl|sQ51_spl),
% 4.86/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1870,f1789])).
% 4.86/1.55 fof(f1881,plain,(
% 4.86/1.55 ~sQ42_spl|sQ51_spl),
% 4.86/1.55 inference(contradiction_clause,[status(thm)],[f1880])).
% 4.86/1.55 fof(f1915,plain,(
% 4.86/1.55 ![X0]: (~knows(X0)|~second(concatenate(kgen(k_a),concatenate(X0,eol)))=n|~sQ43_spl|~sQ50_spl)),
% 4.86/1.55 inference(resolution,[status(thm)],[f1813,f1874])).
% 4.86/1.55 fof(f1917,plain,(
% 4.86/1.55 ![X0]: (~knows(X0)|~head(concatenate(X0,eol))=n|~sQ43_spl|~sQ50_spl)),
% 4.86/1.55 inference(forward_demodulation,[status(thm)],[f70,f1915])).
% 4.86/1.55 fof(f1918,plain,(
% 4.86/1.55 ![X0]: (~knows(X0)|~X0=n|~sQ43_spl|~sQ50_spl)),
% 4.86/1.55 inference(forward_demodulation,[status(thm)],[f48,f1917])).
% 4.86/1.55 fof(f1919,plain,(
% 4.86/1.55 ~knows(n)|~sQ43_spl|~sQ50_spl),
% 4.86/1.55 inference(destructive_equality_resolution,[status(thm)],[f1918])).
% 4.86/1.55 fof(f1920,plain,(
% 4.86/1.55 $false|~sQ43_spl|~sQ50_spl),
% 4.86/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1919,f255])).
% 4.86/1.55 fof(f1921,plain,(
% 4.86/1.55 ~sQ43_spl|~sQ50_spl),
% 4.86/1.55 inference(contradiction_clause,[status(thm)],[f1920])).
% 4.86/1.55 fof(f1924,plain,(
% 4.86/1.55 ![X0]: (~knows(sign(X0,inverse(k_a)))|~second(X0)=k_a|~sQ44_spl)),
% 4.86/1.55 inference(paramodulation,[status(thm)],[f47,f1816])).
% 4.86/1.55 fof(f1925,plain,(
% 4.86/1.55 ![X0]: (~second(X0)=k_a|~knows(X0)|~knows(inverse(k_a))|~sQ44_spl)),
% 4.86/1.55 inference(resolution,[status(thm)],[f1924,f37])).
% 4.86/1.55 fof(f1926,definition,(
% 4.86/1.55 ![X0]: (sQ56_spl <=> (~second(X0)=k_a|~knows(X0)))),
% 4.86/1.55 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 4.86/1.55 fof(f1927,plain,(
% 4.86/1.55 ![X0]: (~second(X0)=k_a|~knows(X0)|~sQ56_spl)),
% 4.86/1.55 inference(component_clause,[status(thm)],[f1926])).
% 4.86/1.55 fof(f1929,definition,(
% 4.86/1.55 sQ57_spl <=> (knows(inverse(k_a)))),
% 4.86/1.55 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 4.86/1.55 fof(f1931,plain,(
% 4.86/1.55 ~knows(inverse(k_a))|sQ57_spl),
% 4.86/1.55 inference(component_clause,[status(thm)],[f1929])).
% 4.86/1.55 fof(f1932,plain,(
% 4.86/1.55 sQ56_spl|~sQ57_spl|~sQ44_spl),
% 4.86/1.55 inference(split_clause,[status(thm)],[f1925,f1926,f1929,f1815])).
% 4.86/1.55 fof(f1962,plain,(
% 4.86/1.55 ![X0,X1]: (~head(X0)=k_a|~knows(concatenate(X1,X0))|~sQ56_spl)),
% 4.86/1.55 inference(paramodulation,[status(thm)],[f70,f1927])).
% 4.86/1.55 fof(f1979,plain,(
% 4.86/1.55 ![X0,X1]: (~head(X0)=k_a|~knows(X1)|~knows(X0)|~sQ56_spl)),
% 4.86/1.55 inference(resolution,[status(thm)],[f1962,f31])).
% 4.86/1.55 fof(f1987,definition,(
% 4.86/1.55 ![X0]: (sQ63_spl <=> (~head(X0)=k_a|~knows(X0)))),
% 4.86/1.55 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 4.86/1.55 fof(f1988,plain,(
% 4.86/1.55 ![X0]: (~head(X0)=k_a|~knows(X0)|~sQ63_spl)),
% 4.86/1.55 inference(component_clause,[status(thm)],[f1987])).
% 4.86/1.55 fof(f1990,plain,(
% 4.86/1.55 sQ63_spl|sQ0_spl|~sQ56_spl),
% 4.86/1.55 inference(split_clause,[status(thm)],[f1979,f1987,f79,f1926])).
% 4.86/1.55 fof(f1991,plain,(
% 4.86/1.55 ![X0]: (~knows(concatenate(k_a,X0))|~sQ63_spl)),
% 4.86/1.55 inference(resolution,[status(thm)],[f1988,f48])).
% 4.86/1.55 fof(f1995,plain,(
% 4.86/1.55 ![X0]: (~knows(k_a)|~knows(X0)|~sQ63_spl)),
% 4.86/1.55 inference(resolution,[status(thm)],[f1991,f31])).
% 4.86/1.55 fof(f1996,plain,(
% 4.86/1.55 ~sQ2_spl|sQ0_spl|~sQ63_spl),
% 4.86/1.55 inference(split_clause,[status(thm)],[f1995,f88,f79,f1987])).
% 4.86/1.55 fof(f1997,plain,(
% 4.86/1.55 $false|sQ57_spl),
% 4.86/1.55 inference(forward_subsumption_resolution,[status(thm)],[f1931,f57])).
% 4.86/1.55 fof(f1998,plain,(
% 4.86/1.55 sQ57_spl),
% 4.86/1.55 inference(contradiction_clause,[status(thm)],[f1997])).
% 4.86/1.55 fof(f1999,plain,(
% 4.86/1.55 $false),
% 4.86/1.55 inference(sat_refutation,[status(thm)],[f134,f211,f267,f345,f1759,f1768,f1775,f1781,f1802,f1818,f1828,f1834,f1848,f1871,f1881,f1921,f1932,f1990,f1996,f1998])).
% 4.86/1.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.37/1.56 % Elapsed time: 1.179063 seconds
% 0.37/1.56 % CPU time: 8.827071 seconds
% 0.37/1.56 % Total memory used: 179.602 MB
% 0.37/1.56 % Net memory used: 172.267 MB
%------------------------------------------------------------------------------