%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : PUZ030-2 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:31:26 PM UTC 2026
% Result : Unsatisfiable 0.30s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ030-2 : TPTP v9.2.1. Released v1.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n008.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:57:44 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52 Execution normal ended with status: unsatisfiable
% 0.30/0.52 Used heuristic: normal
% 0.30/0.52
% 0.30/0.52 Input Clauses:
% 0.30/0.52
% 0.30/0.52 Predicates: salt_mill mustard_barry mustard_lang salt_lang salt_barry mustard_cole mustard_mill salt_cole mustard_dix salt_dix
% 0.30/0.52 Fol Constants: a
% 0.30/0.52 Fol Functions:
% 0.30/0.52 Problem Properties:
% 0.30/0.52 This is a propositional problem.
% 0.30/0.52
% 0.30/0.52 After reduction: Problem Properties:
% 0.30/0.52 This is a propositional problem.
% 0.30/0.52
% 0.30/0.52
% 0.30/0.52 Reduced Input Clauses:
% 0.30/0.52 64:3:0:[30.2,46.3]:: salt_cole,mustard_barry,salt_barry ->
% 0.30/0.52 65:4:0:[37.2,49.1]:: mustard_mill,salt_cole,mustard_dix,salt_dix ->
% 0.30/0.52 66:4:0:[62.2,52.1]:: salt_lang,salt_barry -> salt_dix,mustard_dix
% 0.30/0.52 67:4:0:[60.2,53.2]:: salt_lang,mustard_dix -> salt_barry,mustard_barry
% 0.30/0.52 68:4:0:[36.2,54.1]:: salt_barry,salt_cole,mustard_lang,salt_lang ->
% 0.30/0.52 75:3:0:[2.1,63.0,4.1,69.1,58.0,70.2,57.2,71.3,28.0,72.5,18.0,73.6,26.0,74.7]:: -> salt_lang,mustard_dix,mustard_mill
% 0.30/0.52
% 0.30/0.52 Most General Atoms: salt_mill mustard_barry mustard_lang salt_lang salt_barry mustard_cole mustard_mill salt_cole mustard_dix salt_dix
% 0.30/0.52
% 0.30/0.52 === Starting SPASS-SCL-FOL A Little Less Naive, considering 10 atoms initially, heuristics mode: normal ===
% 0.30/0.52
% 0.30/0.52 === Backtracking. Learning clause 76:3:0:[30.2,39.2]:: salt_barry -> salt_mill,salt_cole
% 0.30/0.52 === Backtracking. Learning clause 77:2:0:[36.1,41.2,57.3,43.1,76.1]:: -> salt_mill,salt_cole
% 0.30/0.52 === Backtracking. Learning clause 79:2:0:[76.2,78.0,15.1,66.3,17.1,11.1,56.2,68.3,34.3,64.2]:: salt_barry -> salt_mill
% 0.30/0.52 === Backtracking. Learning clause 80:1:0:[29.1,41.2,56.3,47.2,24.1,35.3,44.2,77.2,79.1]:: -> salt_mill
% 0.30/0.52 === Backtracking. Learning clause 81:3:0:[40.1,80.1,28.3,64.2,57.1,36.2]:: salt_barry,salt_lang -> mustard_cole
% 0.30/0.52 === Backtracking. Learning clause 84:4:0:[57.2,82.1,77.0,83.2,50.5,10.1]:: mustard_mill -> salt_cole,mustard_cole,salt_dix
% 0.30/0.52 === Conflict found: 75:3:0:[2.1,63.0,4.1,69.1,58.0,70.2,57.2,71.3,28.0,72.5,18.0,73.6,26.0,74.7]:: -> salt_lang,mustard_dix,mustard_mill {}
% 0.30/0.52 === Backtracking. Learning clause 85:2:0:[75.2,10.1,84.1,15.1,80.1,57.3,64.1,34.2,81.2]:: salt_barry -> mustard_cole
% 0.30/0.52 === Backtracking. Learning clause 86:2:0:[14.1,19.2,55.3,34.2,11.2,17.2,5.1,85.2]:: mustard_mill,salt_barry ->
% 0.30/0.52 === Backtracking. Learning clause 87:1:0:[12.3,80.1,17.2,68.3,34.3,64.2,27.2,85.2,86.1]:: salt_barry ->
% 0.30/0.52 === Backtracking. Learning clause 88:2:0:[40.1,80.1]:: mustard_mill -> mustard_barry
% 0.30/0.52 === Backtracking. Learning clause 89:2:0:[42.3,87.1]:: salt_lang -> mustard_lang
% 0.30/0.52 === Backtracking. Learning clause 91:1:0:[80.0,90.0,36.3,6.2,89.2]:: salt_lang ->
% 0.30/0.52 === Backtracking. Learning clause 93:1:0:[91.0,92.1,2.1,80.1]:: -> mustard_barry
% 0.30/0.52
% 0.30/0.52 SZS status Unsatisfiable
% 0.30/0.52
% 0.30/0.52 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/0.52
% 0.30/0.52 SPASS-SCL-FOL Statistics:
% 0.30/0.52 Number of learned clauses: 13
% 0.30/0.52 Number of propagations: 82
% 0.30/0.52 Number of decisions: 19
% 0.30/0.52 Number of resolutions: 57
% 0.30/0.52 Number of condensations: 0
% 0.30/0.52 Number of sub resolutions: 17
% 0.30/0.52 Number of input literals (deduplicated): 10
% 0.30/0.52 Number of grows: 0
% 0.30/0.52 Number of considered ground atoms: 10
% 0.30/0.52
% 0.30/0.52 Needed: 0:00:00.00
% 0.30/0.52
%------------------------------------------------------------------------------