%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWV234+2 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art07.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:10 EST 2010
% Result : Theorem 0.29s
% Output : CNFRefutation 0.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 12
% Syntax : Number of formulae : 59 ( 42 unt; 0 def)
% Number of atoms : 95 ( 23 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 34 ~; 31 |; 3 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 89 ( 12 sgn 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
public(enc(xor(km,imp),xor(kek,xor(pin,data)))),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',initial_knowledge9) ).
fof(3,axiom,
public(a),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',initial_knowledge8) ).
fof(4,axiom,
public(enc(xor(kek,pin),pp)),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',initial_knowledge5) ).
fof(11,conjecture,
public(enc(pp,a)),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',co1) ).
fof(12,axiom,
! [X1,X2,X3] :
( ( public(X2)
& public(enc(xor(X1,X2),X3))
& public(enc(xor(km,imp),X1)) )
=> public(enc(xor(km,X2),X3)) ),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',key_import_cmd) ).
fof(13,axiom,
! [X1,X2,X3] : enc(X1,enc(inv(X1),X2)) = X2,
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',encrypt_decrypt_cancel) ).
fof(14,axiom,
! [X1,X2,X3] : xor(X1,X2) = xor(X2,X1),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',xor_commutes) ).
fof(18,axiom,
public(data),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',initial_knowledge2) ).
fof(19,axiom,
! [X1,X2,X3] : xor(X1,X1) = z,
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',xor_self_cancel) ).
fof(20,axiom,
! [X1,X2,X3] : xor(X1,xor(X2,X3)) = xor(xor(X1,X2),X3),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',xor_assosciative) ).
fof(21,axiom,
! [X1,X2] :
( ( public(X1)
& public(X2) )
=> public(enc(enc(inv(xor(data,km)),X1),X2)) ),
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',encrypt_data_cmd) ).
fof(22,axiom,
! [X1,X2,X3] : xor(X1,z) = X1,
file('/tmp/tmpasfskD/sel_SWV234+2.p_1',xor_zero) ).
fof(23,negated_conjecture,
~ public(enc(pp,a)),
inference(assume_negation,[status(cth)],[11]) ).
fof(24,negated_conjecture,
~ public(enc(pp,a)),
inference(fof_simplification,[status(thm)],[23,theory(equality)]) ).
cnf(28,plain,
public(enc(xor(km,imp),xor(kek,xor(pin,data)))),
inference(split_conjunct,[status(thm)],[2]) ).
cnf(29,plain,
public(a),
inference(split_conjunct,[status(thm)],[3]) ).
cnf(30,plain,
public(enc(xor(kek,pin),pp)),
inference(split_conjunct,[status(thm)],[4]) ).
cnf(39,negated_conjecture,
~ public(enc(pp,a)),
inference(split_conjunct,[status(thm)],[24]) ).
fof(40,plain,
! [X1,X2,X3] :
( ~ public(X2)
| ~ public(enc(xor(X1,X2),X3))
| ~ public(enc(xor(km,imp),X1))
| public(enc(xor(km,X2),X3)) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(41,plain,
! [X4,X5,X6] :
( ~ public(X5)
| ~ public(enc(xor(X4,X5),X6))
| ~ public(enc(xor(km,imp),X4))
| public(enc(xor(km,X5),X6)) ),
inference(variable_rename,[status(thm)],[40]) ).
cnf(42,plain,
( public(enc(xor(km,X1),X2))
| ~ public(enc(xor(km,imp),X3))
| ~ public(enc(xor(X3,X1),X2))
| ~ public(X1) ),
inference(split_conjunct,[status(thm)],[41]) ).
fof(43,plain,
! [X4,X5,X6] : enc(X4,enc(inv(X4),X5)) = X5,
inference(variable_rename,[status(thm)],[13]) ).
cnf(44,plain,
enc(X1,enc(inv(X1),X2)) = X2,
inference(split_conjunct,[status(thm)],[43]) ).
fof(45,plain,
! [X4,X5,X6] : xor(X4,X5) = xor(X5,X4),
inference(variable_rename,[status(thm)],[14]) ).
cnf(46,plain,
xor(X1,X2) = xor(X2,X1),
inference(split_conjunct,[status(thm)],[45]) ).
cnf(56,plain,
public(data),
inference(split_conjunct,[status(thm)],[18]) ).
fof(57,plain,
! [X4,X5,X6] : xor(X4,X4) = z,
inference(variable_rename,[status(thm)],[19]) ).
cnf(58,plain,
xor(X1,X1) = z,
inference(split_conjunct,[status(thm)],[57]) ).
fof(59,plain,
! [X4,X5,X6] : xor(X4,xor(X5,X6)) = xor(xor(X4,X5),X6),
inference(variable_rename,[status(thm)],[20]) ).
cnf(60,plain,
xor(X1,xor(X2,X3)) = xor(xor(X1,X2),X3),
inference(split_conjunct,[status(thm)],[59]) ).
fof(61,plain,
! [X1,X2] :
( ~ public(X1)
| ~ public(X2)
| public(enc(enc(inv(xor(data,km)),X1),X2)) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(62,plain,
! [X3,X4] :
( ~ public(X3)
| ~ public(X4)
| public(enc(enc(inv(xor(data,km)),X3),X4)) ),
inference(variable_rename,[status(thm)],[61]) ).
cnf(63,plain,
( public(enc(enc(inv(xor(data,km)),X1),X2))
| ~ public(X2)
| ~ public(X1) ),
inference(split_conjunct,[status(thm)],[62]) ).
fof(64,plain,
! [X4,X5,X6] : xor(X4,z) = X4,
inference(variable_rename,[status(thm)],[22]) ).
cnf(65,plain,
xor(X1,z) = X1,
inference(split_conjunct,[status(thm)],[64]) ).
cnf(74,plain,
xor(z,X1) = X1,
inference(spm,[status(thm)],[65,46,theory(equality)]) ).
cnf(82,plain,
public(enc(xor(pin,kek),pp)),
inference(rw,[status(thm)],[30,46,theory(equality)]) ).
cnf(83,plain,
enc(X1,X2) = enc(inv(inv(X1)),X2),
inference(spm,[status(thm)],[44,44,theory(equality)]) ).
cnf(88,plain,
xor(X1,xor(X2,xor(X1,X2))) = z,
inference(spm,[status(thm)],[58,60,theory(equality)]) ).
cnf(89,plain,
xor(z,X2) = xor(X1,xor(X1,X2)),
inference(spm,[status(thm)],[60,58,theory(equality)]) ).
cnf(91,plain,
xor(X1,xor(X2,X3)) = xor(X3,xor(X1,X2)),
inference(spm,[status(thm)],[46,60,theory(equality)]) ).
cnf(101,plain,
( public(enc(enc(inv(xor(km,data)),X1),X2))
| ~ public(X2)
| ~ public(X1) ),
inference(rw,[status(thm)],[63,46,theory(equality)]) ).
cnf(102,plain,
( public(enc(X1,X2))
| ~ public(X2)
| ~ public(enc(inv(inv(xor(km,data))),X1)) ),
inference(spm,[status(thm)],[101,44,theory(equality)]) ).
cnf(191,plain,
xor(X1,xor(X1,X2)) = X2,
inference(rw,[status(thm)],[89,74,theory(equality)]) ).
cnf(202,plain,
xor(X1,z) = xor(X2,xor(X1,X2)),
inference(spm,[status(thm)],[191,88,theory(equality)]) ).
cnf(216,plain,
X1 = xor(X2,xor(X1,X2)),
inference(rw,[status(thm)],[202,65,theory(equality)]) ).
cnf(323,plain,
public(enc(xor(km,imp),xor(pin,xor(data,kek)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[28,91,theory(equality)]),46,theory(equality)]),91,theory(equality)]),46,theory(equality)]) ).
cnf(360,plain,
( public(enc(xor(km,X1),X2))
| ~ public(enc(xor(xor(pin,xor(data,kek)),X1),X2))
| ~ public(X1) ),
inference(spm,[status(thm)],[42,323,theory(equality)]) ).
cnf(363,plain,
( public(enc(xor(km,X1),X2))
| ~ public(enc(xor(pin,xor(data,xor(kek,X1))),X2))
| ~ public(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[360,60,theory(equality)]),60,theory(equality)]) ).
cnf(534,plain,
( public(enc(X1,X2))
| ~ public(X2)
| ~ public(enc(xor(km,data),X1)) ),
inference(rw,[status(thm)],[102,83,theory(equality)]) ).
cnf(2097,plain,
( public(enc(xor(km,data),X1))
| ~ public(enc(xor(pin,kek),X1))
| ~ public(data) ),
inference(spm,[status(thm)],[363,216,theory(equality)]) ).
cnf(2119,plain,
( public(enc(xor(km,data),X1))
| ~ public(enc(xor(pin,kek),X1))
| $false ),
inference(rw,[status(thm)],[2097,56,theory(equality)]) ).
cnf(2120,plain,
( public(enc(xor(km,data),X1))
| ~ public(enc(xor(pin,kek),X1)) ),
inference(cn,[status(thm)],[2119,theory(equality)]) ).
cnf(2125,plain,
public(enc(xor(km,data),pp)),
inference(spm,[status(thm)],[2120,82,theory(equality)]) ).
cnf(2130,plain,
( public(enc(pp,X1))
| ~ public(X1) ),
inference(spm,[status(thm)],[534,2125,theory(equality)]) ).
cnf(2134,negated_conjecture,
~ public(a),
inference(spm,[status(thm)],[39,2130,theory(equality)]) ).
cnf(2137,negated_conjecture,
$false,
inference(rw,[status(thm)],[2134,29,theory(equality)]) ).
cnf(2138,negated_conjecture,
$false,
inference(cn,[status(thm)],[2137,theory(equality)]) ).
cnf(2139,negated_conjecture,
$false,
2138,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWV/SWV234+2.p
% --creating new selector for []
% -running prover on /tmp/tmpasfskD/sel_SWV234+2.p_1 with time limit 29
% -prover status Theorem
% Problem SWV234+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWV/SWV234+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWV/SWV234+2.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
%
%------------------------------------------------------------------------------