%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN784-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 : n009.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:16 PM UTC 2026
% Result : Unsatisfiable 3.76s 1.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN784-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n009.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 13:48:26 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.33 SPASS-SCL-FOL version:
% 0.18/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 3.76/1.25 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25 Execution resolution_1 ended with status: unsatisfiable
% 3.76/1.25 Used heuristic: resolution_1
% 3.76/1.25
% 3.76/1.25 Input Clauses:
% 3.76/1.25
% 3.76/1.25 Predicates: ssRr ssPv4 ssPv2 ssPv3 ssPv1
% 3.76/1.25 Fol Constants: a
% 3.76/1.25 Fol Functions: skf3 skf2
% 3.76/1.25 Problem Properties:
% 3.76/1.25 This is a full first-order problem without equality.
% 3.76/1.25
% 3.76/1.25 After reduction: Problem Properties:
% 3.76/1.25 This is a full first-order problem without equality.
% 3.76/1.25
% 3.76/1.25
% 3.76/1.25 Reduced Input Clauses:
% 3.76/1.25
% 3.76/1.25 Most General Atoms: ssPv2(x3) ssPv4(x3) ssRr(x0,x3) ssPv1(x3) ssPv3(x3)
% 3.76/1.25
% 3.76/1.25 === Starting SPASS-SCL-FOL A Little Less Naive, considering 16 atoms initially, heuristics mode: resolution_1 ===
% 3.76/1.25
% 3.76/1.25 === Backtracking. Learning clause 43:5:2:[8.2,2.1]:TopTop: ssRr(x0,x1) -> ssPv4(x1),ssPv3(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Conflict found: 43:5:2:[8.2,2.1]:TopTop: ssRr(x0,x1) -> ssPv4(x1),ssPv3(skf2(x0)),ssPv3(x0),ssPv4(x0) {x0 -> a, x1 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 44:4:1:[43.1,2.1]:Top: -> ssPv4(skf2(x0)),ssPv3(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 45:5:2:[27.1,1.1,2.1]:TopTop: ssRr(x0,x1) -> ssPv1(skf3(x0)),ssPv4(x1),ssPv2(skf2(x0)),ssPv3(x0)
% 3.76/1.25 === Conflict found: 45:5:2:[27.1,1.1,2.1]:TopTop: ssRr(x0,x1) -> ssPv1(skf3(x0)),ssPv4(x1),ssPv2(skf2(x0)),ssPv3(x0) {x0 -> a, x1 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 46:4:1:[45.1,2.1]:Top: -> ssPv1(skf3(x0)),ssPv4(skf2(x0)),ssPv2(skf2(x0)),ssPv3(x0)
% 3.76/1.25 === Backtracking. Learning clause 47:5:2:[38.1,1.1,2.1]:TopTop: ssPv1(skf3(x0)),ssRr(x0,x1),ssPv3(x1),ssPv1(x0) -> ssPv2(skf2(x0))
% 3.76/1.25 === Conflict found: 47:5:2:[38.1,1.1,2.1]:TopTop: ssPv1(skf3(x0)),ssRr(x0,x1),ssPv3(x1),ssPv1(x0) -> ssPv2(skf2(x0)) {x0 -> a, x1 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 48:5:1:[47.2,2.1,46.1,44.2]:Top: ssPv1(x0) -> ssPv2(skf2(x0)),ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 49:4:1:[14.1,2.1,48.2]:Top: ssPv1(x0) -> ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 50:4:1:[4.1,2.1]:Top: ssPv4(skf2(x0)) -> ssPv2(x0),ssPv2(skf2(x0)),ssPv3(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 51:4:1:[18.1,2.1]:Top: ssPv1(x0),ssPv4(skf2(x0)) -> ssPv3(x0),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 52:4:1:[10.1,2.1]:Top: ssPv2(skf2(x0)) -> ssPv3(x0),ssPv2(x0),ssPv3(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 53:5:2:[14.1,2.1]:TopTop: ssPv2(skf2(x0)),ssRr(x0,x1),ssPv1(x0) -> ssPv4(x1),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 54:4:1:[12.1,2.1]:Top: ssPv1(skf2(x0)),ssPv4(skf2(x0)) -> ssPv4(x0),ssPv2(x0)
% 3.76/1.25 === Backtracking. Learning clause 55:4:1:[39.1,1.1,2.1,51.4,49.2]:Top: ssPv1(x0) -> ssPv4(skf3(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 56:4:1:[19.1,1.1,2.1,52.4,51.4,49.2,55.2]:Top: ssPv1(x0) -> ssPv2(x0),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 57:5:1:[32.1,1.1,2.1,44.2]:Top: ssPv3(skf3(x0)) -> ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Conflict found: 56:4:1:[19.1,1.1,2.1,52.4,51.4,49.2,55.2]:Top: ssPv1(x0) -> ssPv2(x0),ssPv3(x0),ssPv4(x0) {x0 -> skf3(a)}
% 3.76/1.25 === Backtracking. Learning clause 58:6:1:[56.1,46.1,57.1]:Top: -> ssPv2(skf3(x0)),ssPv2(skf2(x0)),ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 59:4:1:[8.1,1.1,57.1]:Top: -> ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 60:4:1:[36.1,1.1,2.1,50.4]:Top: ssPv4(skf2(x0)) -> ssPv4(skf3(x0)),ssPv2(x0),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 62:4:1:[55.0,61.0,7.1,2.1,54.1,52.4,60.4,59.2]:Top: -> ssPv2(x0),ssPv4(skf3(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 64:4:1:[59.0,63.0,19.1,1.1,2.1,44.2]:Top: -> ssPv2(x0),ssPv4(skf2(x0)),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 65:5:2:[11.2,1.1]:TopTop: ssRr(x0,skf3(x1)),ssPv4(skf3(x1)) -> ssPv1(x0),ssPv2(x1),ssPv1(skf3(x1))
% 3.76/1.25 === Backtracking. Learning clause 66:4:1:[6.1,1.1]:Top: ssPv3(skf3(x0)),ssPv4(skf3(x0)) -> ssPv1(x0),ssPv1(skf3(x0))
% 3.76/1.25 === Backtracking. Learning clause 68:4:1:[60.1,67.0,19.1,1.1,2.1,50.4]:Top: ssPv4(skf2(x0)) -> ssPv4(x0),ssPv2(x0),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 69:3:1:[7.1,2.1,54.1,52.4,68.4,64.2,56.1]:Top: -> ssPv2(x0),ssPv3(x0),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 70:6:3:[40.5,1.1]:TopTopTop: ssRr(x0,skf3(x1)),ssPv3(x0),ssRr(x2,skf3(x1)),ssPv1(x2),ssPv1(x1),ssPv3(skf3(x1)) ->
% 3.76/1.25 === Backtracking. Learning clause 71:4:1:[9.1,1.1,2.1]:Top: ssPv3(x0) -> ssPv2(skf3(x0)),ssPv4(skf2(x0)),ssPv4(x0)
% 3.76/1.25 === Clause set with instances from active satisfied. Growing active. New size: 19
% 3.76/1.25 === Restarting.
% 3.76/1.25 === Conflict found: 47:5:2:[38.1,1.1,2.1]:TopTop: ssPv1(skf3(x0)),ssRr(x0,x1),ssPv3(x1),ssPv1(x0) -> ssPv2(skf2(x0)) {x0 -> a, x1 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 72:4:1:[47.2,2.1]:Top: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssPv1(x0) -> ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 73:4:1:[7.1,1.1]:Top: ssPv2(x0),ssPv3(x0) -> ssPv1(skf3(x0)),ssPv1(x0)
% 3.76/1.25 === Backtracking. Learning clause 74:5:1:[17.1,1.1,73.3]:Top: ssPv2(x0),ssPv3(x0) -> ssPv4(x0),ssPv3(skf3(x0)),ssPv1(x0)
% 3.76/1.25 === Backtracking. Learning clause 75:6:1:[40.1,1.1,73.3,74.4,1.1,72.1,69.2]:Top: ssPv2(skf3(x0)),ssPv3(skf3(x0)),ssPv1(x0) -> ssPv4(skf3(x0)),ssPv2(skf2(x0)),ssPv4(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 76:6:3:[27.1,1.1]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv1(skf3(x0)),ssPv4(x1),ssPv2(x2),ssPv3(x0)
% 3.76/1.25 === Backtracking. Learning clause 78:7:3:[69.0,77.0,17.1,1.1,76.3]:TopTopTop: ssRr(x0,x1),ssRr(x0,x2) -> ssPv4(x0),ssPv3(skf3(x0)),ssPv4(x1),ssPv2(x2),ssPv3(x0)
% 3.76/1.25 === Clause set with instances from active satisfied. Growing active. New size: 83
% 3.76/1.25 === Backtracking. Learning clause 80:6:1:[60.0,79.6,5.4,34.2,21.4,1.1,14.6,1.1,76.3,1.1,75.2]:Top: ssPv2(skf3(x0)),ssPv1(x0) -> ssPv4(x0),ssPv2(x0),ssPv4(skf3(x0)),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 82:5:1:[49.2,81.1,14.2,80.6,2.1,71.2]:Top: ssPv1(x0) -> ssPv2(x0),ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv4(x0)
% 3.76/1.25 === Conflict found: 60:4:1:[36.1,1.1,2.1,50.4]:Top: ssPv4(skf2(x0)) -> ssPv4(skf3(x0)),ssPv2(x0),ssPv2(skf2(x0)) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 83:5:1:[60.1,82.4]:Top: ssPv1(x0) -> ssPv2(skf2(x0)),ssPv2(x0),ssPv4(skf3(x0)),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 84:4:1:[39.3,82.4,83.2,1.1,2.1]:Top: ssPv1(x0) -> ssPv2(x0),ssPv4(skf3(x0)),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 85:10:4:[11.3,84.3,47.1]:TopTopTopTop: ssRr(x0,skf3(x1)),ssRr(skf3(x1),x2),ssRr(x1,x3),ssPv3(x3),ssPv1(x1) -> ssPv1(x0),ssPv2(x2),ssPv2(x1),ssPv4(x1),ssPv2(skf2(x1))
% 3.76/1.25 === Backtracking. Learning clause 86:10:3:[19.2,84.3,69.2,68.1]:TopTopTop: ssRr(skf3(x0),x1),ssRr(x1,skf2(x2)),ssPv1(x0) -> ssPv2(x1),ssPv4(x1),ssPv2(x0),ssPv4(x0),ssPv4(x2),ssPv2(x2),ssPv2(skf2(x2))
% 3.76/1.25 === Backtracking. Learning clause 88:3:1:[56.2,87.0,15.6,24.2,14.5,86.10,1.1,2.1]:Top: ssPv1(x0) -> ssPv4(x0),ssPv2(x0)
% 3.76/1.25 === Backtracking. Learning clause 90:6:3:[19.1,89.4,26.5,69.2,88.3,88.1]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv3(x2),ssPv1(x0) -> ssPv4(x1),ssPv2(x1)
% 3.76/1.25 === Conflict found: 71:4:1:[9.1,1.1,2.1]:Top: ssPv3(x0) -> ssPv2(skf3(x0)),ssPv4(skf2(x0)),ssPv4(x0) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 91:11:4:[71.1,69.2,7.2,76.6]:TopTopTopTop: ssRr(x0,skf3(x1)),ssRr(skf3(x1),x2),ssRr(skf3(x1),x3) -> ssPv4(skf2(x1)),ssPv2(x1),ssPv4(x1),ssPv1(x0),ssPv1(skf3(x1)),ssPv1(skf3(skf3(x1))),ssPv4(x2),ssPv2(x3)
% 3.76/1.25 === Backtracking. Learning clause 92:7:2:[26.2,90.6,69.2,88.1,19.2,91.7,1.1,90.4,69.2,68.1]:TopTop: ssRr(skf3(x0),x1),ssRr(x1,skf2(x0)) -> ssPv4(x1),ssPv2(x1),ssPv4(x0),ssPv2(x0),ssPv2(skf2(x0))
% 3.76/1.25 === Conflict found: 91:11:4:[71.1,69.2,7.2,76.6]:TopTopTopTop: ssRr(x0,skf3(x1)),ssRr(skf3(x1),x2),ssRr(skf3(x1),x3) -> ssPv4(skf2(x1)),ssPv2(x1),ssPv4(x1),ssPv1(x0),ssPv1(skf3(x1)),ssPv1(skf3(skf3(x1))),ssPv4(x2),ssPv2(x3) {x0 -> skf3(skf3(a)), x1 -> a, x2 -> a, x3 -> a}
% 3.76/1.25 === Backtracking. Learning clause 93:9:3:[91.1,1.1,90.4]:TopTopTop: ssRr(skf3(x0),x1),ssRr(x1,x2),ssPv3(x2) -> ssPv4(skf2(x0)),ssPv2(x0),ssPv4(x0),ssPv1(skf3(skf3(x0))),ssPv4(x1),ssPv2(x1)
% 3.76/1.25 === Backtracking. Learning clause 94:9:5:[27.7,31.2,1.1]:TopTopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x2,x3),ssPv2(x3),ssRr(x2,x4) -> ssPv1(skf3(x0)),ssPv2(x1),ssPv4(x4),ssPv4(x2)
% 3.76/1.25 === Backtracking. Learning clause 95:11:6:[26.5,69.2,88.1,69.1,31.2,19.2]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(x2),ssRr(x1,x3),ssRr(x0,x4),ssRr(x4,x5),ssPv3(x5) -> ssPv4(x3),ssPv4(x1),ssPv2(x4),ssPv4(x4)
% 3.76/1.25 === Backtracking. Learning clause 97:9:4:[1.0,96.0,5.4,34.2,21.4,1.1,14.6,35.2,71.2,38.6,69.2,31.2,1.1,94.6]:TopTopTopTop: ssRr(skf3(x0),x1),ssRr(x1,x2),ssPv2(x2),ssRr(x1,x3) -> ssPv4(skf2(x0)),ssPv2(x0),ssPv4(x0),ssPv4(x3),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 98:13:7:[11.3,36.6,90.4]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssRr(x2,x3),ssPv4(x3),ssRr(x2,x4),ssPv3(x4),ssRr(x1,x5),ssRr(x5,x6),ssPv3(x6) -> ssPv1(x0),ssPv2(x2),ssPv4(x5),ssPv2(x5)
% 3.76/1.25 === Backtracking. Learning clause 99:7:4:[15.2,69.2,98.6]:TopTopTopTop: ssPv4(x0),ssRr(x1,x2),ssRr(x2,x3),ssRr(x3,x0) -> ssPv1(x1),ssPv4(x3),ssPv2(x3)
% 3.76/1.25 === Backtracking. Learning clause 100:11:6:[19.2,36.6]:TopTopTopTopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv3(x2),ssRr(x0,x3),ssRr(x3,x4),ssPv4(x4),ssRr(x3,x5),ssPv3(x5) -> ssPv2(x1),ssPv4(x1),ssPv2(x3)
% 3.76/1.25 === Backtracking. Learning clause 101:2:1:[15.2,69.2,100.3,97.5,92.7,1.1,2.1]:Top: -> ssPv4(x0),ssPv2(x0)
% 3.76/1.25 === Backtracking. Learning clause 102:7:3:[24.5,59.3,101.2]:TopTopTop: ssRr(x0,x1),ssPv3(x1),ssRr(x0,x2) -> ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv4(x0),ssPv4(x2)
% 3.76/1.25 === Conflict found: 72:4:1:[47.2,2.1]:Top: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssPv1(x0) -> ssPv2(skf2(x0)) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 103:11:4:[72.3,26.6,7.5,28.6,101.2,1.1]:TopTopTopTop: ssPv3(skf2(x0)),ssRr(x0,x1),ssPv3(x1),ssPv3(x0),ssRr(x2,skf3(x0)),ssRr(x0,x3),ssPv4(x3) -> ssPv2(skf2(x0)),ssPv1(x2),ssPv4(x0),ssPv4(skf3(x0))
% 3.76/1.25 === Backtracking. Learning clause 104:10:4:[32.2,8.5,1.1,103.4]:TopTopTopTop: ssPv3(skf2(x0)),ssRr(x0,x1),ssPv3(x1),ssRr(x2,skf3(x0)),ssRr(x0,x3),ssPv4(x3) -> ssPv2(skf2(x0)),ssPv1(x2),ssPv4(x0),ssPv4(skf3(x0))
% 3.76/1.25 === Backtracking. Learning clause 106:15:6:[2.0,105.8,32.2,8.5,1.1,24.5,104.7,102.5]:TopTopTopTopTopTop: ssRr(x0,skf2(x1)),ssPv3(skf2(x1)),ssRr(x1,x2),ssPv3(x2),ssRr(x3,skf3(x1)),ssRr(x1,skf2(x4)),ssRr(x4,x5),ssPv3(x5) -> ssPv4(skf3(x0)),ssPv4(x0),ssPv1(x3),ssPv4(x1),ssPv4(skf3(x1)),ssPv4(skf3(x4)),ssPv4(x4)
% 3.76/1.25 === Conflict found: 72:4:1:[47.2,2.1]:Top: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssPv1(x0) -> ssPv2(skf2(x0)) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 107:8:3:[72.3,25.6]:TopTopTop: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssRr(x1,x0),ssPv4(x1),ssRr(x0,x2),ssPv3(x2),ssPv3(x0) -> ssPv2(skf2(x0))
% 3.76/1.25 === Conflict found: 101:2:1:[15.2,69.2,100.3,97.5,92.7,1.1,2.1]:Top: -> ssPv4(x0),ssPv2(x0) {x0 -> skf3(skf3(a))}
% 3.76/1.25 === Backtracking. Learning clause 108:5:3:[101.2,26.2,25.2]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv3(x2),ssPv3(x1) -> ssPv1(x1)
% 3.76/1.25 === Conflict found: 107:8:3:[72.3,25.6]:TopTopTop: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssRr(x1,x0),ssPv4(x1),ssRr(x0,x2),ssPv3(x2),ssPv3(x0) -> ssPv2(skf2(x0)) {x0 -> a, x1 -> skf3(a), x2 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 110:14:6:[2.0,109.7,107.4,106.9,108.5]:TopTopTopTopTopTop: ssPv3(skf2(x0)),ssRr(skf3(x1),x0),ssRr(x0,x2),ssPv3(x2),ssPv3(x0),ssPv3(skf2(x1)),ssRr(x3,skf3(x1)),ssRr(x4,skf3(x0)),ssRr(skf3(x0),x5),ssPv3(x5),ssPv3(skf3(x0)) -> ssPv2(skf2(x0)),ssPv1(x3),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 112:5:2:[2.0,111.0,15.2,16.6,35.2,4.3,42.4,108.5,107.1,106.9,110.11,1.1,24.4]:TopTop: ssPv3(skf2(x0)),ssRr(x1,skf3(x0)),ssPv3(x0) -> ssPv1(x1),ssPv4(x0)
% 3.76/1.25 === Conflict found: 104:10:4:[32.2,8.5,1.1,103.4]:TopTopTopTop: ssPv3(skf2(x0)),ssRr(x0,x1),ssPv3(x1),ssRr(x2,skf3(x0)),ssRr(x0,x3),ssPv4(x3) -> ssPv2(skf2(x0)),ssPv1(x2),ssPv4(x0),ssPv4(skf3(x0)) {x0 -> a, x1 -> skf2(a), x2 -> skf3(skf3(a)), x3 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 113:6:2:[104.2,2.1,101.1]:TopTop: ssPv3(skf2(x0)),ssRr(x1,skf3(x0)) -> ssPv1(x1),ssPv4(x0),ssPv4(skf3(x0)),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 114:17:8:[12.5,23.2,34.2,51.1]:TopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x3),ssRr(x3,x4),ssPv1(x3),ssPv4(x3),ssRr(x2,x5),ssRr(x5,x6),ssRr(x5,x7),ssPv4(x5),ssPv4(skf2(x4)) -> ssPv4(x6),ssPv3(x7),ssPv3(x4),ssPv2(skf2(x4))
% 3.76/1.25 === Backtracking. Learning clause 115:11:4:[6.4,51.1,114.3,101.1,113.5]:TopTopTopTop: ssPv3(skf3(x0)),ssRr(skf3(x0),x1),ssRr(skf3(x0),x2),ssPv3(skf2(x0)),ssRr(x3,skf3(x0)) -> ssPv4(x2),ssPv3(x1),ssPv2(skf2(x1)),ssPv1(x3),ssPv4(x0),ssPv2(skf2(x0))
% 3.76/1.25 === Backtracking. Learning clause 116:6:3:[32.4,2.1]:TopTopTop: ssRr(x0,x1),ssPv3(x0),ssRr(x2,x1),ssPv3(skf2(x1)) -> ssPv4(x2),ssPv3(x1)
% 3.76/1.25 === Backtracking. Learning clause 117:5:2:[31.3,2.1]:TopTop: ssRr(x0,x1),ssPv3(x0),ssPv2(skf2(x1)) -> ssPv4(skf2(x1)),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 118:13:7:[5.4,34.2,42.4]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x2),ssRr(x2,x3),ssRr(x2,x4),ssPv4(x2),ssRr(x1,x5),ssRr(x5,x6),ssPv3(x6),ssPv1(x5) -> ssPv4(x3),ssPv3(x4)
% 3.76/1.25 === Backtracking. Learning clause 119:11:6:[12.5,23.2,34.2,118.11,2.1]:TopTopTopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x2),ssRr(x2,x3),ssRr(x2,x4),ssPv4(x2),ssRr(x1,x5),ssPv3(skf2(x5)) -> ssPv4(x3),ssPv3(x4)
% 3.76/1.25 === Backtracking. Learning clause 121:5:2:[112.2,120.5,21.2,101.2,20.3,2.1,115.8,2.1,49.2,6.4,119.2,116.5,1.1]:TopTop: ssRr(x0,skf3(x1)),ssPv3(skf3(x1)),ssPv3(skf2(x1)) -> ssPv1(x0),ssPv4(x1)
% 3.76/1.25 === Conflict found: 106:15:6:[2.0,105.8,32.2,8.5,1.1,24.5,104.7,102.5]:TopTopTopTopTopTop: ssRr(x0,skf2(x1)),ssPv3(skf2(x1)),ssRr(x1,x2),ssPv3(x2),ssRr(x3,skf3(x1)),ssRr(x1,skf2(x4)),ssRr(x4,x5),ssPv3(x5) -> ssPv4(skf3(x0)),ssPv4(x0),ssPv1(x3),ssPv4(x1),ssPv4(skf3(x1)),ssPv4(skf3(x4)),ssPv4(x4) {x0 -> a, x1 -> a, x2 -> skf2(a), x3 -> skf3(skf3(a)), x4 -> a, x5 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 122:5:2:[106.1,2.1]:TopTop: ssRr(x1,skf3(x0)),ssPv3(skf2(x0)) -> ssPv1(x1),ssPv4(skf3(x0)),ssPv4(x0)
% 3.76/1.25 === Conflict found: 118:13:7:[5.4,34.2,42.4]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x2),ssRr(x2,x3),ssRr(x2,x4),ssPv4(x2),ssRr(x1,x5),ssRr(x5,x6),ssPv3(x6),ssPv1(x5) -> ssPv4(x3),ssPv3(x4) {x0 -> skf3(skf3(a)), x1 -> skf3(a), x2 -> skf3(a), x3 -> a, x4 -> a, x5 -> a, x6 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 124:8:3:[122.3,123.1,118.13,112.3,1.1]:TopTopTop: ssPv1(skf3(x0)),ssRr(x0,x1),ssPv3(x1),ssPv1(x0),ssPv3(skf2(x0)),ssRr(x2,skf3(x0)) -> ssPv1(x2),ssPv4(x0)
% 3.76/1.25 === Conflict found: 119:11:6:[12.5,23.2,34.2,118.11,2.1]:TopTopTopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x2),ssRr(x2,x3),ssRr(x2,x4),ssPv4(x2),ssRr(x1,x5),ssPv3(skf2(x5)) -> ssPv4(x3),ssPv3(x4) {x0 -> skf3(skf3(a)), x1 -> skf3(a), x2 -> skf3(a), x3 -> a, x4 -> a, x5 -> a}
% 3.76/1.25 === Backtracking. Learning clause 126:5:2:[122.3,125.1,119.11,112.3,1.1]:TopTop: ssPv1(skf3(x0)),ssPv3(skf2(x0)),ssRr(x1,skf3(x0)) -> ssPv1(x1),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 128:15:8:[122.3,127.1,4.4,42.4,34.2,121.2]:TopTopTopTopTopTopTopTop: ssRr(x0,skf3(x1)),ssRr(skf3(x1),x2),ssRr(x2,x3),ssPv3(x3),ssPv1(x2),ssRr(x0,x4),ssRr(x4,x5),ssRr(x4,x6),ssPv4(x4),ssRr(x7,skf3(x1)),ssPv3(skf2(x1)) -> ssPv4(x5),ssPv3(x6),ssPv1(x7),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 129:3:1:[6.2,10.4,101.1,4.4,34.2,121.2,112.3,1.1,122.4,126.1,1.1]:Top: ssPv3(skf2(x0)) -> ssPv1(skf3(skf3(x0))),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 130:7:2:[39.5,72.4,102.5,2.1]:TopTop: ssRr(x0,x1),ssPv1(skf3(x1)),ssPv1(x1),ssPv3(skf2(x1)) -> ssPv4(x0),ssPv4(skf3(x1)),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 131:6:2:[8.5,32.2,108.4,2.1,130.3]:TopTop: ssRr(x0,x1),ssPv1(skf3(x1)),ssPv3(skf2(x1)) -> ssPv4(x0),ssPv4(skf3(x1)),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 132:6:2:[24.4,72.4]:TopTop: ssRr(x0,skf2(x1)),ssPv3(x0),ssPv1(skf3(x1)),ssPv3(skf2(x1)),ssPv1(x1) -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 133:6:3:[34.1,1.1]:TopTopTop: ssPv2(skf3(x0)),ssRr(x0,x1),ssRr(x0,x2),ssPv4(x0) -> ssPv4(x1),ssPv3(x2)
% 3.76/1.25 === Backtracking. Learning clause 134:7:2:[5.1,1.1,42.4,133.1,132.2,2.1]:TopTop: ssPv1(x0),ssRr(x0,x1),ssPv4(x0),ssPv1(skf3(x1)),ssPv3(skf2(x1)),ssPv1(x1) -> ssPv4(x1)
% 3.76/1.25 === Conflict found: 114:17:8:[12.5,23.2,34.2,51.1]:TopTopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x3),ssRr(x3,x4),ssPv1(x3),ssPv4(x3),ssRr(x2,x5),ssRr(x5,x6),ssRr(x5,x7),ssPv4(x5),ssPv4(skf2(x4)) -> ssPv4(x6),ssPv3(x7),ssPv3(x4),ssPv2(skf2(x4)) {x0 -> skf3(skf3(a)), x1 -> skf3(a), x2 -> skf3(skf3(a)), x3 -> skf3(a), x4 -> a, x5 -> skf3(a), x6 -> a, x7 -> a}
% 3.76/1.25 === Backtracking. Learning clause 135:7:3:[114.1,1.1,101.1]:TopTopTop: ssRr(x0,x1),ssPv1(x0),ssRr(x0,x2),ssPv4(x0) -> ssPv4(x2),ssPv3(x1),ssPv2(skf2(x1))
% 3.76/1.25 === Conflict found: 119:11:6:[12.5,23.2,34.2,118.11,2.1]:TopTopTopTopTopTop: ssRr(x0,x1),ssPv1(x1),ssPv4(x1),ssRr(x0,x2),ssRr(x2,x3),ssRr(x2,x4),ssPv4(x2),ssRr(x1,x5),ssPv3(skf2(x5)) -> ssPv4(x3),ssPv3(x4) {x0 -> skf3(skf3(a)), x1 -> skf3(a), x2 -> skf3(a), x3 -> a, x4 -> a, x5 -> a}
% 3.76/1.25 === Backtracking. Learning clause 136:3:1:[119.1,1.1,25.5,2.1,134.6,131.4,1.1]:Top: ssPv1(skf3(x0)),ssPv3(skf2(x0)) -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 138:9:3:[2.0,137.3,28.4,102.5,108.4,1.1,1.1]:TopTopTop: ssRr(x0,skf2(x1)),ssRr(x1,x2),ssPv3(x2),ssPv3(x0) -> ssPv4(skf3(x0)),ssPv4(x0),ssPv4(skf3(x1)),ssPv4(x1),ssPv1(skf3(x0))
% 3.76/1.25 === Backtracking. Learning clause 139:8:4:[20.6,22.2,1.1,16.6]:TopTopTopTop: ssPv4(x0),ssRr(x0,x1),ssRr(x0,x2),ssPv4(x2),ssRr(x0,x3),ssPv2(x0) -> ssPv2(x1),ssPv1(x3)
% 3.76/1.25 === Backtracking. Learning clause 140:13:7:[15.2,16.6,139.1,42.4]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssPv4(x1),ssRr(x0,x2),ssRr(x0,x3),ssPv2(x0),ssRr(x4,x5),ssPv4(x4),ssRr(x2,x5),ssRr(x5,x6),ssPv3(x6),ssPv1(x5) -> ssPv3(x1),ssPv1(x3)
% 3.76/1.25 === Backtracking. Learning clause 142:4:1:[2.0,141.1,4.4,42.4,140.5,108.4,1.1,1.1,138.5,136.1]:Top: ssPv1(x0),ssPv3(x0),ssPv3(skf2(x0)) -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 144:6:3:[101.0,143.2,18.2,129.2]:TopTopTop: ssRr(skf3(skf3(x0)),x1),ssRr(x2,x1),ssPv3(skf2(x0)) -> ssPv3(x2),ssPv2(x1),ssPv4(x0)
% 3.76/1.25 === Conflict found: 70:6:3:[40.5,1.1]:TopTopTop: ssRr(x0,skf3(x1)),ssPv3(x0),ssRr(x2,skf3(x1)),ssPv1(x2),ssPv1(x1),ssPv3(skf3(x1)) -> {x0 -> skf3(skf3(a)), x1 -> a, x2 -> skf3(skf3(a))}
% 3.76/1.25 === Backtracking. Learning clause 145:3:1:[70.4,129.2,144.4,4.5,42.4,2.1,1.1,133.1,1.1,55.2,142.2]:Top: ssPv1(x0),ssPv3(skf2(x0)) -> ssPv4(x0)
% 3.76/1.25 === Conflict found: 108:5:3:[101.2,26.2,25.2]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv3(x2),ssPv3(x1) -> ssPv1(x1) {x0 -> skf3(a), x1 -> a, x2 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 146:4:2:[108.2,2.1]:TopTop: ssRr(x0,x1),ssPv3(skf2(x1)),ssPv3(x1) -> ssPv1(x1)
% 3.76/1.25 === Backtracking. Learning clause 147:7:4:[8.5,32.2]:TopTopTopTop: ssRr(x0,x1),ssRr(x0,x2),ssRr(x2,x3),ssPv3(x3) -> ssPv4(x1),ssPv4(x0),ssPv3(x2)
% 3.76/1.25 === Conflict found: 66:4:1:[6.1,1.1]:Top: ssPv3(skf3(x0)),ssPv4(skf3(x0)) -> ssPv1(x0),ssPv1(skf3(x0)) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 149:4:1:[145.0,148.3,66.4,136.1]:Top: ssPv3(skf3(x0)),ssPv4(skf3(x0)),ssPv3(skf2(x0)) -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 150:2:1:[37.2,5.4,1.1,129.2,101.1,1.1,133.1,149.1,147.6,2.1,146.3,1.1,145.1]:Top: ssPv3(skf2(x0)) -> ssPv4(x0)
% 3.76/1.25 === Conflict found: 75:6:1:[40.1,1.1,73.3,74.4,1.1,72.1,69.2]:Top: ssPv2(skf3(x0)),ssPv3(skf3(x0)),ssPv1(x0) -> ssPv4(skf3(x0)),ssPv2(skf2(x0)),ssPv4(skf2(x0)) {x0 -> a}
% 3.76/1.25 === Backtracking. Learning clause 151:8:2:[75.5,14.2]:TopTop: ssPv2(skf3(x0)),ssPv3(skf3(x0)),ssPv1(x0),ssRr(x1,skf2(x0)),ssPv1(x1) -> ssPv4(skf3(x0)),ssPv4(skf2(x0)),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 152:9:3:[15.6,150.1,151.7,101.2]:TopTopTop: ssRr(x0,skf2(x1)),ssPv3(x0),ssPv3(skf3(x1)),ssPv1(x1),ssRr(x2,skf2(x1)),ssPv1(x2) -> ssPv4(x1),ssPv4(x2),ssPv4(skf3(x1))
% 3.76/1.25 === Conflict found: 101:2:1:[15.2,69.2,100.3,97.5,92.7,1.1,2.1]:Top: -> ssPv4(x0),ssPv2(x0) {x0 -> skf2(a)}
% 3.76/1.25 === Backtracking. Learning clause 153:5:3:[101.2,31.4]:TopTopTop: ssRr(x0,x1),ssPv3(x0),ssRr(x1,x2) -> ssPv4(x2),ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 154:6:3:[15.6,150.1,153.4,1.1]:TopTopTop: ssRr(x0,skf2(x1)),ssPv3(x0),ssPv3(skf3(x2)),ssRr(x2,skf2(x1)) -> ssPv4(x1),ssPv4(x2)
% 3.76/1.25 === Backtracking. Learning clause 155:4:2:[14.2,101.2]:TopTop: ssRr(x0,x1),ssPv1(x0) -> ssPv4(x1),ssPv4(x0)
% 3.76/1.25 === Conflict found: 155:4:2:[14.2,101.2]:TopTop: ssRr(x0,x1),ssPv1(x0) -> ssPv4(x1),ssPv4(x0) {x0 -> skf3(skf3(a)), x1 -> skf3(a)}
% 3.76/1.25 === Backtracking. Learning clause 156:3:1:[155.2,7.4,21.5,101.2,9.4,1.1,155.2,1.1]:Top: ssPv3(skf3(x0)) -> ssPv4(x0),ssPv4(skf3(x0))
% 3.76/1.25 === Backtracking. Learning clause 157:9:5:[21.5,147.6]:TopTopTopTopTop: ssRr(x0,x1),ssPv2(x1),ssPv2(x0),ssRr(x0,x2),ssRr(x0,x3),ssRr(x3,x4),ssPv3(x4) -> ssPv4(x2),ssPv3(x3)
% 3.76/1.25 === Backtracking. Learning clause 158:2:1:[10.4,153.2,157.3,101.2,1.1,8.4,1.1,156.1]:Top: -> ssPv4(x0),ssPv4(skf3(x0))
% 3.76/1.25 === Conflict found: 154:6:3:[15.6,150.1,153.4,1.1]:TopTopTop: ssRr(x0,skf2(x1)),ssPv3(x0),ssPv3(skf3(x2)),ssRr(x2,skf2(x1)) -> ssPv4(x1),ssPv4(x2) {x0 -> a, x1 -> a, x2 -> a}
% 3.76/1.25 === Backtracking. Learning clause 159:3:1:[154.1,2.1]:Top: ssPv3(x0),ssPv3(skf3(x0)) -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 160:4:2:[21.2,101.2]:TopTop: ssRr(x0,x1),ssPv2(x0),ssPv4(x0) -> ssPv4(x1)
% 3.76/1.25 === Backtracking. Learning clause 162:4:2:[158.1,161.2,15.6,150.1,71.3,2.1,160.2]:TopTop: ssPv3(x0),ssRr(skf3(x0),x1) -> ssPv4(x0),ssPv4(x1)
% 3.76/1.25 === Conflict found: 160:4:2:[21.2,101.2]:TopTop: ssRr(x0,x1),ssPv2(x0),ssPv4(x0) -> ssPv4(x1) {x0 -> skf3(a), x1 -> a}
% 3.76/1.25 === Backtracking. Learning clause 163:4:2:[160.3,158.2]:TopTop: ssRr(skf3(x0),x1),ssPv2(skf3(x0)) -> ssPv4(x1),ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 164:1:1:[39.5,51.4,16.5,160.4,2.1,101.2,18.6,150.1,66.3,5.2,153.4,4.5,1.1,2.1,133.1,158.2,163.2,162.1,1.1]:Top: -> ssPv4(x0)
% 3.76/1.25 === Backtracking. Learning clause 165:5:3:[42.2,164.1,108.5]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2),ssPv3(x2),ssPv3(x1) ->
% 3.76/1.25 === Backtracking. Learning clause 166:5:3:[42.2,164.1]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2),ssPv3(x2),ssPv1(x1) ->
% 3.76/1.25 === Backtracking. Learning clause 167:3:2:[20.5,164.1,165.5,1.1,164.1,2.1]:TopTop: ssPv2(skf3(x0)),ssRr(x0,x1),ssPv3(x1) ->
% 3.76/1.25 === Conflict found: 165:5:3:[42.2,164.1,108.5]:TopTopTop: ssRr(x0,x1),ssPv2(x0),ssRr(x1,x2),ssPv3(x2),ssPv3(x1) -> {x0 -> skf3(skf3(a)), x1 -> skf3(a), x2 -> a}
% 3.76/1.25 === Backtracking. Learning clause 168:4:2:[165.3,1.1]:TopTop: ssRr(x0,skf3(x1)),ssPv2(x0),ssPv3(x1),ssPv3(skf3(x1)) ->
% 3.76/1.25 === Conflict found: 167:3:2:[20.5,164.1,165.5,1.1,164.1,2.1]:TopTop: ssPv2(skf3(x0)),ssRr(x0,x1),ssPv3(x1) -> {x0 -> skf3(a), x1 -> a}
% 3.76/1.25 === Backtracking. Learning clause 169:2:1:[167.2,1.1]:Top: ssPv2(skf3(skf3(x0))),ssPv3(x0) ->
% 3.76/1.25 === Backtracking. Learning clause 170:3:2:[23.6,40.6,164.1,23.6,164.1,108.5,1.1,164.1,2.1]:TopTop: ssRr(x0,x1),ssPv3(x1),ssPv3(x0) ->
% 3.76/1.25 === Conflict found: 170:3:2:[23.6,40.6,164.1,23.6,164.1,108.5,1.1,164.1,2.1]:TopTop: ssRr(x0,x1),ssPv3(x1),ssPv3(x0) -> {x0 -> skf3(a), x1 -> a}
% 3.76/1.25 === Backtracking. Learning clause 171:2:1:[170.1,1.1]:Top: ssPv3(x0),ssPv3(skf3(x0)) ->
% 3.76/1.25 === Backtracking. Learning clause 172:1:1:[20.5,164.1,164.1,2.1,1.1,171.2]:Top: ssPv3(x0) ->
% 3.76/1.25 === Backtracking. Learning clause 175:9:7:[164.0,173.9,172.0,174.10,18.6,41.4,164.1,23.6,164.1]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x3),ssPv2(x2),ssRr(x3,x1),ssRr(x3,x4),ssPv1(x3),ssRr(x5,x6),ssRr(x6,x4),ssPv1(x6) ->
% 3.76/1.25 === Backtracking. Learning clause 177:3:3:[172.0,176.3,16.2,164.1,175.6,139.7,164.1,175.6,1.1,164.1]:TopTopTop: ssRr(x0,x1),ssRr(x1,x2),ssPv2(skf3(x0)) ->
% 3.76/1.25 === Conflict found: 175:9:7:[164.0,173.9,172.0,174.10,18.6,41.4,164.1,23.6,164.1]:TopTopTopTopTopTopTop: ssRr(x0,x1),ssRr(x2,x3),ssPv2(x2),ssRr(x3,x1),ssRr(x3,x4),ssPv1(x3),ssRr(x5,x6),ssRr(x6,x4),ssPv1(x6) -> {x0 -> a, x1 -> skf2(a), x2 -> skf3(a), x3 -> a, x4 -> skf2(a), x5 -> skf3(a), x6 -> a}
% 3.76/1.25 === Backtracking. Learning clause 180:3:3:[177.2,178.3,172.0,179.4,175.6,23.6,4.4,1.1,164.1,164.1]:TopTopTop: ssRr(x0,x1),ssRr(x2,x0),ssPv1(x2) ->
% 3.76/1.25
% 3.76/1.25 SZS status Unsatisfiable
% 3.76/1.25
% 3.76/1.25 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.76/1.25
% 3.76/1.25 SPASS-SCL-FOL Statistics:
% 3.76/1.25 Number of learned clauses: 112
% 3.76/1.25 Number of propagations: 816
% 3.76/1.25 Number of decisions: 236
% 3.76/1.25 Number of resolutions: 382
% 3.76/1.25 Number of condensations: 41
% 3.76/1.25 Number of sub resolutions: 26
% 3.76/1.25 Number of input literals (deduplicated): 7
% 3.76/1.25 Number of grows: 2
% 3.76/1.25 Number of considered ground atoms: 83
% 3.76/1.25
% 3.76/1.25 Needed: 0:00:00.73
% 3.76/1.25
%------------------------------------------------------------------------------