%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWV235+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Thu Dec 30 08:51:58 EST 2010
% Result : Theorem 1.28s
% Output : Solution 1.28s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP19364/SWV235+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP19364/SWV235+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP19364/SWV235+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 19496
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.012 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:((p(crypt(X1,X2))&p(X1))=>p(X2)),file('/tmp/SRASS.s.p', decrypt_knowledge)).
% fof(2, axiom,![X1]:![X2]:((p(X2)&p(X1))=>p(crypt(X1,X2))),file('/tmp/SRASS.s.p', encrypt_knowledge)).
% fof(3, axiom,p(a),file('/tmp/SRASS.s.p', an_account_number)).
% fof(4, axiom,p(pin),file('/tmp/SRASS.s.p', initial_knowledge_of_intruder_5)).
% fof(5, axiom,p(crypt(xor(km,pin),pp)),file('/tmp/SRASS.s.p', initial_knowledge_of_intruder_6)).
% fof(6, axiom,![X3]:![X4]:((p(X3)&p(X4))=>p(crypt(xor(km,xor(kp,X4)),X3))),file('/tmp/SRASS.s.p', key_part_import___part_1)).
% fof(7, axiom,![X5]:![X4]:![X6]:(((p(X5)&p(crypt(xor(km,xor(kp,X4)),X6)))&p(X4))=>p(crypt(xor(km,xor(X4,kp)),xor(X5,X6)))),file('/tmp/SRASS.s.p', key_part_import___part_2)).
% fof(9, axiom,![X1]:![X2]:((p(X1)&p(X2))=>p(xor(X1,X2))),file('/tmp/SRASS.s.p', combine_with_XOR)).
% fof(10, axiom,p(kp),file('/tmp/SRASS.s.p', initial_knowledge_of_intruder_1)).
% fof(13, axiom,p(exp),file('/tmp/SRASS.s.p', initial_knowledge_of_intruder_11)).
% fof(14, axiom,![X4]:![X5]:![X7]:(((p(crypt(xor(km,X4),X5))&p(X4))&p(crypt(xor(km,exp),X7)))=>p(crypt(xor(X7,X4),X5))),file('/tmp/SRASS.s.p', key_export)).
% fof(24, axiom,p(id),file('/tmp/SRASS.s.p', initial_knowledge_of_intruder_4)).
% fof(25, axiom,![X1]:![X2]:xor(X1,X2)=xor(X2,X1),file('/tmp/SRASS.s.p', xor_commutative)).
% fof(26, axiom,![X1]:![X2]:![X11]:xor(X1,xor(X2,X11))=xor(xor(X1,X2),X11),file('/tmp/SRASS.s.p', xor_associative)).
% fof(27, axiom,![X1]:xor(X1,id)=X1,file('/tmp/SRASS.s.p', xor_rules_1)).
% fof(28, axiom,![X1]:xor(X1,X1)=id,file('/tmp/SRASS.s.p', xor_rules_2)).
% fof(29, conjecture,p(crypt(pp,a)),file('/tmp/SRASS.s.p', find_pin)).
% fof(30, negated_conjecture,~(p(crypt(pp,a))),inference(assume_negation,[status(cth)],[29])).
% fof(31, negated_conjecture,~(p(crypt(pp,a))),inference(fof_simplification,[status(thm)],[30,theory(equality)])).
% fof(32, plain,![X1]:![X2]:((~(p(crypt(X1,X2)))|~(p(X1)))|p(X2)),inference(fof_nnf,[status(thm)],[1])).
% fof(33, plain,![X3]:![X4]:((~(p(crypt(X3,X4)))|~(p(X3)))|p(X4)),inference(variable_rename,[status(thm)],[32])).
% cnf(34,plain,(p(X1)|~p(X2)|~p(crypt(X2,X1))),inference(split_conjunct,[status(thm)],[33])).
% fof(35, plain,![X1]:![X2]:((~(p(X2))|~(p(X1)))|p(crypt(X1,X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(36, plain,![X3]:![X4]:((~(p(X4))|~(p(X3)))|p(crypt(X3,X4))),inference(variable_rename,[status(thm)],[35])).
% cnf(37,plain,(p(crypt(X1,X2))|~p(X1)|~p(X2)),inference(split_conjunct,[status(thm)],[36])).
% cnf(38,plain,(p(a)),inference(split_conjunct,[status(thm)],[3])).
% cnf(39,plain,(p(pin)),inference(split_conjunct,[status(thm)],[4])).
% cnf(40,plain,(p(crypt(xor(km,pin),pp))),inference(split_conjunct,[status(thm)],[5])).
% fof(41, plain,![X3]:![X4]:((~(p(X3))|~(p(X4)))|p(crypt(xor(km,xor(kp,X4)),X3))),inference(fof_nnf,[status(thm)],[6])).
% fof(42, plain,![X5]:![X6]:((~(p(X5))|~(p(X6)))|p(crypt(xor(km,xor(kp,X6)),X5))),inference(variable_rename,[status(thm)],[41])).
% cnf(43,plain,(p(crypt(xor(km,xor(kp,X1)),X2))|~p(X1)|~p(X2)),inference(split_conjunct,[status(thm)],[42])).
% fof(44, plain,![X5]:![X4]:![X6]:(((~(p(X5))|~(p(crypt(xor(km,xor(kp,X4)),X6))))|~(p(X4)))|p(crypt(xor(km,xor(X4,kp)),xor(X5,X6)))),inference(fof_nnf,[status(thm)],[7])).
% fof(45, plain,![X7]:![X8]:![X9]:(((~(p(X7))|~(p(crypt(xor(km,xor(kp,X8)),X9))))|~(p(X8)))|p(crypt(xor(km,xor(X8,kp)),xor(X7,X9)))),inference(variable_rename,[status(thm)],[44])).
% cnf(46,plain,(p(crypt(xor(km,xor(X1,kp)),xor(X2,X3)))|~p(X1)|~p(crypt(xor(km,xor(kp,X1)),X3))|~p(X2)),inference(split_conjunct,[status(thm)],[45])).
% fof(50, plain,![X1]:![X2]:((~(p(X1))|~(p(X2)))|p(xor(X1,X2))),inference(fof_nnf,[status(thm)],[9])).
% fof(51, plain,![X3]:![X4]:((~(p(X3))|~(p(X4)))|p(xor(X3,X4))),inference(variable_rename,[status(thm)],[50])).
% cnf(52,plain,(p(xor(X1,X2))|~p(X2)|~p(X1)),inference(split_conjunct,[status(thm)],[51])).
% cnf(53,plain,(p(kp)),inference(split_conjunct,[status(thm)],[10])).
% cnf(56,plain,(p(exp)),inference(split_conjunct,[status(thm)],[13])).
% fof(57, plain,![X4]:![X5]:![X7]:(((~(p(crypt(xor(km,X4),X5)))|~(p(X4)))|~(p(crypt(xor(km,exp),X7))))|p(crypt(xor(X7,X4),X5))),inference(fof_nnf,[status(thm)],[14])).
% fof(58, plain,![X8]:![X9]:![X10]:(((~(p(crypt(xor(km,X8),X9)))|~(p(X8)))|~(p(crypt(xor(km,exp),X10))))|p(crypt(xor(X10,X8),X9))),inference(variable_rename,[status(thm)],[57])).
% cnf(59,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)],[58])).
% cnf(78,plain,(p(id)),inference(split_conjunct,[status(thm)],[24])).
% fof(79, plain,![X3]:![X4]:xor(X3,X4)=xor(X4,X3),inference(variable_rename,[status(thm)],[25])).
% cnf(80,plain,(xor(X1,X2)=xor(X2,X1)),inference(split_conjunct,[status(thm)],[79])).
% fof(81, plain,![X12]:![X13]:![X14]:xor(X12,xor(X13,X14))=xor(xor(X12,X13),X14),inference(variable_rename,[status(thm)],[26])).
% cnf(82,plain,(xor(X1,xor(X2,X3))=xor(xor(X1,X2),X3)),inference(split_conjunct,[status(thm)],[81])).
% fof(83, plain,![X2]:xor(X2,id)=X2,inference(variable_rename,[status(thm)],[27])).
% cnf(84,plain,(xor(X1,id)=X1),inference(split_conjunct,[status(thm)],[83])).
% fof(85, plain,![X2]:xor(X2,X2)=id,inference(variable_rename,[status(thm)],[28])).
% cnf(86,plain,(xor(X1,X1)=id),inference(split_conjunct,[status(thm)],[85])).
% cnf(87,negated_conjecture,(~p(crypt(pp,a))),inference(split_conjunct,[status(thm)],[31])).
% cnf(89,negated_conjecture,(~p(a)|~p(pp)),inference(spm,[status(thm)],[87,37,theory(equality)])).
% cnf(90,negated_conjecture,($false|~p(pp)),inference(rw,[status(thm)],[89,38,theory(equality)])).
% cnf(91,negated_conjecture,(~p(pp)),inference(cn,[status(thm)],[90,theory(equality)])).
% cnf(96,plain,(xor(id,X1)=X1),inference(spm,[status(thm)],[84,80,theory(equality)])).
% cnf(110,plain,(xor(X1,xor(X2,xor(X1,X2)))=id),inference(spm,[status(thm)],[86,82,theory(equality)])).
% cnf(111,plain,(xor(X1,xor(X2,X3))=xor(X3,xor(X1,X2))),inference(spm,[status(thm)],[80,82,theory(equality)])).
% cnf(116,plain,(xor(id,X2)=xor(X1,xor(X1,X2))),inference(spm,[status(thm)],[82,86,theory(equality)])).
% cnf(117,plain,(xor(xor(X2,X1),X3)=xor(X1,xor(X2,X3))),inference(spm,[status(thm)],[82,80,theory(equality)])).
% cnf(122,plain,(xor(X2,xor(X1,X3))=xor(X1,xor(X2,X3))),inference(rw,[status(thm)],[117,82,theory(equality)])).
% cnf(157,plain,(p(crypt(xor(km,xor(X1,kp)),id))|~p(crypt(xor(km,xor(kp,X1)),X2))|~p(X2)|~p(X1)),inference(spm,[status(thm)],[46,86,theory(equality)])).
% cnf(284,plain,(xor(X1,xor(X1,X2))=X2),inference(rw,[status(thm)],[116,96,theory(equality)])).
% cnf(304,plain,(xor(X1,id)=xor(X2,xor(X1,X2))),inference(spm,[status(thm)],[284,110,theory(equality)])).
% cnf(318,plain,(X1=xor(X2,xor(X1,X2))),inference(rw,[status(thm)],[304,84,theory(equality)])).
% cnf(413,plain,(p(xor(X3,xor(X1,X2)))|~p(xor(X2,X3))|~p(X1)),inference(spm,[status(thm)],[52,111,theory(equality)])).
% cnf(1774,plain,(p(crypt(xor(km,xor(X1,kp)),id))|~p(X2)|~p(X1)),inference(csr,[status(thm)],[157,43])).
% cnf(1775,plain,(p(crypt(xor(km,xor(X1,kp)),id))|~p(X1)),inference(spm,[status(thm)],[1774,78,theory(equality)])).
% cnf(2818,plain,(p(crypt(xor(km,xor(kp,X1)),id))|~p(X1)),inference(spm,[status(thm)],[1775,80,theory(equality)])).
% cnf(3283,plain,(p(crypt(xor(km,X1),id))|~p(xor(kp,X1))),inference(spm,[status(thm)],[2818,284,theory(equality)])).
% cnf(3327,plain,(p(crypt(X1,id))|~p(xor(kp,xor(km,X1)))),inference(spm,[status(thm)],[3283,284,theory(equality)])).
% cnf(3753,plain,(p(crypt(X1,id))|~p(xor(km,xor(kp,X1)))),inference(rw,[status(thm)],[3327,122,theory(equality)])).
% cnf(3772,plain,(p(crypt(X1,id))|~p(xor(X1,km))|~p(kp)),inference(spm,[status(thm)],[3753,413,theory(equality)])).
% cnf(3779,plain,(p(crypt(X1,id))|~p(xor(X1,km))|$false),inference(rw,[status(thm)],[3772,53,theory(equality)])).
% cnf(3780,plain,(p(crypt(X1,id))|~p(xor(X1,km))),inference(cn,[status(thm)],[3779,theory(equality)])).
% cnf(3856,plain,(p(crypt(xor(id,X1),X2))|~p(crypt(xor(km,X1),X2))|~p(X1)|~p(xor(xor(km,exp),km))),inference(spm,[status(thm)],[59,3780,theory(equality)])).
% cnf(3876,plain,(p(crypt(X1,X2))|~p(crypt(xor(km,X1),X2))|~p(X1)|~p(xor(xor(km,exp),km))),inference(rw,[status(thm)],[3856,96,theory(equality)])).
% cnf(3877,plain,(p(crypt(X1,X2))|~p(crypt(xor(km,X1),X2))|~p(X1)|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[3876,82,theory(equality)]),318,theory(equality)]),56,theory(equality)])).
% cnf(3878,plain,(p(crypt(X1,X2))|~p(crypt(xor(km,X1),X2))|~p(X1)),inference(cn,[status(thm)],[3877,theory(equality)])).
% cnf(4213,plain,(p(crypt(pin,pp))|~p(pin)),inference(spm,[status(thm)],[3878,40,theory(equality)])).
% cnf(4268,plain,(p(crypt(pin,pp))|$false),inference(rw,[status(thm)],[4213,39,theory(equality)])).
% cnf(4269,plain,(p(crypt(pin,pp))),inference(cn,[status(thm)],[4268,theory(equality)])).
% cnf(4292,plain,(p(pp)|~p(pin)),inference(spm,[status(thm)],[34,4269,theory(equality)])).
% cnf(4293,plain,(p(pp)|$false),inference(rw,[status(thm)],[4292,39,theory(equality)])).
% cnf(4294,plain,(p(pp)),inference(cn,[status(thm)],[4293,theory(equality)])).
% cnf(4295,plain,($false),inference(sr,[status(thm)],[4294,91,theory(equality)])).
% cnf(4296,plain,($false),4295,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 536
% # ...of these trivial : 10
% # ...subsumed : 330
% # ...remaining for further processing: 196
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 7
% # Backward-rewritten : 4
% # Generated clauses : 2669
% # ...of the previous two non-trivial : 2398
% # Contextual simplify-reflections : 41
% # Paramodulations : 2669
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 156
% # Positive orientable unit clauses: 25
% # Positive unorientable unit clauses: 3
% # Negative unit clauses : 5
% # Non-unit-clauses : 123
% # Current number of unprocessed clauses: 1690
% # ...number of literals in the above : 7342
% # Clause-clause subsumption calls (NU) : 5228
% # Rec. Clause-clause subsumption calls : 2947
% # Unit Clause-clause subsumption calls : 35
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 76
% # Indexed BW rewrite successes : 52
% # Backwards rewriting index: 172 leaves, 1.91+/-2.815 terms/leaf
% # Paramod-from index: 47 leaves, 1.89+/-2.262 terms/leaf
% # Paramod-into index: 153 leaves, 1.67+/-2.016 terms/leaf
% # -------------------------------------------------
% # User time : 0.105 s
% # System time : 0.006 s
% # Total time : 0.111 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.25 CPU 0.33 WC
% FINAL PrfWatch: 0.25 CPU 0.33 WC
% SZS output end Solution for /tmp/SystemOnTPTP19364/SWV235+1.tptp
%
%------------------------------------------------------------------------------