%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP009+1 : TPTP v9.2.1. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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:29:01 PM UTC 2026
% Result : Theorem 4.66s 1.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP009+1 : TPTP v9.2.1. Released v2.4.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.34 % Computer : n002.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Thu May 7 12:43:32 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.66/1.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63 Execution lmodel_grow ended with status: unsatisfiable
% 4.66/1.63 Used heuristic: lmodel_grow
% 4.66/1.63
% 4.66/1.63 Input Clauses:
% 4.66/1.63
% 4.66/1.63 Predicates: hollywood city event street way lonely chevy car white dirty old barrel down in seat furniture front = fellow man young ren1 ren2
% 4.66/1.63 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18
% 4.66/1.63 Fol Functions:
% 4.66/1.63 Problem Properties:
% 4.66/1.63 This is a Bernays Schoenfinkel Ramsey problem.
% 4.66/1.63
% 4.66/1.63
% 4.66/1.63 Reduced Input Clauses:
% 4.66/1.63
% 4.66/1.63 Most General Atoms: ren1 hollywood(x0) city(x0) event(x1) seat(x4) furniture(x4) front(x4) fellow(x6) man(x6) young(x6) in(x8,x4) =(x5,x6) ren2 street(x2) way(x2) lonely(x2) chevy(x3) car(x3) white(x3) dirty(x3) old(x3) barrel(x1,x3) down(x1,x2)
% 4.66/1.63
% 4.66/1.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1604 atoms initially, heuristics mode: lmodel_grow ===
% 4.66/1.63
% 4.66/1.63 === CC is in false state. New clause to be learned: 60:3:0:TAUT:: =(skc1,skc9),in(skc2,skc1) -> in(skc2,skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 61:4:0:TAUT:: =(skc7,skc5),=(skc14,skc5),barrel(skc14,skc7) -> barrel(skc7,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 62:3:0:TAUT:: =(skc8,skc7),barrel(skc7,skc1) -> barrel(skc8,skc1)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 63:3:0:TAUT:: =(skc15,skc10),barrel(skc15,skc5) -> barrel(skc10,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 64:2:0:TAUT:: =(skc5,skc6) -> =(skc6,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 65:2:0:TAUT:: =(skc14,skc16) -> =(skc16,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 66:3:0:TAUT:: =(skc11,skc2),in(skc2,skc11) -> in(skc11,skc2)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 67:4:0:TAUT:: =(skc4,skc15),=(skc15,skc14),white(skc4) -> white(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 68:2:0:TAUT:: =(skc8,skc15) -> =(skc15,skc8)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 69:5:0:TAUT:: =(skc9,skc13),=(skc10,skc9),=(skc10,skc1),chevy(skc13) -> chevy(skc1)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 70:4:0:TAUT:: =(skc3,skc13),=(skc13,skc14),barrel(skc14,skc3) -> barrel(skc3,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 71:3:0:TAUT:: =(skc15,skc10),barrel(skc16,skc10) -> barrel(skc16,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 72:4:0:TAUT:: =(skc8,skc5),=(skc3,skc10),barrel(skc3,skc8) -> barrel(skc10,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 73:4:0:TAUT:: =(skc12,skc8),=(skc18,skc8),barrel(skc15,skc18) -> barrel(skc15,skc12)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 74:1:0:TAUT:: -> =(skc17,skc17)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 75:3:0:TAUT:: =(skc9,skc16),front(skc16) -> front(skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 76:3:0:TAUT:: =(skc18,skc15),=(skc18,skc1) -> =(skc1,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 77:3:0:TAUT:: =(skc17,skc16),barrel(skc17,skc18) -> barrel(skc16,skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 78:1:0:TAUT:: -> =(skc15,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 79:3:0:TAUT:: =(skc7,skc8),barrel(skc7,skc17) -> barrel(skc8,skc17)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 80:3:0:TAUT:: =(skc17,skc5),fellow(skc5) -> fellow(skc17)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 81:4:0:TAUT:: =(skc17,skc6),=(skc8,skc17),=(skc8,skc5) -> =(skc5,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 82:5:0:TAUT:: =(skc14,skc15),=(skc8,skc14),=(skc8,skc11),car(skc15) -> car(skc11)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc16,skc13),lonely(skc13) -> lonely(skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 84:6:0:TAUT:: =(skc13,skc9),=(skc15,skc9),=(skc3,skc11),=(skc3,skc15),in(skc9,skc15) -> in(skc11,skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc7,skc9),=(skc15,skc7) -> =(skc9,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 86:4:0:TAUT:: =(skc7,skc8),=(skc11,skc8),seat(skc7) -> seat(skc11)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc10,skc8),barrel(skc16,skc8) -> barrel(skc16,skc10)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 88:1:0:TAUT:: -> =(skc2,skc2)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 89:2:0:TAUT:: =(skc18,skc15) -> =(skc15,skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 90:1:0:TAUT:: -> =(skc7,skc7)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 91:5:0:TAUT:: =(skc18,skc2),=(skc2,skc1),=(skc1,skc8),street(skc18) -> street(skc8)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 92:2:0:TAUT:: =(skc17,skc14) -> =(skc14,skc17)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === Backtracking. Learning clause 93:1:0:[58.2,31.1,42.1,89.2,56.1,92.2,38.1,35.1,30.1,44.1,49.1,52.1,50.1,48.1,46.1,37.1,53.1,43.1,41.1,47.1,36.1,40.1,57.1,45.1,55.1,33.1,51.1,54.1,39.1,32.1,34.1,59.2,20.2]:: -> man(skc5)
% 4.66/1.63 === CC is in false state. New clause to be learned: 94:3:0:TAUT:: =(skc15,skc14),young(skc14) -> young(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 95:2:0:TAUT:: =(skc15,skc18) -> =(skc18,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 96:2:0:TAUT:: =(skc14,skc17) -> =(skc17,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 97:3:0:TAUT:: =(skc15,skc14),fellow(skc15) -> fellow(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 98:3:0:TAUT:: =(skc15,skc14),man(skc14) -> man(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 99:3:0:TAUT:: =(skc15,skc14),man(skc15) -> man(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 100:3:0:TAUT:: =(skc9,skc6),fellow(skc6) -> fellow(skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 101:5:0:TAUT:: =(skc9,skc6),=(skc9,skc15),=(skc15,skc14),fellow(skc6) -> fellow(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 102:1:0:TAUT:: -> =(skc3,skc3)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 103:2:0:TAUT:: =(skc1,skc12) -> =(skc12,skc1)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 104:5:0:TAUT:: =(skc9,skc16),=(skc14,skc1),=(skc14,skc17),in(skc17,skc16) -> in(skc1,skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 105:1:0:TAUT:: -> =(skc16,skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 106:2:0:TAUT:: =(skc18,skc12) -> =(skc12,skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc7,skc16),furniture(skc7) -> furniture(skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 108:5:0:TAUT:: =(skc13,skc10),=(skc13,skc5),=(skc5,skc18),in(skc10,skc5) -> in(skc18,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 109:4:0:TAUT:: =(skc4,skc6),=(skc8,skc5),down(skc5,skc6) -> down(skc8,skc4)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 110:4:0:TAUT:: =(skc9,skc6),=(skc14,skc9),young(skc6) -> young(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc15,skc14),fellow(skc14) -> fellow(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 112:4:0:TAUT:: =(skc17,skc12),=(skc8,skc5),in(skc5,skc17) -> in(skc8,skc12)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 113:4:0:TAUT:: =(skc17,skc7),=(skc17,skc14),=(skc15,skc14) -> =(skc7,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 114:4:0:TAUT:: =(skc5,skc18),=(skc15,skc18),young(skc5) -> young(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 115:3:0:TAUT:: =(skc3,skc13),way(skc3) -> way(skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 116:5:0:TAUT:: =(skc9,skc6),=(skc8,skc5),=(skc8,skc2),in(skc5,skc9) -> in(skc2,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 117:1:0:TAUT:: -> =(skc4,skc4)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 118:5:0:TAUT:: =(skc15,skc14),=(skc16,skc17),=(skc14,skc17),seat(skc15) -> seat(skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 119:5:0:TAUT:: =(skc12,skc14),=(skc17,skc13),=(skc17,skc14),old(skc12) -> old(skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 120:3:0:TAUT:: =(skc18,skc6),young(skc6) -> young(skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 121:2:0:TAUT:: =(skc9,skc14) -> =(skc14,skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 122:3:0:TAUT:: =(skc12,skc16),chevy(skc16) -> chevy(skc12)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 123:3:0:TAUT:: =(skc8,skc5),fellow(skc5) -> fellow(skc8)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 124:4:0:TAUT:: =(skc15,skc14),=(skc18,skc15),=(skc9,skc18) -> =(skc9,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 125:3:0:TAUT:: =(skc18,skc15),=(skc18,skc8) -> =(skc8,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 126:7:0:TAUT:: =(skc8,skc5),=(skc17,skc14),=(skc1,skc17),=(skc12,skc1),=(skc8,skc12),young(skc5) -> young(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 127:1:0:TAUT:: -> =(skc14,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 128:3:0:TAUT:: =(skc5,skc15),young(skc5) -> young(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 129:3:0:TAUT:: =(skc17,skc14),man(skc17) -> man(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 130:3:0:TAUT:: =(skc18,skc17),in(skc17,skc16) -> in(skc18,skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 131:4:0:TAUT:: =(skc9,skc6),=(skc9,skc15),young(skc6) -> young(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 132:3:0:TAUT:: =(skc1,skc3),=(skc1,skc7) -> =(skc7,skc3)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 133:3:0:TAUT:: =(skc9,skc6),young(skc6) -> young(skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 134:3:0:TAUT:: =(skc4,skc12),car(skc4) -> car(skc12)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 135:5:0:TAUT:: =(skc17,skc14),=(skc11,skc17),=(skc17,skc12),in(skc12,skc14) -> in(skc17,skc11)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 136:5:0:TAUT:: =(skc15,skc14),=(skc4,skc14),=(skc4,skc2),barrel(skc2,skc4) -> barrel(skc15,skc4)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 137:3:0:TAUT:: =(skc13,skc4),down(skc11,skc4) -> down(skc11,skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 138:3:0:TAUT:: =(skc15,skc14),young(skc15) -> young(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 139:5:0:TAUT:: =(skc4,skc9),=(skc6,skc7),=(skc9,skc6),in(skc4,skc3) -> in(skc7,skc3)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 140:4:0:TAUT:: =(skc15,skc14),=(skc14,skc17),in(skc15,skc16) -> in(skc17,skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 141:5:0:TAUT:: =(skc16,skc9),=(skc9,skc6),=(skc18,skc17),barrel(skc18,skc16) -> barrel(skc17,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 142:4:0:TAUT:: =(skc14,skc17),=(skc18,skc15),in(skc15,skc14) -> in(skc18,skc17)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 143:3:0:TAUT:: =(skc13,skc4),car(skc4) -> car(skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 144:3:0:TAUT:: =(skc14,skc17),young(skc17) -> young(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 145:3:0:TAUT:: =(skc2,skc16),in(skc2,skc1) -> in(skc16,skc1)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 146:3:0:TAUT:: =(skc14,skc17),barrel(skc17,skc7) -> barrel(skc14,skc7)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 147:6:0:TAUT:: =(skc17,skc14),=(skc15,skc14),=(skc13,skc18),=(skc18,skc15),way(skc17) -> way(skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 148:3:0:TAUT:: =(skc8,skc5),in(skc8,skc7) -> in(skc5,skc7)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 149:4:0:TAUT:: =(skc9,skc6),=(skc16,skc9),in(skc16,skc5) -> in(skc6,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 150:4:0:TAUT:: =(skc6,skc7),=(skc9,skc6),front(skc7) -> front(skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 151:4:0:TAUT:: =(skc14,skc17),=(skc1,skc2),down(skc2,skc17) -> down(skc1,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 152:3:0:TAUT:: =(skc18,skc3),way(skc3) -> way(skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 153:3:0:TAUT:: =(skc8,skc5),in(skc8,skc15) -> in(skc5,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 154:4:0:TAUT:: =(skc2,skc5),=(skc8,skc5),barrel(skc2,skc4) -> barrel(skc8,skc4)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 155:3:0:TAUT:: =(skc17,skc14),barrel(skc17,skc14) -> barrel(skc14,skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 156:3:0:TAUT:: =(skc11,skc6),=(skc11,skc5) -> =(skc5,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 157:5:0:TAUT:: =(skc10,skc15),=(skc10,skc16),=(skc16,skc17),=(skc17,skc14) -> =(skc14,skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 158:5:0:TAUT:: =(skc14,skc4),=(skc15,skc13),=(skc15,skc14),old(skc4) -> old(skc13)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 159:3:0:TAUT:: =(skc18,skc15),fellow(skc18) -> fellow(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 160:4:0:TAUT:: =(skc17,skc14),=(skc2,skc17),in(skc14,skc18) -> in(skc2,skc18)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 161:3:0:TAUT:: =(skc9,skc6),in(skc9,skc7) -> in(skc6,skc7)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 162:4:0:TAUT:: =(skc2,skc9),=(skc9,skc6),barrel(skc2,skc4) -> barrel(skc6,skc4)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 163:3:0:TAUT:: =(skc9,skc6),=(skc9,skc5) -> =(skc5,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 164:3:0:TAUT:: =(skc6,skc16),chevy(skc16) -> chevy(skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 165:1:0:TAUT:: -> =(skc10,skc10)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 166:5:0:TAUT:: =(skc9,skc6),=(skc10,skc6),=(skc17,skc14),down(skc14,skc10) -> down(skc17,skc9)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 167:4:0:TAUT:: =(skc9,skc6),=(skc3,skc6),=(skc3,skc5) -> =(skc9,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 168:3:0:TAUT:: =(skc5,skc14),young(skc5) -> young(skc14)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 169:3:0:TAUT:: =(skc9,skc6),down(skc9,skc5) -> down(skc6,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 170:4:0:TAUT:: =(skc9,skc13),=(skc12,skc13),in(skc9,skc7) -> in(skc12,skc7)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 171:5:0:TAUT:: =(skc17,skc14),=(skc15,skc14),=(skc18,skc15),in(skc18,skc16) -> in(skc17,skc16)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 172:5:0:TAUT:: =(skc8,skc5),=(skc18,skc15),=(skc15,skc14),barrel(skc14,skc8) -> barrel(skc18,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 173:3:0:TAUT:: =(skc15,skc18),man(skc18) -> man(skc15)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 174:4:0:TAUT:: =(skc8,skc5),=(skc4,skc14),down(skc14,skc5) -> down(skc4,skc8)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 175:1:0:TAUT:: -> =(skc6,skc6)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === CC is in false state. New clause to be learned: 176:1:0:TAUT:: -> =(skc5,skc5)
% 4.66/1.63 === Restarting.
% 4.66/1.63 === Backtracking. Learning clause 180:1:0:[93.0,177.0,175.0,178.1,176.0,179.2,29.25,161.3,17.1,21.1,10.1,18.1,27.1,15.1,23.1,9.1,14.1,6.1,19.1,1.1,16.1,148.3,24.1,8.1,28.1,25.1,22.1,11.1,26.1,2.1,12.1,7.1,13.1,5.1,4.1,3.1,59.1,41.2]:: -> barrel(skc11,skc12)
% 4.66/1.63 === Conflict found: 92:2:0:TAUT:: =(skc17,skc14) -> =(skc14,skc17) {}
% 4.66/1.63 === Backtracking. Learning clause 182:1:0:[41.0,181.0,92.2,58.26,54.1,53.1,45.1,34.1,50.1,89.2,35.1,40.1,56.1,36.1,32.1,47.1,44.1,30.1,48.1,57.1,37.1,39.1,33.1,38.1,51.1,55.1,42.1,31.1,43.1,52.1,49.1,46.1]:: -> ren2
% 4.66/1.63 === CC is in false state. New clause to be learned: 183:2:0:TAUT:: =(skc8,skc5) -> =(skc5,skc8)
% 4.66/1.63 === Restarting.
% 4.66/1.63
% 4.66/1.63 SZS status Unsatisfiable
% 4.66/1.63
% 4.66/1.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.66/1.63
% 4.66/1.63 SPASS-SCL-FOL Statistics:
% 4.66/1.63 Number of learned clauses: 3
% 4.66/1.63 Number of propagations: 4643
% 4.66/1.63 Number of decisions: 5192
% 4.66/1.63 Number of resolutions: 125
% 4.66/1.63 Number of condensations: 0
% 4.66/1.63 Number of sub resolutions: 4
% 4.66/1.63 Number of input literals (deduplicated): 79
% 4.66/1.63 Number of grows: 0
% 4.66/1.63 Number of considered ground atoms: 1604
% 4.66/1.63
% 4.66/1.63 Needed: 0:00:01.06
% 4.66/1.63
%------------------------------------------------------------------------------