%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP126-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 : n007.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 0.58s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP126-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.17/0.34 % Computer : n007.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:44:39 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.58/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62 Execution resolution_1 ended with status: satisfiable
% 0.58/0.62 Used heuristic: resolution_1
% 0.58/0.62
% 0.58/0.62 Input Clauses:
% 0.58/0.62
% 0.58/0.62 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 lonely present agent in down
% 0.58/0.62 Fol Constants: skc5 skc9 skc8 skc7 skc6
% 0.58/0.62 Fol Functions:
% 0.58/0.62 Problem Properties:
% 0.58/0.62 This is a Bernays Schoenfinkel Ramsey problem.
% 0.58/0.62
% 0.58/0.62
% 0.58/0.62 Reduced Input Clauses:
% 0.58/0.62
% 0.58/0.62 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) lonely(skc5,skc9) present(skc5,skc6) agent(skc5,skc6,skc7) in(skc5,skc6,skc7) down(skc5,skc6,skc9)
% 0.58/0.62
% 0.58/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 23 atoms initially, heuristics mode: resolution_1 ===
% 0.58/0.62
% 0.58/0.62 === Backtracking. Learning clause 53:2:2:[10.2,17.1]:TopTop: artifact(x0,x1) -> unisex(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 54:2:2:[20.2,21.1]:TopTop: relation(x0,x1) -> thing(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 56:2:2:[31.2,32.1]:TopTop: transport(x0,x1) -> artifact(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 58:4:1:[38.0,57.1,35.2,49.1]:Top: placename(skc5,x0),of(skc5,x0,skc7),entity(skc5,skc7) -> =(skc8,x0)
% 0.58/0.62 === CC model inconsistency. New clause to be learned: 59:1:0:TAUT:: -> =(skc5,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === CC is in false state. New clause to be learned: 61:2:0:[38.0,60.1]:: =(skc5,skc8) -> placename(skc5,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === CC is in false state. New clause to be learned: 62:2:0:TAUT:: =(skc8,skc5) -> =(skc5,skc8)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 63:2:2:[20.2,24.1]:TopTop: relation(x0,x1) -> unisex(x0,x1)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 30
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 65:2:2:[19.2,54.1]:TopTop: relname(x0,x1) -> thing(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 66:2:2:[30.2,56.1]:TopTop: vehicle(x0,x1) -> artifact(x0,x1)
% 0.58/0.62 === CC is in false state. New clause to be learned: 67:1:0:TAUT:: -> =(skc8,skc8)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 68:2:2:[9.2,53.1]:TopTop: way(x0,x1) -> unisex(x0,x1)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 33
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 69:2:2:[19.2,63.1,18.2]:TopTop: placename(x0,x1) -> unisex(x0,x1)
% 0.58/0.62 === Conflict found: 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1) {x0 -> skc5, x1 -> skc7}
% 0.58/0.62 === Backtracking. Learning clause 70:1:0:[55.1,40.1]:: -> object(skc5,skc7)
% 0.58/0.62 === Backtracking. Learning clause 71:2:2:[29.2,66.1]:TopTop: car(x0,x1) -> artifact(x0,x1)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 36
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 72:2:2:[8.2,68.1]:TopTop: street(x0,x1) -> unisex(x0,x1)
% 0.58/0.62 === Conflict found: 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1) {x0 -> skc5, x1 -> skc8}
% 0.58/0.62 === Backtracking. Learning clause 73:1:0:[64.1,38.1]:: -> thing(skc5,skc8)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 38
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 74:1:0:[17.1,70.1]:: -> unisex(skc5,skc7)
% 0.58/0.62 === Backtracking. Learning clause 75:2:2:[28.2,71.1]:TopTop: chevy(x0,x1) -> artifact(x0,x1)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 40
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 76:2:2:[11.2,13.1,10.2,9.2,8.2]:TopTop: street(x0,x1) -> specific(x0,x1)
% 0.58/0.62 === Backtracking. Learning clause 77:2:2:[11.2,13.1,10.2]:TopTop: artifact(x0,x1) -> specific(x0,x1)
% 0.58/0.62 === Conflict found: 69:2:2:[19.2,63.1,18.2]:TopTop: placename(x0,x1) -> unisex(x0,x1) {x0 -> skc5, x1 -> skc8}
% 0.58/0.62 === Backtracking. Learning clause 78:1:0:[69.1,38.1]:: -> unisex(skc5,skc8)
% 0.58/0.62 === CC is in false state. New clause to be learned: 79:2:0:TAUT:: =(skc5,skc8) -> =(skc8,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Conflict found: 72:2:2:[8.2,68.1]:TopTop: street(x0,x1) -> unisex(x0,x1) {x0 -> skc5, x1 -> skc9}
% 0.58/0.62 === Backtracking. Learning clause 80:1:0:[72.1,37.1]:: -> unisex(skc5,skc9)
% 0.58/0.62 === Backtracking. Learning clause 81:2:2:[23.2,33.1,20.2,19.2]:TopTop: specific(x0,x1),relname(x0,x1) ->
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 41
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Conflict found: 76:2:2:[11.2,13.1,10.2,9.2,8.2]:TopTop: street(x0,x1) -> specific(x0,x1) {x0 -> skc5, x1 -> skc9}
% 0.58/0.62 === Backtracking. Learning clause 82:1:0:[76.1,37.1]:: -> specific(skc5,skc9)
% 0.58/0.62 === Backtracking. Learning clause 83:2:2:[14.2,34.2]:TopTop: entity(x0,x1),nonexistent(x0,x1) ->
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 100
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 164
% 0.58/0.62 === Backtracking. Learning clause 84:2:2:[9.2,77.1]:TopTop: way(x0,x1) -> specific(x0,x1)
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 228
% 0.58/0.62 === Clause set with instances from active satisfied. Growing active. New size: 292
% 0.58/0.62 === Backtracking. Learning clause 85:2:2:[19.2,20.1,18.2]:TopTop: placename(x0,x1) -> abstraction(x0,x1)
% 0.58/0.62 === CC is in false state. New clause to be learned: 86:1:0:TAUT:: -> =(skc9,skc9)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 87:1:0:[6.1,2.2,83.2,48.1]:: entity(skc5,skc6) ->
% 0.58/0.62 === CC is in false state. New clause to be learned: 88:3:0:TAUT:: =(skc9,skc5),nonexistent(skc9,skc9) -> nonexistent(skc5,skc9)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === Backtracking. Learning clause 89:2:2:[33.2,13.2,23.2,20.2]:TopTop: entity(x0,x1),relation(x0,x1) ->
% 0.58/0.62 === CC is in false state. New clause to be learned: 90:3:0:TAUT:: =(skc5,skc6),nonexistent(skc5,skc6) -> nonexistent(skc5,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === CC is in false state. New clause to be learned: 91:2:0:TAUT:: =(skc5,skc9) -> =(skc9,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === CC is in false state. New clause to be learned: 92:3:0:TAUT:: =(skc5,skc6),general(skc5,skc5) -> general(skc5,skc6)
% 0.58/0.62 === Restarting.
% 0.58/0.62 === CC is in false state. New clause to be learned: 93:3:0:TAUT:: =(skc5,skc7),entity(skc5,skc7) -> entity(skc5,skc5)
% 0.58/0.62 === Restarting.
% 0.58/0.62
% 0.58/0.62 Linear Model Building succeeded.
% 0.58/0.62 SZS status Satisfiable
% 0.58/0.62
% 0.58/0.62 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.62
% 0.58/0.62 SPASS-SCL-FOL Statistics:
% 0.58/0.62 Number of learned clauses: 28
% 0.58/0.62 Number of propagations: 2231
% 0.58/0.62 Number of decisions: 528
% 0.58/0.62 Number of resolutions: 41
% 0.58/0.62 Number of condensations: 0
% 0.58/0.62 Number of sub resolutions: 2
% 0.58/0.62 Number of input literals (deduplicated): 49
% 0.58/0.62 Number of grows: 10
% 0.58/0.62 Number of considered ground atoms: 292
% 0.58/0.62
% 0.58/0.62 Needed: 0:00:00.08
% 0.58/0.62
%------------------------------------------------------------------------------