%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP005-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 : n015.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 : Satisfiable 27.40s 7.31s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP005-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.16/0.34 % Computer : n015.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Thu May 7 12:43:17 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 27.40/7.31 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 Execution resolution_1 ended with status: satisfiable % 27.40/7.31 Used heuristic: resolution_1 % 27.40/7.31 % 27.40/7.31 Input Clauses: % 27.40/7.31 % 27.40/7.31 Predicates: city event old street seat young fellow hollywood front ssSkC0 lonely way chevy car white dirty man furniture down barrel in = % 27.40/7.31 Fol Constants: skc29 skc28 skc27 skc26 skc25 skc24 skc23 skc22 skc21 skc20 skc19 skc18 skc17 skc16 skc15 % 27.40/7.31 Fol Functions: % 27.40/7.31 Problem Properties: % 27.40/7.31 This is a Bernays Schoenfinkel Ramsey problem. % 27.40/7.31 % 27.40/7.31 % 27.40/7.31 Reduced Input Clauses: % 27.40/7.31 % 27.40/7.31 Most General Atoms: ssSkC0 event(x2) hollywood(x3) city(x3) chevy(x0) car(x0) white(x0) dirty(x0) old(x0) lonely(x1) way(x1) street(x1) barrel(x2,x0) down(x2,x1) in(x6,x7) front(x7) furniture(x7) seat(x7) young(x6) man(x6) fellow(x6) =(x6,x5) % 27.40/7.31 % 27.40/7.31 === Starting SPASS-SCL-FOL A Little Less Naive, considering 36 atoms initially, heuristics mode: resolution_1 === % 27.40/7.31 % 27.40/7.31 === Backtracking. Learning clause 64:23:6:[25.1,58.18,26.1,59.19,6.0,60.20,23.1,61.25,24.1,62.26,7.0,63.27,57.30,54.1]:TopTopTopTopTopTop: chevy(x0),car(x0),white(x0),dirty(x0),old(x0),lonely(x1),way(x1),street(x1),event(x2),barrel(x2,x0),down(x2,x1),in(x2,x3),city(x3),hollywood(x3),seat(x4),furniture(x4),front(x4),in(skc24,x4),in(skc23,x5),front(x5),furniture(x5),seat(x5) -> ssSkC0 % 27.40/7.31 === CC model inconsistency. New clause to be learned: 65:3:0:TAUT:: =(skc15,skc23),in(skc15,skc29) -> in(skc23,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 67:2:0:[15.0,66.1]:: =(skc15,skc16) -> young(skc16) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 69:2:0:[15.0,68.1]:: =(skc15,skc23) -> young(skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 70:1:0:TAUT:: -> =(skc29,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 72:2:0:[14.0,71.1]:: =(skc15,skc16) -> fellow(skc15) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 74:3:0:[15.0,73.2]:: =(skc29,skc15),=(skc29,skc16) -> young(skc16) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 75:4:0:TAUT:: =(skc15,skc23),=(skc29,skc15),in(skc23,skc29) -> in(skc29,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 76:2:0:TAUT:: =(skc29,skc15) -> =(skc15,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 77:2:0:TAUT:: =(skc15,skc29) -> =(skc29,skc15) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 79:2:0:[7.0,78.1]:: =(skc15,skc23) -> fellow(skc15) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 80:1:0:TAUT:: -> =(skc15,skc15) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 81:1:0:TAUT:: -> =(skc23,skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc29,skc15),in(skc29,skc29) -> in(skc15,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc15,skc16),man(skc16) -> man(skc15) % 27.40/7.31 === Restarting. % 27.40/7.31 === Clause set with instances from active satisfied. Growing active. New size: 73 % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc29,skc16),young(skc16) -> young(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc23,skc24),in(skc23,skc29) -> in(skc24,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === Clause set with instances from active satisfied. Growing active. New size: 123 % 27.40/7.31 === Backtracking. Learning clause 86:1:0:[57.1,18.2,3.1,48.2,45.2,2.1,16.2,4.1,44.2,21.2,46.2,19.2,17.2,20.2,54.1,47.2,28.2,24.2,26.2,27.2,22.2,7.1,25.2,23.2,6.1,5.1,1.1]:: -> ssSkC0 % 27.40/7.31 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc23,skc24),in(skc23,skc25) -> in(skc24,skc25) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc29,skc16),=(skc29,skc15) -> =(skc15,skc16) % 27.40/7.31 === Restarting. % 27.40/7.31 === Clause set with instances from active satisfied. Growing active. New size: 169 % 27.40/7.31 === CC model inconsistency. New clause to be learned: 90:3:0:[1.0,89.2]:: =(skc16,skc29),=(skc16,skc17) -> city(skc17) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc29,skc16),barrel(skc16,skc29) -> barrel(skc29,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc16,skc29),event(skc16) -> event(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 94:2:0:[2.0,93.1]:: =(skc29,skc28) -> event(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc15,skc29),event(skc15) -> event(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 96:3:0:TAUT:: =(skc29,skc26),event(skc29) -> event(skc26) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 98:2:0:[7.0,97.1]:: =(skc23,skc24) -> fellow(skc24) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 99:3:0:TAUT:: =(skc23,skc24),man(skc24) -> man(skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 101:2:0:[6.0,100.1]:: =(skc23,skc24) -> young(skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 102:3:0:TAUT:: =(skc29,skc27),street(skc29) -> street(skc27) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 103:3:0:TAUT:: =(skc29,skc27),young(skc27) -> young(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 104:3:0:TAUT:: =(skc23,skc24),in(skc24,skc25) -> in(skc23,skc25) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc15,skc29),man(skc15) -> man(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 106:3:0:TAUT:: =(skc29,skc26),way(skc26) -> way(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 107:2:0:TAUT:: =(skc16,skc29) -> =(skc29,skc16) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc29,skc28),chevy(skc29) -> chevy(skc28) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 109:3:0:TAUT:: =(skc15,skc29),fellow(skc15) -> fellow(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 110:3:0:TAUT:: =(skc29,skc26),old(skc26) -> old(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 111:4:0:TAUT:: =(skc16,skc17),=(skc16,skc29),in(skc16,skc17) -> in(skc29,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 112:3:0:TAUT:: =(skc23,skc24),man(skc23) -> man(skc24) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 113:3:0:TAUT:: =(skc29,skc26),young(skc26) -> young(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 115:2:0:[1.0,114.1]:: =(skc29,skc26) -> city(skc26) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 116:3:0:TAUT:: =(skc15,skc23),in(skc15,skc18) -> in(skc23,skc18) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 117:3:0:TAUT:: =(skc29,skc26),lonely(skc26) -> lonely(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 118:3:0:TAUT:: =(skc16,skc29),down(skc16,skc26) -> down(skc29,skc26) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 120:2:0:[14.0,119.1]:: =(skc16,skc29) -> fellow(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 121:4:0:TAUT:: =(skc15,skc23),=(skc23,skc24),man(skc15) -> man(skc24) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 122:3:0:TAUT:: =(skc29,skc15),down(skc15,skc29) -> down(skc29,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 123:3:0:TAUT:: =(skc23,skc24),in(skc24,skc29) -> in(skc23,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 124:2:0:TAUT:: =(skc29,skc16) -> =(skc16,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 125:3:0:TAUT:: =(skc15,skc23),barrel(skc23,skc29) -> barrel(skc15,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 126:3:0:TAUT:: =(skc29,skc27),white(skc27) -> white(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC model inconsistency. New clause to be learned: 128:3:0:[1.0,127.2]:: =(skc23,skc29),=(skc23,skc25) -> city(skc25) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 130:2:0:[15.0,129.1]:: =(skc29,skc15) -> young(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 131:3:0:TAUT:: =(skc16,skc29),down(skc29,skc29) -> down(skc16,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 132:4:0:TAUT:: =(skc16,skc29),=(skc23,skc29),young(skc16) -> young(skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 133:3:0:TAUT:: =(skc23,skc29),in(skc29,skc29) -> in(skc23,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 135:2:0:[1.0,134.1]:: =(skc29,skc27) -> city(skc27) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 136:3:0:TAUT:: =(skc29,skc28),in(skc29,skc28) -> in(skc28,skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 137:3:0:TAUT:: =(skc23,skc29),young(skc23) -> young(skc29) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 138:3:0:TAUT:: =(skc29,skc28),old(skc29) -> old(skc28) % 27.40/7.31 === Restarting. % 27.40/7.31 === CC is in false state. New clause to be learned: 139:3:0:TAUT:: =(skc23,skc29),=(skc29,skc15) -> =(skc15,skc23) % 27.40/7.31 === Restarting. % 27.40/7.31 % 27.40/7.31 Linear Model Building succeeded. % 27.40/7.31 SZS status Satisfiable % 27.40/7.31 % 27.40/7.31 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 27.40/7.31 % 27.40/7.31 SPASS-SCL-FOL Statistics: % 27.40/7.31 Number of learned clauses: 2 % 27.40/7.31 Number of propagations: 2425 % 27.40/7.31 Number of decisions: 3083 % 27.40/7.31 Number of resolutions: 27 % 27.40/7.31 Number of condensations: 0 % 27.40/7.31 Number of sub resolutions: 20 % 27.40/7.31 Number of input literals (deduplicated): 77 % 27.40/7.31 Number of grows: 3 % 27.40/7.31 Number of considered ground atoms: 174 % 27.40/7.31 % 27.40/7.31 Needed: 0:00:06.76 % 27.40/7.31 %------------------------------------------------------------------------------