%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : NLP094-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 : n006.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:11 PM UTC 2026
% Result : Unsatisfiable 0.53s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : NLP094-1 : TPTP v9.2.1. Released v2.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n006.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 12:44:01 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.18/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.53/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.57 Execution resolution_1 ended with status: unsatisfiable
% 0.53/0.57 Used heuristic: resolution_1
% 0.53/0.57
% 0.53/0.57 Input Clauses:
% 0.53/0.57
% 0.53/0.57 Predicates: actual_world ssSkC0 customer restaurant in event past nonreflexive see human_person drink coffee agent patient
% 0.53/0.57 Fol Constants: skc13 skc2
% 0.53/0.57 Fol Functions: skf39 skf34 skf25 skf20 skf26 skf29 skf27 skf28 skf12 skf14 skf13 skf15
% 0.53/0.57 Problem Properties:
% 0.53/0.57 This is a full first-order problem without equality.
% 0.53/0.57
% 0.53/0.57 After reduction: Problem Properties:
% 0.53/0.57 This is a full first-order problem without equality.
% 0.53/0.57
% 0.53/0.57
% 0.53/0.57 Reduced Input Clauses:
% 0.53/0.58
% 0.53/0.58 Most General Atoms: actual_world(x0) ssSkC0 customer(x0,skf39(x0)) restaurant(x0,skf34(x0)) customer(x0,skf25(x0)) restaurant(x0,skf20(x0)) in(x0,skf39(x0),skf34(x0)) in(x0,skf25(x0),skf20(x0)) restaurant(skc13,x0) in(skc13,x1,x0) customer(skc13,x1) restaurant(skc2,x0) in(skc2,x1,x0) customer(skc2,x1) see(x0,x1) agent(x0,x3,x2) human_person(x0,x2) drink(x0,x3) nonreflexive(x0,x3) past(x0,x3) event(x0,x3) coffee(x0,x4) patient(x0,x3,x4)
% 0.53/0.58
% 0.53/0.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 105 atoms initially, heuristics mode: resolution_1 ===
% 0.53/0.58
% 0.53/0.58 === Backtracking. Learning clause 49:7:4:[9.4,39.0,10.4,40.2,11.4,41.3,12.4,42.4,14.4,43.7,15.4,44.8,16.4,45.9,17.4,46.10,13.4,47.11,1.0,48.12,37.14,31.5,32.5]:TopTopTopTop: agent(skc13,skf26(x0),skf39(skc13)),patient(skc13,skf27(x0),x1),coffee(skc13,x1),restaurant(skc13,x2),in(skc13,x3,x2),customer(skc13,x3) -> ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 51:17:4:[1.0,50.13,37.2,29.5]:TopTopTopTop: event(skc13,skf26(skf39(skc13))),past(skc13,skf26(skf39(skc13))),nonreflexive(skc13,skf26(skf39(skc13))),see(skc13,skf26(skf39(skc13))),patient(skc13,x0,x1),coffee(skc13,x1),drink(skc13,x0),nonreflexive(skc13,x0),past(skc13,x0),event(skc13,x0),human_person(skc13,x2),agent(skc13,x0,x2),patient(skc13,skf26(skf39(skc13)),x2),restaurant(skc13,x3),in(skc13,skf39(skc13),x3),customer(skc13,skf39(skc13)) -> ssSkC0
% 0.53/0.58 === Clause set with instances from active satisfied. Growing active. New size: 129
% 0.53/0.58 === Restarting.
% 0.53/0.58 === Backtracking. Learning clause 53:4:1:[1.0,52.2,13.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> human_person(skc13,skf29(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 55:4:1:[1.0,54.2,12.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> see(skc13,skf26(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 57:4:1:[1.0,56.2,10.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> past(skc13,skf26(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 59:4:1:[1.0,58.2,9.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> event(skc13,skf26(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 61:4:1:[1.0,60.2,18.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> coffee(skc13,skf28(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 63:4:1:[1.0,62.2,15.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> nonreflexive(skc13,skf27(x0)),ssSkC0
% 0.53/0.58 === Backtracking. Learning clause 65:4:1:[1.0,64.2,16.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> past(skc13,skf27(x0)),ssSkC0
% 0.53/0.58 === Conflict found: 49:7:4:[9.4,39.0,10.4,40.2,11.4,41.3,12.4,42.4,14.4,43.7,15.4,44.8,16.4,45.9,17.4,46.10,13.4,47.11,1.0,48.12,37.14,31.5,32.5]:TopTopTopTop: agent(skc13,skf26(x0),skf39(skc13)),patient(skc13,skf27(x0),x1),coffee(skc13,x1),restaurant(skc13,x2),in(skc13,x3,x2),customer(skc13,x3) -> ssSkC0 {x0 -> skf39(skc13), x1 -> skc13, x2 -> skf34(skc13), x3 -> skf39(skc13)}
% 0.53/0.58 === Backtracking. Learning clause 66:6:2:[49.1,29.5]:TopTop: patient(skc13,skf27(skf39(skc13)),x0),coffee(skc13,x0),restaurant(skc13,x1),in(skc13,skf39(skc13),x1),customer(skc13,skf39(skc13)) -> ssSkC0
% 0.53/0.58 === Clause set with instances from active satisfied. Growing active. New size: 131
% 0.53/0.58 === Restarting.
% 0.53/0.58 === Backtracking. Learning clause 78:5:3:[19.4,67.0,20.4,68.2,21.4,69.3,22.4,70.4,28.4,71.5,24.4,72.6,25.4,73.7,26.4,74.8,27.4,75.9,23.4,76.10,2.0,77.11,38.14,36.5,35.5,34.5]:TopTopTop: agent(skc2,skf12(x0),skf25(skc2)),restaurant(skc2,x1),in(skc2,x2,x1),customer(skc2,x2),ssSkC0 ->
% 0.53/0.58 === Backtracking. Learning clause 79:4:1:[30.5,78.1]:Top: restaurant(skc2,x0),in(skc2,skf25(skc2),x0),customer(skc2,skf25(skc2)),ssSkC0 ->
% 0.53/0.58 === Conflict found: 79:4:1:[30.5,78.1]:Top: restaurant(skc2,x0),in(skc2,skf25(skc2),x0),customer(skc2,skf25(skc2)),ssSkC0 -> {x0 -> skf20(skc2)}
% 0.53/0.58 === Backtracking. Learning clause 80:1:0:[79.2,8.3,6.3,5.3,2.1]:: ssSkC0 ->
% 0.53/0.58 === Backtracking. Learning clause 83:3:1:[1.0,81.2,80.0,82.4,17.2,7.3]:Top: restaurant(skc13,skf34(skc13)),customer(skc13,skf39(skc13)) -> event(skc13,skf27(x0))
% 0.53/0.58 === Backtracking. Learning clause 85:4:1:[80.0,84.4,33.5,66.1]:Top: coffee(skc13,skf28(skf39(skc13))),restaurant(skc13,x0),in(skc13,skf39(skc13),x0),customer(skc13,skf39(skc13)) ->
% 0.53/0.58 === Conflict found: 85:4:1:[80.0,84.4,33.5,66.1]:Top: coffee(skc13,skf28(skf39(skc13))),restaurant(skc13,x0),in(skc13,skf39(skc13),x0),customer(skc13,skf39(skc13)) -> {x0 -> skf34(skc13)}
% 0.53/0.58
% 0.53/0.58 SZS status Unsatisfiable
% 0.53/0.58
% 0.53/0.58 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.53/0.58
% 0.53/0.58 SPASS-SCL-FOL Statistics:
% 0.53/0.58 Number of learned clauses: 15
% 0.53/0.58 Number of propagations: 279
% 0.53/0.58 Number of decisions: 1074
% 0.53/0.58 Number of resolutions: 27
% 0.53/0.58 Number of condensations: 5
% 0.53/0.58 Number of sub resolutions: 32
% 0.53/0.58 Number of input literals (deduplicated): 55
% 0.53/0.58 Number of grows: 2
% 0.53/0.58 Number of considered ground atoms: 131
% 0.53/0.58
% 0.53/0.58 Needed: 0:00:00.07
% 0.53/0.58
%------------------------------------------------------------------------------