%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP125-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 : n016.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:16 PM UTC 2026
% Result : Satisfiable 1.45s 0.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP125-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.33 % Computer : n016.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Thu May 7 12:45:52 EDT 2026
% 0.17/0.33 % CPUTime :
% 0.17/0.33 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 1.45/0.88 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88 Execution resolution_1 ended with status: satisfiable
% 1.45/0.88 Used heuristic: resolution_1
% 1.45/0.88
% 1.45/0.88 Input Clauses:
% 1.45/0.88
% 1.45/0.88 Predicates: barrel event eventuality thing singleton specific nonexistent unisex street way artifact object entity existent nonliving impartial placename relname relation abstraction nonhuman general hollywood_placename city location chevy car vehicle transport instrumentality of = actual_world white dirty old present lonely agent in down
% 1.45/0.88 Fol Constants: skc5 skc9 skc7 skc6 skc8
% 1.45/0.88 Fol Functions:
% 1.45/0.88 Problem Properties:
% 1.45/0.88 This is a Bernays Schoenfinkel Ramsey problem.
% 1.45/0.88
% 1.45/0.88
% 1.45/0.88 Reduced Input Clauses:
% 1.45/0.88
% 1.45/0.88 Most General Atoms: barrel(x0,x1) event(x0,x1) eventuality(x0,x1) thing(x0,x1) singleton(x0,x1) specific(x0,x1) nonexistent(x0,x1) unisex(x0,x1) street(x0,x1) way(x0,x1) artifact(x0,x1) object(x0,x1) existent(x0,x1) nonliving(x0,x1) impartial(x0,x1) relname(x0,x1) relation(x0,x1) abstraction(x0,x1) nonhuman(x0,x1) general(x0,x1) hollywood_placename(x0,x1) city(x0,x1) location(x0,x1) chevy(x0,x1) car(x0,x1) vehicle(x0,x1) transport(x0,x1) instrumentality(x0,x1) placename(x0,x2) of(x0,x1,x3) entity(x0,x3) =(x2,x1) actual_world(skc5) white(skc5,skc7) dirty(skc5,skc7) old(skc5,skc7) present(skc5,skc6) lonely(skc5,skc8) agent(skc5,skc6,skc7) in(skc5,skc6,skc8) down(skc5,skc6,skc8)
% 1.45/0.88
% 1.45/0.88 === Starting SPASS-SCL-FOL A Little Less Naive, considering 23 atoms initially, heuristics mode: resolution_1 ===
% 1.45/0.88
% 1.45/0.88 === Backtracking. Learning clause 53:2:2:[10.2,17.1]:TopTop: artifact(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 54:2:2:[20.2,21.1]:TopTop: relation(x0,x1) -> thing(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 56:2:2:[31.2,32.1]:TopTop: transport(x0,x1) -> artifact(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 58:4:1:[38.0,57.1,35.2,49.1]:Top: placename(skc5,x0),of(skc5,x0,skc8),entity(skc5,skc8) -> =(skc9,x0)
% 1.45/0.88 === CC model inconsistency. New clause to be learned: 59:1:0:TAUT:: -> =(skc5,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 61:2:0:[38.0,60.1]:: =(skc5,skc9) -> placename(skc5,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 62:2:0:TAUT:: =(skc9,skc5) -> =(skc5,skc9)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 63:2:2:[20.2,24.1]:TopTop: relation(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 30
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 65:2:2:[19.2,54.1]:TopTop: relname(x0,x1) -> thing(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 66:2:2:[30.2,56.1]:TopTop: vehicle(x0,x1) -> artifact(x0,x1)
% 1.45/0.88 === CC is in false state. New clause to be learned: 67:1:0:TAUT:: -> =(skc9,skc9)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 68:2:2:[9.2,53.1]:TopTop: way(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 33
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 69:2:2:[19.2,63.1,18.2]:TopTop: placename(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Conflict found: 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1) {x0 -> skc5, x1 -> skc8}
% 1.45/0.88 === Backtracking. Learning clause 70:1:0:[55.1,48.1]:: -> object(skc5,skc8)
% 1.45/0.88 === Backtracking. Learning clause 71:2:2:[29.2,66.1]:TopTop: car(x0,x1) -> artifact(x0,x1)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 36
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 72:2:2:[8.2,68.1]:TopTop: street(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Conflict found: 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1) {x0 -> skc5, x1 -> skc9}
% 1.45/0.88 === Backtracking. Learning clause 73:1:0:[64.1,38.1]:: -> thing(skc5,skc9)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 37
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 74:2:2:[19.2,63.1]:TopTop: relname(x0,x1) -> unisex(x0,x1)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 93
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 157
% 1.45/0.88 === Backtracking. Learning clause 75:2:2:[10.1,71.2,11.1,13.1,33.2,23.2,20.2,19.2,28.2]:TopTop: relname(x0,x1),chevy(x0,x1) ->
% 1.45/0.88 === Backtracking. Learning clause 76:2:2:[19.2,20.1,18.2,23.1,33.1,25.2]:TopTop: specific(x0,x1),hollywood_placename(x0,x1) ->
% 1.45/0.88 === Backtracking. Learning clause 77:2:2:[23.2,33.1,20.2]:TopTop: specific(x0,x1),relation(x0,x1) ->
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 221
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 285
% 1.45/0.88 === CC is in false state. New clause to be learned: 79:2:0:[38.0,78.1]:: =(skc9,skc7) -> placename(skc5,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 81:2:0:[38.0,80.1]:: =(skc9,skc6) -> placename(skc5,skc6)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc5,skc6),general(skc5,skc5) -> general(skc5,skc6)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 83:2:2:[13.2,77.1,11.2,10.2,9.2]:TopTop: relation(x0,x1),way(x0,x1) ->
% 1.45/0.88 === Backtracking. Learning clause 84:2:2:[13.2,76.1,11.2,10.2,66.2]:TopTop: hollywood_placename(x0,x1),vehicle(x0,x1) ->
% 1.45/0.88 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc5,skc8),entity(skc5,skc8) -> entity(skc5,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 349
% 1.45/0.88 === Backtracking. Learning clause 86:2:2:[33.1,23.2,5.2]:TopTop: abstraction(x0,x1),eventuality(x0,x1) ->
% 1.45/0.88 === CC is in false state. New clause to be learned: 87:3:0:TAUT:: =(skc7,skc5),nonexistent(skc7,skc5) -> nonexistent(skc5,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 89:2:0:[49.0,88.1]:: =(skc5,skc9) -> of(skc5,skc5,skc8)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 90:3:0:TAUT:: =(skc5,skc9),entity(skc5,skc8) -> entity(skc9,skc8)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 91:3:0:TAUT:: =(skc5,skc7),general(skc7,skc5) -> general(skc5,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc9,skc8),entity(skc5,skc8) -> entity(skc5,skc9)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 93:3:0:TAUT:: =(skc5,skc6),nonexistent(skc5,skc6) -> nonexistent(skc5,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 94:3:0:TAUT:: =(skc5,skc8),nonexistent(skc9,skc5) -> nonexistent(skc9,skc8)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc7,skc5),general(skc5,skc5) -> general(skc5,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC model inconsistency. New clause to be learned: 96:1:0:TAUT:: -> =(skc7,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 405
% 1.45/0.88 === Backtracking. Learning clause 97:2:2:[12.2,4.1,11.2,27.2]:TopTop: location(x0,x1) -> singleton(x0,x1)
% 1.45/0.88 === CC is in false state. New clause to be learned: 98:2:0:TAUT:: =(skc5,skc7) -> =(skc7,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Backtracking. Learning clause 99:2:2:[20.1,19.2,86.1,2.2,18.2]:TopTop: event(x0,x1),placename(x0,x1) ->
% 1.45/0.88 === CC is in false state. New clause to be learned: 100:2:0:TAUT:: =(skc7,skc9) -> =(skc9,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 469
% 1.45/0.88 === Backtracking. Learning clause 101:2:2:[9.2,10.1,8.2,11.1,12.1]:TopTop: street(x0,x1) -> thing(x0,x1)
% 1.45/0.88 === Backtracking. Learning clause 102:2:2:[6.2,34.1,2.2,1.2,14.2]:TopTop: barrel(x0,x1),entity(x0,x1) ->
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 533
% 1.45/0.88 === Backtracking. Learning clause 103:2:2:[10.2,11.1]:TopTop: artifact(x0,x1) -> entity(x0,x1)
% 1.45/0.88 === Clause set with instances from active satisfied. Growing active. New size: 597
% 1.45/0.88 === CC is in false state. New clause to be learned: 104:2:0:TAUT:: =(skc6,skc5) -> =(skc5,skc6)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 105:3:0:TAUT:: =(skc7,skc8),general(skc9,skc8) -> general(skc9,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 106:3:0:TAUT:: =(skc7,skc8),of(skc5,skc5,skc7) -> of(skc5,skc5,skc8)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc5,skc8),placename(skc7,skc8) -> placename(skc7,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 108:2:0:TAUT:: =(skc6,skc9) -> =(skc9,skc6)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 109:3:0:TAUT:: =(skc7,skc6),nonexistent(skc5,skc6) -> nonexistent(skc5,skc7)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 111:2:0:[48.0,110.1]:: =(skc5,skc8) -> city(skc5,skc5)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC model inconsistency. New clause to be learned: 112:1:0:TAUT:: -> =(skc6,skc6)
% 1.45/0.88 === Restarting.
% 1.45/0.88 === CC is in false state. New clause to be learned: 113:3:0:TAUT:: =(skc7,skc8),nonexistent(skc7,skc7) -> nonexistent(skc7,skc8)
% 1.45/0.88 === Restarting.
% 1.45/0.88
% 1.45/0.88 Linear Model Building succeeded.
% 1.45/0.88 SZS status Satisfiable
% 1.45/0.88
% 1.45/0.88 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.45/0.88
% 1.45/0.88 SPASS-SCL-FOL Statistics:
% 1.45/0.88 Number of learned clauses: 27
% 1.45/0.88 Number of propagations: 9598
% 1.45/0.88 Number of decisions: 2111
% 1.45/0.88 Number of resolutions: 59
% 1.45/0.88 Number of condensations: 0
% 1.45/0.88 Number of sub resolutions: 6
% 1.45/0.88 Number of input literals (deduplicated): 49
% 1.45/0.88 Number of grows: 13
% 1.45/0.88 Number of considered ground atoms: 598
% 1.45/0.88
% 1.45/0.88 Needed: 0:00:00.31
% 1.45/0.88
%------------------------------------------------------------------------------