%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP004+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 : n011.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 2.30s 1.05s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP004+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.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 12:42:48 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 2.30/1.05 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 Execution normal ended with status: unsatisfiable % 2.30/1.05 Used heuristic: normal % 2.30/1.05 % 2.30/1.05 Input Clauses: % 2.30/1.05 % 2.30/1.05 Predicates: seat furniture front hollywood city event street way lonely chevy car white dirty old barrel down in = fellow man young ren1 ren2 % 2.30/1.05 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20 % 2.30/1.05 Fol Functions: % 2.30/1.05 Problem Properties: % 2.30/1.05 This is a Bernays Schoenfinkel Ramsey problem. % 2.30/1.05 % 2.30/1.05 % 2.30/1.05 Reduced Input Clauses: % 2.30/1.05 % 2.30/1.05 Most General Atoms: ren1 seat(x1) furniture(x1) front(x1) hollywood(x2) city(x2) event(x3) fellow(x7) man(x7) young(x7) in(x9,x1) =(x6,x7) ren2 street(x4) way(x4) lonely(x4) chevy(x5) car(x5) white(x5) dirty(x5) old(x5) barrel(x3,x5) down(x3,x4) % 2.30/1.05 % 2.30/1.05 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1942 atoms initially, heuristics mode: normal === % 2.30/1.05 % 2.30/1.05 === CC is in false state. New clause to be learned: 66:4:0:TAUT:: =(skc12,skc13),=(skc10,skc13),=(skc10,skc8) -> =(skc8,skc12) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 67:6:0:TAUT:: =(skc10,skc8),=(skc11,skc19),=(skc11,skc10),=(skc20,skc7),down(skc20,skc8) -> down(skc7,skc19) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 68:3:0:TAUT:: =(skc9,skc7),barrel(skc7,skc10) -> barrel(skc9,skc10) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 69:6:0:TAUT:: =(skc4,skc13),=(skc6,skc13),=(skc9,skc7),=(skc6,skc9),in(skc4,skc3) -> in(skc7,skc3) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 70:3:0:TAUT:: =(skc14,skc7),in(skc7,skc15) -> in(skc14,skc15) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 71:3:0:TAUT:: =(skc11,skc3),barrel(skc1,skc11) -> barrel(skc1,skc3) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 72:2:0:TAUT:: =(skc1,skc13) -> =(skc13,skc1) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 73:5:0:TAUT:: =(skc15,skc6),=(skc17,skc15),=(skc17,skc12),car(skc6) -> car(skc12) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 74:3:0:TAUT:: =(skc14,skc17),city(skc17) -> city(skc14) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 75:4:0:TAUT:: =(skc4,skc8),=(skc8,skc19),barrel(skc11,skc4) -> barrel(skc11,skc19) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 76:3:0:TAUT:: =(skc11,skc7),lonely(skc11) -> lonely(skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 77:1:0:TAUT:: -> =(skc18,skc18) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 78:3:0:TAUT:: =(skc5,skc15),barrel(skc14,skc15) -> barrel(skc14,skc5) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 79:5:0:TAUT:: =(skc20,skc10),=(skc8,skc13),=(skc10,skc8),down(skc13,skc10) -> down(skc20,skc20) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 80:1:0:TAUT:: -> =(skc9,skc9) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 81:2:0:TAUT:: =(skc20,skc18) -> =(skc18,skc20) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc16,skc2),in(skc4,skc16) -> in(skc4,skc2) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 83:4:0:TAUT:: =(skc2,skc6),=(skc6,skc13),in(skc2,skc7) -> in(skc13,skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 84:4:0:TAUT:: =(skc11,skc13),=(skc13,skc12),barrel(skc13,skc13) -> barrel(skc12,skc11) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc17,skc18),in(skc17,skc9) -> in(skc18,skc9) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 86:4:0:TAUT:: =(skc3,skc6),=(skc20,skc11),=(skc6,skc20) -> =(skc11,skc3) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 87:1:0:TAUT:: -> =(skc13,skc13) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 88:5:0:TAUT:: =(skc10,skc8),=(skc10,skc13),=(skc1,skc13),in(skc10,skc13) -> in(skc1,skc8) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 89:2:0:TAUT:: =(skc19,skc17) -> =(skc17,skc19) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 90:1:0:TAUT:: -> =(skc4,skc4) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc18,skc10),barrel(skc18,skc9) -> barrel(skc10,skc9) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 92:4:0:TAUT:: =(skc4,skc8),=(skc17,skc4),=(skc17,skc7) -> =(skc8,skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 93:4:0:TAUT:: =(skc18,skc15),=(skc10,skc17),in(skc17,skc15) -> in(skc10,skc18) % 2.30/1.05 === Restarting. % 2.30/1.05 === Backtracking. Learning clause 94:1:0:[64.28,63.1,51.1,81.2,62.1,46.1,40.1,58.1,56.1,47.1,36.1,89.2,38.1,59.1,39.1,50.1,55.1,60.1,43.1,42.1,35.1,48.1,52.1,37.1,54.1,45.1,33.1,34.1,53.1,49.1,61.1,44.1,41.1,57.1,65.2,14.2]:: -> car(skc6) % 2.30/1.05 === CC is in false state. New clause to be learned: 95:2:0:TAUT:: =(skc18,skc20) -> =(skc20,skc18) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 96:3:0:TAUT:: =(skc10,skc8),=(skc7,skc10) -> =(skc8,skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 97:2:0:TAUT:: =(skc17,skc19) -> =(skc19,skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 98:1:0:TAUT:: -> =(skc11,skc11) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 99:3:0:TAUT:: =(skc18,skc17),young(skc18) -> young(skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 100:3:0:TAUT:: =(skc14,skc5),barrel(skc5,skc15) -> barrel(skc14,skc15) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 101:3:0:TAUT:: =(skc18,skc20),barrel(skc1,skc20) -> barrel(skc1,skc18) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 102:3:0:TAUT:: =(skc2,skc11),furniture(skc2) -> furniture(skc11) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 103:4:0:TAUT:: =(skc12,skc10),=(skc10,skc8),seat(skc12) -> seat(skc8) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 104:5:0:TAUT:: =(skc9,skc7),=(skc17,skc5),=(skc5,skc9),man(skc7) -> man(skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 105:5:0:TAUT:: =(skc2,skc4),=(skc17,skc12),=(skc2,skc17),barrel(skc4,skc6) -> barrel(skc12,skc6) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 106:1:0:TAUT:: -> =(skc7,skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 107:4:0:TAUT:: =(skc8,skc19),=(skc19,skc17),man(skc8) -> man(skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 108:1:0:TAUT:: -> =(skc14,skc14) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 109:3:0:TAUT:: =(skc16,skc18),=(skc18,skc20) -> =(skc20,skc16) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 110:3:0:TAUT:: =(skc18,skc17),man(skc18) -> man(skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc15,skc6),old(skc6) -> old(skc15) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 112:6:0:TAUT:: =(skc10,skc8),=(skc10,skc14),=(skc5,skc14),=(skc4,skc5),=(skc13,skc4) -> =(skc13,skc8) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 113:5:0:TAUT:: =(skc20,skc16),=(skc20,skc19),=(skc17,skc19),barrel(skc2,skc16) -> barrel(skc2,skc17) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 114:3:0:TAUT:: =(skc7,skc8),=(skc10,skc8) -> =(skc7,skc10) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 115:3:0:TAUT:: =(skc12,skc1),front(skc1) -> front(skc12) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 116:2:0:TAUT:: =(skc9,skc7) -> =(skc7,skc9) % 2.30/1.05 === Restarting. % 2.30/1.05 === CC is in false state. New clause to be learned: 117:2:0:TAUT:: =(skc10,skc8) -> =(skc8,skc10) % 2.30/1.05 === Restarting. % 2.30/1.05 === Backtracking. Learning clause 119:1:0:[94.0,118.0,32.25,26.1,114.1,17.1,11.1,117.2,25.1,96.2,2.1,7.1,8.1,6.1,9.1,30.1,10.1,27.1,13.1,3.1,23.1,1.1,15.1,116.2,21.1,31.1,4.1,29.1,12.1,18.1,20.1,19.1,22.1,28.1,16.1,5.1,24.1,65.1,33.2]:: -> seat(skc11) % 2.30/1.05 === Backtracking. Learning clause 121:1:0:[14.0,120.0,32.2,5.1,13.1,9.1,3.1,6.1,23.1,22.1,4.1,18.1,20.1,26.1,19.1,1.1,12.1,17.1,16.1,31.1,8.1,21.1,7.1,117.2,29.1,116.2,24.1,2.1,27.1,28.1,30.1,10.1,15.1,11.1,25.1]:: -> ren1 % 2.30/1.05 === CC is in false state. New clause to be learned: 122:3:0:TAUT:: =(skc8,skc7),fellow(skc8) -> fellow(skc7) % 2.30/1.05 === Restarting. % 2.30/1.05 % 2.30/1.05 SZS status Unsatisfiable % 2.30/1.05 % 2.30/1.05 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.30/1.05 % 2.30/1.05 SPASS-SCL-FOL Statistics: % 2.30/1.05 Number of learned clauses: 3 % 2.30/1.05 Number of propagations: 1603 % 2.30/1.05 Number of decisions: 2379 % 2.30/1.05 Number of resolutions: 138 % 2.30/1.05 Number of condensations: 0 % 2.30/1.05 Number of sub resolutions: 2 % 2.30/1.05 Number of input literals (deduplicated): 85 % 2.30/1.05 Number of grows: 0 % 2.30/1.05 Number of considered ground atoms: 1942 % 2.30/1.05 % 2.30/1.05 Needed: 0:00:00.51 % 2.30/1.05 %------------------------------------------------------------------------------