%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP008+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 : n021.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:00 PM UTC 2026
% Result : CounterSatisfiable 146.09s 29.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NLP008+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.10 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.29 % Computer : n021.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8042.1875MB
% 0.12/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Thu May 7 12:44:13 EDT 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.29 SPASS-SCL-FOL version:
% 0.12/0.34 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 146.09/29.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63 Execution resolution_1 ended with status: satisfiable
% 146.09/29.63 Used heuristic: resolution_1
% 146.09/29.63
% 146.09/29.63 Input Clauses:
% 146.09/29.63
% 146.09/29.63 Predicates: seat furniture front hollywood city event street way lonely chevy car white dirty old barrel down in = fellow man young ren1 ren2
% 146.09/29.63 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19
% 146.09/29.63 Fol Functions:
% 146.09/29.63 Problem Properties:
% 146.09/29.63 This is a Bernays Schoenfinkel Ramsey problem.
% 146.09/29.63
% 146.09/29.63
% 146.09/29.63 Reduced Input Clauses:
% 146.09/29.63
% 146.09/29.63 Most General Atoms: ren1 hollywood(x1) city(x1) event(x2) seat(x5) furniture(x5) front(x5) ren2 street(x3) way(x3) lonely(x3) chevy(x4) car(x4) white(x4) dirty(x4) old(x4) barrel(x2,x4) down(x2,x3) fellow(x5) man(x5) young(x5) in(x8,x0) =(x5,x6)
% 146.09/29.63
% 146.09/29.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_1 ===
% 146.09/29.63
% 146.09/29.63 === Backtracking. Learning clause 69:25:8:[22.0,63.20,23.0,64.21,24.0,65.22,19.0,66.23,20.0,67.24,21.0,68.25,29.31,18.1]:TopTopTopTopTopTopTopTop: seat(x0),furniture(x0),front(x0),hollywood(x1),city(x1),event(x2),chevy(x3),car(x3),white(x3),dirty(x3),old(x3),street(x4),way(x4),lonely(x4),barrel(x2,x3),down(x2,x4),in(x2,x1),seat(x5),furniture(x5),front(x5),=(skc7,x6),in(x6,x5),=(skc6,x7),in(x7,x0) -> ren1
% 146.09/29.63 === Backtracking. Learning clause 70:41:11:[61.24,25.1,29.29]:TopTopTopTopTopTopTopTopTopTopTop: seat(x0),furniture(x0),front(x0),fellow(x1),man(x1),young(x1),in(skc6,x0),=(x1,x2),in(x2,x0),seat(x3),furniture(x3),front(x3),hollywood(x4),city(x4),event(x5),chevy(x6),car(x6),white(x6),dirty(x6),old(x6),street(x7),way(x7),lonely(x7),barrel(x5,x6),down(x5,x7),in(x5,x4),seat(x8),furniture(x8),front(x8),fellow(x9),man(x9),young(x9),fellow(skc8),man(skc8),young(skc8),=(x9,x10),in(x10,x8),in(x1,x3) -> ren2,=(x9,skc8),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 71:2:0:TAUT:: =(skc1,skc8) -> =(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 72:3:0:TAUT:: =(skc1,skc8),man(skc8) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 73:1:0:TAUT:: -> =(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 74:3:0:TAUT:: =(skc1,skc8),fellow(skc8) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 75:3:0:TAUT:: =(skc1,skc8),young(skc1) -> young(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 76:3:0:TAUT:: =(skc7,skc1),fellow(skc7) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 77:3:0:TAUT:: =(skc1,skc9),fellow(skc1) -> fellow(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 78:3:0:TAUT:: =(skc1,skc9),young(skc1) -> young(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 79:3:0:TAUT:: =(skc1,skc9),fellow(skc9) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 80:3:0:TAUT:: =(skc1,skc9),young(skc9) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 81:3:0:TAUT:: =(skc7,skc1),young(skc7) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 82:2:0:TAUT:: =(skc8,skc1) -> =(skc1,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc1,skc8),fellow(skc1) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc6,skc1),fellow(skc1) -> fellow(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc6,skc1),fellow(skc6) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 86:3:0:TAUT:: =(skc8,skc6),fellow(skc6) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc8,skc6),young(skc6) -> young(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc7,skc6),fellow(skc7) -> fellow(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 89:3:0:TAUT:: =(skc8,skc6),man(skc6) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 90:3:0:TAUT:: =(skc7,skc1),in(skc1,skc1) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 91:4:0:TAUT:: =(skc6,skc1),=(skc1,skc8),man(skc6) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc7,skc1),=(skc7,skc6) -> =(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 89:3:0:TAUT:: =(skc8,skc6),man(skc6) -> man(skc8) {}
% 146.09/29.63 === Backtracking. Learning clause 94:2:0:[20.0,93.0,89.1,25.1]:: -> man(skc8),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc9,skc7),fellow(skc7) -> fellow(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 96:3:0:TAUT:: =(skc7,skc1),man(skc7) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 97:3:0:TAUT:: =(skc6,skc1),man(skc6) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 87:3:0:TAUT:: =(skc8,skc6),young(skc6) -> young(skc8) {}
% 146.09/29.63 === Backtracking. Learning clause 99:2:0:[21.0,98.0,87.1,25.1]:: -> young(skc8),ren1
% 146.09/29.63 === Conflict found: 86:3:0:TAUT:: =(skc8,skc6),fellow(skc6) -> fellow(skc8) {}
% 146.09/29.63 === Backtracking. Learning clause 101:2:0:[19.0,100.0,86.1,25.1]:: -> fellow(skc8),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 102:3:0:TAUT:: =(skc9,skc7),man(skc7) -> man(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 103:4:0:TAUT:: =(skc16,skc1),=(skc1,skc9),fellow(skc16) -> fellow(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 104:4:0:TAUT:: =(skc15,skc1),=(skc6,skc1),man(skc15) -> man(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc1,skc9),man(skc9) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 106:1:0:TAUT:: -> =(skc16,skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc1,skc8),young(skc8) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc6,skc1),man(skc1) -> man(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 109:4:0:TAUT:: =(skc1,skc8),=(skc7,skc1),fellow(skc8) -> fellow(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 110:2:0:TAUT:: =(skc9,skc1) -> =(skc1,skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc15,skc1),fellow(skc15) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 112:3:0:TAUT:: =(skc1,skc8),man(skc1) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 102:3:0:TAUT:: =(skc9,skc7),man(skc7) -> man(skc9) {}
% 146.09/29.63 === Backtracking. Learning clause 114:2:0:[23.0,113.0,102.1,27.1]:: -> man(skc9),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 115:3:0:TAUT:: =(skc9,skc7),young(skc7) -> young(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 115:3:0:TAUT:: =(skc9,skc7),young(skc7) -> young(skc9) {}
% 146.09/29.63 === Backtracking. Learning clause 117:2:0:[24.0,116.0,115.1,27.1]:: -> young(skc9),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 118:3:0:TAUT:: =(skc15,skc1),man(skc15) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 119:3:0:TAUT:: =(skc16,skc1),fellow(skc16) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 120:3:0:TAUT:: =(skc6,skc1),=(skc8,skc6) -> =(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 95:3:0:TAUT:: =(skc9,skc7),fellow(skc7) -> fellow(skc9) {}
% 146.09/29.63 === Backtracking. Learning clause 122:2:0:[22.0,121.0,95.1,27.1]:: -> fellow(skc9),ren1
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 123:1:0:TAUT:: -> =(skc15,skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 124:1:0:TAUT:: -> =(skc7,skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 125:3:0:TAUT:: =(skc6,skc1),=(skc7,skc1) -> =(skc7,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 126:3:0:TAUT:: =(skc7,skc6),fellow(skc6) -> fellow(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 127:1:0:TAUT:: -> =(skc9,skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 125:3:0:TAUT:: =(skc6,skc1),=(skc7,skc1) -> =(skc7,skc6) {}
% 146.09/29.63 === Backtracking. Learning clause 128:3:0:[125.3,18.1]:: =(skc6,skc1),=(skc7,skc1) -> ren1
% 146.09/29.63 === Conflict found: 120:3:0:TAUT:: =(skc6,skc1),=(skc8,skc6) -> =(skc8,skc1) {}
% 146.09/29.63 === Backtracking. Learning clause 129:3:0:[120.2,25.1,82.1]:: =(skc6,skc1) -> ren1,=(skc1,skc8)
% 146.09/29.63 === CC is in false state. New clause to be learned: 130:3:0:TAUT:: =(skc7,skc1),=(skc9,skc7) -> =(skc9,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 131:3:0:TAUT:: =(skc1,skc9),man(skc1) -> man(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 132:3:0:TAUT:: =(skc16,skc1),man(skc16) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 133:1:0:TAUT:: -> =(skc6,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 134:3:0:TAUT:: =(skc16,skc15),fellow(skc15) -> fellow(skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 135:3:0:TAUT:: =(skc8,skc6),fellow(skc8) -> fellow(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 136:1:0:TAUT:: -> =(skc8,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 137:4:0:TAUT:: =(skc8,skc6),=(skc1,skc8),=(skc7,skc1) -> =(skc7,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Clause set with instances from active satisfied. Growing active. New size: 89
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 138:3:0:TAUT:: =(skc1,skc6),man(skc6) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 139:3:0:TAUT:: =(skc1,skc7),man(skc7) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 140:3:0:TAUT:: =(skc1,skc7),fellow(skc7) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 141:3:0:TAUT:: =(skc1,skc6),young(skc6) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 142:3:0:TAUT:: =(skc1,skc6),man(skc1) -> man(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 143:3:0:TAUT:: =(skc1,skc15),fellow(skc1) -> fellow(skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 144:3:0:TAUT:: =(skc1,skc16),fellow(skc16) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 145:3:0:TAUT:: =(skc1,skc18),fellow(skc1) -> fellow(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 146:3:0:TAUT:: =(skc1,skc18),fellow(skc18) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 147:3:0:TAUT:: =(skc1,skc15),man(skc15) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 148:3:0:TAUT:: =(skc1,skc19),in(skc1,skc1) -> in(skc19,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 149:3:0:TAUT:: =(skc1,skc16),young(skc16) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 150:4:0:TAUT:: =(skc8,skc6),=(skc16,skc8),in(skc6,skc1) -> in(skc16,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 151:3:0:TAUT:: =(skc1,skc16),man(skc16) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 152:4:0:TAUT:: =(skc1,skc8),=(skc1,skc6),in(skc8,skc1) -> in(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 153:3:0:TAUT:: =(skc1,skc7),fellow(skc1) -> fellow(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 154:3:0:TAUT:: =(skc1,skc15),young(skc15) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 155:3:0:TAUT:: =(skc8,skc6),=(skc7,skc8) -> =(skc7,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 156:3:0:TAUT:: =(skc1,skc6),fellow(skc6) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 157:4:0:TAUT:: =(skc1,skc6),=(skc1,skc16),fellow(skc6) -> fellow(skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 158:3:0:TAUT:: =(skc1,skc18),man(skc18) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 159:3:0:TAUT:: =(skc7,skc8),young(skc8) -> young(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 160:3:0:TAUT:: =(skc9,skc7),fellow(skc9) -> fellow(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 161:3:0:TAUT:: =(skc7,skc8),fellow(skc7) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 162:3:0:TAUT:: =(skc7,skc8),in(skc8,skc1) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 163:3:0:TAUT:: =(skc1,skc19),fellow(skc1) -> fellow(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 164:3:0:TAUT:: =(skc1,skc19),young(skc1) -> young(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 165:3:0:TAUT:: =(skc1,skc18),young(skc1) -> young(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 166:3:0:TAUT:: =(skc1,skc7),man(skc1) -> man(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 167:2:0:TAUT:: =(skc18,skc1) -> =(skc1,skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 168:3:0:TAUT:: =(skc1,skc16),fellow(skc1) -> fellow(skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 169:3:0:TAUT:: =(skc1,skc7),in(skc1,skc1) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 170:3:0:TAUT:: =(skc7,skc6),man(skc6) -> man(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 171:3:0:TAUT:: =(skc8,skc6),in(skc8,skc1) -> in(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 155:3:0:TAUT:: =(skc8,skc6),=(skc7,skc8) -> =(skc7,skc6) {}
% 146.09/29.63 === Backtracking. Learning clause 173:2:0:[18.0,172.1,155.1,25.1]:: =(skc7,skc8) -> ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 174:3:0:TAUT:: =(skc9,skc8),=(skc9,skc7) -> =(skc7,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 171:3:0:TAUT:: =(skc8,skc6),in(skc8,skc1) -> in(skc6,skc1) {}
% 146.09/29.63 === Backtracking. Learning clause 175:2:0:[171.1,25.1,26.1]:: -> in(skc6,skc1),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 176:4:0:TAUT:: =(skc8,skc6),=(skc15,skc8),in(skc6,skc1) -> in(skc15,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 177:3:0:TAUT:: =(skc9,skc7),in(skc9,skc1) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 178:2:0:TAUT:: =(skc7,skc1) -> =(skc1,skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 179:4:0:TAUT:: =(skc8,skc6),=(skc18,skc8),fellow(skc6) -> fellow(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 180:3:0:TAUT:: =(skc1,skc15),fellow(skc15) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 181:3:0:TAUT:: =(skc1,skc9),in(skc9,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 182:3:0:TAUT:: =(skc1,skc18),in(skc18,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 177:3:0:TAUT:: =(skc9,skc7),in(skc9,skc1) -> in(skc7,skc1) {}
% 146.09/29.63 === Backtracking. Learning clause 183:2:0:[177.1,27.1,28.1]:: -> in(skc7,skc1),ren1
% 146.09/29.63 === CC is in false state. New clause to be learned: 184:4:0:TAUT:: =(skc8,skc6),=(skc18,skc8),in(skc6,skc1) -> in(skc18,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 185:3:0:TAUT:: =(skc9,skc8),fellow(skc8) -> fellow(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 186:2:0:TAUT:: =(skc15,skc1) -> =(skc1,skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 187:3:0:TAUT:: =(skc1,skc9),=(skc9,skc8) -> =(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 188:3:0:TAUT:: =(skc1,skc18),=(skc18,skc15) -> =(skc15,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 189:3:0:TAUT:: =(skc1,skc7),young(skc7) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 190:3:0:TAUT:: =(skc1,skc6),in(skc6,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 191:3:0:TAUT:: =(skc1,skc8),in(skc8,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 192:3:0:TAUT:: =(skc16,skc15),man(skc16) -> man(skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 193:2:0:TAUT:: =(skc6,skc1) -> =(skc1,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 194:3:0:TAUT:: =(skc1,skc19),fellow(skc19) -> fellow(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 195:3:0:TAUT:: =(skc9,skc8),man(skc9) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 196:3:0:TAUT:: =(skc15,skc8),man(skc15) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 197:3:0:TAUT:: =(skc1,skc19),man(skc19) -> man(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 198:3:0:TAUT:: =(skc1,skc15),young(skc1) -> young(skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 199:3:0:TAUT:: =(skc7,skc6),in(skc7,skc1) -> in(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 200:3:0:TAUT:: =(skc9,skc7),man(skc9) -> man(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 201:3:0:TAUT:: =(skc18,skc15),=(skc15,skc8) -> =(skc18,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 202:3:0:TAUT:: =(skc18,skc8),man(skc8) -> man(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 203:4:0:TAUT:: =(skc8,skc6),=(skc15,skc8),man(skc6) -> man(skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 201:3:0:TAUT:: =(skc18,skc15),=(skc15,skc8) -> =(skc18,skc8) {}
% 146.09/29.63 === Backtracking. Learning clause 204:3:0:[201.1,57.1]:: =(skc15,skc8) -> =(skc18,skc8),ren2
% 146.09/29.63 === CC is in false state. New clause to be learned: 205:4:0:TAUT:: =(skc8,skc6),=(skc18,skc8),young(skc6) -> young(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 206:2:0:TAUT:: =(skc19,skc1) -> =(skc1,skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 207:3:0:TAUT:: =(skc1,skc6),fellow(skc1) -> fellow(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 208:3:0:TAUT:: =(skc15,skc8),fellow(skc15) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 209:3:0:TAUT:: =(skc16,skc8),man(skc16) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 210:3:0:TAUT:: =(skc1,skc19),man(skc1) -> man(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 211:3:0:TAUT:: =(skc1,skc18),young(skc18) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 212:3:0:TAUT:: =(skc18,skc8),fellow(skc8) -> fellow(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 213:3:0:TAUT:: =(skc18,skc15),young(skc15) -> young(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 214:3:0:TAUT:: =(skc1,skc16),young(skc1) -> young(skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 215:3:0:TAUT:: =(skc1,skc7),in(skc7,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 213:3:0:TAUT:: =(skc18,skc15),young(skc15) -> young(skc18) {}
% 146.09/29.63 === Backtracking. Learning clause 217:2:0:[53.0,216.0,213.1,57.1]:: -> young(skc18),ren2
% 146.09/29.63 === CC is in false state. New clause to be learned: 218:3:0:TAUT:: =(skc18,skc15),fellow(skc15) -> fellow(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 219:3:0:TAUT:: =(skc18,skc15),man(skc15) -> man(skc18)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 219:3:0:TAUT:: =(skc18,skc15),man(skc15) -> man(skc18) {}
% 146.09/29.63 === Backtracking. Learning clause 221:2:0:[52.0,220.0,219.1,57.1]:: -> man(skc18),ren2
% 146.09/29.63 === Conflict found: 218:3:0:TAUT:: =(skc18,skc15),fellow(skc15) -> fellow(skc18) {}
% 146.09/29.63 === Backtracking. Learning clause 223:2:0:[51.0,222.0,218.1,57.1]:: -> fellow(skc18),ren2
% 146.09/29.63 === CC is in false state. New clause to be learned: 224:3:0:TAUT:: =(skc18,skc15),in(skc18,skc1) -> in(skc15,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 224:3:0:TAUT:: =(skc18,skc15),in(skc18,skc1) -> in(skc15,skc1) {}
% 146.09/29.63 === Backtracking. Learning clause 225:3:0:[224.1,57.1]:: in(skc18,skc1) -> in(skc15,skc1),ren2
% 146.09/29.63 === CC is in false state. New clause to be learned: 226:4:0:TAUT:: =(skc8,skc6),=(skc19,skc8),in(skc6,skc1) -> in(skc19,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 227:3:0:TAUT:: =(skc19,skc8),fellow(skc8) -> fellow(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 228:3:0:TAUT:: =(skc1,skc19),young(skc19) -> young(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 229:2:0:TAUT:: =(skc1,skc18) -> =(skc18,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 230:3:0:TAUT:: =(skc16,skc8),fellow(skc16) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 231:3:0:TAUT:: =(skc7,skc6),man(skc7) -> man(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 232:3:0:TAUT:: =(skc18,skc15),in(skc15,skc1) -> in(skc18,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 233:3:0:TAUT:: =(skc15,skc8),in(skc15,skc1) -> in(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 234:3:0:TAUT:: =(skc19,skc16),=(skc16,skc8) -> =(skc19,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Conflict found: 232:3:0:TAUT:: =(skc18,skc15),in(skc15,skc1) -> in(skc18,skc1) {}
% 146.09/29.63 === Backtracking. Learning clause 235:3:0:[232.1,57.1]:: in(skc15,skc1) -> in(skc18,skc1),ren2
% 146.09/29.63 === CC is in false state. New clause to be learned: 236:3:0:TAUT:: =(skc19,skc8),man(skc19) -> man(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 237:3:0:TAUT:: =(skc7,skc8),man(skc8) -> man(skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 238:3:0:TAUT:: =(skc1,skc16),in(skc16,skc1) -> in(skc1,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 239:2:0:TAUT:: =(skc16,skc1) -> =(skc1,skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 240:3:0:TAUT:: =(skc16,skc8),in(skc8,skc1) -> in(skc16,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 241:4:0:TAUT:: =(skc1,skc16),=(skc16,skc8),=(skc8,skc6) -> =(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 242:4:0:TAUT:: =(skc8,skc6),=(skc16,skc8),fellow(skc6) -> fellow(skc16)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 243:3:0:TAUT:: =(skc19,skc16),fellow(skc16) -> fellow(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 244:3:0:TAUT:: =(skc19,skc16),young(skc16) -> young(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 245:3:0:TAUT:: =(skc16,skc15),=(skc15,skc8) -> =(skc16,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 246:4:0:TAUT:: =(skc8,skc6),=(skc15,skc8),young(skc6) -> young(skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Clause set with instances from active satisfied. Growing active. New size: 146
% 146.09/29.63 === Backtracking. Learning clause 247:2:0:[61.8,8.1,10.1,5.1,15.1,16.1,9.1,17.1,13.1,12.1,4.1,7.1,6.1,14.1,11.1,174.1,27.1,136.1,173.1,26.1,183.1,117.1,99.1,114.1,94.1,122.1,101.1,3.1,2.1,1.1]:: -> ren2,ren1
% 146.09/29.63 === Backtracking. Learning clause 248:1:0:[29.31,174.1,6.1,16.1,14.1,12.1,1.1,10.1,17.1,2.1,4.1,5.1,136.1,15.1,3.1,13.1,9.1,8.1,11.1,7.1,94.1,99.1,101.1,114.1,117.1,122.1,173.1,26.1,183.1,27.1]:: -> ren1
% 146.09/29.63 === Backtracking. Learning clause 249:1:0:[62.2,57.2,248.1]:: -> =(skc18,skc15)
% 146.09/29.63 === CC is in false state. New clause to be learned: 251:2:0:[249.0,250.1]:: =(skc18,skc8) -> =(skc15,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 252:4:0:TAUT:: =(skc7,skc8),=(skc9,skc7),young(skc9) -> young(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 253:3:0:TAUT:: =(skc9,skc8),young(skc8) -> young(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 254:3:0:TAUT:: =(skc9,skc7),in(skc7,skc1) -> in(skc9,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 255:3:0:TAUT:: =(skc7,skc8),in(skc7,skc1) -> in(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 256:3:0:TAUT:: =(skc9,skc8),fellow(skc9) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 257:3:0:TAUT:: =(skc8,skc1),=(skc8,skc6) -> =(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 258:3:0:TAUT:: =(skc19,skc1),=(skc19,skc16) -> =(skc16,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 259:3:0:TAUT:: =(skc19,skc16),in(skc16,skc1) -> in(skc19,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 260:3:0:TAUT:: =(skc19,skc8),=(skc19,skc16) -> =(skc16,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 261:3:0:TAUT:: =(skc8,skc1),=(skc7,skc1) -> =(skc7,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 262:3:0:TAUT:: =(skc6,skc1),=(skc8,skc1) -> =(skc8,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 263:3:0:TAUT:: =(skc19,skc16),in(skc19,skc1) -> in(skc16,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 264:4:0:TAUT:: =(skc8,skc17),=(skc8,skc2),furniture(skc17) -> furniture(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 265:5:0:TAUT:: =(skc8,skc2),=(skc7,skc8),=(skc9,skc7),young(skc9) -> young(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 266:3:0:TAUT:: =(skc8,skc1),=(skc7,skc8) -> =(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 267:4:0:TAUT:: =(skc8,skc6),=(skc7,skc6),=(skc9,skc7) -> =(skc9,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 268:3:0:TAUT:: =(skc1,skc2),seat(skc2) -> seat(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 269:3:0:TAUT:: =(skc8,skc6),in(skc6,skc1) -> in(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 270:4:0:TAUT:: =(skc7,skc17),=(skc7,skc1),furniture(skc17) -> furniture(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 271:3:0:TAUT:: =(skc8,skc2),=(skc8,skc1) -> =(skc1,skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 272:3:0:TAUT:: =(skc19,skc16),man(skc16) -> man(skc19)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 273:3:0:TAUT:: =(skc18,skc8),in(skc8,skc1) -> in(skc18,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 274:4:0:TAUT:: =(skc8,skc17),=(skc8,skc1),front(skc17) -> front(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 275:4:0:TAUT:: =(skc8,skc1),=(skc8,skc2),furniture(skc1) -> furniture(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 276:4:0:TAUT:: =(skc7,skc8),=(skc9,skc7),fellow(skc9) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 277:4:0:TAUT:: =(skc8,skc17),=(skc8,skc1),seat(skc17) -> seat(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 278:3:0:TAUT:: =(skc7,skc8),=(skc9,skc8) -> =(skc9,skc7)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 279:2:0:TAUT:: =(skc1,skc9) -> =(skc9,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 280:3:0:TAUT:: =(skc1,skc2),front(skc2) -> front(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 281:4:0:TAUT:: =(skc8,skc1),=(skc8,skc6),=(skc7,skc6) -> =(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 283:4:0:[249.0,282.0]:: =(skc19,skc16),=(skc19,skc1),=(skc18,skc1) -> =(skc16,skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 284:3:0:TAUT:: =(skc8,skc6),man(skc8) -> man(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 285:3:0:TAUT:: =(skc8,skc1),in(skc1,skc1) -> in(skc8,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 286:3:0:TAUT:: =(skc7,skc6),in(skc6,skc1) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 287:5:0:TAUT:: =(skc7,skc1),=(skc7,skc17),=(skc8,skc17),=(skc8,skc6) -> =(skc1,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 288:4:0:TAUT:: =(skc19,skc16),=(skc19,skc1),=(skc15,skc1) -> =(skc16,skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 289:3:0:TAUT:: =(skc1,skc6),=(skc7,skc1) -> =(skc7,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 290:3:0:TAUT:: =(skc1,skc2),lonely(skc2) -> lonely(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 291:3:0:TAUT:: =(skc1,skc2),=(skc8,skc1) -> =(skc8,skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 292:4:0:TAUT:: =(skc8,skc1),=(skc8,skc2),street(skc1) -> street(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 293:4:0:TAUT:: =(skc8,skc1),=(skc1,skc2),young(skc8) -> young(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 295:3:0:[249.0,294.0]:: =(skc18,skc1),=(skc1,skc16) -> =(skc16,skc15)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 296:5:0:TAUT:: =(skc8,skc6),=(skc1,skc2),=(skc6,skc1),fellow(skc8) -> fellow(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 297:3:0:TAUT:: =(skc1,skc2),front(skc1) -> front(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 298:4:0:TAUT:: =(skc8,skc2),=(skc8,skc1),city(skc2) -> city(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 299:3:0:TAUT:: =(skc8,skc6),young(skc8) -> young(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 300:3:0:TAUT:: =(skc8,skc6),=(skc7,skc6) -> =(skc7,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 301:4:0:TAUT:: =(skc7,skc8),=(skc9,skc7),man(skc8) -> man(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 302:3:0:TAUT:: =(skc7,skc6),young(skc7) -> young(skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 303:3:0:TAUT:: =(skc19,skc16),in(skc19,skc10) -> in(skc16,skc10)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 304:3:0:TAUT:: =(skc18,skc8),young(skc18) -> young(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 305:4:0:TAUT:: =(skc6,skc17),=(skc6,skc2),seat(skc17) -> seat(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 306:4:0:TAUT:: =(skc8,skc1),=(skc8,skc2),old(skc1) -> old(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 308:4:0:[249.0,307.2]:: =(skc6,skc1),=(skc15,skc1),in(skc18,skc1) -> in(skc6,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 309:4:0:TAUT:: =(skc7,skc8),=(skc9,skc7),young(skc8) -> young(skc9)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 310:3:0:TAUT:: =(skc6,skc2),=(skc8,skc6) -> =(skc8,skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 311:3:0:TAUT:: =(skc8,skc2),fellow(skc2) -> fellow(skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 313:2:0:[249.0,312.1]:: =(skc15,skc1) -> =(skc18,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 314:3:0:TAUT:: =(skc1,skc2),furniture(skc1) -> furniture(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 315:4:0:TAUT:: =(skc8,skc2),=(skc8,skc17),seat(skc17) -> seat(skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 316:3:0:TAUT:: =(skc7,skc8),=(skc9,skc7) -> =(skc9,skc8)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 317:3:0:TAUT:: =(skc6,skc17),=(skc7,skc6) -> =(skc7,skc17)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 318:5:0:TAUT:: =(skc8,skc2),=(skc8,skc1),=(skc7,skc8),in(skc1,skc2) -> in(skc7,skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 319:3:0:TAUT:: =(skc8,skc1),in(skc1,skc2) -> in(skc8,skc2)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC model inconsistency. New clause to be learned: 321:2:0:[249.0,320.0]:: in(skc18,skc17) -> in(skc15,skc17)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === CC is in false state. New clause to be learned: 322:3:0:TAUT:: =(skc6,skc2),=(skc8,skc2) -> =(skc8,skc6)
% 146.09/29.63 === Restarting.
% 146.09/29.63 === Clause set with instances from active satisfied. Growing active. New size: 188
% 146.09/29.63 === CC is in false state. New clause to be learned: 323:3:0:TAUT:: =(skc1,skc3),hollywood(skc3) -> hollywood(skc1)
% 146.09/29.63 === Restarting.
% 146.09/29.63
% 146.09/29.63 Linear Model Building succeeded.
% 146.09/29.63 SZS status Satisfiable
% 146.09/29.63
% 146.09/29.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 146.09/29.63
% 146.09/29.63 SPASS-SCL-FOL Statistics:
% 146.09/29.63 Number of learned clauses: 22
% 146.09/29.63 Number of propagations: 8732
% 146.09/29.63 Number of decisions: 9142
% 146.09/29.63 Number of resolutions: 83
% 146.09/29.63 Number of condensations: 1
% 146.09/29.63 Number of sub resolutions: 22
% 146.09/29.63 Number of input literals (deduplicated): 82
% 146.09/29.63 Number of grows: 3
% 146.09/29.63 Number of considered ground atoms: 188
% 146.09/29.63
% 146.09/29.63 Needed: 0:0:29.22
% 146.09/29.63
%------------------------------------------------------------------------------