%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN982-1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:40:29 PM UTC 2026
% Result : Unsatisfiable 68.52s 14.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN982-1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n008.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:51:14 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 68.52/14.24 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24 Execution resolution_3 ended with status: unsatisfiable
% 68.52/14.24 Used heuristic: resolution_3
% 68.52/14.24
% 68.52/14.24 Input Clauses:
% 68.52/14.24
% 68.52/14.24 Predicates: ssNonce ssP ssBf ssTk ssBk ssSa ssAk ssIm ssM ssIk ssSb
% 68.52/14.24 Fol Constants: na t b a bt at
% 68.52/14.24 Fol Functions: nb tb kt key pair sent triple quadr encr
% 68.52/14.24 Problem Properties:
% 68.52/14.24 This is a full first-order problem without equality.
% 68.52/14.24
% 68.52/14.24 After reduction: Problem Properties:
% 68.52/14.24 This is a full first-order problem without equality.
% 68.52/14.24
% 68.52/14.24
% 68.52/14.24 Reduced Input Clauses:
% 68.52/14.24
% 68.52/14.24 Most General Atoms: ssIm(x3) ssP(x2) ssM(sent(x1,x2,x0)) ssIk(key(x1,x2)) ssBf(x1) ssSa(pair(x0,x1)) ssAk(key(x2,x0)) ssSb(pair(x0,x2)) ssBk(key(x1,x0)) ssTk(key(x6,x2)) ssNonce(x3)
% 68.52/14.24
% 68.52/14.24 === Starting SPASS-SCL-FOL A Little Less Naive, considering 39 atoms initially, heuristics mode: resolution_3 ===
% 68.52/14.24
% 68.52/14.24 === Backtracking. Learning clause 38:1:0:[20.1,16.1,14.1]:: -> ssIm(na)
% 68.52/14.24 === Backtracking. Learning clause 39:4:3:[29.2,25.3]:TopTopTop: ssIm(x0),ssIm(x2),ssP(x1) -> ssIm(encr(x0,x2))
% 68.52/14.24 === Backtracking. Learning clause 41:2:1:[4.0,40.2,37.1,25.3]:Top: ssBk(key(x0,a)),ssIm(x0) ->
% 68.52/14.24 === Backtracking. Learning clause 43:4:2:[4.0,42.3,30.1,27.4]:TopTop: ssBf(x0),ssIm(pair(x1,x0)),ssP(x1) -> ssSb(pair(x1,x0))
% 68.52/14.24 === Backtracking. Learning clause 44:1:0:[20.1,16.1]:: -> ssIm(pair(a,na))
% 68.52/14.24 === Backtracking. Learning clause 47:3:6:[2.0,45.1,5.0,46.2,27.4,32.1]:TopTopTopTopTopTop: ssIm(triple(encr(quadr(x0,x1,x2,x3),at),x4,x5)),ssSa(pair(x0,x1)) -> ssAk(key(x2,x0))
% 68.52/14.24 === Backtracking. Learning clause 48:3:2:[20.1,33.3]:TopTop: ssM(sent(x0,b,pair(x0,x1))),ssBf(x1) -> ssIm(triple(b,nb(x1),encr(triple(x0,x1,tb(x1)),bt)))
% 68.52/14.24 === Backtracking. Learning clause 50:4:3:[4.0,49.2,27.4,34.1]:TopTopTop: ssIm(pair(encr(triple(x0,x1,tb(x2)),bt),encr(nb(x2),x1))),ssP(x0),ssSb(pair(x0,x2)) -> ssBk(key(x1,x0))
% 68.52/14.24 === Backtracking. Learning clause 51:5:7:[20.1,36.5]:TopTopTopTopTopTopTop: ssM(sent(x0,t,triple(x0,x1,encr(triple(x2,x3,x4),x5)))),ssTk(key(x5,x0)),ssTk(key(x6,x2)),ssNonce(x3) -> ssIm(triple(encr(quadr(x0,x3,kt(x3),x4),x6),encr(triple(x2,kt(x3),x4),x5),x1))
% 68.52/14.24 === Backtracking. Learning clause 53:5:5:[10.0,52.2,36.5,32.1]:TopTopTopTopTop: ssM(sent(x0,t,triple(x0,x1,encr(triple(a,x2,x3),x4)))),ssTk(key(x4,x0)),ssNonce(x2),ssSa(pair(x0,x2)) -> ssAk(key(kt(x2),x0))
% 68.52/14.24 === Clause set with instances from active satisfied. Growing active. New size: 54
% 68.52/14.24 === Restarting.
% 68.52/14.24 === Backtracking. Learning clause 54:1:0:[15.1,44.1]:: -> ssIm(a)
% 68.52/14.24 === Backtracking. Learning clause 55:3:4:[28.4,47.1]:TopTopTopTop: ssIm(encr(quadr(x0,x1,x2,x3),at)),ssSa(pair(x0,x1)) -> ssAk(key(x2,x0))
% 68.52/14.24 === Conflict found: 48:3:2:[20.1,33.3]:TopTop: ssM(sent(x0,b,pair(x0,x1))),ssBf(x1) -> ssIm(triple(b,nb(x1),encr(triple(x0,x1,tb(x1)),bt))) {x0 -> na, x1 -> na}
% 68.52/14.24 === Backtracking. Learning clause 57:5:2:[4.0,56.2,48.3,19.1,27.4,26.3]:TopTop: ssBf(x0),ssP(x1),ssIm(x1),ssIm(x0) -> ssIm(b)
% 68.52/14.24 === Conflict found: 48:3:2:[20.1,33.3]:TopTop: ssM(sent(x0,b,pair(x0,x1))),ssBf(x1) -> ssIm(triple(b,nb(x1),encr(triple(x0,x1,tb(x1)),bt))) {x0 -> na, x1 -> na}
% 68.52/14.24 === Backtracking. Learning clause 59:5:2:[4.0,58.2,48.3,18.1,27.4,26.3]:TopTop: ssBf(x0),ssP(x1),ssIm(x1),ssIm(x0) -> ssIm(nb(x0))
% 68.52/14.24 === Backtracking. Learning clause 60:3:2:[17.1,48.3]:TopTop: ssM(sent(x0,b,pair(x0,x1))),ssBf(x1) -> ssIm(encr(triple(x0,x1,tb(x1)),bt))
% 68.52/14.24 === Backtracking. Learning clause 63:5:2:[4.0,61.0,59.4,62.1,26.3,50.1,60.3,27.4,39.4,43.4,26.3]:TopTop: ssBf(x0),ssP(x1),ssIm(x1),ssIm(x0) -> ssBk(key(x0,x1))
% 68.52/14.24 === Conflict found: 63:5:2:[4.0,61.0,59.4,62.1,26.3,50.1,60.3,27.4,39.4,43.4,26.3]:TopTop: ssBf(x0),ssP(x1),ssIm(x1),ssIm(x0) -> ssBk(key(x0,x1)) {x0 -> na, x1 -> a}
% 68.52/14.24
% 68.52/14.24 SZS status Unsatisfiable
% 68.52/14.24
% 68.52/14.24 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.52/14.24
% 68.52/14.24 SPASS-SCL-FOL Statistics:
% 68.52/14.24 Number of learned clauses: 16
% 68.52/14.24 Number of propagations: 231
% 68.52/14.24 Number of decisions: 136
% 68.52/14.24 Number of resolutions: 31
% 68.52/14.24 Number of condensations: 2
% 68.52/14.24 Number of sub resolutions: 10
% 68.52/14.24 Number of input literals (deduplicated): 38
% 68.52/14.24 Number of grows: 1
% 68.52/14.24 Number of considered ground atoms: 54
% 68.52/14.24
% 68.52/14.24 Needed: 0:0:13.71
% 68.52/14.24
%------------------------------------------------------------------------------