%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : NLP008-1 : TPTP v9.2.1. Released v2.4.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/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:01 PM UTC 2026 % Result : Satisfiable 0.31s 0.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP008-1 : TPTP v9.2.1. Released v2.4.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n011.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:03 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] % 0.31/0.53 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 Execution resolution_1 ended with status: satisfiable % 0.31/0.53 Used heuristic: resolution_1 % 0.31/0.53 % 0.31/0.53 Input Clauses: % 0.31/0.53 % 0.31/0.53 Predicates: city event lonely chevy seat young fellow old street front ssSkC0 dirty white car way hollywood man furniture down barrel in = % 0.31/0.53 Fol Constants: skc29 skc28 skc27 skc26 skc25 skc24 skc23 skc22 skc21 skc20 skc19 skc18 skc17 skc16 skc15 % 0.31/0.53 Fol Functions: % 0.31/0.53 Problem Properties: % 0.31/0.53 This is a Bernays Schoenfinkel Ramsey problem. % 0.31/0.53 % 0.31/0.53 % 0.31/0.53 Reduced Input Clauses: % 0.31/0.53 % 0.31/0.53 Most General Atoms: ssSkC0 event(x2) hollywood(x3) city(x3) lonely(x0) way(x0) street(x0) chevy(x1) car(x1) white(x1) dirty(x1) old(x1) down(x2,x0) barrel(x2,x1) young(x6) man(x6) fellow(x6) seat(x7) furniture(x7) front(x7) in(x6,x7) =(x6,x4) % 0.31/0.53 % 0.31/0.53 === Starting SPASS-SCL-FOL A Little Less Naive, considering 36 atoms initially, heuristics mode: resolution_1 === % 0.31/0.53 % 0.31/0.53 === 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: lonely(x0),way(x0),street(x0),chevy(x1),car(x1),white(x1),dirty(x1),old(x1),down(x2,x0),barrel(x2,x1),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 % 0.31/0.53 === CC model inconsistency. New clause to be learned: 65:3:0:TAUT:: =(skc15,skc23),in(skc15,skc29) -> in(skc23,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 67:2:0:[15.0,66.1]:: =(skc15,skc16) -> young(skc16) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 69:2:0:[15.0,68.1]:: =(skc15,skc23) -> young(skc23) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC model inconsistency. New clause to be learned: 70:1:0:TAUT:: -> =(skc29,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 72:2:0:[14.0,71.1]:: =(skc15,skc16) -> fellow(skc15) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC model inconsistency. New clause to be learned: 74:3:0:[15.0,73.2]:: =(skc29,skc15),=(skc29,skc16) -> young(skc16) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 75:4:0:TAUT:: =(skc15,skc23),=(skc29,skc15),in(skc23,skc29) -> in(skc29,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC model inconsistency. New clause to be learned: 76:2:0:TAUT:: =(skc29,skc15) -> =(skc15,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 77:2:0:TAUT:: =(skc15,skc29) -> =(skc29,skc15) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 79:2:0:[7.0,78.1]:: =(skc15,skc23) -> fellow(skc15) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC model inconsistency. New clause to be learned: 80:1:0:TAUT:: -> =(skc15,skc15) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC model inconsistency. New clause to be learned: 81:1:0:TAUT:: -> =(skc23,skc23) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc29,skc15),in(skc29,skc29) -> in(skc15,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 83:3:0:TAUT:: =(skc15,skc16),man(skc16) -> man(skc15) % 0.31/0.53 === Restarting. % 0.31/0.53 === Clause set with instances from active satisfied. Growing active. New size: 73 % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc29,skc16),young(skc16) -> young(skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc23,skc24),in(skc23,skc29) -> in(skc24,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === Clause set with instances from active satisfied. Growing active. New size: 123 % 0.31/0.53 === Backtracking. Learning clause 86:1:0:[57.6,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,22.2,27.2,7.1,25.2,23.2,6.1,5.1,1.1]:: -> ssSkC0 % 0.31/0.53 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc23,skc24),man(skc24) -> man(skc23) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc15,skc23),down(skc23,skc29) -> down(skc15,skc29) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 90:2:0:[1.0,89.1]:: =(skc29,skc28) -> city(skc28) % 0.31/0.53 === Restarting. % 0.31/0.53 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc23,skc24),in(skc23,skc25) -> in(skc24,skc25) % 0.31/0.53 === Restarting. % 0.31/0.53 % 0.31/0.53 Linear Model Building succeeded. % 0.31/0.53 SZS status Satisfiable % 0.31/0.53 % 0.31/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.31/0.53 % 0.31/0.53 SPASS-SCL-FOL Statistics: % 0.31/0.53 Number of learned clauses: 2 % 0.31/0.53 Number of propagations: 471 % 0.31/0.53 Number of decisions: 774 % 0.31/0.53 Number of resolutions: 27 % 0.31/0.53 Number of condensations: 0 % 0.31/0.53 Number of sub resolutions: 12 % 0.31/0.53 Number of input literals (deduplicated): 77 % 0.31/0.53 Number of grows: 2 % 0.31/0.53 Number of considered ground atoms: 123 % 0.31/0.53 % 0.31/0.53 Needed: 0:00:00.02 % 0.31/0.53 %------------------------------------------------------------------------------