%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP007+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 : n020.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 : Theorem 3.48s 1.32s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP007+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.15/0.34 % Computer : n020.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 12:43:05 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 3.48/1.32 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 Execution lmodel_grow ended with status: unsatisfiable % 3.48/1.32 Used heuristic: lmodel_grow % 3.48/1.32 % 3.48/1.32 Input Clauses: % 3.48/1.32 % 3.48/1.32 Predicates: seat furniture front hollywood city event chevy car white dirty old street way lonely barrel down in = fellow man young ren1 ren2 % 3.48/1.32 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 % 3.48/1.32 Fol Functions: % 3.48/1.32 Problem Properties: % 3.48/1.32 This is a Bernays Schoenfinkel Ramsey problem. % 3.48/1.32 % 3.48/1.32 % 3.48/1.32 Reduced Input Clauses: % 3.48/1.32 % 3.48/1.32 Most General Atoms: ren1 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) seat(x5) furniture(x5) front(x5) fellow(x7) man(x7) young(x7) =(x6,x7) ren2 in(x9,x0) % 3.48/1.32 % 3.48/1.32 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1942 atoms initially, heuristics mode: lmodel_grow === % 3.48/1.32 % 3.48/1.32 === CC is in false state. New clause to be learned: 66:2:0:TAUT:: =(skc6,skc7) -> =(skc7,skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 67:4:0:TAUT:: =(skc1,skc19),=(skc20,skc7),down(skc7,skc19) -> down(skc20,skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 68:1:0:TAUT:: -> =(skc18,skc18) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 69:4:0:TAUT:: =(skc11,skc12),=(skc20,skc11),down(skc11,skc12) -> down(skc12,skc20) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 70:3:0:TAUT:: =(skc10,skc5),in(skc10,skc1) -> in(skc5,skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 71:3:0:TAUT:: =(skc9,skc6),fellow(skc6) -> fellow(skc9) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 72:3:0:TAUT:: =(skc9,skc6),down(skc8,skc6) -> down(skc8,skc9) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 73:2:0:TAUT:: =(skc4,skc20) -> =(skc20,skc4) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 74:4:0:TAUT:: =(skc6,skc18),=(skc9,skc6),down(skc9,skc6) -> down(skc6,skc18) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 75:5:0:TAUT:: =(skc15,skc6),=(skc19,skc6),=(skc19,skc16),down(skc13,skc15) -> down(skc13,skc16) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 76:3:0:TAUT:: =(skc9,skc6),in(skc9,skc8) -> in(skc6,skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 77:3:0:TAUT:: =(skc20,skc10),barrel(skc20,skc8) -> barrel(skc10,skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 78:3:0:TAUT:: =(skc3,skc1),=(skc19,skc1) -> =(skc19,skc3) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 79:3:0:TAUT:: =(skc9,skc6),young(skc6) -> young(skc9) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 80:3:0:TAUT:: =(skc15,skc1),in(skc1,skc13) -> in(skc15,skc13) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 81:3:0:TAUT:: =(skc13,skc9),barrel(skc13,skc19) -> barrel(skc9,skc19) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 82:4:0:TAUT:: =(skc7,skc11),=(skc10,skc7),down(skc10,skc7) -> down(skc11,skc11) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 83:4:0:TAUT:: =(skc20,skc17),=(skc20,skc10),down(skc17,skc20) -> down(skc10,skc17) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 84:1:0:TAUT:: -> =(skc6,skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 85:1:0:TAUT:: -> =(skc7,skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 86:4:0:TAUT:: =(skc20,skc17),=(skc3,skc20),fellow(skc17) -> fellow(skc3) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 87:2:0:TAUT:: =(skc10,skc7) -> =(skc7,skc10) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc5,skc15),barrel(skc12,skc15) -> barrel(skc12,skc5) % 3.48/1.32 === Restarting. % 3.48/1.32 === Backtracking. Learning clause 90:1:0:[84.0,89.0,32.23,27.1,2.1,19.1,12.1,13.1,25.1,3.1,16.1,23.1,21.1,76.3,15.1,6.1,18.1,87.2,31.1,9.1,4.1,7.1,30.1,29.1,11.1,26.1,5.1,1.1,24.1,22.1,10.1,17.1,28.1,14.1,8.1,20.1,65.1,58.2]:: -> man(skc17) % 3.48/1.32 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc9,skc6),in(skc6,skc8) -> in(skc9,skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc3,skc10),in(skc10,skc1) -> in(skc3,skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 93:3:0:TAUT:: =(skc7,skc10),=(skc10,skc6) -> =(skc6,skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 94:3:0:TAUT:: =(skc14,skc16),=(skc19,skc16) -> =(skc19,skc14) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc10,skc7),chevy(skc10) -> chevy(skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 96:4:0:TAUT:: =(skc1,skc16),=(skc16,skc17),=(skc11,skc17) -> =(skc11,skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 97:3:0:TAUT:: =(skc7,skc6),fellow(skc7) -> fellow(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 98:1:0:TAUT:: -> =(skc13,skc13) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 99:4:0:TAUT:: =(skc13,skc11),=(skc3,skc11),event(skc13) -> event(skc3) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 100:3:0:TAUT:: =(skc7,skc6),man(skc7) -> man(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 101:2:0:TAUT:: =(skc7,skc10) -> =(skc10,skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 102:3:0:TAUT:: =(skc17,skc15),in(skc15,skc15) -> in(skc15,skc17) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 103:4:0:TAUT:: =(skc8,skc7),=(skc7,skc1),seat(skc8) -> seat(skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 104:3:0:TAUT:: =(skc7,skc6),fellow(skc6) -> fellow(skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc8,skc1),front(skc8) -> front(skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 106:3:0:TAUT:: =(skc7,skc6),man(skc6) -> man(skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 107:1:0:TAUT:: -> =(skc20,skc20) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 108:5:0:TAUT:: =(skc19,skc16),=(skc9,skc6),=(skc19,skc9),fellow(skc16) -> fellow(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 109:3:0:TAUT:: =(skc9,skc6),=(skc19,skc6) -> =(skc19,skc9) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 110:3:0:TAUT:: =(skc7,skc6),young(skc6) -> young(skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc4,skc14),dirty(skc14) -> dirty(skc4) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 112:3:0:TAUT:: =(skc7,skc10),=(skc7,skc6) -> =(skc6,skc10) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 113:3:0:TAUT:: =(skc7,skc5),barrel(skc7,skc15) -> barrel(skc5,skc15) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 114:3:0:TAUT:: =(skc2,skc1),seat(skc1) -> seat(skc2) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 115:1:0:TAUT:: -> =(skc8,skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 116:4:0:TAUT:: =(skc11,skc10),=(skc10,skc7),furniture(skc11) -> furniture(skc7) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 117:3:0:TAUT:: =(skc11,skc1),front(skc11) -> front(skc1) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 118:1:0:TAUT:: -> =(skc12,skc12) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 119:3:0:TAUT:: =(skc11,skc8),seat(skc11) -> seat(skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 120:3:0:TAUT:: =(skc7,skc6),young(skc7) -> young(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 121:3:0:TAUT:: =(skc6,skc16),young(skc16) -> young(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 122:4:0:TAUT:: =(skc20,skc8),=(skc10,skc7),barrel(skc10,skc8) -> barrel(skc7,skc20) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 123:3:0:TAUT:: =(skc2,skc8),front(skc2) -> front(skc8) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 124:3:0:TAUT:: =(skc19,skc16),in(skc19,skc11) -> in(skc16,skc11) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 125:1:0:TAUT:: -> =(skc17,skc17) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 126:3:0:TAUT:: =(skc4,skc14),old(skc14) -> old(skc4) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 127:3:0:TAUT:: =(skc19,skc16),young(skc16) -> young(skc19) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 128:4:0:TAUT:: =(skc3,skc16),=(skc19,skc16),down(skc19,skc19) -> down(skc3,skc3) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 129:5:0:TAUT:: =(skc15,skc10),=(skc7,skc10),=(skc6,skc14),=(skc14,skc7) -> =(skc6,skc15) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 130:1:0:TAUT:: -> =(skc14,skc14) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 131:4:0:TAUT:: =(skc10,skc8),=(skc10,skc6),furniture(skc8) -> furniture(skc6) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 132:2:0:TAUT:: =(skc20,skc17) -> =(skc17,skc20) % 3.48/1.32 === Restarting. % 3.48/1.32 === CC is in false state. New clause to be learned: 133:2:0:TAUT:: =(skc19,skc16) -> =(skc16,skc19) % 3.48/1.32 === Restarting. % 3.48/1.32 === Backtracking. Learning clause 135:1:0:[90.0,134.0,64.14,46.1,56.1,45.1,51.1,133.2,63.1,60.1,49.1,35.1,34.1,55.1,47.1,61.1,40.1,132.2,38.1,36.1,62.1,59.1,44.1,33.1,37.1,41.1,50.1,54.1,42.1,57.1,43.1,53.1,39.1,48.1,52.1,65.2,8.2]:: -> car(skc4) % 3.48/1.32 === Backtracking. Learning clause 137:1:0:[90.0,136.0,64.29,133.2,35.1,63.1,132.2,51.1,36.1,44.1,62.1,47.1,56.1,52.1,34.1,38.1,55.1,46.1,59.1,57.1,39.1,37.1,42.1,41.1,50.1,49.1,54.1,53.1,48.1,33.1,43.1,60.1,61.1,45.1,40.1,65.2]:: ren1 -> % 3.48/1.32 === CC is in false state. New clause to be learned: 138:2:0:TAUT:: =(skc17,skc20) -> =(skc20,skc17) % 3.48/1.32 === Restarting. % 3.48/1.32 === Backtracking. Learning clause 140:1:0:[137.0,139.0,32.22,90.1,54.1,41.1,37.1,42.1,38.1,34.1,132.2,133.2,56.1,60.1,49.1,36.1,33.1,57.1,53.1,39.1,43.1,51.1,46.1,45.1,63.1,48.1,35.1,59.1,47.1,50.1,55.1,61.1,52.1,44.1,62.1,40.1]:: -> ren2 % 3.48/1.32 % 3.48/1.32 SZS status Unsatisfiable % 3.48/1.32 % 3.48/1.32 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 3.48/1.32 % 3.48/1.32 SPASS-SCL-FOL Statistics: % 3.48/1.32 Number of learned clauses: 4 % 3.48/1.32 Number of propagations: 2573 % 3.48/1.32 Number of decisions: 3111 % 3.48/1.32 Number of resolutions: 170 % 3.48/1.32 Number of condensations: 0 % 3.48/1.32 Number of sub resolutions: 4 % 3.48/1.32 Number of input literals (deduplicated): 85 % 3.48/1.32 Number of grows: 0 % 3.48/1.32 Number of considered ground atoms: 1942 % 3.48/1.32 % 3.48/1.32 Needed: 0:00:00.78 % 3.48/1.32 %------------------------------------------------------------------------------