%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP024-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 : n014.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:03 PM UTC 2026
% Result : Satisfiable 0.47s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP024-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.17/0.34 % Computer : n014.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:43:37 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.47/0.69 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69 Execution lmodel_grow ended with status: satisfiable
% 0.47/0.69 Used heuristic: lmodel_grow
% 0.47/0.69
% 0.47/0.69 Input Clauses:
% 0.47/0.69
% 0.47/0.69 Predicates: dance event eventuality thing singleton specific nonexistent unisex desire_want proposition relation abstraction nonhuman general forename relname mia_forename woman human_person organism entity existent impartial living human animate female vincent_forename man male accessible_world present agent theme of = actual_world
% 0.47/0.69 Fol Constants: skc8 skc15 skc10 skc13 skc12 skc11 skc9 skc14
% 0.47/0.69 Fol Functions:
% 0.47/0.69 Problem Properties:
% 0.47/0.69 This is a Bernays Schoenfinkel Ramsey problem.
% 0.47/0.69
% 0.47/0.69
% 0.47/0.69 Reduced Input Clauses:
% 0.47/0.69 94:9:3:[1.1,93.6]:TopTopTop: present(skc8,x0),desire_want(skc8,x0),agent(skc8,x0,skc15),dance(x1,x2),present(x1,x2),agent(x1,x2,skc15),accessible_world(skc8,x1),theme(skc8,x0,x1),proposition(skc8,x1) ->
% 0.47/0.69
% 0.47/0.69 Most General Atoms: accessible_world(x0,x1) dance(x1,x2) event(x1,x2) eventuality(x1,x2) thing(x1,x2) singleton(x1,x2) specific(x1,x2) nonexistent(x1,x2) unisex(x1,x2) present(x1,x2) relation(x1,x2) abstraction(x1,x2) nonhuman(x1,x2) general(x1,x2) forename(x1,x2) relname(x1,x2) mia_forename(x1,x2) woman(x1,x2) human_person(x1,x2) organism(x1,x2) existent(x1,x2) impartial(x1,x2) living(x1,x2) human(x1,x2) animate(x1,x2) female(x1,x2) vincent_forename(x1,x2) man(x1,x2) male(x1,x2) agent(x1,x2,x3) of(x0,x1,x3) entity(x0,x3) proposition(x0,x3) desire_want(x0,x4) theme(x0,x4,x3) =(x3,x2) actual_world(skc8)
% 0.47/0.69
% 0.47/0.69 === Starting SPASS-SCL-FOL A Little Less Naive, considering 62 atoms initially, heuristics mode: lmodel_grow ===
% 0.47/0.69
% 0.47/0.69 === CC is in false state. New clause to be learned: 95:1:0:TAUT:: -> =(skc8,skc8)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC model inconsistency. New clause to be learned: 96:4:0:TAUT:: =(skc8,skc15),=(skc8,skc10),dance(skc10,skc15) -> dance(skc8,skc8)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC is in false state. New clause to be learned: 98:2:0:[82.0,97.1]:: =(skc8,skc10) -> proposition(skc8,skc8)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC is in false state. New clause to be learned: 100:2:0:[75.0,99.1]:: =(skc8,skc15) -> man(skc8,skc8)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === Backtracking. Learning clause 101:2:2:[23.2,37.2,20.2]:TopTop: nonexistent(x0,x1),organism(x0,x1) ->
% 0.47/0.69 === CC model inconsistency. New clause to be learned: 103:3:0:[79.0,102.2]:: =(skc13,skc8),=(skc15,skc8) -> dance(skc10,skc15)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC model inconsistency. New clause to be learned: 105:2:0:[79.0,104.1]:: =(skc13,skc15) -> dance(skc10,skc15)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC model inconsistency. New clause to be learned: 106:1:0:TAUT:: -> =(skc13,skc13)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === Backtracking. Learning clause 107:2:2:[27.1,18.2]:TopTop: woman(x0,x1) -> animate(x0,x1)
% 0.47/0.69 === CC is in false state. New clause to be learned: 108:2:0:TAUT:: =(skc15,skc8) -> =(skc8,skc15)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === CC model inconsistency. New clause to be learned: 109:1:0:TAUT:: -> =(skc15,skc15)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 92
% 0.47/0.69 === CC is in false state. New clause to be learned: 111:2:0:[76.0,110.1]:: =(skc13,skc8) -> event(skc10,skc8)
% 0.47/0.69 === Restarting.
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 104
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 122
% 0.47/0.69 === Backtracking. Learning clause 112:2:2:[20.1,19.2]:TopTop: human_person(x0,x1) -> entity(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 137
% 0.47/0.69 === Conflict found: 101:2:2:[23.2,37.2,20.2]:TopTop: nonexistent(x0,x1),organism(x0,x1) -> {x0 -> skc10, x1 -> skc8}
% 0.47/0.69 === Backtracking. Learning clause 113:3:3:[101.1,6.2,58.3]:TopTopTop: eventuality(x0,x1),accessible_world(x2,x0),organism(x2,x1) ->
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 159
% 0.47/0.69 === Backtracking. Learning clause 114:3:3:[33.2,7.2,65.3]:TopTopTop: eventuality(x0,x1),accessible_world(x2,x0),female(x2,x1) ->
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 191
% 0.47/0.69 === Backtracking. Learning clause 115:4:4:[40.3,113.1]:TopTopTopTop: accessible_world(x0,x1),eventuality(x0,x2),accessible_world(x3,x1),organism(x3,x2) ->
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 219
% 0.47/0.69 === Backtracking. Learning clause 116:2:2:[1.2,2.1]:TopTop: dance(x0,x1) -> eventuality(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 242
% 0.47/0.69 === Backtracking. Learning clause 117:2:2:[36.1,28.2]:TopTop: male(x0,x1),woman(x0,x1) ->
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 261
% 0.47/0.69 === Backtracking. Learning clause 118:2:2:[20.2,22.1]:TopTop: organism(x0,x1) -> specific(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 272
% 0.47/0.69 === Backtracking. Learning clause 119:2:2:[5.1,2.2]:TopTop: event(x0,x1) -> specific(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 285
% 0.47/0.69 === Backtracking. Learning clause 120:2:2:[10.2,13.1]:TopTop: relation(x0,x1) -> general(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 290
% 0.47/0.69 === Backtracking. Learning clause 121:2:2:[34.2,22.2,120.2,16.2]:TopTop: entity(x0,x1),relname(x0,x1) ->
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 292
% 0.47/0.69 === Backtracking. Learning clause 122:2:2:[15.2,16.1]:TopTop: forename(x0,x1) -> relation(x0,x1)
% 0.47/0.69 === Clause set with instances from active satisfied. Growing active. New size: 294
% 0.47/0.69
% 0.47/0.69 Linear Model Building succeeded.
% 0.47/0.69 SZS status Satisfiable
% 0.47/0.69
% 0.47/0.69 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.69
% 0.47/0.69 SPASS-SCL-FOL Statistics:
% 0.47/0.69 Number of learned clauses: 13
% 0.47/0.69 Number of propagations: 2169
% 0.47/0.69 Number of decisions: 874
% 0.47/0.69 Number of resolutions: 18
% 0.47/0.69 Number of condensations: 0
% 0.47/0.69 Number of sub resolutions: 6
% 0.47/0.69 Number of input literals (deduplicated): 62
% 0.47/0.69 Number of grows: 14
% 0.47/0.69 Number of considered ground atoms: 294
% 0.47/0.69
% 0.47/0.69 Needed: 0:00:00.12
% 0.47/0.69
%------------------------------------------------------------------------------