%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP129-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 : n012.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:17 PM UTC 2026
% Result : Satisfiable 0.64s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : NLP129-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.08 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.29 % Computer : n012.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Thu May 7 12:45:16 EDT 2026
% 0.10/0.29 % CPUTime :
% 0.10/0.29 SPASS-SCL-FOL version:
% 0.16/0.35 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.64/0.53 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53 Execution resolution_1 ended with status: satisfiable
% 0.64/0.53 Used heuristic: resolution_1
% 0.64/0.53
% 0.64/0.53 Input Clauses:
% 0.64/0.53
% 0.64/0.53 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 lonely white dirty old present down in agent
% 0.64/0.53 Fol Constants: skc5 skc9 skc8 skc7 skc6
% 0.64/0.53 Fol Functions:
% 0.64/0.53 Problem Properties:
% 0.64/0.53 This is a Bernays Schoenfinkel Ramsey problem.
% 0.64/0.53
% 0.64/0.53
% 0.64/0.53 Reduced Input Clauses:
% 0.64/0.53
% 0.64/0.53 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) lonely(skc5,skc7) white(skc5,skc9) dirty(skc5,skc9) old(skc5,skc9) present(skc5,skc6) down(skc5,skc6,skc7) in(skc5,skc6,skc7) agent(skc5,skc6,skc9)
% 0.64/0.53
% 0.64/0.53 === Starting SPASS-SCL-FOL A Little Less Naive, considering 23 atoms initially, heuristics mode: resolution_1 ===
% 0.64/0.53
% 0.64/0.53 === Backtracking. Learning clause 53:2:2:[10.2,17.1]:TopTop: artifact(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Backtracking. Learning clause 54:2:2:[20.2,21.1]:TopTop: relation(x0,x1) -> thing(x0,x1)
% 0.64/0.53 === Backtracking. Learning clause 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1)
% 0.64/0.53 === Backtracking. Learning clause 56:2:2:[31.2,32.1]:TopTop: transport(x0,x1) -> artifact(x0,x1)
% 0.64/0.53 === 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.64/0.53 === CC model inconsistency. New clause to be learned: 59:1:0:TAUT:: -> =(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 61:2:0:[38.0,60.1]:: =(skc5,skc8) -> placename(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 62:2:0:TAUT:: =(skc8,skc5) -> =(skc5,skc8)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 63:2:2:[20.2,24.1]:TopTop: relation(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 30
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1)
% 0.64/0.53 === Backtracking. Learning clause 65:2:2:[19.2,54.1]:TopTop: relname(x0,x1) -> thing(x0,x1)
% 0.64/0.53 === Backtracking. Learning clause 66:2:2:[30.2,56.1]:TopTop: vehicle(x0,x1) -> artifact(x0,x1)
% 0.64/0.53 === CC is in false state. New clause to be learned: 67:1:0:TAUT:: -> =(skc8,skc8)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 68:2:2:[9.2,53.1]:TopTop: way(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 33
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 69:2:2:[19.2,63.1,18.2]:TopTop: placename(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Conflict found: 55:2:2:[26.2,27.1]:TopTop: city(x0,x1) -> object(x0,x1) {x0 -> skc5, x1 -> skc7}
% 0.64/0.53 === Backtracking. Learning clause 70:1:0:[55.1,40.1]:: -> object(skc5,skc7)
% 0.64/0.53 === Backtracking. Learning clause 71:2:2:[29.2,66.1]:TopTop: car(x0,x1) -> artifact(x0,x1)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 36
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 72:2:2:[8.2,68.1]:TopTop: street(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Conflict found: 64:2:2:[19.2,54.1,18.2]:TopTop: placename(x0,x1) -> thing(x0,x1) {x0 -> skc5, x1 -> skc8}
% 0.64/0.53 === Backtracking. Learning clause 73:1:0:[64.1,38.1]:: -> thing(skc5,skc8)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 37
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 74:2:2:[19.2,63.1]:TopTop: relname(x0,x1) -> unisex(x0,x1)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.64/0.53 === CC is in false state. New clause to be learned: 75:3:0:TAUT:: =(skc5,skc9),unisex(skc5,skc9) -> unisex(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 157
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 221
% 0.64/0.53 === Backtracking. Learning clause 76:2:2:[20.2,23.1]:TopTop: relation(x0,x1) -> general(x0,x1)
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 285
% 0.64/0.53 === Backtracking. Learning clause 77:2:2:[14.2,34.2,11.2,27.2]:TopTop: nonexistent(x0,x1),location(x0,x1) ->
% 0.64/0.53 === CC is in false state. New clause to be learned: 78:2:0:TAUT:: =(skc9,skc5) -> =(skc5,skc9)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 79:4:0:TAUT:: =(skc5,skc7),=(skc8,skc5),entity(skc5,skc7) -> entity(skc5,skc8)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 80:2:2:[13.2,33.2,11.2,76.2,10.2,66.2]:TopTop: relation(x0,x1),vehicle(x0,x1) ->
% 0.64/0.53 === Backtracking. Learning clause 81:2:2:[18.2,19.1,25.2]:TopTop: hollywood_placename(x0,x1) -> relation(x0,x1)
% 0.64/0.53 === CC is in false state. New clause to be learned: 82:3:0:TAUT:: =(skc9,skc5),nonexistent(skc9,skc5) -> nonexistent(skc5,skc9)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 83:2:2:[10.2,11.1]:TopTop: artifact(x0,x1) -> entity(x0,x1)
% 0.64/0.53 === CC is in false state. New clause to be learned: 84:3:0:TAUT:: =(skc5,skc6),nonexistent(skc5,skc6) -> nonexistent(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 85:3:0:TAUT:: =(skc9,skc5),general(skc5,skc5) -> general(skc5,skc9)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 86:3:0:TAUT:: =(skc5,skc7),entity(skc5,skc7) -> entity(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 87:2:0:TAUT:: =(skc5,skc9) -> =(skc9,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 88:2:2:[34.1,6.2,14.2]:TopTop: eventuality(x0,x1),entity(x0,x1) ->
% 0.64/0.53 === CC is in false state. New clause to be learned: 89:1:0:TAUT:: -> =(skc9,skc9)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 90:3:0:TAUT:: =(skc5,skc7),entity(skc9,skc7) -> entity(skc9,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 91:2:2:[13.1,11.2,33.2,76.2]:TopTop: object(x0,x1),relation(x0,x1) ->
% 0.64/0.53 === CC is in false state. New clause to be learned: 93:2:0:[40.0,92.1]:: =(skc5,skc7) -> city(skc5,skc5)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === CC is in false state. New clause to be learned: 94:3:0:TAUT:: =(skc5,skc6),general(skc5,skc5) -> general(skc5,skc6)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Conflict found: 83:2:2:[10.2,11.1]:TopTop: artifact(x0,x1) -> entity(x0,x1) {x0 -> skc5, x1 -> skc9}
% 0.64/0.53 === Backtracking. Learning clause 95:2:2:[83.2,14.1,71.2,28.2]:TopTop: chevy(x0,x1) -> existent(x0,x1)
% 0.64/0.53 === CC is in false state. New clause to be learned: 97:2:0:[38.0,96.1]:: =(skc9,skc5) -> placename(skc9,skc8)
% 0.64/0.53 === Restarting.
% 0.64/0.53 === Backtracking. Learning clause 98:2:2:[2.2,88.1,1.2]:TopTop: entity(x0,x1),barrel(x0,x1) ->
% 0.64/0.53 === Clause set with instances from active satisfied. Growing active. New size: 340
% 0.64/0.53 === Backtracking. Learning clause 99:2:2:[28.2,71.1]:TopTop: chevy(x0,x1) -> artifact(x0,x1)
% 0.64/0.53
% 0.64/0.53 Linear Model Building succeeded.
% 0.64/0.53 SZS status Satisfiable
% 0.64/0.53
% 0.64/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.64/0.53
% 0.64/0.53 SPASS-SCL-FOL Statistics:
% 0.64/0.53 Number of learned clauses: 26
% 0.64/0.53 Number of propagations: 3857
% 0.64/0.53 Number of decisions: 726
% 0.64/0.53 Number of resolutions: 41
% 0.64/0.53 Number of condensations: 0
% 0.64/0.53 Number of sub resolutions: 4
% 0.64/0.53 Number of input literals (deduplicated): 49
% 0.64/0.53 Number of grows: 9
% 0.64/0.53 Number of considered ground atoms: 340
% 0.64/0.53
% 0.64/0.53 Needed: 0:00:00.09
% 0.64/0.53
%------------------------------------------------------------------------------