%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN796-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.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:17 PM UTC 2026
% Result : Unsatisfiable 1.67s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYN796-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n028.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:48:46 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.67/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83 Execution resolution_1 ended with status: unsatisfiable
% 1.67/0.83 Used heuristic: resolution_1
% 1.67/0.83
% 1.67/0.83 Input Clauses:
% 1.67/0.83
% 1.67/0.83 Predicates: ssRr ssPv3 ssPv1 ssPv4 ssPv2
% 1.67/0.83 Fol Constants: a
% 1.67/0.83 Fol Functions: skf3 skf2
% 1.67/0.83 Problem Properties:
% 1.67/0.83 This is a full first-order problem without equality.
% 1.67/0.83
% 1.67/0.83 After reduction: Problem Properties:
% 1.67/0.83 This is a full first-order problem without equality.
% 1.67/0.83
% 1.67/0.83
% 1.67/0.83 Reduced Input Clauses:
% 1.67/0.83 53:5:3:[27.2,14.4]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x1) -> ssPv1(x0),ssPv1(x1)
% 1.67/0.83
% 1.67/0.83 Most General Atoms: ssPv4(x3) ssPv2(x3) ssPv1(x3) ssRr(x3,x1) ssPv3(x3)
% 1.67/0.83
% 1.67/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 16 atoms initially, heuristics mode: resolution_1 ===
% 1.67/0.83
% 1.67/0.83 === Backtracking. Learning clause 54:4:1:[5.1,2.1]:Top: ssPv2(skf2(x0)) -> ssPv2(x0),ssPv1(skf2(x0)),ssPv4(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 55:4:1:[3.1,2.1]:Top: -> ssPv3(skf2(x0)),ssPv1(x0),ssPv3(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 56:5:1:[8.1,1.1,2.1,54.1]:Top: -> ssPv4(skf3(x0)),ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0)),ssPv4(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 57:4:1:[28.1,2.1]:Top: ssPv4(skf2(x0)),ssPv2(skf2(x0)) -> ssPv1(x0),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 58:4:1:[8.1,1.1,2.1,57.2,56.5]:Top: -> ssPv4(skf3(x0)),ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 59:4:1:[4.1,1.1]:Top: ssPv4(skf3(x0)) -> ssPv1(x0),ssPv2(skf3(x0)),ssPv3(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 60:6:1:[10.1,1.1,58.1]:Top: -> ssPv3(skf3(x0)),ssPv3(x0),ssPv4(x0),ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 61:4:1:[16.1,2.1]:Top: ssPv1(skf2(x0)) -> ssPv4(skf2(x0)),ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 62:5:1:[11.1,2.1,57.2,61.2,60.6]:Top: -> ssPv3(skf3(x0)),ssPv3(x0),ssPv4(x0),ssPv1(x0),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 63:5:1:[50.1,1.1,2.1,58.1]:Top: ssPv3(skf3(x0)),ssPv3(skf2(x0)) -> ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 64:5:2:[11.1,2.1]:TopTop: ssPv1(skf2(x0)),ssRr(x0,x1) -> ssPv2(x1),ssPv3(x0),ssPv4(x0)
% 1.67/0.83 === Conflict found: 64:5:2:[11.1,2.1]:TopTop: ssPv1(skf2(x0)),ssRr(x0,x1) -> ssPv2(x1),ssPv3(x0),ssPv4(x0) {x0 -> a, x1 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 65:4:1:[64.2,2.1,57.2,61.2,63.5,55.1,62.1]:Top: -> ssPv3(x0),ssPv4(x0),ssPv1(x0),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 66:6:1:[45.1,1.1,2.1,65.4]:Top: ssPv3(skf2(x0)),ssPv2(x0) -> ssPv1(skf2(x0)),ssPv3(skf3(x0)),ssPv4(skf3(x0)),ssPv1(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 67:6:1:[45.1,1.1,2.1,59.3,66.5]:Top: ssPv3(skf2(x0)),ssPv2(x0) -> ssPv1(x0),ssPv1(skf2(x0)),ssPv3(skf3(x0)),ssPv1(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 68:6:1:[27.1,1.1,2.1,61.2,67.4]:Top: ssPv3(skf2(x0)),ssPv2(x0) -> ssPv4(x0),ssPv1(x0),ssPv3(skf3(x0)),ssPv1(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 69:4:1:[5.1,1.1]:Top: ssPv2(x0) -> ssPv2(skf3(x0)),ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 70:5:1:[45.1,1.1,2.1,69.2]:Top: ssPv3(skf2(x0)),ssPv2(x0) -> ssPv1(skf2(x0)),ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 72:4:1:[62.4,71.0,44.1,1.1,2.1,69.2,70.3,55.1]:Top: -> ssPv3(skf3(x0)),ssPv1(x0),ssPv3(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 73:5:2:[16.1,2.1]:TopTop: ssPv1(skf2(x0)),ssRr(x0,x1) -> ssPv4(x1),ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 74:5:1:[27.1,1.1,2.1,61.2,70.3]:Top: ssPv3(skf2(x0)),ssPv2(x0) -> ssPv1(skf3(x0)),ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 75:3:1:[32.1,1.1,74.3,55.1,72.1,65.4]:Top: -> ssPv3(x0),ssPv4(x0),ssPv1(x0)
% 1.67/0.83 === Backtracking. Learning clause 76:4:1:[4.1,2.1]:Top: ssPv4(x0) -> ssPv1(skf2(x0)),ssPv2(x0),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 77:4:1:[10.1,2.1]:Top: ssPv4(x0) -> ssPv3(x0),ssPv3(skf2(x0)),ssPv4(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 78:5:1:[48.1,1.1,2.1,59.3,75.2]:Top: ssPv4(x0) -> ssPv3(skf2(x0)),ssPv1(x0),ssPv3(skf3(x0)),ssPv1(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 79:4:1:[23.1,1.1,2.1]:Top: ssPv1(skf2(x0)),ssPv4(x0) -> ssPv2(skf3(x0)),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 80:6:1:[42.1,1.1,2.1,77.4]:Top: ssPv1(skf3(x0)),ssPv4(x0) -> ssPv4(skf3(x0)),ssPv2(x0),ssPv3(x0),ssPv3(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 82:5:1:[55.3,81.0,48.1,1.1,2.1,79.3,80.3,76.2,78.5]:Top: -> ssPv2(x0),ssPv3(x0),ssPv3(skf2(x0)),ssPv1(x0),ssPv3(skf3(x0))
% 1.67/0.83 === Backtracking. Learning clause 83:4:1:[20.1,2.1]:Top: ssPv1(skf2(x0)),ssPv2(skf2(x0)) -> ssPv3(x0),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 84:3:1:[12.1,1.1,2.1,83.2,79.3,76.2]:Top: ssPv4(x0) -> ssPv2(x0),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 86:3:1:[75.1,85.0,6.1,1.1]:Top: -> ssPv2(skf3(x0)),ssPv1(x0),ssPv3(x0)
% 1.67/0.83 === Clause set with instances from active satisfied. Growing active. New size: 80
% 1.67/0.83 === Conflict found: 53:5:3:[27.2,14.4]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x1) -> ssPv1(x0),ssPv1(x1) {x0 -> a, x1 -> skf2(a), x2 -> skf2(skf2(a))}
% 1.67/0.83 === Backtracking. Learning clause 88:4:1:[55.3,87.0,53.2,2.1,2.1,84.2,77.4]:Top: -> ssPv1(x0),ssPv1(skf2(x0)),ssPv3(x0),ssPv3(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 90:4:1:[82.0,89.0,44.2,86.1,88.2,1.1,2.1]:Top: -> ssPv3(skf3(x0)),ssPv1(x0),ssPv3(x0),ssPv3(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 91:4:1:[45.4,90.4,44.5,86.1,1.1,2.1]:Top: ssPv2(x0) -> ssPv3(skf3(x0)),ssPv1(x0),ssPv3(x0)
% 1.67/0.83 === Conflict found: 88:4:1:[55.3,87.0,53.2,2.1,2.1,84.2,77.4]:Top: -> ssPv1(x0),ssPv1(skf2(x0)),ssPv3(x0),ssPv3(skf2(x0)) {x0 -> a}
% 1.67/0.83 === Backtracking. Learning clause 92:7:3:[88.4,45.4]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,skf2(x2)),ssPv2(x1) -> ssPv1(x2),ssPv1(skf2(x2)),ssPv3(x2)
% 1.67/0.83 === Backtracking. Learning clause 93:18:9:[40.2,91.2,48.2,17.4]:TopTopTopTopTopTopTopTopTop: ssRr(skf3(x0),x1),ssRr(x2,x1),ssRr(x1,x3),ssPv2(x0),ssRr(x2,x4),ssRr(x5,x4),ssPv2(x5),ssRr(x4,x6),ssPv4(x4),ssRr(x7,x8),ssPv2(x7),ssRr(x8,x3) -> ssPv3(x1),ssPv1(x0),ssPv3(x0),ssPv3(x6),ssPv1(x8),ssPv3(x8)
% 1.67/0.83 === Conflict found: 92:7:3:[88.4,45.4]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,skf2(x2)),ssPv2(x1) -> ssPv1(x2),ssPv1(skf2(x2)),ssPv3(x2) {x0 -> skf3(a), x1 -> a, x2 -> a}
% 1.67/0.83 === Backtracking. Learning clause 94:8:3:[92.2,86.1]:TopTopTop: ssRr(skf3(x0),x1),ssRr(x1,skf2(x2)),ssPv2(x1) -> ssPv1(x2),ssPv1(skf2(x2)),ssPv3(x2),ssPv1(x0),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 95:2:1:[50.2,40.6,91.2,17.4,93.16,86.1,1.1,2.1,84.2,75.2]:Top: -> ssPv3(x0),ssPv1(x0)
% 1.67/0.83 === Backtracking. Learning clause 96:8:3:[26.4,95.2,54.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssPv2(skf2(x1)) -> ssPv2(x0),ssPv3(x0),ssPv3(x2),ssPv1(skf2(x1)),ssPv4(skf2(x1))
% 1.67/0.83 === Backtracking. Learning clause 97:6:3:[11.2,95.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv2(x2),ssPv3(x0),ssPv4(x0),ssPv3(x1)
% 1.67/0.83 === Backtracking. Learning clause 98:6:3:[26.4,95.2,97.3,40.2]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x2) -> ssPv2(x0),ssPv4(x0),ssPv3(x1)
% 1.67/0.83 === Backtracking. Learning clause 99:3:2:[22.4,95.2,95.1]:TopTop: ssRr(x0,x1) -> ssPv1(x1),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 100:11:6:[38.6,25.3]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv1(x2),ssRr(x1,x3),ssRr(x4,x5),ssRr(x5,x3),ssPv1(x5) -> ssPv4(x0),ssPv2(x1),ssPv2(x4),ssPv2(x5)
% 1.67/0.83 === Conflict found: 97:6:3:[11.2,95.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv2(x2),ssPv3(x0),ssPv4(x0),ssPv3(x1) {x0 -> a, x1 -> skf2(a), x2 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 101:10:3:[97.5,79.2,83.2]:TopTopTop: ssRr(x0,x1),ssRr(x0,skf2(x2)),ssPv1(skf2(x0)),ssPv1(skf2(x2)) -> ssPv3(x0),ssPv3(x1),ssPv2(skf3(x0)),ssPv2(x0),ssPv3(x2),ssPv2(x2)
% 1.67/0.83 === Backtracking. Learning clause 102:15:8:[21.4,97.5,26.6,98.3]:TopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x3),ssRr(x1,x2),ssRr(x0,x4),ssPv2(x4),ssRr(x0,x5),ssPv1(x5),ssRr(x6,x7),ssRr(x7,x2) -> ssPv3(x1),ssPv3(x3),ssPv2(x0),ssPv2(x6),ssPv4(x6),ssPv3(x7)
% 1.67/0.83 === Backtracking. Learning clause 105:7:3:[95.1,103.3,2.0,104.4,52.6,99.2,2.1,101.8]:TopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv1(x2),ssPv1(skf2(x0)) -> ssPv3(x1),ssPv2(skf3(x0)),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 106:8:2:[11.6,79.2,83.2]:TopTop: ssRr(x0,skf2(x1)),ssPv1(skf2(x0)),ssPv1(skf2(x1)) -> ssPv3(x0),ssPv2(skf3(x0)),ssPv2(x0),ssPv3(x1),ssPv2(x1)
% 1.67/0.83 === Conflict found: 105:7:3:[95.1,103.3,2.0,104.4,52.6,99.2,2.1,101.8]:TopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv1(x2),ssPv1(skf2(x0)) -> ssPv3(x1),ssPv2(skf3(x0)),ssPv3(x0) {x0 -> a, x1 -> skf2(a), x2 -> a}
% 1.67/0.83 === Backtracking. Learning clause 107:5:2:[105.3,95.2]:TopTop: ssRr(x0,x1),ssPv1(skf2(x0)) -> ssPv3(x1),ssPv2(skf3(x0)),ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 109:6:3:[99.1,108.3,32.2,18.6,31.3,2.1,34.6]:TopTopTop: ssRr(x0,x1),ssPv2(x1),ssRr(x2,x1),ssPv3(x1),ssPv1(x0) -> ssPv3(x2)
% 1.67/0.83 === Backtracking. Learning clause 111:8:5:[99.1,110.2,21.2,47.7,11.6,109.2,95.2,107.3]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssRr(x1,x3),ssRr(x4,x3),ssPv1(skf2(x4)) -> ssPv3(x1),ssPv2(skf3(x4)),ssPv3(x4)
% 1.67/0.83 === Backtracking. Learning clause 113:11:7:[99.1,112.8,30.5,44.7,34.6,95.2,111.7,26.5]:TopTopTopTopTopTopTop: ssRr(skf3(x0),x1),ssRr(x2,x3),ssRr(x3,x4),ssRr(x0,x4),ssPv1(skf2(x0)),ssRr(x1,x5),ssPv2(x5),ssRr(x1,x6) -> ssPv3(x3),ssPv3(x0),ssPv3(x1)
% 1.67/0.83 === Backtracking. Learning clause 114:1:1:[44.7,21.2,111.7,84.2,11.6,113.7,1.1,99.2,2.1]:Top: -> ssPv3(x0)
% 1.67/0.83 === Backtracking. Learning clause 118:8:6:[99.2,115.2,114.0,116.4,99.2,117.6,50.2,15.4]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssRr(x1,x3),ssRr(x4,x5),ssRr(x0,x5) -> ssPv1(x1),ssPv1(x5),ssPv4(x5)
% 1.67/0.83 === Conflict found: 54:4:1:[5.1,2.1]:Top: ssPv2(skf2(x0)) -> ssPv2(x0),ssPv1(skf2(x0)),ssPv4(skf2(x0)) {x0 -> a}
% 1.67/0.83 === Backtracking. Learning clause 119:8:3:[54.4,25.3]:TopTopTop: ssPv2(skf2(x0)),ssRr(x1,x2),ssRr(x2,skf2(x0)),ssPv1(x2) -> ssPv2(x0),ssPv1(skf2(x0)),ssPv2(x1),ssPv2(x2)
% 1.67/0.83 === Backtracking. Learning clause 120:4:2:[24.4,114.1,1.1]:TopTop: ssRr(x0,x1),ssPv2(x1) -> ssPv2(skf3(x0)),ssPv2(x0)
% 1.67/0.83 === Backtracking. Learning clause 122:4:3:[114.0,121.2,30.2,118.6]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2) -> ssPv4(x1)
% 1.67/0.83 === Backtracking. Learning clause 125:14:9:[99.2,123.9,114.0,124.11,37.6,28.2,50.2]:TopTopTopTopTopTopTopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x2,x1),ssRr(x1,x3),ssRr(x4,x3),ssRr(x4,x5),ssPv2(x5),ssRr(x2,x6),ssRr(x7,x6),ssRr(x6,x8) -> ssPv2(x1),ssPv1(x4),ssPv2(x4),ssPv1(x6)
% 1.67/0.83 === Backtracking. Learning clause 126:5:3:[29.4,114.1]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv4(x2),ssPv4(x1) -> ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 127:3:2:[32.5,114.1,34.4,122.4,125.12,1.1,120.3]:TopTop: ssRr(x0,x1),ssPv2(x1) -> ssPv2(x0)
% 1.67/0.83 === Conflict found: 118:8:6:[99.2,115.2,114.0,116.4,99.2,117.6,50.2,15.4]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssRr(x1,x3),ssRr(x4,x5),ssRr(x0,x5) -> ssPv1(x1),ssPv1(x5),ssPv4(x5) {x0 -> skf3(a), x1 -> a, x2 -> skf3(a), x3 -> skf2(a), x4 -> skf3(a), x5 -> a}
% 1.67/0.83 === Backtracking. Learning clause 128:3:2:[118.1,1.1]:TopTop: ssRr(x0,x1) -> ssPv1(x0),ssPv4(x0)
% 1.67/0.83 === Backtracking. Learning clause 130:4:3:[127.2,129.1,45.4,114.1]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x1) -> ssPv1(x2)
% 1.67/0.83 === Backtracking. Learning clause 131:4:2:[51.6,114.1,50.2,114.1,130.4,127.3,1.1]:TopTop: ssPv3(skf3(x0)),ssRr(x0,x1),ssPv2(x1) -> ssPv1(x0)
% 1.67/0.83 === Backtracking. Learning clause 132:1:1:[30.4,127.3,34.6,130.4,127.3,1.1,131.4,2.1,114.1]:Top: ssPv2(skf2(x0)) ->
% 1.67/0.83 === Conflict found: 63:5:1:[50.1,1.1,2.1,58.1]:Top: ssPv3(skf3(x0)),ssPv3(skf2(x0)) -> ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0)) {x0 -> a}
% 1.67/0.83 === Backtracking. Learning clause 133:3:1:[63.1,114.1,114.1]:Top: -> ssPv1(x0),ssPv2(x0),ssPv1(skf2(x0))
% 1.67/0.83 === Backtracking. Learning clause 134:3:2:[45.3,2.1,127.3,114.1,133.2]:TopTop: ssRr(x0,x1) -> ssPv1(x1),ssPv1(skf2(x1))
% 1.67/0.83 === Conflict found: 128:3:2:[118.1,1.1]:TopTop: ssRr(x0,x1) -> ssPv1(x0),ssPv4(x0) {x0 -> a, x1 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 136:3:1:[133.2,135.0,128.1,2.1,79.2]:Top: -> ssPv1(x0),ssPv2(skf3(x0)),ssPv2(x0)
% 1.67/0.83 === Conflict found: 122:4:3:[114.0,121.2,30.2,118.6]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2) -> ssPv4(x1) {x0 -> skf3(a), x1 -> a, x2 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 137:3:2:[122.3,2.1]:TopTop: ssRr(x0,x1),ssPv2(x0) -> ssPv4(x1)
% 1.67/0.83 === Backtracking. Learning clause 138:3:2:[50.2,8.3,114.1,132.1,114.1,2.1]:TopTop: ssRr(x0,x1) -> ssPv1(x1),ssPv2(x1)
% 1.67/0.83 === Backtracking. Learning clause 139:2:2:[51.6,114.1,50.2,114.1,134.3,114.1,2.1]:TopTop: ssRr(x0,x1) -> ssPv1(x1)
% 1.67/0.83 === Conflict found: 100:11:6:[38.6,25.3]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv1(x2),ssRr(x1,x3),ssRr(x4,x5),ssRr(x5,x3),ssPv1(x5) -> ssPv4(x0),ssPv2(x1),ssPv2(x4),ssPv2(x5) {x0 -> a, x1 -> skf2(a), x2 -> skf2(skf2(a)), x3 -> skf2(skf2(a)), x4 -> a, x5 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 140:5:3:[100.3,139.2,2.1,132.1]:TopTopTop: ssRr(x0,skf2(x1)),ssRr(x2,skf2(x1)),ssPv1(skf2(x1)) -> ssPv4(x0),ssPv2(x2)
% 1.67/0.83 === Backtracking. Learning clause 141:7:5:[46.4,114.1,132.1,140.4]:TopTopTopTopTop: ssRr(x0,skf2(x1)),ssRr(x2,skf2(x1)),ssPv1(x2),ssRr(x0,skf2(x3)),ssRr(x4,skf2(x3)),ssPv1(skf2(x3)) -> ssPv2(x4)
% 1.67/0.83 === Conflict found: 122:4:3:[114.0,121.2,30.2,118.6]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2) -> ssPv4(x1) {x0 -> skf3(a), x1 -> a, x2 -> skf2(a)}
% 1.67/0.83 === Backtracking. Learning clause 142:5:4:[122.2,127.3]:TopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssRr(x0,x3),ssPv2(x3) -> ssPv4(x1)
% 1.67/0.83
% 1.67/0.83 SZS status Unsatisfiable
% 1.67/0.83
% 1.67/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.67/0.83
% 1.67/0.83 SPASS-SCL-FOL Statistics:
% 1.67/0.83 Number of learned clauses: 71
% 1.67/0.83 Number of propagations: 441
% 1.67/0.83 Number of decisions: 150
% 1.67/0.83 Number of resolutions: 216
% 1.67/0.83 Number of condensations: 16
% 1.67/0.83 Number of sub resolutions: 19
% 1.67/0.83 Number of input literals (deduplicated): 7
% 1.67/0.83 Number of grows: 1
% 1.67/0.83 Number of considered ground atoms: 80
% 1.67/0.83
% 1.67/0.83 Needed: 0:00:00.29
% 1.67/0.83
%------------------------------------------------------------------------------