%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP042+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 : n027.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:05 PM UTC 2026
% Result : CounterSatisfiable 0.40s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : NLP042+1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.35 % Computer : n027.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:35 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.40/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66 Execution resolution_1 ended with status: satisfiable
% 0.40/0.66 Used heuristic: resolution_1
% 0.40/0.66
% 0.40/0.66 Input Clauses:
% 0.40/0.66
% 0.40/0.66 Predicates: woman female human_person animate human organism living impartial entity mia_forename forename abstraction unisex general nonhuman thing relation relname object nonliving existent specific substance_matter food beverage shake_beverage order event eventuality nonexistent singleton act of = nonreflexive agent patient actual_world past
% 0.40/0.66 Fol Constants: skc1 skc2 skc3 skc4 skc5
% 0.40/0.66 Fol Functions:
% 0.40/0.66 Problem Properties:
% 0.40/0.66 This is a Bernays Schoenfinkel Ramsey problem.
% 0.40/0.66
% 0.40/0.66
% 0.40/0.66 Reduced Input Clauses:
% 0.40/0.66
% 0.40/0.66 Most General Atoms: woman(x0,x1) female(x0,x1) human_person(x0,x1) animate(x0,x1) human(x0,x1) organism(x0,x1) living(x0,x1) impartial(x0,x1) entity(x0,x1) mia_forename(x0,x1) abstraction(x0,x1) unisex(x0,x1) general(x0,x1) nonhuman(x0,x1) thing(x0,x1) relation(x0,x1) relname(x0,x1) object(x0,x1) nonliving(x0,x1) existent(x0,x1) specific(x0,x1) substance_matter(x0,x1) food(x0,x1) beverage(x0,x1) shake_beverage(x0,x1) order(x0,x1) event(x0,x1) eventuality(x0,x1) nonexistent(x0,x1) singleton(x0,x1) act(x0,x1) forename(x0,x3) of(x0,x3,x1) nonreflexive(x0,x1) agent(x0,x1,x2) patient(x0,x1,x3) =(x2,x3) actual_world(skc1) past(skc1,skc5)
% 0.40/0.66
% 0.40/0.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 34 atoms initially, heuristics mode: resolution_1 ===
% 0.40/0.66
% 0.40/0.66 === Backtracking. Learning clause 57:2:2:[10.2,42.1]:TopTop: abstraction(x0,x1),female(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 58:2:2:[15.1,16.2,14.1,57.1]:TopTop: forename(x0,x1),female(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 59:2:2:[41.1,21.2]:TopTop: general(x0,x1),entity(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 60:1:0:[27.1,50.1]:: -> beverage(skc1,skc4)
% 0.40/0.66 === Backtracking. Learning clause 61:2:2:[34.2,29.1,28.2]:TopTop: order(x0,x1) -> unisex(x0,x1)
% 0.40/0.66 === Backtracking. Learning clause 62:2:2:[34.2,29.1]:TopTop: event(x0,x1) -> unisex(x0,x1)
% 0.40/0.66 === Backtracking. Learning clause 64:2:1:[55.0,63.0,44.3,53.1]:Top: agent(skc1,skc5,x0),=(x0,skc4) ->
% 0.40/0.66 === CC model inconsistency. New clause to be learned: 65:1:0:TAUT:: -> =(skc3,skc3)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 66:2:2:[12.2,39.1]:TopTop: abstraction(x0,x1),human(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 67:2:2:[15.1,16.2,14.1,66.1]:TopTop: forename(x0,x1),human(x0,x1) ->
% 0.40/0.66 === CC is in false state. New clause to be learned: 69:2:0:[49.0,68.1]:: =(skc1,skc3) -> forename(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === CC is in false state. New clause to be learned: 70:2:0:TAUT:: =(skc3,skc1) -> =(skc1,skc3)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 44
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Conflict found: 67:2:2:[15.1,16.2,14.1,66.1]:TopTop: forename(x0,x1),human(x0,x1) -> {x0 -> skc1, x1 -> skc3}
% 0.40/0.66 === Backtracking. Learning clause 71:1:0:[67.1,49.1]:: human(skc1,skc3) ->
% 0.40/0.66 === Backtracking. Learning clause 72:1:0:[26.1,60.1]:: -> food(skc1,skc4)
% 0.40/0.66 === Conflict found: 61:2:2:[34.2,29.1,28.2]:TopTop: order(x0,x1) -> unisex(x0,x1) {x0 -> skc1, x1 -> skc5}
% 0.40/0.66 === Backtracking. Learning clause 73:1:0:[61.1,56.1]:: -> unisex(skc1,skc5)
% 0.40/0.66 === Conflict found: 64:2:1:[55.0,63.0,44.3,53.1]:Top: agent(skc1,skc5,x0),=(x0,skc4) -> {x0 -> skc2}
% 0.40/0.66 === Backtracking. Learning clause 74:1:0:[64.1,52.1]:: =(skc2,skc4) ->
% 0.40/0.66 === CC model inconsistency. New clause to be learned: 75:1:0:TAUT:: -> =(skc2,skc2)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 48
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 76:1:0:[42.1,73.1]:: female(skc1,skc5) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 49
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 77:2:2:[9.2,58.1]:TopTop: mia_forename(x0,x1),female(x0,x1) ->
% 0.40/0.66 === Conflict found: 58:2:2:[15.1,16.2,14.1,57.1]:TopTop: forename(x0,x1),female(x0,x1) -> {x0 -> skc1, x1 -> skc3}
% 0.40/0.66 === Backtracking. Learning clause 78:1:0:[58.1,49.1]:: female(skc1,skc3) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 51
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 79:1:0:[1.2,76.1]:: woman(skc1,skc5) ->
% 0.40/0.66 === CC model inconsistency. New clause to be learned: 80:1:0:TAUT:: -> =(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 81:1:0:[1.2,78.1]:: woman(skc1,skc3) ->
% 0.40/0.66 === Backtracking. Learning clause 82:1:0:[25.1,72.1]:: -> substance_matter(skc1,skc4)
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 53
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 83:1:0:[3.2,71.1]:: human_person(skc1,skc3) ->
% 0.40/0.66 === Backtracking. Learning clause 84:1:0:[24.1,82.1]:: -> object(skc1,skc4)
% 0.40/0.66 === CC is in false state. New clause to be learned: 86:2:0:[84.0,85.1]:: =(skc1,skc4) -> object(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 87:2:2:[30.2,38.2,34.2,28.2]:TopTop: existent(x0,x1),order(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 88:2:2:[30.2,38.2,34.2]:TopTop: existent(x0,x1),event(x0,x1) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 57
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 89:2:2:[15.1,16.2,14.1]:TopTop: forename(x0,x1) -> abstraction(x0,x1)
% 0.40/0.66 === Backtracking. Learning clause 90:2:2:[11.2,59.1,89.2,9.2]:TopTop: entity(x0,x1),mia_forename(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 91:2:2:[11.2,59.1,89.2]:TopTop: entity(x0,x1),forename(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 92:1:0:[23.1,84.1]:: -> entity(skc1,skc4)
% 0.40/0.66 === Backtracking. Learning clause 93:2:2:[30.2,38.2]:TopTop: eventuality(x0,x1),existent(x0,x1) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 58
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 94:2:2:[9.2,67.1]:TopTop: mia_forename(x0,x1),human(x0,x1) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 122
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 186
% 0.40/0.66 === CC is in false state. New clause to be learned: 95:3:0:TAUT:: =(skc1,skc5),agent(skc1,skc1,skc1) -> agent(skc1,skc5,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === CC is in false state. New clause to be learned: 96:2:0:TAUT:: =(skc1,skc3) -> =(skc3,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 97:2:2:[31.2,41.1]:TopTop: eventuality(x0,x1),general(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 98:2:2:[35.2,34.1]:TopTop: act(x0,x1) -> eventuality(x0,x1)
% 0.40/0.66 === CC is in false state. New clause to be learned: 99:3:0:TAUT:: =(skc1,skc5),specific(skc1,skc5) -> specific(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === CC is in false state. New clause to be learned: 100:3:0:TAUT:: =(skc1,skc5),thing(skc1,skc5) -> thing(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === CC is in false state. New clause to be learned: 101:3:0:TAUT:: =(skc1,skc2),entity(skc1,skc2) -> entity(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 102:2:2:[39.2,3.2]:TopTop: nonhuman(x0,x1),human_person(x0,x1) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 241
% 0.40/0.66 === Conflict found: 89:2:2:[15.1,16.2,14.1]:TopTop: forename(x0,x1) -> abstraction(x0,x1) {x0 -> skc2, x1 -> skc2}
% 0.40/0.66 === Backtracking. Learning clause 103:2:2:[89.2,13.1]:TopTop: forename(x0,x1) -> thing(x0,x1)
% 0.40/0.66 === CC is in false state. New clause to be learned: 104:3:0:TAUT:: =(skc2,skc1),human(skc1,skc2) -> human(skc1,skc1)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 305
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 369
% 0.40/0.66 === Backtracking. Learning clause 105:2:2:[41.2,11.2,31.2,34.2,28.2]:TopTop: abstraction(x0,x1),order(x0,x1) ->
% 0.40/0.66 === Backtracking. Learning clause 106:2:2:[30.1,34.2]:TopTop: event(x0,x1) -> nonexistent(x0,x1)
% 0.40/0.66 === CC is in false state. New clause to be learned: 107:3:0:TAUT:: =(skc2,skc5),entity(skc1,skc2) -> entity(skc1,skc5)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === CC is in false state. New clause to be learned: 108:2:0:TAUT:: =(skc2,skc1) -> =(skc1,skc2)
% 0.40/0.66 === Restarting.
% 0.40/0.66 === Backtracking. Learning clause 109:2:2:[11.2,97.2,89.2]:TopTop: eventuality(x0,x1),forename(x0,x1) ->
% 0.40/0.66 === Clause set with instances from active satisfied. Growing active. New size: 430
% 0.40/0.66 === Backtracking. Learning clause 110:2:2:[9.2,89.1]:TopTop: mia_forename(x0,x1) -> abstraction(x0,x1)
% 0.40/0.66
% 0.40/0.66 Linear Model Building succeeded.
% 0.40/0.66 SZS status Satisfiable
% 0.40/0.66
% 0.40/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.40/0.66
% 0.40/0.66 SPASS-SCL-FOL Statistics:
% 0.40/0.66 Number of learned clauses: 37
% 0.40/0.66 Number of propagations: 3269
% 0.40/0.66 Number of decisions: 852
% 0.40/0.66 Number of resolutions: 53
% 0.40/0.66 Number of condensations: 0
% 0.40/0.66 Number of sub resolutions: 3
% 0.40/0.66 Number of input literals (deduplicated): 49
% 0.40/0.66 Number of grows: 13
% 0.40/0.66 Number of considered ground atoms: 430
% 0.40/0.66
% 0.40/0.66 Needed: 0:00:00.09
% 0.40/0.66
%------------------------------------------------------------------------------