%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : KRS009-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 : n021.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 0.68s 0.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS009-1 : TPTP v9.2.1. Released v2.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n021.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % 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:20:13 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.68/0.80 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80 Execution lmodel_grow ended with status: satisfiable
% 0.68/0.80 Used heuristic: lmodel_grow
% 0.68/0.80
% 0.68/0.80 Input Clauses:
% 0.68/0.80
% 0.68/0.80 Predicates: e p2least c equalish p p1most d a r t s s1most r1most t3least
% 0.68/0.80 Fol Constants: exist
% 0.68/0.80 Fol Functions: u1r2 u1r1 u3r2 u3r1 u7r1 u8r2 u8r1 u8r3 u9r2 u9r1 u10r2 u10r1
% 0.68/0.80 Problem Properties:
% 0.68/0.80 This is a full first-order problem without equality.
% 0.68/0.80
% 0.68/0.80 After reduction: Problem Properties:
% 0.68/0.80 This is a full first-order problem without equality.
% 0.68/0.80
% 0.68/0.80
% 0.68/0.80 Reduced Input Clauses:
% 0.68/0.80
% 0.68/0.80 Most General Atoms: p2least(x0) p(x0,x2) p1most(x0) c(x1) d(x1) e(x0) s1most(x0) r1most(x0) t3least(x0) a(x1) t(x0,x3) equalish(x2,x3) r(x0,x2) s(x0,x2)
% 0.68/0.80
% 0.68/0.80 === Starting SPASS-SCL-FOL A Little Less Naive, considering 69 atoms initially, heuristics mode: lmodel_grow ===
% 0.68/0.80
% 0.68/0.80 === Backtracking. Learning clause 42:2:2:[10.3,5.2,4.2,6.2,2.2,17.2]:TopTop: p1most(x0),r(x1,x0) ->
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 84
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 99
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 142
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 158
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 172
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 193
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 210
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 229
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 242
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 260
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 272
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 289
% 0.68/0.80 === Backtracking. Learning clause 43:2:1:[10.4,4.2,6.2,5.2,2.2]:Top: p1most(x0),c(x0) ->
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 302
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 315
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 333
% 0.68/0.80 === Backtracking. Learning clause 44:4:2:[7.4,11.1]:TopTop: p(x0,u3r2(x1)),p(x0,u3r1(x1)) -> p2least(x0),p1most(x1)
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 346
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 357
% 0.68/0.80 === Backtracking. Learning clause 45:4:2:[3.1,44.3]:TopTop: p(x0,u3r2(x1)),p(x0,u3r1(x1)) -> c(x0),p1most(x1)
% 0.68/0.80 === Backtracking. Learning clause 46:4:2:[9.2,15.1,45.4,16.1]:TopTop: p(x0,u3r2(x1)),p(x0,u3r1(x1)) -> a(x1),a(x0)
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 382
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 399
% 0.68/0.80 === Conflict found: 46:4:2:[9.2,15.1,45.4,16.1]:TopTop: p(x0,u3r2(x1)),p(x0,u3r1(x1)) -> a(x1),a(x0) {x0 -> u10r1(u9r1(exist)), x1 -> u10r1(u9r1(exist))}
% 0.68/0.80 === Backtracking. Learning clause 48:1:1:[15.0,47.1,46.2,12.2,13.2,9.1]:Top: -> a(x0)
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 414
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 434
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 450
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 470
% 0.68/0.80 === Conflict found: 43:2:1:[10.4,4.2,6.2,5.2,2.2]:Top: p1most(x0),c(x0) -> {x0 -> u10r2(u8r1(exist))}
% 0.68/0.80 === Backtracking. Learning clause 49:2:1:[43.1,8.2]:Top: c(x0),d(x0) ->
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 495
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 510
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 522
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 537
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 545
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 558
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 572
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 583
% 0.68/0.80 === Conflict found: 44:4:2:[7.4,11.1]:TopTop: p(x0,u3r2(x1)),p(x0,u3r1(x1)) -> p2least(x0),p1most(x1) {x0 -> u7r1(u9r1(exist)), x1 -> u7r1(u9r1(exist))}
% 0.68/0.80 === Backtracking. Learning clause 51:2:1:[13.1,50.0,44.2,12.2,3.1]:Top: -> p1most(x0),c(x0)
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 598
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 609
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 619
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 628
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 636
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 643
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 650
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 657
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 668
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 676
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 686
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 692
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 699
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 701
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 703
% 0.68/0.80 === Clause set with instances from active satisfied. Growing active. New size: 705
% 0.68/0.80
% 0.68/0.80 Linear Model Building succeeded.
% 0.68/0.80 SZS status Satisfiable
% 0.68/0.80
% 0.68/0.80 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.68/0.80
% 0.68/0.80 SPASS-SCL-FOL Statistics:
% 0.68/0.80 Number of learned clauses: 8
% 0.68/0.80 Number of propagations: 1330
% 0.68/0.80 Number of decisions: 1471
% 0.68/0.80 Number of resolutions: 20
% 0.68/0.80 Number of condensations: 0
% 0.68/0.80 Number of sub resolutions: 2
% 0.68/0.80 Number of input literals (deduplicated): 35
% 0.68/0.80 Number of grows: 48
% 0.68/0.80 Number of considered ground atoms: 705
% 0.68/0.80
% 0.68/0.80 Needed: 0:00:00.22
% 0.68/0.80
%------------------------------------------------------------------------------