%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV235+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 12:26:15 EST 2010
% Result : Theorem 0.48s
% Output : CNFRefutation 0.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 14
% Syntax : Number of formulae : 63 ( 29 unt; 0 def)
% Number of atoms : 136 ( 10 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 136 ( 63 ~; 61 |; 7 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 77 ( 1 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
p(a),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',an_account_number) ).
fof(6,axiom,
! [X1,X2] :
( ( p(crypt(X1,X2))
& p(X1) )
=> p(X2) ),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',decrypt_knowledge) ).
fof(10,axiom,
p(pin),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',initial_knowledge_of_intruder_5) ).
fof(11,axiom,
! [X8,X9] :
( ( p(X8)
& p(X9) )
=> p(crypt(xor(km,xor(kp,X9)),X8)) ),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',key_part_import___part_1) ).
fof(13,axiom,
! [X5,X9,X10] :
( ( p(X5)
& p(crypt(xor(km,xor(X9,kp)),X10))
& p(X9) )
=> p(crypt(xor(km,X9),xor(X10,X5))) ),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',key_part_import___part_3) ).
fof(15,axiom,
p(crypt(xor(km,imp),rand)),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',initial_knowledge_of_intruder_8) ).
fof(16,axiom,
! [X1,X2] : xor(X1,X2) = xor(X2,X1),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',xor_commutative) ).
fof(18,conjecture,
p(crypt(pp,a)),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',find_pin) ).
fof(20,axiom,
p(crypt(xor(km,pin),pp)),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',initial_knowledge_of_intruder_6) ).
fof(21,axiom,
! [X1] : xor(X1,id) = X1,
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',xor_rules_1) ).
fof(23,axiom,
! [X1] : xor(X1,X1) = id,
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',xor_rules_2) ).
fof(24,axiom,
p(exp),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',initial_knowledge_of_intruder_11) ).
fof(28,axiom,
! [X1,X2] :
( ( p(X2)
& p(X1) )
=> p(crypt(X1,X2)) ),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',encrypt_knowledge) ).
fof(29,axiom,
! [X9,X5,X3] :
( ( p(crypt(xor(km,X9),X5))
& p(X9)
& p(crypt(xor(km,exp),X3)) )
=> p(crypt(xor(X3,X9),X5)) ),
file('/tmp/tmpxQCInf/sel_SWV235+1.p_1',key_export) ).
fof(30,negated_conjecture,
~ p(crypt(pp,a)),
inference(assume_negation,[status(cth)],[18]) ).
fof(31,negated_conjecture,
~ p(crypt(pp,a)),
inference(fof_simplification,[status(thm)],[30,theory(equality)]) ).
cnf(34,plain,
p(a),
inference(split_conjunct,[status(thm)],[2]) ).
fof(44,plain,
! [X1,X2] :
( ~ p(crypt(X1,X2))
| ~ p(X1)
| p(X2) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(45,plain,
! [X3,X4] :
( ~ p(crypt(X3,X4))
| ~ p(X3)
| p(X4) ),
inference(variable_rename,[status(thm)],[44]) ).
cnf(46,plain,
( p(X1)
| ~ p(X2)
| ~ p(crypt(X2,X1)) ),
inference(split_conjunct,[status(thm)],[45]) ).
cnf(50,plain,
p(pin),
inference(split_conjunct,[status(thm)],[10]) ).
fof(51,plain,
! [X8,X9] :
( ~ p(X8)
| ~ p(X9)
| p(crypt(xor(km,xor(kp,X9)),X8)) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(52,plain,
! [X10,X11] :
( ~ p(X10)
| ~ p(X11)
| p(crypt(xor(km,xor(kp,X11)),X10)) ),
inference(variable_rename,[status(thm)],[51]) ).
cnf(53,plain,
( p(crypt(xor(km,xor(kp,X1)),X2))
| ~ p(X1)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[52]) ).
fof(57,plain,
! [X5,X9,X10] :
( ~ p(X5)
| ~ p(crypt(xor(km,xor(X9,kp)),X10))
| ~ p(X9)
| p(crypt(xor(km,X9),xor(X10,X5))) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(58,plain,
! [X11,X12,X13] :
( ~ p(X11)
| ~ p(crypt(xor(km,xor(X12,kp)),X13))
| ~ p(X12)
| p(crypt(xor(km,X12),xor(X13,X11))) ),
inference(variable_rename,[status(thm)],[57]) ).
cnf(59,plain,
( p(crypt(xor(km,X1),xor(X2,X3)))
| ~ p(X1)
| ~ p(crypt(xor(km,xor(X1,kp)),X2))
| ~ p(X3) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(62,plain,
p(crypt(xor(km,imp),rand)),
inference(split_conjunct,[status(thm)],[15]) ).
fof(63,plain,
! [X3,X4] : xor(X3,X4) = xor(X4,X3),
inference(variable_rename,[status(thm)],[16]) ).
cnf(64,plain,
xor(X1,X2) = xor(X2,X1),
inference(split_conjunct,[status(thm)],[63]) ).
cnf(66,negated_conjecture,
~ p(crypt(pp,a)),
inference(split_conjunct,[status(thm)],[31]) ).
cnf(68,plain,
p(crypt(xor(km,pin),pp)),
inference(split_conjunct,[status(thm)],[20]) ).
fof(69,plain,
! [X2] : xor(X2,id) = X2,
inference(variable_rename,[status(thm)],[21]) ).
cnf(70,plain,
xor(X1,id) = X1,
inference(split_conjunct,[status(thm)],[69]) ).
fof(72,plain,
! [X2] : xor(X2,X2) = id,
inference(variable_rename,[status(thm)],[23]) ).
cnf(73,plain,
xor(X1,X1) = id,
inference(split_conjunct,[status(thm)],[72]) ).
cnf(74,plain,
p(exp),
inference(split_conjunct,[status(thm)],[24]) ).
fof(82,plain,
! [X1,X2] :
( ~ p(X2)
| ~ p(X1)
| p(crypt(X1,X2)) ),
inference(fof_nnf,[status(thm)],[28]) ).
fof(83,plain,
! [X3,X4] :
( ~ p(X4)
| ~ p(X3)
| p(crypt(X3,X4)) ),
inference(variable_rename,[status(thm)],[82]) ).
cnf(84,plain,
( p(crypt(X1,X2))
| ~ p(X1)
| ~ p(X2) ),
inference(split_conjunct,[status(thm)],[83]) ).
fof(85,plain,
! [X9,X5,X3] :
( ~ p(crypt(xor(km,X9),X5))
| ~ p(X9)
| ~ p(crypt(xor(km,exp),X3))
| p(crypt(xor(X3,X9),X5)) ),
inference(fof_nnf,[status(thm)],[29]) ).
fof(86,plain,
! [X10,X11,X12] :
( ~ p(crypt(xor(km,X10),X11))
| ~ p(X10)
| ~ p(crypt(xor(km,exp),X12))
| p(crypt(xor(X12,X10),X11)) ),
inference(variable_rename,[status(thm)],[85]) ).
cnf(87,plain,
( p(crypt(xor(X1,X2),X3))
| ~ p(crypt(xor(km,exp),X1))
| ~ p(X2)
| ~ p(crypt(xor(km,X2),X3)) ),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(88,negated_conjecture,
( ~ p(a)
| ~ p(pp) ),
inference(spm,[status(thm)],[66,84,theory(equality)]) ).
cnf(90,negated_conjecture,
( $false
| ~ p(pp) ),
inference(rw,[status(thm)],[88,34,theory(equality)]) ).
cnf(91,negated_conjecture,
~ p(pp),
inference(cn,[status(thm)],[90,theory(equality)]) ).
cnf(100,plain,
xor(id,X1) = X1,
inference(spm,[status(thm)],[70,64,theory(equality)]) ).
cnf(129,plain,
( p(crypt(xor(km,xor(X1,kp)),X2))
| ~ p(X2)
| ~ p(X1) ),
inference(spm,[status(thm)],[53,64,theory(equality)]) ).
cnf(649,plain,
( p(crypt(xor(km,X1),xor(X2,X3)))
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ),
inference(spm,[status(thm)],[59,129,theory(equality)]) ).
cnf(6226,plain,
( p(crypt(xor(km,X1),id))
| ~ p(X2)
| ~ p(X1) ),
inference(spm,[status(thm)],[649,73,theory(equality)]) ).
cnf(6331,plain,
( p(crypt(xor(km,X1),id))
| ~ p(X1) ),
inference(spm,[status(thm)],[6226,62,theory(equality)]) ).
cnf(6518,plain,
( p(crypt(xor(id,X1),X2))
| ~ p(crypt(xor(km,X1),X2))
| ~ p(X1)
| ~ p(exp) ),
inference(spm,[status(thm)],[87,6331,theory(equality)]) ).
cnf(6553,plain,
( p(crypt(X1,X2))
| ~ p(crypt(xor(km,X1),X2))
| ~ p(X1)
| ~ p(exp) ),
inference(rw,[status(thm)],[6518,100,theory(equality)]) ).
cnf(6554,plain,
( p(crypt(X1,X2))
| ~ p(crypt(xor(km,X1),X2))
| ~ p(X1)
| $false ),
inference(rw,[status(thm)],[6553,74,theory(equality)]) ).
cnf(6555,plain,
( p(crypt(X1,X2))
| ~ p(crypt(xor(km,X1),X2))
| ~ p(X1) ),
inference(cn,[status(thm)],[6554,theory(equality)]) ).
cnf(7014,plain,
( p(crypt(pin,pp))
| ~ p(pin) ),
inference(spm,[status(thm)],[6555,68,theory(equality)]) ).
cnf(7049,plain,
( p(crypt(pin,pp))
| $false ),
inference(rw,[status(thm)],[7014,50,theory(equality)]) ).
cnf(7050,plain,
p(crypt(pin,pp)),
inference(cn,[status(thm)],[7049,theory(equality)]) ).
cnf(7103,plain,
( p(pp)
| ~ p(pin) ),
inference(spm,[status(thm)],[46,7050,theory(equality)]) ).
cnf(7105,plain,
( p(pp)
| $false ),
inference(rw,[status(thm)],[7103,50,theory(equality)]) ).
cnf(7106,plain,
p(pp),
inference(cn,[status(thm)],[7105,theory(equality)]) ).
cnf(7107,plain,
$false,
inference(sr,[status(thm)],[7106,91,theory(equality)]) ).
cnf(7108,plain,
$false,
7107,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV235+1.p
% --creating new selector for []
% -running prover on /tmp/tmpxQCInf/sel_SWV235+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWV235+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV235+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV235+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------