%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS008-1 : TPTP v9.2.1. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:26:15 PM UTC 2026
% Result : Satisfiable 15.20s 3.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS008-1 : TPTP v9.2.1. Released v2.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.34 % Computer : n010.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Thu May 7 12:19:07 EDT 2026
% 0.18/0.34 % CPUTime :
% 0.18/0.34 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 15.20/3.58 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.58 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.58 Execution lmodel_grow ended with status: satisfiable
% 15.20/3.58 Used heuristic: lmodel_grow
% 15.20/3.58
% 15.20/3.58 Input Clauses:
% 15.20/3.58
% 15.20/3.58 Predicates: e f s2least c equalish s s1most d r r2most
% 15.20/3.58 Fol Constants: exist
% 15.20/3.58 Fol Functions: u1r2 u1r1 u3r2 u3r1 u4r2 u4r1 u5r2 u5r1 u5r3 u6r2 u6r1 u6r4 u6r3
% 15.20/3.58 Problem Properties:
% 15.20/3.58 This is a full first-order problem without equality.
% 15.20/3.58
% 15.20/3.58 After reduction: Problem Properties:
% 15.20/3.58 This is a full first-order problem without equality.
% 15.20/3.58
% 15.20/3.58
% 15.20/3.58 Reduced Input Clauses:
% 15.20/3.58
% 15.20/3.58 Most General Atoms: s2least(x0) s(x0,x2) s1most(x0) e(x0) r2most(x0) r(x0,x3) equalish(x2,x3) f(x0) d(x1) c(x2)
% 15.20/3.58
% 15.20/3.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 74 atoms initially, heuristics mode: lmodel_grow ===
% 15.20/3.58
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 89
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 102
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 120
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 133
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 151
% 15.20/3.58 === Backtracking. Learning clause 55:4:2:[8.4,12.1]:TopTop: s(x0,u3r2(x1)),s(x0,u3r1(x1)) -> s2least(x0),s1most(x1)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 171
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 192
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 212
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 224
% 15.20/3.58 === Backtracking. Learning clause 56:8:5:[4.1,8.3,20.3]:TopTopTopTopTop: s(x0,x1),s(x0,x2),r2most(x3),r(x3,x0),r(x3,x4),d(x4) -> equalish(x1,x2),e(x3)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 249
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 267
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 287
% 15.20/3.58 === Backtracking. Learning clause 57:8:4:[4.2,20.3,55.3]:TopTopTopTop: r2most(x0),r(x0,x1),r(x0,x2),d(x2),s(x1,u3r2(x3)),s(x1,u3r1(x3)) -> e(x0),s1most(x3)
% 15.20/3.58 === Conflict found: 55:4:2:[8.4,12.1]:TopTop: s(x0,u3r2(x1)),s(x0,u3r1(x1)) -> s2least(x0),s1most(x1) {x0 -> u6r3(u6r2(exist)), x1 -> u6r3(u6r2(exist))}
% 15.20/3.58 === Backtracking. Learning clause 58:2:1:[55.2,13.2,14.2,10.1]:Top: -> s2least(x0),d(x0)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 309
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 322
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 339
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 355
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 373
% 15.20/3.58 === Backtracking. Learning clause 59:2:1:[11.4,5.2,7.2,6.2,3.2]:Top: s1most(x0),c(x0) ->
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 399
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 414
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 426
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 436
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 443
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 452
% 15.20/3.58 === Backtracking. Learning clause 60:6:3:[4.1,58.1,29.4,4.2]:TopTopTop: f(x0),r(x0,x1),r(x0,x2),s2least(x2) -> d(x1),equalish(x1,x2)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 473
% 15.20/3.58 === Conflict found: 57:8:4:[4.2,20.3,55.3]:TopTopTopTop: r2most(x0),r(x0,x1),r(x0,x2),d(x2),s(x1,u3r2(x3)),s(x1,u3r1(x3)) -> e(x0),s1most(x3) {x0 -> u6r2(exist), x1 -> u6r4(u4r1(exist)), x2 -> u6r2(u6r2(exist)), x3 -> u6r4(u4r1(exist))}
% 15.20/3.58 === Backtracking. Learning clause 61:8:4:[57.4,10.2]:TopTopTopTop: r2most(x0),r(x0,x1),r(x0,x2),s(x1,u3r2(x3)),s(x1,u3r1(x3)),s1most(x2) -> e(x0),s1most(x3)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 494
% 15.20/3.58 === Conflict found: 58:2:1:[55.2,13.2,14.2,10.1]:Top: -> s2least(x0),d(x0) {x0 -> u6r2(u6r2(exist))}
% 15.20/3.58 === Backtracking. Learning clause 62:2:1:[58.1,4.1]:Top: -> d(x0),c(x0)
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 517
% 15.20/3.58 === Backtracking. Learning clause 63:2:1:[4.2,59.2]:Top: s2least(x0),s1most(x0) ->
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 535
% 15.20/3.58 === Backtracking. Learning clause 64:2:1:[9.2,59.1]:Top: d(x0),c(x0) ->
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 559
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 585
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 604
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 617
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 625
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 637
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 644
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 649
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 659
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 668
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 676
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 683
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 691
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 700
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 707
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 713
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 722
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 731
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 741
% 15.20/3.58 === Clause set with instances from active satisfied. Growing active. New size: 751
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 760
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 765
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 775
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 786
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 798
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 803
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 811
% 15.20/3.59 === Backtracking. Learning clause 66:3:1:[22.0,65.1,28.5,60.5,26.2,58.1,28.5,25.2,24.1,23.1,27.2,62.1]:Top: f(x0) -> r2most(x0),c(u5r3(x0))
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 821
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 831
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 841
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 850
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 856
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 862
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 867
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 879
% 15.20/3.59 === Backtracking. Learning clause 67:8:3:[29.6,24.1,26.2,62.2,27.2,66.3,28.4,58.2,33.2]:TopTopTop: f(x0),r(x0,u5r2(x1)),r(x0,x2),equalish(u6r2(x1),u6r1(x1)) -> r2most(x1),equalish(u5r2(x1),x2),s2least(x2),r(x1,u6r3(x1))
% 15.20/3.59 === Conflict found: 66:3:1:[22.0,65.1,28.5,60.5,26.2,58.1,28.5,25.2,24.1,23.1,27.2,62.1]:Top: f(x0) -> r2most(x0),c(u5r3(x0)) {x0 -> u6r3(exist)}
% 15.20/3.59 === Backtracking. Learning clause 68:7:3:[66.3,29.4]:TopTopTop: f(x0),f(x1),r(x1,u5r3(x0)),r(x1,x2),c(x2) -> r2most(x0),equalish(u5r3(x0),x2)
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 888
% 15.20/3.59 === Conflict found: 68:7:3:[66.3,29.4]:TopTopTop: f(x0),f(x1),r(x1,u5r3(x0)),r(x1,x2),c(x2) -> r2most(x0),equalish(u5r3(x0),x2) {x0 -> u4r2(exist), x1 -> u4r2(exist), x2 -> u5r1(u4r2(exist))}
% 15.20/3.59 === Backtracking. Learning clause 69:3:1:[68.7,23.1,27.2,25.2]:Top: f(x0),c(u5r1(x0)) -> r2most(x0)
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 898
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 907
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 914
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 922
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 929
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 935
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 940
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 945
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 956
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 963
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 971
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 977
% 15.20/3.59 === Clause set with instances from active satisfied. Growing active. New size: 983
% 15.20/3.59
% 15.20/3.59 Linear Model Building succeeded.
% 15.20/3.59 SZS status Satisfiable
% 15.20/3.59
% 15.20/3.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.20/3.59
% 15.20/3.59 SPASS-SCL-FOL Statistics:
% 15.20/3.59 Number of learned clauses: 14
% 15.20/3.59 Number of propagations: 2062
% 15.20/3.59 Number of decisions: 2726
% 15.20/3.59 Number of resolutions: 40
% 15.20/3.59 Number of condensations: 0
% 15.20/3.59 Number of sub resolutions: 1
% 15.20/3.59 Number of input literals (deduplicated): 38
% 15.20/3.59 Number of grows: 76
% 15.20/3.59 Number of considered ground atoms: 983
% 15.20/3.59
% 15.20/3.59 Needed: 0:00:03.05
% 15.20/3.59
%------------------------------------------------------------------------------