%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP012-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 : n028.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 : Satisfiable 33.75s 7.29s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP012-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 : n028.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:31 EDT 2026 % 0.16/0.34 % CPUTime : % 0.16/0.34 SPASS-SCL-FOL version: % 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 33.75/7.29 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 Execution resolution_1 ended with status: satisfiable % 33.75/7.29 Used heuristic: resolution_1 % 33.75/7.29 % 33.75/7.29 Input Clauses: % 33.75/7.29 % 33.75/7.29 Predicates: hollywood event chevy lonely seat young fellow city front ssSkC0 street way old dirty white car man furniture barrel down in = % 33.75/7.29 Fol Constants: skc29 skc28 skc27 skc26 skc25 skc24 skc23 skc22 skc21 skc20 skc19 skc18 skc17 skc16 skc15 % 33.75/7.29 Fol Functions: % 33.75/7.29 Problem Properties: % 33.75/7.29 This is a Bernays Schoenfinkel Ramsey problem. % 33.75/7.29 % 33.75/7.29 % 33.75/7.29 Reduced Input Clauses: % 33.75/7.29 % 33.75/7.29 Most General Atoms: ssSkC0 event(x2) city(x3) hollywood(x3) old(x0) dirty(x0) white(x0) car(x0) chevy(x0) street(x1) way(x1) lonely(x1) down(x2,x1) barrel(x2,x0) young(x6) man(x6) fellow(x6) seat(x7) furniture(x7) front(x7) in(x6,x7) =(x6,x4) % 33.75/7.29 % 33.75/7.29 === Starting SPASS-SCL-FOL A Little Less Naive, considering 36 atoms initially, heuristics mode: resolution_1 === % 33.75/7.29 % 33.75/7.29 === Backtracking. Learning clause 64:23:6:[25.1,58.14,26.1,59.15,6.0,60.16,23.1,61.21,24.1,62.22,7.0,63.23,57.30,54.1]:TopTopTopTopTopTop: old(x0),dirty(x0),white(x0),car(x0),chevy(x0),street(x1),way(x1),lonely(x1),down(x2,x1),barrel(x2,x0),event(x2),hollywood(x3),city(x3),in(x2,x3),in(skc24,x4),front(x4),furniture(x4),seat(x4),seat(x5),furniture(x5),front(x5),in(skc23,x5) -> ssSkC0 % 33.75/7.29 === CC model inconsistency. New clause to be learned: 65:3:0:TAUT:: =(skc15,skc23),in(skc15,skc29) -> in(skc23,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 67:2:0:[15.0,66.1]:: =(skc15,skc16) -> young(skc16) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 69:2:0:[15.0,68.1]:: =(skc15,skc23) -> young(skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC model inconsistency. New clause to be learned: 70:1:0:TAUT:: -> =(skc29,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 72:2:0:[14.0,71.1]:: =(skc15,skc16) -> fellow(skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC model inconsistency. New clause to be learned: 74:3:0:[15.0,73.2]:: =(skc29,skc15),=(skc29,skc16) -> young(skc16) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 75:4:0:TAUT:: =(skc15,skc23),=(skc29,skc15),in(skc23,skc29) -> in(skc29,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC model inconsistency. New clause to be learned: 76:2:0:TAUT:: =(skc29,skc15) -> =(skc15,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 77:2:0:TAUT:: =(skc15,skc29) -> =(skc29,skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 79:2:0:[7.0,78.1]:: =(skc15,skc23) -> fellow(skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC model inconsistency. New clause to be learned: 80:1:0:TAUT:: -> =(skc15,skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC model inconsistency. New clause to be learned: 81:1:0:TAUT:: -> =(skc23,skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc29,skc15),in(skc29,skc29) -> in(skc15,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc15,skc16),man(skc16) -> man(skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === Clause set with instances from active satisfied. Growing active. New size: 73 % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc29,skc16),young(skc16) -> young(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc23,skc24),in(skc23,skc29) -> in(skc24,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === Clause set with instances from active satisfied. Growing active. New size: 123 % 33.75/7.29 === 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 % 33.75/7.29 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc23,skc24),in(skc23,skc25) -> in(skc24,skc25) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc29,skc16),=(skc29,skc15) -> =(skc15,skc16) % 33.75/7.29 === Restarting. % 33.75/7.29 === Clause set with instances from active satisfied. Growing active. New size: 169 % 33.75/7.29 === CC model inconsistency. New clause to be learned: 90:3:0:[1.0,89.2]:: =(skc16,skc29),=(skc16,skc17) -> hollywood(skc17) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc29,skc16),down(skc16,skc29) -> down(skc29,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc16,skc29),event(skc16) -> event(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 94:2:0:[2.0,93.1]:: =(skc29,skc28) -> event(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc15,skc29),event(skc15) -> event(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 96:3:0:TAUT:: =(skc29,skc26),event(skc29) -> event(skc26) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 98:2:0:[7.0,97.1]:: =(skc23,skc24) -> fellow(skc24) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 100:2:0:[6.0,99.1]:: =(skc23,skc24) -> young(skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 101:4:0:TAUT:: =(skc15,skc23),=(skc23,skc24),man(skc15) -> man(skc24) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 102:3:0:TAUT:: =(skc23,skc24),man(skc23) -> man(skc24) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 104:2:0:[15.0,103.1]:: =(skc15,skc29) -> young(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc15,skc23),event(skc15) -> event(skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 106:4:0:TAUT:: =(skc29,skc15),=(skc29,skc28),fellow(skc15) -> fellow(skc28) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc23,skc24),in(skc24,skc29) -> in(skc23,skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc29,skc26),seat(skc26) -> seat(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 110:2:0:[14.0,109.1]:: =(skc29,skc16) -> fellow(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 111:3:0:TAUT:: =(skc23,skc24),man(skc24) -> man(skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 113:2:0:[1.0,112.1]:: =(skc29,skc26) -> hollywood(skc26) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 114:3:0:TAUT:: =(skc29,skc27),city(skc29) -> city(skc27) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 116:2:0:[4.0,115.1]:: =(skc29,skc26) -> lonely(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 117:3:0:TAUT:: =(skc29,skc28),lonely(skc29) -> lonely(skc28) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 118:3:0:TAUT:: =(skc23,skc24),in(skc24,skc25) -> in(skc23,skc25) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 119:3:0:TAUT:: =(skc29,skc28),furniture(skc29) -> furniture(skc28) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 120:3:0:TAUT:: =(skc29,skc26),fellow(skc26) -> fellow(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 121:3:0:TAUT:: =(skc15,skc29),event(skc29) -> event(skc15) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 122:3:0:TAUT:: =(skc29,skc15),fellow(skc15) -> fellow(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 123:3:0:TAUT:: =(skc15,skc23),man(skc15) -> man(skc23) % 33.75/7.29 === Restarting. % 33.75/7.29 === CC is in false state. New clause to be learned: 124:3:0:TAUT:: =(skc16,skc29),man(skc16) -> man(skc29) % 33.75/7.29 === Restarting. % 33.75/7.29 % 33.75/7.29 Linear Model Building succeeded. % 33.75/7.29 SZS status Satisfiable % 33.75/7.29 % 33.75/7.29 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 33.75/7.29 % 33.75/7.29 SPASS-SCL-FOL Statistics: % 33.75/7.29 Number of learned clauses: 2 % 33.75/7.29 Number of propagations: 1700 % 33.75/7.29 Number of decisions: 2101 % 33.75/7.29 Number of resolutions: 27 % 33.75/7.29 Number of condensations: 0 % 33.75/7.29 Number of sub resolutions: 19 % 33.75/7.29 Number of input literals (deduplicated): 77 % 33.75/7.29 Number of grows: 3 % 33.75/7.29 Number of considered ground atoms: 171 % 33.75/7.29 % 33.75/7.29 Needed: 0:00:06.73 % 33.75/7.29 %------------------------------------------------------------------------------