%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRA117-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:22:44 PM UTC 2026
% Result : Unsatisfiable 0.61s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : GRA117-1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.37 % Computer : n005.cluster.edu
% 0.18/0.37 % Model : x86_64 x86_64
% 0.18/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.37 % Memory : 8042.1875MB
% 0.18/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.37 % CPULimit : 300
% 0.18/0.37 % WCLimit : 300
% 0.18/0.37 % DateTime : Thu May 7 11:59:31 EDT 2026
% 0.18/0.37 % CPUTime :
% 0.18/0.37 SPASS-SCL-FOL version:
% 0.18/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.61/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63 Execution resolution_3 ended with status: unsatisfiable
% 0.61/0.63 Used heuristic: resolution_3
% 0.61/0.63
% 0.61/0.63 Input Clauses:
% 0.61/0.63
% 0.61/0.63 Predicates: r =
% 0.61/0.63 Fol Constants: v0 v1 v2 v3 v4 v5
% 0.61/0.63 Fol Functions:
% 0.61/0.63 Problem Properties:
% 0.61/0.63 This is a Bernays Schoenfinkel Ramsey problem.
% 0.61/0.63
% 0.61/0.63
% 0.61/0.63 Reduced Input Clauses:
% 0.61/0.63
% 0.61/0.63 Most General Atoms: r(x1,x2) =(x1,x2)
% 0.61/0.63
% 0.61/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 42 atoms initially, heuristics mode: resolution_3 ===
% 0.61/0.63
% 0.61/0.63 === Backtracking. Learning clause 19:5:1:[2.6,6.1]:Top: r(x0,v2),r(x0,v1),r(v2,v1) -> =(x0,v2),=(x0,v1)
% 0.61/0.63 === CC is in false state. New clause to be learned: 21:1:0:[5.0,20.1]:: =(v0,v2) ->
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 19:5:1:[2.6,6.1]:Top: r(x0,v2),r(x0,v1),r(v2,v1) -> =(x0,v2),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 22:4:0:[19.4,21.1]:: r(v0,v2),r(v0,v1),r(v2,v1) -> =(v0,v1)
% 0.61/0.63 === CC is in false state. New clause to be learned: 24:1:0:[4.0,23.1]:: =(v0,v1) ->
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 22:4:0:[19.4,21.1]:: r(v0,v2),r(v0,v1),r(v2,v1) -> =(v0,v1) {}
% 0.61/0.63 === Backtracking. Learning clause 25:3:0:[22.4,24.1]:: r(v0,v2),r(v0,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 26:5:1:[2.6,8.1]:Top: r(x0,v3),r(x0,v1),r(v3,v1) -> =(x0,v3),=(x0,v1)
% 0.61/0.63 === CC is in false state. New clause to be learned: 28:1:0:[7.0,27.1]:: =(v0,v3) ->
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 26:5:1:[2.6,8.1]:Top: r(x0,v3),r(x0,v1),r(v3,v1) -> =(x0,v3),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 29:3:0:[26.4,28.1,24.1]:: r(v0,v3),r(v0,v1),r(v3,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 30:3:0:[2.6,9.1,28.1,21.1]:: r(v0,v3),r(v0,v2),r(v3,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 31:3:0:[3.1,9.1,8.1,6.1,30.3,29.3,25.3]:: r(v0,v3),r(v0,v2),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 32:5:1:[2.6,11.1]:Top: r(x0,v4),r(x0,v1),r(v4,v1) -> =(x0,v4),=(x0,v1)
% 0.61/0.63 === CC is in false state. New clause to be learned: 33:3:0:TAUT:: =(v0,v4),r(v4,v3) -> r(v0,v3)
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 32:5:1:[2.6,11.1]:Top: r(x0,v4),r(x0,v1),r(v4,v1) -> =(x0,v4),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 34:5:0:[32.4,33.1,24.1]:: r(v0,v4),r(v0,v1),r(v4,v1),r(v4,v3) -> r(v0,v3)
% 0.61/0.63 === CC is in false state. New clause to be learned: 36:1:0:[10.0,35.1]:: =(v0,v4) ->
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 32:5:1:[2.6,11.1]:Top: r(x0,v4),r(x0,v1),r(v4,v1) -> =(x0,v4),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 37:3:0:[32.4,36.1,24.1]:: r(v0,v4),r(v0,v1),r(v4,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 38:3:0:[2.6,12.1,36.1,21.1]:: r(v0,v4),r(v0,v2),r(v4,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 39:3:0:[3.1,12.1,11.1,6.1,38.3,37.3,25.3]:: r(v0,v4),r(v0,v2),r(v0,v1) ->
% 0.61/0.63 === Conflict found: 26:5:1:[2.6,8.1]:Top: r(x0,v3),r(x0,v1),r(v3,v1) -> =(x0,v3),=(x0,v1) {x0 -> v4}
% 0.61/0.63 === Backtracking. Learning clause 40:3:0:[26.4,13.1,11.1]:: r(v4,v3),r(v4,v1),r(v3,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 41:4:0:[3.3,13.1,36.1,28.1,40.1]:: r(v4,v1),r(v3,v1) -> r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 42:3:0:[2.4,13.1,12.1,9.1]:: r(v4,v3),r(v4,v2),r(v3,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 43:4:0:[3.3,13.1,36.1,28.1,42.1]:: r(v4,v2),r(v3,v2) -> r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 44:5:0:[3.1,12.1,11.1,6.1,43.1,41.1]:: r(v3,v2),r(v3,v1) -> r(v2,v1),r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 45:5:1:[2.6,15.1]:Top: r(x0,v5),r(x0,v1),r(v5,v1) -> =(x0,v5),=(x0,v1)
% 0.61/0.63 === CC is in false state. New clause to be learned: 46:3:0:TAUT:: =(v0,v5),r(v5,v3) -> r(v0,v3)
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 45:5:1:[2.6,15.1]:Top: r(x0,v5),r(x0,v1),r(v5,v1) -> =(x0,v5),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 47:5:0:[45.4,46.1,24.1]:: r(v0,v5),r(v0,v1),r(v5,v1),r(v5,v3) -> r(v0,v3)
% 0.61/0.63 === CC is in false state. New clause to be learned: 48:3:0:TAUT:: =(v0,v5),r(v5,v4) -> r(v0,v4)
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 45:5:1:[2.6,15.1]:Top: r(x0,v5),r(x0,v1),r(v5,v1) -> =(x0,v5),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 49:5:0:[45.4,48.1,24.1]:: r(v0,v5),r(v0,v1),r(v5,v1),r(v5,v4) -> r(v0,v4)
% 0.61/0.63 === CC is in false state. New clause to be learned: 51:1:0:[14.0,50.1]:: =(v0,v5) ->
% 0.61/0.63 === Restarting.
% 0.61/0.63 === Conflict found: 45:5:1:[2.6,15.1]:Top: r(x0,v5),r(x0,v1),r(v5,v1) -> =(x0,v5),=(x0,v1) {x0 -> v0}
% 0.61/0.63 === Backtracking. Learning clause 52:3:0:[45.4,51.1,24.1]:: r(v0,v5),r(v0,v1),r(v5,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 53:3:0:[2.6,16.1,51.1,21.1]:: r(v0,v5),r(v0,v2),r(v5,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 54:3:0:[3.1,16.1,15.1,6.1,53.3,52.3,25.3]:: r(v0,v5),r(v0,v2),r(v0,v1) ->
% 0.61/0.63 === Conflict found: 26:5:1:[2.6,8.1]:Top: r(x0,v3),r(x0,v1),r(v3,v1) -> =(x0,v3),=(x0,v1) {x0 -> v5}
% 0.61/0.63 === Backtracking. Learning clause 55:3:0:[26.4,17.1,15.1]:: r(v5,v3),r(v5,v1),r(v3,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 56:4:0:[3.3,17.1,51.1,28.1,55.1]:: r(v5,v1),r(v3,v1) -> r(v0,v5),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 57:3:0:[2.4,18.1,17.1,13.1]:: r(v5,v4),r(v5,v3),r(v4,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 58:4:0:[3.3,18.1,51.1,36.1,57.1]:: r(v5,v3),r(v4,v3) -> r(v0,v5),r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 59:4:0:[3.3,17.1,51.1,28.1,58.1]:: r(v4,v3) -> r(v0,v3),r(v0,v5),r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 60:2:0:[3.3,13.1,36.1,28.1,59.1,54.1,39.1,31.1]:: r(v0,v2),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 61:4:0:[3.1,13.1,11.1,8.1,42.1]:: r(v4,v2),r(v3,v2) -> r(v4,v1),r(v3,v1)
% 0.61/0.63 === Backtracking. Learning clause 62:3:0:[2.6,13.1,36.1,28.1]:: r(v0,v4),r(v0,v3),r(v4,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 63:3:0:[3.1,13.1,11.1,8.1,62.3,37.3,29.3]:: r(v0,v4),r(v0,v3),r(v0,v1) ->
% 0.61/0.63 === Conflict found: 19:5:1:[2.6,6.1]:Top: r(x0,v2),r(x0,v1),r(v2,v1) -> =(x0,v2),=(x0,v1) {x0 -> v4}
% 0.61/0.63 === Backtracking. Learning clause 64:3:0:[19.4,12.1,11.1]:: r(v4,v2),r(v4,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 65:4:0:[3.3,12.1,36.1,21.1,64.1]:: r(v4,v1),r(v2,v1) -> r(v0,v4),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 66:5:0:[3.3,12.1,36.1,21.1,61.1,65.1]:: r(v3,v2),r(v2,v1) -> r(v3,v1),r(v0,v4),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 67:3:0:[2.6,17.1,51.1,28.1]:: r(v0,v5),r(v0,v3),r(v5,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 68:3:0:[3.1,17.1,15.1,8.1,67.3,52.3,29.3]:: r(v0,v5),r(v0,v3),r(v0,v1) ->
% 0.61/0.63 === Conflict found: 19:5:1:[2.6,6.1]:Top: r(x0,v2),r(x0,v1),r(v2,v1) -> =(x0,v2),=(x0,v1) {x0 -> v5}
% 0.61/0.63 === Backtracking. Learning clause 69:3:0:[19.4,16.1,15.1]:: r(v5,v2),r(v5,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 70:4:0:[3.3,16.1,51.1,21.1,69.1]:: r(v5,v1),r(v2,v1) -> r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 71:6:0:[3.1,17.1,15.1,8.1,58.1,70.1]:: r(v4,v3),r(v2,v1) -> r(v3,v1),r(v0,v4),r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 75:3:0:[68.0,72.3,63.0,73.4,25.0,74.5,3.1,13.1,11.1,8.1,71.1,65.1,29.3]:: r(v2,v1),r(v0,v3),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 76:3:0:[2.4,17.1,16.1,9.1]:: r(v5,v3),r(v5,v2),r(v3,v2) ->
% 0.61/0.63 === Conflict found: 32:5:1:[2.6,11.1]:Top: r(x0,v4),r(x0,v1),r(v4,v1) -> =(x0,v4),=(x0,v1) {x0 -> v5}
% 0.61/0.63 === Backtracking. Learning clause 77:3:0:[32.4,18.1,15.1]:: r(v5,v4),r(v5,v1),r(v4,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 78:5:0:[3.1,18.1,17.1,13.1,77.1,76.1]:: r(v5,v1),r(v4,v1),r(v5,v2),r(v3,v2) -> r(v4,v3)
% 0.61/0.63 === Backtracking. Learning clause 79:6:0:[3.3,16.1,51.1,21.1,78.3]:: r(v5,v1),r(v4,v1),r(v3,v2) -> r(v0,v5),r(v0,v2),r(v4,v3)
% 0.61/0.63 === Backtracking. Learning clause 80:4:0:[3.1,17.1,15.1,8.1,76.1]:: r(v5,v2),r(v3,v2) -> r(v5,v1),r(v3,v1)
% 0.61/0.63 === Backtracking. Learning clause 82:5:0:[61.2,81.0,3.3,16.1,51.1,21.1,80.1,79.1,42.1]:: r(v4,v2),r(v3,v2) -> r(v3,v1),r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 83:5:0:[3.3,12.1,36.1,21.1,82.1]:: r(v3,v2) -> r(v0,v4),r(v3,v1),r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 85:2:0:[31.1,84.2,3.1,9.1,8.1,6.1,83.1,29.3,75.1,68.1,63.1]:: r(v0,v3),r(v0,v1) ->
% 0.61/0.63 === Conflict found: 19:5:1:[2.6,6.1]:Top: r(x0,v2),r(x0,v1),r(v2,v1) -> =(x0,v2),=(x0,v1) {x0 -> v3}
% 0.61/0.63 === Backtracking. Learning clause 86:3:0:[19.4,9.1,8.1]:: r(v3,v2),r(v3,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 87:4:0:[3.3,9.1,28.1,21.1,86.1]:: r(v3,v1),r(v2,v1) -> r(v0,v3),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 88:4:0:[3.1,18.1,16.1,12.1,57.1]:: r(v5,v3),r(v4,v3) -> r(v5,v2),r(v4,v2)
% 0.61/0.63 === Backtracking. Learning clause 90:5:0:[42.1,89.4,3.1,17.1,15.1,8.1,88.1,80.1,52.3]:: r(v4,v3),r(v3,v2),r(v0,v5),r(v0,v1) -> r(v3,v1)
% 0.61/0.63 === Backtracking. Learning clause 91:5:0:[3.1,13.1,11.1,8.1,90.1,37.3]:: r(v3,v2),r(v0,v5),r(v0,v4),r(v0,v1) -> r(v3,v1)
% 0.61/0.63 === Backtracking. Learning clause 94:4:0:[63.1,92.4,25.0,93.5,3.3,9.1,28.1,21.1,91.1,87.1]:: r(v0,v5),r(v0,v4),r(v0,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 95:3:0:[2.6,18.1,51.1,36.1]:: r(v0,v5),r(v0,v4),r(v5,v4) ->
% 0.61/0.63 === Backtracking. Learning clause 96:5:0:[3.1,18.1,17.1,13.1,95.3,76.1]:: r(v0,v5),r(v0,v4),r(v5,v2),r(v3,v2) -> r(v4,v3)
% 0.61/0.63 === Backtracking. Learning clause 98:5:0:[94.3,97.5,3.1,16.1,15.1,6.1,96.3,52.3,42.1]:: r(v0,v4),r(v0,v5),r(v0,v1),r(v4,v2),r(v3,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 100:4:0:[94.3,99.4,3.1,12.1,11.1,6.1,98.4,37.3]:: r(v0,v5),r(v3,v2),r(v0,v4),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 103:3:0:[63.1,101.3,39.1,102.4,3.3,9.1,28.1,21.1,100.2]:: r(v0,v5),r(v0,v4),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 105:4:0:[86.1,104.2,3.3,16.1,51.1,21.1,80.1,70.1]:: r(v3,v2),r(v2,v1) -> r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 106:4:0:[3.3,9.1,28.1,21.1,105.1]:: r(v2,v1) -> r(v0,v3),r(v0,v5),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 107:4:0:[3.3,17.1,51.1,28.1,76.1]:: r(v5,v2),r(v3,v2) -> r(v0,v5),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 108:4:0:[3.3,16.1,51.1,21.1,107.1]:: r(v3,v2) -> r(v0,v2),r(v0,v5),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 111:2:0:[39.1,109.2,63.1,110.3,3.3,9.1,28.1,21.1,108.1,103.1]:: r(v0,v4),r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 112:4:0:[3.3,9.1,28.1,21.1,66.1,87.1]:: r(v2,v1) -> r(v0,v4),r(v0,v3),r(v0,v2)
% 0.61/0.63 === Backtracking. Learning clause 114:4:0:[87.1,113.2,3.3,9.1,28.1,21.1,44.1]:: r(v3,v1) -> r(v0,v2),r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 115:4:0:[3.3,12.1,36.1,21.1,43.1]:: r(v3,v2) -> r(v0,v2),r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 116:1:0:[3.3,9.1,28.1,21.1,115.1,111.1,85.1,60.1]:: r(v0,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 117:3:0:[3.1,13.1,12.1,9.1,62.3,38.3,30.3]:: r(v0,v4),r(v0,v3),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 119:3:0:[86.0,118.3,3.1,13.1,12.1,9.1,40.1,64.1]:: r(v3,v1),r(v4,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 121:3:0:[116.0,120.3,3.3,11.1,36.1,24.1,119.2]:: r(v3,v1),r(v2,v1) -> r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 122:3:0:[3.1,17.1,16.1,9.1,67.3,53.3,30.3]:: r(v0,v5),r(v0,v3),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 123:6:0:[3.1,17.1,16.1,9.1,58.1,69.1]:: r(v4,v3),r(v5,v1),r(v2,v1) -> r(v3,v2),r(v0,v5),r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 125:5:0:[116.0,124.2,3.3,15.1,51.1,24.1,123.2]:: r(v4,v3),r(v2,v1) -> r(v3,v2),r(v0,v5),r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 126:5:0:[3.1,13.1,12.1,9.1,125.1,64.1]:: r(v4,v1),r(v2,v1) -> r(v3,v2),r(v0,v5),r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 130:3:0:[25.1,127.3,122.0,128.4,117.0,129.5,3.3,11.1,36.1,24.1,126.1,30.3]:: r(v2,v1),r(v0,v3),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 132:3:0:[40.0,131.3,3.1,18.1,17.1,13.1,77.1,55.1]:: r(v4,v1),r(v5,v1),r(v3,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 134:3:0:[116.0,133.3,3.3,15.1,51.1,24.1,132.2]:: r(v4,v1),r(v3,v1) -> r(v0,v5)
% 0.61/0.63 === Backtracking. Learning clause 136:3:0:[116.0,135.2,3.3,11.1,36.1,24.1,134.1]:: r(v3,v1) -> r(v0,v4),r(v0,v5)
% 0.61/0.63 === Backtracking. Learning clause 137:2:0:[3.1,9.1,8.1,6.1,30.3,136.1,130.1,122.1,117.1]:: r(v0,v3),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 138:5:0:[3.1,17.1,16.1,9.1,55.1,53.3]:: r(v5,v1),r(v3,v1),r(v0,v5),r(v0,v2) -> r(v3,v2)
% 0.61/0.63 === Backtracking. Learning clause 139:5:0:[3.1,17.1,16.1,9.1,88.1,53.3]:: r(v4,v3),r(v0,v5),r(v0,v2) -> r(v3,v2),r(v4,v2)
% 0.61/0.63 === Backtracking. Learning clause 141:4:0:[121.2,140.1,3.1,13.1,12.1,9.1,139.1,38.3,86.1]:: r(v0,v5),r(v0,v2),r(v3,v1),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 144:3:0:[122.1,142.3,25.1,143.4,3.3,8.1,28.1,24.1,141.3]:: r(v0,v5),r(v0,v2),r(v2,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 147:3:0:[134.2,145.0,119.2,146.4,3.1,16.1,15.1,6.1,53.3,132.2]:: r(v0,v2),r(v4,v1),r(v3,v1) ->
% 0.61/0.63 === Backtracking. Learning clause 148:4:0:[3.1,12.1,11.1,6.1,38.3,147.2]:: r(v0,v4),r(v0,v2),r(v3,v1) -> r(v2,v1)
% 0.61/0.63 === Backtracking. Learning clause 151:3:0:[117.1,149.3,39.2,150.4,3.3,8.1,28.1,24.1,148.3,144.3]:: r(v0,v4),r(v0,v5),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 153:3:0:[116.0,152.1,3.3,15.1,51.1,24.1,56.1]:: r(v3,v1) -> r(v0,v5),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 156:2:0:[39.2,154.2,117.1,155.3,3.3,8.1,28.1,24.1,153.1,151.2]:: r(v0,v4),r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 158:3:0:[116.0,157.1,3.3,11.1,36.1,24.1,41.1]:: r(v3,v1) -> r(v0,v4),r(v0,v3)
% 0.61/0.63 === Backtracking. Learning clause 160:1:0:[60.1,159.1,3.3,8.1,28.1,24.1,158.1,156.1,137.1]:: r(v0,v2) ->
% 0.61/0.63 === Backtracking. Learning clause 161:5:0:[3.1,17.1,16.1,9.1,67.3,69.1]:: r(v0,v5),r(v0,v3),r(v5,v1),r(v2,v1) -> r(v3,v2)
% 0.61/0.63 === Backtracking. Learning clause 162:3:0:[3.1,18.1,17.1,13.1,95.3,67.3,62.3]:: r(v0,v5),r(v0,v4),r(v0,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 165:2:0:[116.0,163.1,160.0,164.3,3.3,15.1,51.1,24.1,70.1]:: r(v2,v1) -> r(v0,v5)
% 0.61/0.63 === Backtracking. Learning clause 168:2:0:[117.2,166.2,63.2,167.3,3.3,6.1,21.1,24.1,165.1,162.1]:: r(v0,v4),r(v0,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 171:2:0:[116.0,169.1,160.0,170.3,3.3,11.1,36.1,24.1,65.1]:: r(v2,v1) -> r(v0,v4)
% 0.61/0.63 === Backtracking. Learning clause 174:1:0:[137.1,172.1,85.1,173.2,3.3,6.1,21.1,24.1,171.1,168.1]:: r(v0,v3) ->
% 0.61/0.63 === Backtracking. Learning clause 178:1:0:[116.0,175.1,174.0,176.2,160.0,177.3,3.3,8.1,28.1,24.1,87.1]:: r(v2,v1) ->
% 0.61/0.63
% 0.61/0.63 SZS status Unsatisfiable
% 0.61/0.63
% 0.61/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.63
% 0.61/0.63 SPASS-SCL-FOL Statistics:
% 0.61/0.63 Number of learned clauses: 99
% 0.61/0.63 Number of propagations: 2321
% 0.61/0.63 Number of decisions: 607
% 0.61/0.63 Number of resolutions: 418
% 0.61/0.63 Number of condensations: 0
% 0.61/0.63 Number of sub resolutions: 53
% 0.61/0.63 Number of input literals (deduplicated): 17
% 0.61/0.63 Number of grows: 0
% 0.61/0.63 Number of considered ground atoms: 42
% 0.61/0.63
% 0.61/0.63 Needed: 0:00:00.05
% 0.61/0.63
%------------------------------------------------------------------------------