%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : MSC016+1 : TPTP v9.2.1. Released v3.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:28:57 PM UTC 2026
% Result : CounterSatisfiable 5.44s 1.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MSC016+1 : TPTP v9.2.1. Released v3.5.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.33 % Computer : n009.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Thu May 7 12:42:41 EDT 2026
% 0.17/0.33 % CPUTime :
% 0.17/0.33 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.44/1.84 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84 Execution lmodel_grow ended with status: satisfiable
% 5.44/1.84 Used heuristic: lmodel_grow
% 5.44/1.84
% 5.44/1.84 Input Clauses:
% 5.44/1.84
% 5.44/1.84 Predicates: p flower animal ld__ ren1 ren2 ren3 ren4 ren5 ren6 ren7
% 5.44/1.84 Fol Constants: a b c e w d k lkg hill lilly pig horse cow aparna
% 5.44/1.84 Fol Functions: g h pet
% 5.44/1.84 Problem Properties:
% 5.44/1.84 This is a full first-order problem without equality.
% 5.44/1.84
% 5.44/1.84 After reduction: Problem Properties:
% 5.44/1.84 This is a full first-order problem without equality.
% 5.44/1.84
% 5.44/1.84
% 5.44/1.84 Reduced Input Clauses:
% 5.44/1.84
% 5.44/1.84 Most General Atoms: flower(lilly) animal(pig) animal(horse) animal(cow) animal(pet(aparna)) ld__(x1,x0) ren1(x2,x3,x0,x1) ren2(x1,x2,x0) ren3(x1,x2,x0) ren4(x1,x2,x0) ren5(x1,x2,x0) ren6(x1,x2,x0) ren7(x1,x2,x0) p(x0,x1,x2)
% 5.44/1.84
% 5.44/1.84 === Starting SPASS-SCL-FOL A Little Less Naive, considering 154 atoms initially, heuristics mode: lmodel_grow ===
% 5.44/1.84
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 166
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 177
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 186
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 194
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 206
% 5.44/1.84 === Backtracking. Learning clause 157:6:2:[151.1,126.1,156.6]:TopTop: p(x0,lkg,x1),ren2(x0,lkg,x1),ren3(x0,lkg,x1),ren4(x0,lkg,x1),ren5(x0,lkg,x1),ren7(x0,lkg,x1) ->
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 221
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 236
% 5.44/1.84 === Backtracking. Learning clause 158:2:3:[154.1,12.2]:TopTopTop: ld__(a,x0) -> ren7(x1,x0,x2)
% 5.44/1.84 === Backtracking. Learning clause 159:7:3:[156.4,146.2,142.2,152.2,139.2,155.2,147.2]:TopTopTop: p(x0,x1,x2),ld__(x2,c),ld__(x1,g(e,e)),ld__(x2,g(b,b)),ld__(x1,lkg),ld__(x2,a),ld__(x0,g(e,e)) ->
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 248
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 261
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 269
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 278
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 292
% 5.44/1.84 === Backtracking. Learning clause 160:1:2:[12.1,126.1]:TopTop: -> ld__(g(x0,x1),lkg)
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 311
% 5.44/1.84 === Backtracking. Learning clause 161:2:3:[146.1,12.2]:TopTopTop: ld__(c,x0) -> ren4(x1,x2,x0)
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 327
% 5.44/1.84 === Backtracking. Learning clause 162:2:4:[81.1,79.2,12.1,142.1]:TopTopTopTop: ld__(e,x0) -> ren3(x1,g(x0,x2),x3)
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 340
% 5.44/1.84 === Backtracking. Learning clause 163:7:3:[156.7,155.2,152.2,146.2,139.2,149.2]:TopTopTop: p(x0,x1,x2),ren3(x0,x1,x2),ld__(x2,a),ld__(x2,g(b,b)),ld__(x2,c),ld__(x1,lkg),ld__(x2,b) ->
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 361
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 376
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 393
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 409
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 427
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 439
% 5.44/1.84 === Backtracking. Learning clause 164:2:3:[145.1,12.2]:TopTopTop: ld__(b,x0) -> ren4(x1,x0,x2)
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 451
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 463
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 469
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 474
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 479
% 5.44/1.84 === Backtracking. Learning clause 165:1:2:[12.1,93.1]:TopTop: -> ld__(g(x0,x1),b)
% 5.44/1.84 === Conflict found: 162:2:4:[81.1,79.2,12.1,142.1]:TopTopTopTop: ld__(e,x0) -> ren3(x1,g(x0,x2),x3) {x0 -> a, x1 -> h(d), x2 -> c, x3 -> g(aparna,cow)}
% 5.44/1.84 === Backtracking. Learning clause 166:1:3:[162.1,90.1]:TopTopTop: -> ren3(x0,g(a,x1),x2)
% 5.44/1.84 === Backtracking. Learning clause 167:1:2:[141.1,87.1]:TopTop: -> ren3(a,x0,x1)
% 5.44/1.84 === Conflict found: 157:6:2:[151.1,126.1,156.6]:TopTop: p(x0,lkg,x1),ren2(x0,lkg,x1),ren3(x0,lkg,x1),ren4(x0,lkg,x1),ren5(x0,lkg,x1),ren7(x0,lkg,x1) -> {x0 -> k, x1 -> hill}
% 5.44/1.84 === Backtracking. Learning clause 168:6:2:[157.6,155.2,139.2]:TopTop: p(x0,lkg,x1),ren3(x0,lkg,x1),ren4(x0,lkg,x1),ren5(x0,lkg,x1),ld__(x1,a),ld__(lkg,lkg) ->
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 484
% 5.44/1.84 === Backtracking. Learning clause 169:1:2:[12.1,91.1]:TopTop: -> ld__(g(x0,x1),a)
% 5.44/1.84 === Conflict found: 157:6:2:[151.1,126.1,156.6]:TopTop: p(x0,lkg,x1),ren2(x0,lkg,x1),ren3(x0,lkg,x1),ren4(x0,lkg,x1),ren5(x0,lkg,x1),ren7(x0,lkg,x1) -> {x0 -> k, x1 -> hill}
% 5.44/1.84 === Backtracking. Learning clause 171:5:2:[137.0,170.5,157.3,143.2,148.2]:TopTop: p(x0,lkg,x1),ren2(x0,lkg,x1),ren4(x0,lkg,x1),ren7(x0,lkg,x1),ld__(x1,k) ->
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 498
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 505
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 514
% 5.44/1.84 === Backtracking. Learning clause 172:1:2:[12.1,103.1]:TopTop: -> ld__(g(x0,x1),c)
% 5.44/1.84 === Backtracking. Learning clause 173:1:0:[156.4,146.2,149.2,97.1,5.1,154.2,85.1,109.1,143.2,133.1,151.2,126.1]:: ren2(k,lkg,hill) ->
% 5.44/1.84 === Backtracking. Learning clause 174:2:4:[81.1,80.2]:TopTopTopTop: ld__(x0,x1) -> ld__(g(x2,x0),g(x3,x1))
% 5.44/1.84 === Backtracking. Learning clause 175:1:0:[12.1,88.1]:: -> ld__(a,k)
% 5.44/1.84 === Backtracking. Learning clause 176:1:3:[147.1,123.1]:TopTopTop: -> ren5(h(x0),x1,x2)
% 5.44/1.84 === Conflict found: 174:2:4:[81.1,80.2]:TopTopTopTop: ld__(x0,x1) -> ld__(g(x2,x0),g(x3,x1)) {x0 -> a, x1 -> e, x2 -> e, x3 -> e}
% 5.44/1.84 === Backtracking. Learning clause 177:2:4:[174.1,12.2,142.1]:TopTopTopTop: ld__(e,x0) -> ren3(x1,g(x2,x0),x3)
% 5.44/1.84 === Backtracking. Learning clause 178:2:4:[152.1,174.2]:TopTopTopTop: ld__(x0,b) -> ren6(x1,x2,g(x3,x0))
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 519
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 524
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 529
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 537
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 542
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 546
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 551
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 555
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 559
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 563
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 567
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 571
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 575
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 579
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 583
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 587
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 591
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 595
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 600
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 604
% 5.44/1.84 === Backtracking. Learning clause 179:2:4:[12.1,174.2]:TopTopTopTop: ld__(x0,x1) -> ld__(g(x2,x1),g(x3,x0))
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 612
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 617
% 5.44/1.84 === Backtracking. Learning clause 180:2:4:[81.1,79.2]:TopTopTopTop: ld__(x0,x1) -> ld__(g(x0,x2),g(x1,x3))
% 5.44/1.84 === Backtracking. Learning clause 181:7:3:[156.7,158.2]:TopTopTop: p(x0,x1,x2),ren2(x0,x1,x2),ren3(x0,x1,x2),ren4(x0,x1,x2),ren5(x0,x1,x2),ren6(x0,x1,x2),ld__(a,x1) ->
% 5.44/1.84 === Backtracking. Learning clause 182:1:2:[142.1,124.1]:TopTop: -> ren3(x0,w,x1)
% 5.44/1.84 === Backtracking. Learning clause 183:2:2:[12.1,82.2]:TopTop: ld__(x0,x1) -> ld__(h(x1),h(x0))
% 5.44/1.84 === Backtracking. Learning clause 184:1:0:[12.1,100.1]:: -> ld__(c,b)
% 5.44/1.84 === Backtracking. Learning clause 186:6:3:[141.1,185.2,156.6,150.2]:TopTopTop: p(x0,x1,x2),ren2(x0,x1,x2),ren4(x0,x1,x2),ren5(x0,x1,x2),ren7(x0,x1,x2),ld__(x0,h(d)) ->
% 5.44/1.84 === Conflict found: 186:6:3:[141.1,185.2,156.6,150.2]:TopTopTop: p(x0,x1,x2),ren2(x0,x1,x2),ren4(x0,x1,x2),ren5(x0,x1,x2),ren7(x0,x1,x2),ld__(x0,h(d)) -> {x0 -> a, x1 -> b, x2 -> c}
% 5.44/1.84 === Backtracking. Learning clause 187:6:3:[186.4,149.2,145.2]:TopTopTop: p(x0,x1,x2),ren2(x0,x1,x2),ren7(x0,x1,x2),ld__(x0,h(d)),ld__(x2,b),ld__(x1,b) ->
% 5.44/1.84 === Backtracking. Learning clause 188:7:3:[156.2,138.2]:TopTopTop: p(x0,x1,x2),ren3(x0,x1,x2),ren4(x0,x1,x2),ren5(x0,x1,x2),ren6(x0,x1,x2),ren7(x0,x1,x2),ld__(x0,k) ->
% 5.44/1.84 === Conflict found: 158:2:3:[154.1,12.2]:TopTopTop: ld__(a,x0) -> ren7(x1,x0,x2) {x0 -> b, x1 -> a, x2 -> c}
% 5.44/1.84 === Backtracking. Learning clause 191:1:0:[184.0,189.1,175.0,190.2,158.1,92.1,156.7,1.1,167.1,150.2,87.1,149.2,138.2]:: ren4(a,b,c) ->
% 5.44/1.84 === Backtracking. Learning clause 192:1:2:[149.1,184.1]:TopTop: -> ren5(x0,x1,c)
% 5.44/1.84 === Backtracking. Learning clause 193:1:0:[82.1,116.1]:: -> ld__(h(d),h(e))
% 5.44/1.84 === Conflict found: 163:7:3:[156.7,155.2,152.2,146.2,139.2,149.2]:TopTopTop: p(x0,x1,x2),ren3(x0,x1,x2),ld__(x2,a),ld__(x2,g(b,b)),ld__(x2,c),ld__(x1,lkg),ld__(x2,b) -> {x0 -> h(d), x1 -> g(a,c), x2 -> g(aparna,horse)}
% 5.44/1.84 === Backtracking. Learning clause 195:2:4:[172.0,194.1,163.4,180.2,160.1,169.1,165.1,166.1]:TopTopTopTop: p(x0,g(a,x1),g(x2,x3)),ld__(x2,b) ->
% 5.44/1.84 === Conflict found: 180:2:4:[81.1,79.2]:TopTopTopTop: ld__(x0,x1) -> ld__(g(x0,x2),g(x1,x3)) {x0 -> aparna, x1 -> w, x2 -> a, x3 -> a}
% 5.44/1.84 === Backtracking. Learning clause 196:1:2:[180.2,12.1,73.1]:TopTop: -> ld__(g(w,x0),g(aparna,x1))
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 622
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 628
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 634
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 639
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 644
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 649
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 655
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 660
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 665
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 668
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 670
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 674
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 678
% 5.44/1.84 === Clause set with instances from active satisfied. Growing active. New size: 681
% 5.44/1.84
% 5.44/1.84 Linear Model Building succeeded.
% 5.44/1.84 SZS status Satisfiable
% 5.44/1.84
% 5.44/1.84 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.44/1.84
% 5.44/1.84 SPASS-SCL-FOL Statistics:
% 5.44/1.84 Number of learned clauses: 35
% 5.44/1.84 Number of propagations: 10352
% 5.44/1.84 Number of decisions: 347
% 5.44/1.84 Number of resolutions: 73
% 5.44/1.84 Number of condensations: 0
% 5.44/1.84 Number of sub resolutions: 5
% 5.44/1.84 Number of input literals (deduplicated): 154
% 5.44/1.84 Number of grows: 66
% 5.44/1.84 Number of considered ground atoms: 681
% 5.44/1.84
% 5.44/1.84 Needed: 0:00:01.26
% 5.44/1.84
%------------------------------------------------------------------------------