%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP023-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 : n013.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 8.56s 2.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : NLP023-1 : TPTP v9.2.1. Released v2.4.0.
% 0.13/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.35 % Computer : n013.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Thu May 7 12:43:12 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 SPASS-SCL-FOL version:
% 0.17/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 8.56/2.26 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26 Execution resolution_3 ended with status: satisfiable
% 8.56/2.26 Used heuristic: resolution_3
% 8.56/2.26
% 8.56/2.26 Input Clauses:
% 8.56/2.26
% 8.56/2.26 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 accessible_world present agent theme of = actual_world
% 8.56/2.26 Fol Constants: skc6 skc8 skc11 skc10 skc9 skc7
% 8.56/2.26 Fol Functions:
% 8.56/2.26 Problem Properties:
% 8.56/2.26 This is a Bernays Schoenfinkel Ramsey problem.
% 8.56/2.26
% 8.56/2.26
% 8.56/2.26 Reduced Input Clauses:
% 8.56/2.26
% 8.56/2.26 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) 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(skc6)
% 8.56/2.26
% 8.56/2.26 === Starting SPASS-SCL-FOL A Little Less Naive, considering 64 atoms initially, heuristics mode: resolution_3 ===
% 8.56/2.26
% 8.56/2.26 === Backtracking. Learning clause 81:2:2:[13.2,30.1,10.2,9.2]:TopTop: specific(x0,x1),proposition(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 82:2:2:[13.2,30.1,10.2]:TopTop: specific(x0,x1),relation(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 83:2:2:[13.2,30.1]:TopTop: abstraction(x0,x1),specific(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 84:2:2:[15.2,16.1]:TopTop: forename(x0,x1) -> relation(x0,x1)
% 8.56/2.26 === Backtracking. Learning clause 85:2:2:[23.2,32.2,20.2,19.2,18.2]:TopTop: nonexistent(x0,x1),woman(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 86:2:2:[23.2,32.2,20.2,19.2]:TopTop: nonexistent(x0,x1),human_person(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 87:2:2:[23.2,32.2,20.2]:TopTop: nonexistent(x0,x1),organism(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 88:2:2:[23.2,32.2]:TopTop: entity(x0,x1),nonexistent(x0,x1) ->
% 8.56/2.26 === Backtracking. Learning clause 89:2:1:[59.1,74.1]:Top: animate(skc6,x0) -> animate(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 90:2:1:[57.1,74.1]:Top: living(skc6,x0) -> living(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 91:2:1:[56.1,74.1]:Top: impartial(skc6,x0) -> impartial(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 92:2:1:[46.1,74.1]:Top: nonhuman(skc6,x0) -> nonhuman(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 93:2:1:[42.1,74.1,8.1]:Top: desire_want(skc6,x0) -> event(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 94:2:1:[40.1,74.1]:Top: unisex(skc6,x0) -> unisex(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 95:2:1:[39.1,74.1]:Top: nonexistent(skc6,x0) -> nonexistent(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 96:2:1:[38.1,74.1]:Top: specific(skc6,x0) -> specific(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 97:2:1:[37.1,74.1]:Top: singleton(skc6,x0) -> singleton(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 98:2:1:[36.1,74.1]:Top: thing(skc6,x0) -> thing(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 99:2:1:[35.1,74.1]:Top: eventuality(skc6,x0) -> eventuality(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 100:2:1:[34.1,74.1]:Top: event(skc6,x0) -> event(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 101:2:1:[42.1,74.1]:Top: desire_want(skc6,x0) -> desire_want(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 102:2:1:[33.1,74.1]:Top: dance(skc6,x0) -> dance(skc8,x0)
% 8.56/2.26 === Backtracking. Learning clause 103:2:1:[41.2,69.1]:Top: accessible_world(skc8,x0) -> present(x0,skc11)
% 8.56/2.26 === CC is in false state. New clause to be learned: 104:1:0:TAUT:: -> =(skc6,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 106:3:0:[71.0,105.2]:: =(skc6,skc9),=(skc6,skc8) -> forename(skc8,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 108:3:0:[71.0,107.2]:: =(skc9,skc6),=(skc8,skc6) -> forename(skc8,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 109:2:0:TAUT:: =(skc9,skc6) -> =(skc6,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 110:1:0:TAUT:: -> =(skc9,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 111:1:0:TAUT:: -> =(skc8,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 86
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Conflict found: 93:2:1:[42.1,74.1,8.1]:Top: desire_want(skc6,x0) -> event(skc8,x0) {x0 -> skc7}
% 8.56/2.26 === Backtracking. Learning clause 112:1:0:[93.1,75.1]:: -> event(skc8,skc7)
% 8.56/2.26 === Backtracking. Learning clause 113:1:0:[8.1,75.1]:: -> event(skc6,skc7)
% 8.56/2.26 === Conflict found: 81:2:2:[13.2,30.1,10.2,9.2]:TopTop: specific(x0,x1),proposition(x0,x1) -> {x0 -> skc6, x1 -> skc8}
% 8.56/2.26 === Backtracking. Learning clause 114:1:0:[81.2,73.1]:: specific(skc6,skc8) ->
% 8.56/2.26 === Conflict found: 84:2:2:[15.2,16.1]:TopTop: forename(x0,x1) -> relation(x0,x1) {x0 -> skc6, x1 -> skc9}
% 8.56/2.26 === Backtracking. Learning clause 115:1:0:[84.1,71.1]:: -> relation(skc6,skc9)
% 8.56/2.26 === Conflict found: 85:2:2:[23.2,32.2,20.2,19.2,18.2]:TopTop: nonexistent(x0,x1),woman(x0,x1) -> {x0 -> skc6, x1 -> skc10}
% 8.56/2.26 === Backtracking. Learning clause 116:1:0:[85.2,68.1]:: nonexistent(skc6,skc10) ->
% 8.56/2.26 === Backtracking. Learning clause 117:2:1:[61.2,79.1]:Top: accessible_world(skc8,x0) -> agent(x0,skc11,skc10)
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 89
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 118:1:0:[5.2,114.1]:: eventuality(skc6,skc8) ->
% 8.56/2.26 === Backtracking. Learning clause 119:1:0:[6.2,116.1]:: eventuality(skc6,skc10) ->
% 8.56/2.26 === Conflict found: 82:2:2:[13.2,30.1,10.2]:TopTop: specific(x0,x1),relation(x0,x1) -> {x0 -> skc6, x1 -> skc9}
% 8.56/2.26 === Backtracking. Learning clause 120:1:0:[82.2,115.1]:: specific(skc6,skc9) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 92
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 121:1:0:[2.2,118.1]:: event(skc6,skc8) ->
% 8.56/2.26 === Backtracking. Learning clause 122:1:0:[2.2,119.1]:: event(skc6,skc10) ->
% 8.56/2.26 === Backtracking. Learning clause 123:1:0:[5.2,120.1]:: eventuality(skc6,skc9) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 95
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 124:1:0:[1.2,121.1]:: dance(skc6,skc8) ->
% 8.56/2.26 === Backtracking. Learning clause 125:1:0:[1.2,122.1]:: dance(skc6,skc10) ->
% 8.56/2.26 === Backtracking. Learning clause 126:1:0:[2.2,123.1]:: event(skc6,skc9) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 96
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 127:1:0:[1.2,126.1]:: dance(skc6,skc9) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 160
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 224
% 8.56/2.26 === CC is in false state. New clause to be learned: 128:3:0:TAUT:: =(skc6,skc11),present(skc6,skc11) -> present(skc6,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 130:2:0:[71.0,129.1]:: =(skc9,skc6) -> forename(skc6,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 132:2:0:[72.0,131.1]:: =(skc6,skc9) -> mia_forename(skc6,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 134:2:0:[70.0,133.1]:: =(skc6,skc11) -> dance(skc8,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 135:2:2:[20.2,22.1]:TopTop: organism(x0,x1) -> specific(x0,x1)
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 288
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 352
% 8.56/2.26 === Backtracking. Learning clause 136:3:3:[29.1,60.3]:TopTopTop: unisex(x0,x1),accessible_world(x2,x0),female(x2,x1) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 416
% 8.56/2.26 === Backtracking. Learning clause 137:3:3:[43.3,81.2]:TopTopTop: accessible_world(x0,x1),proposition(x0,x2),specific(x1,x2) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 480
% 8.56/2.26 === Backtracking. Learning clause 138:3:3:[31.2,46.3]:TopTopTop: human(x0,x1),accessible_world(x2,x0),nonhuman(x2,x1) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 140:2:0:[114.0,139.2]:: =(skc8,skc10),specific(skc6,skc10) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 544
% 8.56/2.26 === CC is in false state. New clause to be learned: 141:3:0:TAUT:: =(skc8,skc9),thing(skc11,skc8) -> thing(skc11,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 142:3:0:TAUT:: =(skc8,skc9),proposition(skc8,skc8) -> proposition(skc8,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 144:2:0:[74.0,143.1]:: =(skc8,skc9) -> accessible_world(skc6,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 145:3:3:[22.2,30.2,54.3,20.2]:TopTopTop: general(x0,x1),accessible_world(x2,x0),organism(x2,x1) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 608
% 8.56/2.26 === CC is in false state. New clause to be learned: 146:3:0:TAUT:: =(skc8,skc7),dance(skc8,skc7) -> dance(skc8,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 147:2:1:[4.1,11.2,97.1]:Top: abstraction(skc6,x0) -> singleton(skc8,x0)
% 8.56/2.26 === CC is in false state. New clause to be learned: 148:3:0:TAUT:: =(skc8,skc9),nonexistent(skc6,skc8) -> nonexistent(skc6,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Conflict found: 95:2:1:[39.1,74.1]:Top: nonexistent(skc6,x0) -> nonexistent(skc8,x0) {x0 -> skc7}
% 8.56/2.26 === Backtracking. Learning clause 149:2:1:[95.2,85.1,6.2,2.2]:Top: woman(skc8,x0),event(skc6,x0) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 150:3:0:TAUT:: =(skc8,skc9),forename(skc11,skc9) -> forename(skc11,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 151:3:0:TAUT:: =(skc6,skc11),relation(skc11,skc6) -> relation(skc6,skc11)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 152:3:0:TAUT:: =(skc9,skc6),specific(skc11,skc6) -> specific(skc11,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 153:3:0:TAUT:: =(skc8,skc10),specific(skc8,skc10) -> specific(skc8,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 154:3:0:TAUT:: =(skc8,skc9),dance(skc11,skc9) -> dance(skc11,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 155:2:2:[16.2,82.2]:TopTop: relname(x0,x1),specific(x0,x1) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 672
% 8.56/2.26 === Backtracking. Learning clause 156:2:2:[32.1,6.2]:TopTop: existent(x0,x1),eventuality(x0,x1) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 157:3:0:TAUT:: =(skc6,skc11),organism(skc11,skc6) -> organism(skc6,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 158:3:0:TAUT:: =(skc8,skc9),theme(skc6,skc6,skc9) -> theme(skc6,skc6,skc8)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 160:2:0:[70.0,159.1]:: =(skc8,skc7) -> dance(skc7,skc11)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 162:2:0:[69.0,161.1]:: =(skc6,skc11) -> present(skc8,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 163:2:0:TAUT:: =(skc11,skc6) -> =(skc6,skc11)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 164:1:0:TAUT:: -> =(skc11,skc11)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 737
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 801
% 8.56/2.26 === Backtracking. Learning clause 165:3:3:[13.1,10.2,145.1,9.2]:TopTopTop: accessible_world(x0,x1),organism(x0,x2),proposition(x1,x2) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 168:1:0:[113.0,166.1,121.0,167.2]:: =(skc8,skc7) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 170:2:0:[69.0,169.1]:: =(skc11,skc10) -> present(skc8,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 865
% 8.56/2.26 === Backtracking. Learning clause 171:2:2:[6.2,87.1,2.2,8.2]:TopTop: organism(x0,x1),desire_want(x0,x1) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 173:2:0:[70.0,172.1]:: =(skc11,skc10) -> dance(skc8,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 175:2:0:[71.0,174.1]:: =(skc11,skc9) -> forename(skc6,skc11)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 929
% 8.56/2.26 === Backtracking. Learning clause 176:2:2:[31.2,12.2,26.2]:TopTop: abstraction(x0,x1),human_person(x0,x1) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 993
% 8.56/2.26 === Backtracking. Learning clause 177:3:3:[10.1,9.2,14.1,136.1]:TopTopTop: proposition(x0,x1),accessible_world(x2,x0),female(x2,x1) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 178:2:0:TAUT:: =(skc10,skc6) -> =(skc6,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 179:2:2:[15.1,17.2,16.1,10.1,176.1]:TopTop: mia_forename(x0,x1),human_person(x0,x1) ->
% 8.56/2.26 === CC model inconsistency. New clause to be learned: 180:1:0:TAUT:: -> =(skc10,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 1058
% 8.56/2.26 === Backtracking. Learning clause 181:2:2:[20.1,19.2]:TopTop: human_person(x0,x1) -> entity(x0,x1)
% 8.56/2.26 === CC is in false state. New clause to be learned: 183:2:0:[119.0,182.2]:: =(skc10,skc6),eventuality(skc10,skc6) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 185:2:0:[121.0,184.2]:: =(skc10,skc6),event(skc10,skc8) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 186:3:0:TAUT:: =(skc10,skc6),dance(skc6,skc7) -> dance(skc10,skc7)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 1120
% 8.56/2.26 === Backtracking. Learning clause 187:3:3:[55.3,156.1]:TopTopTop: accessible_world(x0,x1),existent(x0,x2),eventuality(x1,x2) ->
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 1174
% 8.56/2.26 === CC is in false state. New clause to be learned: 189:2:0:[125.0,188.2]:: =(skc10,skc7),dance(skc6,skc7) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 191:2:0:[71.0,190.1]:: =(skc10,skc9) -> forename(skc6,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 192:2:2:[17.2,15.1]:TopTop: mia_forename(x0,x1) -> relname(x0,x1)
% 8.56/2.26 === CC is in false state. New clause to be learned: 193:3:0:TAUT:: =(skc10,skc6),thing(skc6,skc6) -> thing(skc10,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 194:3:0:TAUT:: =(skc10,skc6),thing(skc8,skc10) -> thing(skc8,skc6)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 195:3:0:TAUT:: =(skc10,skc7),dance(skc7,skc10) -> dance(skc10,skc7)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 196:3:3:[31.1,58.3]:TopTopTop: nonhuman(x0,x1),accessible_world(x2,x0),human(x2,x1) ->
% 8.56/2.26 === CC is in false state. New clause to be learned: 197:3:0:TAUT:: =(skc10,skc6),specific(skc6,skc6) -> specific(skc10,skc10)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Clause set with instances from active satisfied. Growing active. New size: 1208
% 8.56/2.26 === CC is in false state. New clause to be learned: 198:2:0:TAUT:: =(skc9,skc11) -> =(skc11,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 201:1:0:[113.0,199.1,122.0,200.2]:: =(skc10,skc7) ->
% 8.56/2.26 === Restarting.
% 8.56/2.26 === CC is in false state. New clause to be learned: 202:2:0:TAUT:: =(skc9,skc8) -> =(skc8,skc9)
% 8.56/2.26 === Restarting.
% 8.56/2.26 === Backtracking. Learning clause 203:2:2:[5.2,81.1,2.2]:TopTop: proposition(x0,x1),event(x0,x1) ->
% 8.56/2.26
% 8.56/2.26 Linear Model Building succeeded.
% 8.56/2.26 SZS status Satisfiable
% 8.56/2.26
% 8.56/2.26 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/2.26
% 8.56/2.26 SPASS-SCL-FOL Statistics:
% 8.56/2.26 Number of learned clauses: 58
% 8.56/2.26 Number of propagations: 28577
% 8.56/2.26 Number of decisions: 6883
% 8.56/2.26 Number of resolutions: 84
% 8.56/2.26 Number of condensations: 0
% 8.56/2.26 Number of sub resolutions: 20
% 8.56/2.26 Number of input literals (deduplicated): 48
% 8.56/2.26 Number of grows: 23
% 8.56/2.26 Number of considered ground atoms: 1208
% 8.56/2.26
% 8.56/2.26 Needed: 0:00:01.66
% 8.56/2.26
%------------------------------------------------------------------------------