%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 : Tue Sep 29 01:20:31 PM UTC 2026
% Result : Theorem 0.18s 0.27s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 25
% Syntax : Number of formulae : 169 ( 40 unt; 10 def)
% Number of atoms : 594 ( 49 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 803 ( 378 ~; 365 |; 42 &)
% ( 10 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 11 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 9 con; 0-2 aty)
% Number of variables : 238 ( 0 sgn 238 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( knows(encrypt(X0,X1))
& knows(inverse(X1)) )
=> knows(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',encrypt_equation) ).
fof(f2,axiom,
! [X0,X1] :
( ( knows(symmetric_encrypt(X0,X1))
& knows(X1) )
=> knows(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',symmetric_encrypt_equation) ).
fof(f3,axiom,
! [X0,X1] :
( ( knows(sign(X0,inverse(X1)))
& knows(X1) )
=> knows(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sign_equation) ).
fof(f4,axiom,
! [X0,X1] :
( ( knows(X0)
& knows(X1) )
=> ( knows(concatenate(X0,X1))
& knows(encrypt(X0,X1))
& knows(symmetric_encrypt(X0,X1))
& knows(decrypt(X0,X1))
& knows(symmetric_decrypt(X0,X1))
& knows(extract(X0,X1))
& knows(sign(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',construct_message_1) ).
fof(f5,axiom,
! [X0,X1] :
( knows(concatenate(X0,X1))
=> ( knows(X0)
& knows(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',construct_message_2) ).
fof(f6,axiom,
! [X0] :
( knows(X0)
=> ( knows(head(X0))
& knows(tail(X0))
& knows(hash(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',construct_message_3) ).
fof(f7,axiom,
! [X0,X1] : decrypt(encrypt(X0,X1),inverse(X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',decrypt_axiom) ).
fof(f9,axiom,
! [X0,X1] : extract(sign(X0,inverse(X1)),X1) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sign_axiom) ).
fof(f10,axiom,
! [X0,X1] : head(concatenate(X0,X1)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_axiom) ).
fof(f11,axiom,
! [X0,X1] : tail(concatenate(X0,X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tail_axiom) ).
fof(f12,axiom,
! [X0] : first(X0) = head(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first_axiom) ).
fof(f13,axiom,
! [X0] : second(X0) = head(tail(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second_axiom) ).
fof(f17,axiom,
( knows(k_ca)
& knows(inverse(k_a))
& knows(k_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',previous_knowledge) ).
fof(f18,axiom,
! [X0,X1,X2,X3,X4] :
( knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))
& ( ( knows(X3)
& knows(X4)
& first(extract(X4,k_ca)) = s
& second(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca)))) = n )
=> knows(symmetric_encrypt(secret,first(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca)))))) )
& ( ( 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)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',protocol) ).
fof(f19,conjecture,
knows(secret),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',attack) ).
fof(f20,negated_conjecture,
~ knows(secret),
inference(negated_conjecture,[status(cth)],[f19]) ).
fof(f21,plain,
~ knows(secret),
inference(flattening,[],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(encrypt(X0,X1))
| ~ knows(inverse(X1)) ),
inference(ennf_transformation,[],[f1]) ).
fof(f23,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(encrypt(X0,X1))
| ~ knows(inverse(X1)) ),
inference(flattening,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(symmetric_encrypt(X0,X1))
| ~ knows(X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f25,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(symmetric_encrypt(X0,X1))
| ~ knows(X1) ),
inference(flattening,[],[f24]) ).
fof(f26,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(sign(X0,inverse(X1)))
| ~ knows(X1) ),
inference(ennf_transformation,[],[f3]) ).
fof(f27,plain,
! [X0,X1] :
( knows(X0)
| ~ knows(sign(X0,inverse(X1)))
| ~ knows(X1) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
! [X0,X1] :
( ( knows(concatenate(X0,X1))
& knows(encrypt(X0,X1))
& knows(symmetric_encrypt(X0,X1))
& knows(decrypt(X0,X1))
& knows(symmetric_decrypt(X0,X1))
& knows(extract(X0,X1))
& knows(sign(X0,X1)) )
| ~ knows(X0)
| ~ knows(X1) ),
inference(ennf_transformation,[],[f4]) ).
fof(f29,plain,
! [X0,X1] :
( ( knows(concatenate(X0,X1))
& knows(encrypt(X0,X1))
& knows(symmetric_encrypt(X0,X1))
& knows(decrypt(X0,X1))
& knows(symmetric_decrypt(X0,X1))
& knows(extract(X0,X1))
& knows(sign(X0,X1)) )
| ~ knows(X0)
| ~ knows(X1) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1] :
( ( knows(X0)
& knows(X1) )
| ~ knows(concatenate(X0,X1)) ),
inference(ennf_transformation,[],[f5]) ).
fof(f31,plain,
! [X0] :
( ( knows(head(X0))
& knows(tail(X0))
& knows(hash(X0)) )
| ~ knows(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4] :
( knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))
& ( knows(symmetric_encrypt(secret,first(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca))))))
| ~ knows(X3)
| ~ knows(X4)
| first(extract(X4,k_ca)) != s
| n != second(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca)))) )
& ( knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| ~ knows(X0)
| ~ knows(X1)
| ~ knows(X2)
| second(extract(X2,X1)) != X1 ) ),
inference(ennf_transformation,[],[f18]) ).
fof(f35,plain,
! [X0,X1,X2,X3,X4] :
( knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))))
& ( knows(symmetric_encrypt(secret,first(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca))))))
| ~ knows(X3)
| ~ knows(X4)
| first(extract(X4,k_ca)) != s
| n != second(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca)))) )
& ( knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| ~ knows(X0)
| ~ knows(X1)
| ~ knows(X2)
| second(extract(X2,X1)) != X1 ) ),
inference(flattening,[],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( ~ knows(encrypt(X0,X1))
| knows(X0)
| ~ knows(inverse(X1)) ),
inference(cnf_transformation,[],[f23]) ).
fof(f37,plain,
! [X0,X1] :
( ~ knows(symmetric_encrypt(X0,X1))
| knows(X0)
| ~ knows(X1) ),
inference(cnf_transformation,[],[f25]) ).
fof(f38,plain,
! [X0,X1] :
( ~ knows(sign(X0,inverse(X1)))
| knows(X0)
| ~ knows(X1) ),
inference(cnf_transformation,[],[f27]) ).
fof(f39,plain,
! [X0,X1] :
( knows(sign(X0,X1))
| ~ knows(X0)
| ~ knows(X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f44,plain,
! [X0,X1] :
( knows(encrypt(X0,X1))
| ~ knows(X0)
| ~ knows(X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f45,plain,
! [X0,X1] :
( knows(concatenate(X0,X1))
| ~ knows(X0)
| ~ knows(X1) ),
inference(cnf_transformation,[],[f29]) ).
fof(f46,plain,
! [X0,X1] :
( ~ knows(concatenate(X0,X1))
| knows(X1) ),
inference(cnf_transformation,[],[f30]) ).
fof(f47,plain,
! [X0,X1] :
( ~ knows(concatenate(X0,X1))
| knows(X0) ),
inference(cnf_transformation,[],[f30]) ).
fof(f50,plain,
! [X0] :
( knows(head(X0))
| ~ knows(X0) ),
inference(cnf_transformation,[],[f31]) ).
fof(f51,plain,
! [X0,X1] : decrypt(encrypt(X0,X1),inverse(X1)) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f53,plain,
! [X0,X1] : extract(sign(X0,inverse(X1)),X1) = X0,
inference(cnf_transformation,[],[f9]) ).
fof(f54,plain,
! [X0,X1] : head(concatenate(X0,X1)) = X0,
inference(cnf_transformation,[],[f10]) ).
fof(f55,plain,
! [X0,X1] : tail(concatenate(X0,X1)) = X1,
inference(cnf_transformation,[],[f11]) ).
fof(f56,plain,
! [X0] : head(X0) = first(X0),
inference(cnf_transformation,[],[f12]) ).
fof(f57,plain,
! [X0] : second(X0) = head(tail(X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f61,plain,
knows(k_a),
inference(cnf_transformation,[],[f17]) ).
fof(f62,plain,
knows(inverse(k_a)),
inference(cnf_transformation,[],[f17]) ).
fof(f63,plain,
knows(k_ca),
inference(cnf_transformation,[],[f17]) ).
fof(f64,plain,
! [X2,X0,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))))
| ~ knows(X0)
| ~ knows(X1)
| ~ knows(X2)
| second(extract(X2,X1)) != X1 ),
inference(cnf_transformation,[],[f35]) ).
fof(f65,plain,
! [X3,X4] :
( knows(symmetric_encrypt(secret,first(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca))))))
| ~ knows(X3)
| ~ knows(X4)
| first(extract(X4,k_ca)) != s
| n != second(extract(decrypt(X3,inverse(k_c)),second(extract(X4,k_ca)))) ),
inference(cnf_transformation,[],[f35]) ).
fof(f66,plain,
knows(concatenate(n,concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))))),
inference(cnf_transformation,[],[f35]) ).
fof(f67,plain,
~ knows(secret),
inference(cnf_transformation,[],[f21]) ).
fof(f69,plain,
! [X0] : second(X0) = first(tail(X0)),
inference(definition_unfolding,[],[f57,f56]) ).
fof(f71,plain,
! [X0] :
( knows(first(X0))
| ~ knows(X0) ),
inference(definition_unfolding,[],[f50,f56]) ).
fof(f72,plain,
! [X0,X1] : first(concatenate(X0,X1)) = X0,
inference(definition_unfolding,[],[f54,f56]) ).
fof(f73,plain,
! [X3,X4] :
( n != first(tail(extract(decrypt(X3,inverse(k_c)),first(tail(extract(X4,k_ca))))))
| ~ knows(X3)
| ~ knows(X4)
| first(extract(X4,k_ca)) != s
| knows(symmetric_encrypt(secret,first(extract(decrypt(X3,inverse(k_c)),first(tail(extract(X4,k_ca))))))) ),
inference(definition_unfolding,[],[f65,f69,f69,f69]) ).
fof(f74,plain,
! [X2,X0,X1] :
( first(tail(extract(X2,X1))) != X1
| ~ knows(X0)
| ~ knows(X1)
| ~ knows(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)))) ),
inference(definition_unfolding,[],[f64,f69]) ).
fof(f86,plain,
knows(n),
inference(resolution,[],[f66,f47]) ).
fof(f87,plain,
knows(concatenate(k_c,sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c)))),
inference(resolution,[],[f66,f46]) ).
fof(f88,plain,
! [X2,X0,X1] :
( first(tail(X0)) != X1
| ~ knows(X2)
| ~ knows(X1)
| ~ knows(sign(X0,inverse(X1)))
| knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X2,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) ),
inference(superposition,[],[f74,f53]) ).
fof(f89,plain,
! [X0,X1] :
( n != first(tail(extract(X0,first(tail(extract(X1,k_ca))))))
| ~ knows(encrypt(X0,k_c))
| ~ knows(X1)
| s != first(extract(X1,k_ca))
| knows(symmetric_encrypt(secret,first(extract(X0,first(tail(extract(X1,k_ca))))))) ),
inference(superposition,[],[f73,f51]) ).
fof(f91,plain,
knows(k_c),
inference(resolution,[],[f87,f47]) ).
fof(f92,plain,
knows(sign(concatenate(c,concatenate(k_c,eol)),inverse(k_c))),
inference(resolution,[],[f87,f46]) ).
fof(f94,plain,
! [X0,X1] :
( s != first(extract(X1,k_ca))
| ~ knows(encrypt(sign(X0,inverse(first(tail(extract(X1,k_ca))))),k_c))
| ~ knows(X1)
| n != first(tail(X0))
| knows(symmetric_encrypt(secret,first(X0))) ),
inference(superposition,[],[f89,f53]) ).
fof(f97,plain,
! [X2,X3,X0,X1] :
( first(X0) != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(sign(concatenate(X1,X0),inverse(X2)))
| knows(concatenate(encrypt(sign(concatenate(kgen(X2),concatenate(X3,eol)),inverse(k_s)),X2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) ),
inference(superposition,[],[f88,f55]) ).
fof(f98,plain,
! [X0,X1] :
( knows(concatenate(encrypt(sign(concatenate(kgen(first(tail(X1))),concatenate(X0,eol)),inverse(k_s)),first(tail(X1))),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| ~ knows(first(tail(X1)))
| ~ knows(sign(X1,inverse(first(tail(X1)))))
| ~ knows(X0) ),
inference(equality_resolution,[],[f88]) ).
fof(f104,plain,
! [X0,X1] :
( n != first(tail(X1))
| ~ knows(encrypt(sign(X1,inverse(first(tail(X0)))),k_c))
| ~ knows(sign(X0,inverse(k_ca)))
| first(X0) != s
| knows(symmetric_encrypt(secret,first(X1))) ),
inference(superposition,[],[f94,f53]) ).
fof(f110,plain,
! [X2,X0,X1] :
( first(X0) != n
| ~ knows(encrypt(sign(concatenate(X1,X0),inverse(first(tail(X2)))),k_c))
| ~ knows(sign(X2,inverse(k_ca)))
| s != first(X2)
| knows(symmetric_encrypt(secret,first(concatenate(X1,X0)))) ),
inference(superposition,[],[f104,f55]) ).
fof(f111,plain,
! [X2,X0,X1] :
( s != first(X2)
| first(X0) != n
| ~ knows(encrypt(sign(concatenate(X1,X0),inverse(first(tail(X2)))),k_c))
| ~ knows(sign(X2,inverse(k_ca)))
| knows(symmetric_encrypt(secret,X1)) ),
inference(forward_demodulation,[],[f110,f72]) ).
fof(f114,plain,
! [X2,X3,X0,X1,X4] :
( X0 != X2
| ~ knows(X3)
| ~ knows(X2)
| ~ knows(sign(concatenate(X4,concatenate(X0,X1)),inverse(X2)))
| knows(concatenate(encrypt(sign(concatenate(kgen(X2),concatenate(X3,eol)),inverse(k_s)),X2),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) ),
inference(superposition,[],[f97,f72]) ).
fof(f116,plain,
! [X2,X3,X0,X1] :
( s != X0
| n != first(X2)
| ~ knows(encrypt(sign(concatenate(X3,X2),inverse(first(tail(concatenate(X0,X1))))),k_c))
| ~ knows(sign(concatenate(X0,X1),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X3)) ),
inference(superposition,[],[f111,f72]) ).
fof(f117,plain,
! [X2,X3,X0,X1] :
( n != first(X2)
| s != X0
| ~ knows(encrypt(sign(concatenate(X3,X2),inverse(first(X1))),k_c))
| ~ knows(sign(concatenate(X0,X1),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X3)) ),
inference(forward_demodulation,[],[f116,f55]) ).
fof(f118,plain,
! [X0,X1] :
( knows(encrypt(sign(concatenate(kgen(first(tail(X0))),concatenate(X1,eol)),inverse(k_s)),first(tail(X0))))
| ~ knows(sign(X0,inverse(first(tail(X0)))))
| ~ knows(X1)
| ~ knows(first(tail(X0))) ),
inference(resolution,[],[f98,f47]) ).
fof(f122,definition,
( spl0_1
<=> knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f124,plain,
( knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f126,definition,
( spl0_2
<=> ! [X1] : ~ knows(X1) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f127,plain,
( ! [X1] : ~ knows(X1)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f133,plain,
( $false
| ~ spl0_2 ),
inference(resolution,[],[f127,f62]) ).
fof(f167,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f133]) ).
fof(f205,definition,
( spl0_8
<=> ! [X0] :
( ~ knows(inverse(first(X0)))
| ~ knows(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f206,plain,
( ! [X0] :
( ~ knows(inverse(first(X0)))
| ~ knows(X0) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f205]) ).
fof(f214,plain,
! [X2,X3,X0,X1] :
( ~ knows(sign(concatenate(X2,concatenate(X1,X3)),inverse(X1)))
| ~ knows(X1)
| ~ knows(X0)
| knows(concatenate(encrypt(sign(concatenate(kgen(X1),concatenate(X0,eol)),inverse(k_s)),X1),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) ),
inference(equality_resolution,[],[f114]) ).
fof(f217,plain,
( ! [X0,X1] :
( ~ knows(concatenate(X0,X1))
| ~ knows(inverse(X0)) )
| ~ spl0_8 ),
inference(superposition,[],[f206,f72]) ).
fof(f219,plain,
( ! [X0,X1] :
( ~ knows(inverse(X0))
| ~ knows(X0)
| ~ knows(X1) )
| ~ spl0_8 ),
inference(resolution,[],[f217,f45]) ).
fof(f226,definition,
( spl0_9
<=> ! [X0] :
( ~ knows(inverse(X0))
| ~ knows(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f227,plain,
( ! [X0] :
( ~ knows(inverse(X0))
| ~ knows(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( spl0_2
| spl0_9
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f219,f205,f226,f126]) ).
fof(f229,plain,
( knows(concatenate(s,concatenate(k_s,eol)))
| ~ knows(k_ca)
| ~ spl0_1 ),
inference(resolution,[],[f124,f38]) ).
fof(f230,plain,
( knows(concatenate(s,concatenate(k_s,eol)))
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f229,f63]) ).
fof(f232,plain,
( knows(concatenate(k_s,eol))
| ~ spl0_1 ),
inference(resolution,[],[f230,f46]) ).
fof(f233,plain,
! [X0,X1] :
( ~ knows(sign(X0,inverse(first(tail(X0)))))
| ~ knows(X1)
| ~ knows(first(tail(X0)))
| knows(sign(concatenate(kgen(first(tail(X0))),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(inverse(first(tail(X0)))) ),
inference(resolution,[],[f118,f36]) ).
fof(f237,plain,
( knows(k_s)
| ~ spl0_1 ),
inference(resolution,[],[f232,f47]) ).
fof(f244,plain,
! [X0,X1] :
( ~ knows(X0)
| ~ knows(first(tail(X1)))
| knows(sign(concatenate(kgen(first(tail(X1))),concatenate(X0,eol)),inverse(k_s)))
| ~ knows(inverse(first(tail(X1))))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1)))) ),
inference(resolution,[],[f233,f39]) ).
fof(f246,plain,
! [X0,X1] :
( knows(sign(concatenate(kgen(first(tail(X1))),concatenate(X0,eol)),inverse(k_s)))
| ~ knows(first(tail(X1)))
| ~ knows(X0)
| ~ knows(inverse(first(tail(X1))))
| ~ knows(X1) ),
inference(duplicate_literal_removal,[],[f244]) ).
fof(f256,plain,
! [X0] :
( ~ knows(k_c)
| ~ knows(X0)
| knows(concatenate(encrypt(sign(concatenate(kgen(k_c),concatenate(X0,eol)),inverse(k_s)),k_c),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca)))) ),
inference(resolution,[],[f214,f92]) ).
fof(f258,plain,
! [X0] :
( knows(concatenate(encrypt(sign(concatenate(kgen(k_c),concatenate(X0,eol)),inverse(k_s)),k_c),sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))))
| ~ knows(X0) ),
inference(forward_subsumption_resolution,[],[f256,f91]) ).
fof(f260,plain,
! [X0] :
( ~ knows(X0)
| knows(sign(concatenate(s,concatenate(k_s,eol)),inverse(k_ca))) ),
inference(resolution,[],[f258,f46]) ).
fof(f304,plain,
! [X0,X1] :
( ~ knows(first(tail(X0)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X0))))
| ~ knows(X0)
| knows(concatenate(kgen(first(tail(X0))),concatenate(X1,eol)))
| ~ knows(k_s) ),
inference(resolution,[],[f246,f38]) ).
fof(f305,plain,
! [X2,X0,X1] :
( ~ knows(concatenate(X1,X0))
| ~ knows(first(X0))
| ~ knows(X2)
| ~ knows(inverse(first(X0)))
| knows(sign(concatenate(kgen(first(X0)),concatenate(X2,eol)),inverse(k_s))) ),
inference(superposition,[],[f246,f55]) ).
fof(f315,definition,
( spl0_19
<=> ! [X0] :
( ~ knows(first(tail(X0)))
| ~ knows(X0)
| ~ knows(inverse(first(tail(X0)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f316,plain,
( ! [X0] :
( ~ knows(inverse(first(tail(X0))))
| ~ knows(X0)
| ~ knows(first(tail(X0))) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f321,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f260,f126,f122]) ).
fof(f323,definition,
( spl0_20
<=> knows(k_s) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f327,definition,
( spl0_21
<=> ! [X0,X1] :
( ~ knows(first(tail(X0)))
| knows(concatenate(kgen(first(tail(X0))),concatenate(X1,eol)))
| ~ knows(X0)
| ~ knows(inverse(first(tail(X0))))
| ~ knows(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f328,plain,
( ! [X0,X1] :
( knows(concatenate(kgen(first(tail(X0))),concatenate(X1,eol)))
| ~ knows(first(tail(X0)))
| ~ knows(X0)
| ~ knows(inverse(first(tail(X0))))
| ~ knows(X1) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f329,plain,
( ~ spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f304,f327,f323]) ).
fof(f332,plain,
( spl0_20
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f237,f122,f323]) ).
fof(f349,plain,
( ~ knows(k_a)
| ~ spl0_9 ),
inference(resolution,[],[f227,f62]) ).
fof(f350,plain,
( $false
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f349,f61]) ).
fof(f351,plain,
~ spl0_9,
inference(avatar_contradiction_clause,[],[f350]) ).
fof(f381,plain,
! [X2,X3,X0,X1,X4] :
( s != X2
| n != X0
| ~ knows(encrypt(sign(concatenate(X3,concatenate(X0,X1)),inverse(first(X4))),k_c))
| ~ knows(sign(concatenate(X2,X4),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X3)) ),
inference(superposition,[],[f117,f72]) ).
fof(f382,plain,
( ! [X0,X1] :
( ~ knows(concatenate(X1,X0))
| ~ knows(inverse(first(X0)))
| ~ knows(first(X0)) )
| ~ spl0_19 ),
inference(superposition,[],[f316,f55]) ).
fof(f383,plain,
( ! [X0,X1] :
( ~ knows(inverse(first(X0)))
| ~ knows(first(X0))
| ~ knows(X1)
| ~ knows(X0) )
| ~ spl0_19 ),
inference(resolution,[],[f382,f45]) ).
fof(f395,plain,
( ! [X0,X1] :
( ~ knows(inverse(first(X0)))
| ~ knows(X1)
| ~ knows(X0) )
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f383,f71]) ).
fof(f396,plain,
( spl0_2
| spl0_8
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f395,f315,f205,f126]) ).
fof(f408,plain,
( ! [X0,X1] :
( ~ knows(first(tail(X0)))
| ~ knows(X0)
| ~ knows(inverse(first(tail(X0))))
| ~ knows(X1)
| knows(kgen(first(tail(X0)))) )
| ~ spl0_21 ),
inference(resolution,[],[f328,f47]) ).
fof(f416,definition,
( spl0_25
<=> ! [X0] :
( ~ knows(first(tail(X0)))
| knows(kgen(first(tail(X0))))
| ~ knows(inverse(first(tail(X0))))
| ~ knows(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f417,plain,
( ! [X0] :
( ~ knows(inverse(first(tail(X0))))
| knows(kgen(first(tail(X0))))
| ~ knows(first(tail(X0)))
| ~ knows(X0) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( spl0_2
| spl0_25
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f408,f327,f416,f126]) ).
fof(f447,plain,
( ! [X0,X1] :
( ~ knows(concatenate(X1,X0))
| knows(kgen(first(X0)))
| ~ knows(first(X0))
| ~ knows(inverse(first(X0))) )
| ~ spl0_25 ),
inference(superposition,[],[f417,f55]) ).
fof(f471,plain,
( ! [X0,X1] :
( knows(kgen(first(concatenate(X0,eol))))
| ~ knows(first(concatenate(X0,eol)))
| ~ knows(inverse(first(concatenate(X0,eol))))
| ~ knows(first(tail(X1)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1))))
| ~ knows(X0) )
| ~ spl0_21
| ~ spl0_25 ),
inference(resolution,[],[f447,f328]) ).
fof(f473,plain,
( ! [X0,X1] :
( knows(kgen(X0))
| ~ knows(first(concatenate(X0,eol)))
| ~ knows(inverse(first(concatenate(X0,eol))))
| ~ knows(first(tail(X1)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1))))
| ~ knows(X0) )
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_demodulation,[],[f471,f72]) ).
fof(f478,plain,
( ! [X0,X1] :
( ~ knows(X0)
| knows(kgen(X0))
| ~ knows(inverse(first(concatenate(X0,eol))))
| ~ knows(first(tail(X1)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1))))
| ~ knows(X0) )
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_demodulation,[],[f473,f72]) ).
fof(f479,plain,
( ! [X0,X1] :
( ~ knows(X0)
| knows(kgen(X0))
| ~ knows(inverse(first(concatenate(X0,eol))))
| ~ knows(first(tail(X1)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1)))) )
| ~ spl0_21
| ~ spl0_25 ),
inference(duplicate_literal_removal,[],[f478]) ).
fof(f487,plain,
( ! [X0,X1] :
( ~ knows(inverse(X0))
| ~ knows(X0)
| knows(kgen(X0))
| ~ knows(first(tail(X1)))
| ~ knows(X1)
| ~ knows(inverse(first(tail(X1)))) )
| ~ spl0_21
| ~ spl0_25 ),
inference(forward_demodulation,[],[f479,f72]) ).
fof(f492,definition,
( spl0_30
<=> ! [X0] :
( ~ knows(inverse(X0))
| knows(kgen(X0))
| ~ knows(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f493,plain,
( ! [X0] :
( ~ knows(inverse(X0))
| knows(kgen(X0))
| ~ knows(X0) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f492]) ).
fof(f494,plain,
( spl0_19
| spl0_30
| ~ spl0_21
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f487,f416,f327,f492,f315]) ).
fof(f514,plain,
( ! [X2,X0,X1] :
( ~ knows(first(concatenate(X0,eol)))
| ~ knows(X1)
| ~ knows(inverse(first(concatenate(X0,eol))))
| knows(sign(concatenate(kgen(first(concatenate(X0,eol))),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(first(tail(X2)))
| ~ knows(X2)
| ~ knows(inverse(first(tail(X2))))
| ~ knows(X0) )
| ~ spl0_21 ),
inference(resolution,[],[f305,f328]) ).
fof(f516,plain,
( ! [X2,X0,X1] :
( ~ knows(X0)
| ~ knows(X1)
| ~ knows(inverse(first(concatenate(X0,eol))))
| knows(sign(concatenate(kgen(first(concatenate(X0,eol))),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(first(tail(X2)))
| ~ knows(X2)
| ~ knows(inverse(first(tail(X2))))
| ~ knows(X0) )
| ~ spl0_21 ),
inference(forward_demodulation,[],[f514,f72]) ).
fof(f517,plain,
( ! [X2,X0,X1] :
( ~ knows(X0)
| ~ knows(X1)
| ~ knows(inverse(first(concatenate(X0,eol))))
| knows(sign(concatenate(kgen(first(concatenate(X0,eol))),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(first(tail(X2)))
| ~ knows(X2)
| ~ knows(inverse(first(tail(X2)))) )
| ~ spl0_21 ),
inference(duplicate_literal_removal,[],[f516]) ).
fof(f522,plain,
( ! [X2,X0,X1] :
( ~ knows(inverse(X0))
| ~ knows(X0)
| ~ knows(X1)
| knows(sign(concatenate(kgen(first(concatenate(X0,eol))),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(first(tail(X2)))
| ~ knows(X2)
| ~ knows(inverse(first(tail(X2)))) )
| ~ spl0_21 ),
inference(forward_demodulation,[],[f517,f72]) ).
fof(f530,plain,
( ! [X2,X0,X1] :
( knows(sign(concatenate(kgen(X0),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(inverse(X0))
| ~ knows(X0)
| ~ knows(X1)
| ~ knows(first(tail(X2)))
| ~ knows(X2)
| ~ knows(inverse(first(tail(X2)))) )
| ~ spl0_21 ),
inference(forward_demodulation,[],[f522,f72]) ).
fof(f535,definition,
( spl0_32
<=> ! [X0,X1] :
( knows(sign(concatenate(kgen(X0),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(X1)
| ~ knows(X0)
| ~ knows(inverse(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f536,plain,
( ! [X0,X1] :
( knows(sign(concatenate(kgen(X0),concatenate(X1,eol)),inverse(k_s)))
| ~ knows(X1)
| ~ knows(X0)
| ~ knows(inverse(X0)) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f537,plain,
( spl0_19
| spl0_32
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f530,f327,f535,f315]) ).
fof(f600,plain,
! [X2,X3,X0,X1] :
( n != X0
| ~ knows(encrypt(sign(concatenate(X1,concatenate(X0,X2)),inverse(first(X3))),k_c))
| ~ knows(sign(concatenate(s,X3),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X1)) ),
inference(equality_resolution,[],[f381]) ).
fof(f784,plain,
! [X2,X0,X1] :
( ~ knows(encrypt(sign(concatenate(X0,concatenate(n,X1)),inverse(first(X2))),k_c))
| ~ knows(sign(concatenate(s,X2),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X0)) ),
inference(equality_resolution,[],[f600]) ).
fof(f994,plain,
! [X2,X0,X1] :
( ~ knows(sign(concatenate(s,X0),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X1))
| ~ knows(sign(concatenate(X1,concatenate(n,X2)),inverse(first(X0))))
| ~ knows(k_c) ),
inference(resolution,[],[f784,f44]) ).
fof(f996,plain,
! [X2,X0,X1] :
( ~ knows(sign(concatenate(X1,concatenate(n,X2)),inverse(first(X0))))
| knows(symmetric_encrypt(secret,X1))
| ~ knows(sign(concatenate(s,X0),inverse(k_ca))) ),
inference(forward_subsumption_resolution,[],[f994,f91]) ).
fof(f1012,plain,
! [X2,X3,X0,X1] :
( ~ knows(sign(concatenate(s,concatenate(X0,X3)),inverse(k_ca)))
| knows(symmetric_encrypt(secret,X1))
| ~ knows(sign(concatenate(X1,concatenate(n,X2)),inverse(X0))) ),
inference(superposition,[],[f996,f72]) ).
fof(f1036,plain,
( ! [X0,X1] :
( ~ knows(sign(concatenate(X0,concatenate(n,X1)),inverse(k_s)))
| knows(symmetric_encrypt(secret,X0)) )
| ~ spl0_1 ),
inference(resolution,[],[f1012,f124]) ).
fof(f1042,plain,
( ! [X0] :
( knows(symmetric_encrypt(secret,kgen(X0)))
| ~ knows(n)
| ~ knows(X0)
| ~ knows(inverse(X0)) )
| ~ spl0_1
| ~ spl0_32 ),
inference(resolution,[],[f1036,f536]) ).
fof(f1046,plain,
( ! [X0] :
( knows(symmetric_encrypt(secret,kgen(X0)))
| ~ knows(X0)
| ~ knows(inverse(X0)) )
| ~ spl0_1
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1042,f86]) ).
fof(f1051,plain,
( ! [X0] :
( ~ knows(X0)
| ~ knows(inverse(X0))
| knows(secret)
| ~ knows(kgen(X0)) )
| ~ spl0_1
| ~ spl0_32 ),
inference(resolution,[],[f1046,f37]) ).
fof(f1052,plain,
( ! [X0] :
( ~ knows(X0)
| ~ knows(inverse(X0))
| knows(secret) )
| ~ spl0_1
| ~ spl0_30
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1051,f493]) ).
fof(f1053,plain,
( ! [X0] :
( ~ knows(X0)
| ~ knows(inverse(X0)) )
| ~ spl0_1
| ~ spl0_30
| ~ spl0_32 ),
inference(forward_subsumption_resolution,[],[f1052,f67]) ).
fof(f1054,plain,
( spl0_9
| ~ spl0_1
| ~ spl0_30
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f1053,f535,f492,f122,f226]) ).
cnf(s13,plain,
~ spl0_2,
inference(sat_conversion,[],[f167]) ).
cnf(s18,plain,
( spl0_2
| ~ spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f228]) ).
cnf(s28,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f321]) ).
cnf(s29,plain,
( ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f329]) ).
cnf(s32,plain,
( ~ spl0_1
| spl0_20 ),
inference(sat_conversion,[],[f332]) ).
cnf(s34,plain,
~ spl0_9,
inference(sat_conversion,[],[f351]) ).
cnf(s38,plain,
( spl0_2
| spl0_8
| ~ spl0_19 ),
inference(sat_conversion,[],[f396]) ).
cnf(s41,plain,
( spl0_2
| ~ spl0_21
| spl0_25 ),
inference(sat_conversion,[],[f418]) ).
cnf(s48,plain,
( spl0_19
| ~ spl0_21
| ~ spl0_25
| spl0_30 ),
inference(sat_conversion,[],[f494]) ).
cnf(s50,plain,
( spl0_19
| ~ spl0_21
| spl0_32 ),
inference(sat_conversion,[],[f537]) ).
cnf(s105,plain,
( ~ spl0_1
| spl0_9
| ~ spl0_30
| ~ spl0_32 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s106,plain,
( spl0_2
| ~ spl0_8 ),
inference(rat,[],[s18,s34]) ).
cnf(s112,plain,
spl0_1,
inference(rat,[],[s28,s13]) ).
cnf(s114,plain,
~ spl0_8,
inference(rat,[],[s106,s13]) ).
cnf(s117,plain,
spl0_20,
inference(rat,[],[s32,s112]) ).
cnf(s118,plain,
~ spl0_19,
inference(rat,[],[s38,s13,s114]) ).
cnf(s123,plain,
spl0_21,
inference(rat,[],[s29,s117]) ).
cnf(s136,plain,
spl0_32,
inference(rat,[],[s50,s118,s123]) ).
cnf(s137,plain,
spl0_25,
inference(rat,[],[s41,s13,s123]) ).
cnf(s145,plain,
~ spl0_30,
inference(rat,[],[s105,s112,s34,s136]) ).
cnf(s147,plain,
$false,
inference(rat,[],[s48,s123,s118,s145,s137]) ).
fof(f1055,plain,
$false,
inference(avatar_sat_refutation,[],[s147]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV233+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 10:14:19 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.27 % (3906290)Will run a generic schedule for satisfiability detection.
% 0.18/0.27 % (3906298)dis+10_1_sil=32000:sp=arity:random_seed=4044000744:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.27 % (3906296)% WARNING: option uhcvi not known.
% 0.18/0.27 % (3906295)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3859842359_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.27 % (3906296)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=948558996:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.27 % (3906299)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1616586229:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.27 % (3906297)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1820999911:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.27 % (3906300)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3337744721:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.27 % (3906301)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3555539954:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.27 % TRYING [1]
% 0.18/0.27 % TRYING [2]
% 0.18/0.27 % TRYING [3]
% 0.18/0.27 % TRYING [4]
% 0.18/0.27 % (3906298) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3906290-3906298"...
% 0.18/0.27 % (3906296) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3906290-3906296"...
% 0.18/0.27 % (3906298)...printing done.
% 0.18/0.27 % (3906298)Refutation found. Thanks to Tanya!
% 0.18/0.27 % SZS status Theorem for theBenchmark
% 0.18/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.27 % (3906298)------------------------------
% 0.18/0.27 % (3906298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.27 % (3906298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.27 % (3906298)CaDiCaL version: 2.1.3
% 0.18/0.27 % (3906298)Termination reason: Refutation
% 0.18/0.27 % (3906298)Time elapsed: 0.021 s
% 0.18/0.27 % (3906298)Peak memory usage: 13 MB
% 0.18/0.27 % (3906298)Instructions burned: 56 (million)
% 0.18/0.27 % (3906290)Success in time 0.052 s
% 0.18/0.27 % Vampire exiting
%------------------------------------------------------------------------------