%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP011+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:01 PM UTC 2026
% Result : Theorem 5.42s 1.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP011+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.32 % Computer : n015.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Thu May 7 12:43:32 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.21/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.42/1.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.57 Execution normal ended with status: unsatisfiable
% 5.42/1.57 Used heuristic: normal
% 5.42/1.57
% 5.42/1.57 Input Clauses:
% 5.42/1.58
% 5.42/1.58 Predicates: seat furniture front hollywood city event street way lonely chevy car white dirty old barrel down in = fellow man young ren1 ren2
% 5.42/1.58 Fol Constants: skc1 skc2 skc3 skc4 skc5 skc6 skc7 skc8 skc9 skc10 skc11 skc12 skc13 skc14 skc15 skc16 skc17 skc18 skc19 skc20
% 5.42/1.58 Fol Functions:
% 5.42/1.58 Problem Properties:
% 5.42/1.58 This is a Bernays Schoenfinkel Ramsey problem.
% 5.42/1.58
% 5.42/1.58
% 5.42/1.58 Reduced Input Clauses:
% 5.42/1.58
% 5.42/1.58 Most General Atoms: ren1 hollywood(x1) city(x1) event(x2) street(x3) way(x3) lonely(x3) chevy(x4) car(x4) white(x4) dirty(x4) old(x4) barrel(x2,x4) down(x2,x3) seat(x5) furniture(x5) front(x5) fellow(x7) man(x7) young(x7) =(x6,x7) ren2 in(x9,x0)
% 5.42/1.58
% 5.42/1.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 1942 atoms initially, heuristics mode: normal ===
% 5.42/1.58
% 5.42/1.58 === CC is in false state. New clause to be learned: 66:2:0:TAUT:: =(skc6,skc7) -> =(skc7,skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 67:4:0:TAUT:: =(skc1,skc19),=(skc20,skc7),down(skc7,skc19) -> down(skc20,skc1)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 68:1:0:TAUT:: -> =(skc18,skc18)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 69:4:0:TAUT:: =(skc11,skc12),=(skc20,skc11),down(skc11,skc12) -> down(skc12,skc20)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 70:3:0:TAUT:: =(skc10,skc5),in(skc10,skc1) -> in(skc5,skc1)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 71:3:0:TAUT:: =(skc9,skc6),fellow(skc6) -> fellow(skc9)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 72:3:0:TAUT:: =(skc9,skc6),down(skc8,skc6) -> down(skc8,skc9)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 73:2:0:TAUT:: =(skc4,skc20) -> =(skc20,skc4)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 74:4:0:TAUT:: =(skc6,skc18),=(skc9,skc6),down(skc9,skc6) -> down(skc6,skc18)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 75:4:0:TAUT:: =(skc19,skc16),=(skc19,skc6),man(skc16) -> man(skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 76:3:0:TAUT:: =(skc9,skc6),in(skc9,skc8) -> in(skc6,skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 77:3:0:TAUT:: =(skc20,skc10),barrel(skc20,skc8) -> barrel(skc10,skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 78:3:0:TAUT:: =(skc3,skc1),=(skc19,skc1) -> =(skc19,skc3)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 79:3:0:TAUT:: =(skc9,skc6),young(skc6) -> young(skc9)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 80:3:0:TAUT:: =(skc15,skc1),in(skc1,skc13) -> in(skc15,skc13)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 81:3:0:TAUT:: =(skc13,skc9),barrel(skc13,skc19) -> barrel(skc9,skc19)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 82:4:0:TAUT:: =(skc7,skc11),=(skc10,skc7),down(skc10,skc7) -> down(skc11,skc11)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 83:4:0:TAUT:: =(skc20,skc17),=(skc20,skc10),down(skc17,skc20) -> down(skc10,skc17)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 84:1:0:TAUT:: -> =(skc6,skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 85:1:0:TAUT:: -> =(skc7,skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 86:4:0:TAUT:: =(skc20,skc17),=(skc3,skc20),fellow(skc17) -> fellow(skc3)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 87:2:0:TAUT:: =(skc10,skc7) -> =(skc7,skc10)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 88:4:0:TAUT:: =(skc5,skc15),=(skc12,skc13),barrel(skc13,skc15) -> barrel(skc12,skc5)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === Backtracking. Learning clause 90:2:0:[84.0,89.1,32.21,22.1,15.1,76.3,31.1,4.1,29.1,16.1,3.1,2.1,20.1,7.1,28.1,14.1,27.1,17.1,66.1,26.1,12.1,1.1,10.1,5.1,87.2,9.1,23.1,19.1,8.1,30.1,18.1,25.1,21.1,11.1,6.1,24.1,65.1,54.2]:: dirty(skc5) -> fellow(skc16)
% 5.42/1.58 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc20,skc17),=(skc20,skc16) -> =(skc16,skc17)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc6,skc7),fellow(skc6) -> fellow(skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 93:3:0:TAUT:: =(skc6,skc7),young(skc7) -> young(skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 94:2:0:TAUT:: =(skc7,skc6) -> =(skc6,skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc9,skc6),in(skc6,skc8) -> in(skc9,skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 96:3:0:TAUT:: =(skc6,skc7),young(skc6) -> young(skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 97:2:0:TAUT:: =(skc7,skc10) -> =(skc10,skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 98:3:0:TAUT:: =(skc6,skc7),man(skc6) -> man(skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 99:3:0:TAUT:: =(skc16,skc14),down(skc1,skc14) -> down(skc1,skc16)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === Backtracking. Learning clause 100:1:0:[13.1,90.1,65.1,54.2]:: -> fellow(skc16)
% 5.42/1.58 === Conflict found: 76:3:0:TAUT:: =(skc9,skc6),in(skc9,skc8) -> in(skc6,skc8) {}
% 5.42/1.58 === Backtracking. Learning clause 102:15:4:[84.0,101.14,76.2,29.1,32.28,31.1,26.1,66.1,19.1,1.1,2.1,87.2,24.1,21.1,25.1,27.1,30.1,28.1,23.1,18.1,3.1,22.1,20.1]:TopTopTopTop: hollywood(x0),city(x0),event(x1),street(x2),way(x2),lonely(x2),chevy(x3),car(x3),white(x3),dirty(x3),old(x3),barrel(x1,x3),down(x1,x2),in(x1,x0) -> ren1
% 5.42/1.58 === CC is in false state. New clause to be learned: 103:1:0:TAUT:: -> =(skc9,skc9)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === Conflict found: 102:15:4:[84.0,101.14,76.2,29.1,32.28,31.1,26.1,66.1,19.1,1.1,2.1,87.2,24.1,21.1,25.1,27.1,30.1,28.1,23.1,18.1,3.1,22.1,20.1]:TopTopTopTop: hollywood(x0),city(x0),event(x1),street(x2),way(x2),lonely(x2),chevy(x3),car(x3),white(x3),dirty(x3),old(x3),barrel(x1,x3),down(x1,x2),in(x1,x0) -> ren1 {x0 -> skc2, x1 -> skc3, x2 -> skc4, x3 -> skc5}
% 5.42/1.58 === Backtracking. Learning clause 104:1:0:[102.7,10.1,8.1,6.1,15.1,14.1,4.1,7.1,9.1,11.1,12.1,17.1,16.1,5.1,13.1]:: -> ren1
% 5.42/1.58 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc20,skc17),fellow(skc17) -> fellow(skc20)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 106:1:0:TAUT:: -> =(skc19,skc19)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 107:1:0:TAUT:: -> =(skc4,skc4)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 108:3:0:TAUT:: =(skc4,skc14),way(skc14) -> way(skc4)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 109:3:0:TAUT:: =(skc17,skc6),man(skc17) -> man(skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 110:3:0:TAUT:: =(skc1,skc8),front(skc1) -> front(skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 111:4:0:TAUT:: =(skc1,skc14),=(skc14,skc11),front(skc11) -> front(skc1)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 112:3:0:TAUT:: =(skc11,skc1),front(skc11) -> front(skc1)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 113:3:0:TAUT:: =(skc9,skc6),=(skc19,skc9) -> =(skc19,skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 114:4:0:TAUT:: =(skc15,skc13),=(skc19,skc16),in(skc16,skc15) -> in(skc19,skc13)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 115:5:0:TAUT:: =(skc19,skc7),=(skc16,skc5),=(skc19,skc16),in(skc5,skc7) -> in(skc19,skc5)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 116:5:0:TAUT:: =(skc9,skc6),=(skc6,skc15),=(skc6,skc7),in(skc15,skc6) -> in(skc7,skc9)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 117:4:0:TAUT:: =(skc10,skc1),=(skc7,skc10),in(skc10,skc1) -> in(skc10,skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 118:2:0:TAUT:: =(skc16,skc17) -> =(skc17,skc16)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 119:2:0:TAUT:: =(skc1,skc11) -> =(skc11,skc1)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 120:2:0:TAUT:: =(skc16,skc11) -> =(skc11,skc16)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 121:3:0:TAUT:: =(skc9,skc8),seat(skc9) -> seat(skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 122:3:0:TAUT:: =(skc7,skc6),fellow(skc7) -> fellow(skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 123:3:0:TAUT:: =(skc5,skc15),white(skc15) -> white(skc5)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 124:3:0:TAUT:: =(skc6,skc4),barrel(skc6,skc6) -> barrel(skc6,skc4)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 125:4:0:TAUT:: =(skc20,skc17),=(skc20,skc7),fellow(skc17) -> fellow(skc7)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 126:3:0:TAUT:: =(skc6,skc7),man(skc7) -> man(skc6)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 127:3:0:TAUT:: =(skc12,skc10),=(skc7,skc10) -> =(skc7,skc12)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 128:3:0:TAUT:: =(skc8,skc11),furniture(skc11) -> furniture(skc8)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 129:2:0:TAUT:: =(skc20,skc17) -> =(skc17,skc20)
% 5.42/1.58 === Restarting.
% 5.42/1.58 === CC is in false state. New clause to be learned: 130:2:0:TAUT:: =(skc19,skc16) -> =(skc16,skc19)
% 5.42/1.58 === Restarting.
% 5.42/1.58
% 5.42/1.58 SZS status Unsatisfiable
% 5.42/1.58
% 5.42/1.58 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.58
% 5.42/1.58 SPASS-SCL-FOL Statistics:
% 5.42/1.58 Number of learned clauses: 4
% 5.42/1.58 Number of propagations: 2225
% 5.42/1.58 Number of decisions: 2723
% 5.42/1.58 Number of resolutions: 108
% 5.42/1.58 Number of condensations: 0
% 5.42/1.58 Number of sub resolutions: 2
% 5.42/1.58 Number of input literals (deduplicated): 85
% 5.42/1.58 Number of grows: 0
% 5.42/1.58 Number of considered ground atoms: 1942
% 5.42/1.58
% 5.42/1.58 Needed: 0:00:01.07
% 5.42/1.58
%------------------------------------------------------------------------------