%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : MSC009-1 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n027.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:56 PM UTC 2026
% Result : Satisfiable 145.14s 36.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : MSC009-1 : TPTP v9.2.1. Released v1.2.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 : n027.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:43:05 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 145.14/36.70 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70 Execution lmodel_grow ended with status: satisfiable
% 145.14/36.70 Used heuristic: lmodel_grow
% 145.14/36.70
% 145.14/36.70 Input Clauses:
% 145.14/36.70
% 145.14/36.70 Predicates: female male person sex parent child mother father grandparent parent_with_sons_only child_with_parent
% 145.14/36.70 Fol Constants: a
% 145.14/36.70 Fol Functions: sex_of1 child_of1 sex_of2 child_of2 female_child_of sex_of3
% 145.14/36.70 Problem Properties:
% 145.14/36.70 This is a full first-order problem without equality.
% 145.14/36.70
% 145.14/36.70 After reduction: Problem Properties:
% 145.14/36.70 This is a full first-order problem without equality.
% 145.14/36.70
% 145.14/36.70
% 145.14/36.70 Reduced Input Clauses:
% 145.14/36.70
% 145.14/36.70 Most General Atoms: sex(x0,x1) male(x1) female(x1) child(x0,x1) person(x1) mother(x0) father(x0) grandparent(x0) parent(x1) parent_with_sons_only(x0) child_with_parent(x1)
% 145.14/36.70
% 145.14/36.70 === Starting SPASS-SCL-FOL A Little Less Naive, considering 66 atoms initially, heuristics mode: lmodel_grow ===
% 145.14/36.70
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 76
% 145.14/36.70 === Backtracking. Learning clause 29:2:2:[2.2,6.2,5.2]:TopTop: sex(x0,x1) -> person(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 90
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 100
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 110
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 128
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 143
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 154
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 167
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 173
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 185
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 194
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 203
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 208
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 218
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 227
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 235
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 245
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 253
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 260
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 269
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 279
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 287
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 292
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 298
% 145.14/36.70 === Backtracking. Learning clause 30:5:3:[2.2,14.3,28.2]:TopTopTop: parent(x0),sex(x0,x1),sex(x2,x1) -> mother(x0),child_with_parent(x2)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 319
% 145.14/36.70 === Conflict found: 30:5:3:[2.2,14.3,28.2]:TopTopTop: parent(x0),sex(x0,x1),sex(x2,x1) -> mother(x0),child_with_parent(x2) {x0 -> child_of2(child_of1(a)), x1 -> sex_of3(child_of2(child_of1(a))), x2 -> child_of2(child_of1(a))}
% 145.14/36.70 === Backtracking. Learning clause 32:4:3:[15.1,31.0,30.4,16.2]:TopTopTop: sex(x0,x1),sex(x2,x1),father(x0) -> child_with_parent(x2)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 335
% 145.14/36.70 === Backtracking. Learning clause 33:5:4:[10.3,6.3,29.2]:TopTopTopTop: child(x0,x1),sex(x1,x2),female(x2),sex(x0,x3) -> parent(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 355
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 375
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 391
% 145.14/36.70 === Backtracking. Learning clause 34:3:2:[28.2,2.1]:TopTop: sex(x0,x1) -> child_with_parent(x0),female(x1)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 411
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 425
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 438
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 445
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 451
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 456
% 145.14/36.70 === Backtracking. Learning clause 35:4:4:[10.3,29.2,29.2]:TopTopTopTop: child(x0,x1),sex(x1,x2),sex(x0,x3) -> parent(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 484
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 503
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 526
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 545
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 562
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 584
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 606
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 630
% 145.14/36.70 === Conflict found: 30:5:3:[2.2,14.3,28.2]:TopTopTop: parent(x0),sex(x0,x1),sex(x2,x1) -> mother(x0),child_with_parent(x2) {x0 -> child_of2(child_of2(female_child_of(a))), x1 -> sex_of1(child_of2(child_of2(female_child_of(a)))), x2 -> child_of2(child_of2(female_child_of(a)))}
% 145.14/36.70 === Backtracking. Learning clause 37:3:1:[7.1,36.1,30.2,3.2]:Top: parent(x0) -> mother(x0),child_with_parent(x0)
% 145.14/36.70 === Conflict found: 35:4:4:[10.3,29.2,29.2]:TopTopTopTop: child(x0,x1),sex(x1,x2),sex(x0,x3) -> parent(x0) {x0 -> child_of2(a), x1 -> child_of2(a), x2 -> sex_of1(child_of2(a)), x3 -> sex_of1(child_of2(a))}
% 145.14/36.70 === Backtracking. Learning clause 38:3:2:[35.4,21.1]:TopTop: sex(x0,x1),child(x0,x0) -> grandparent(x0)
% 145.14/36.70 === Backtracking. Learning clause 39:4:2:[21.3,10.4,8.2,9.2]:TopTop: child(child_of1(x0),x1),person(x1),parent(x0) -> grandparent(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 657
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 680
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 700
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 723
% 145.14/36.70 === Backtracking. Learning clause 40:3:1:[23.2,19.2]:Top: parent_with_sons_only(x0),grandparent(x0) -> child_with_parent(child_of2(x0))
% 145.14/36.70 === Backtracking. Learning clause 41:6:3:[21.1,10.4]:TopTopTop: child(x0,x1),parent(x1),person(x0),child(x0,x2),person(x2) -> grandparent(x0)
% 145.14/36.70 === Conflict found: 37:3:1:[7.1,36.1,30.2,3.2]:Top: parent(x0) -> mother(x0),child_with_parent(x0) {x0 -> child_of2(child_of2(child_of2(female_child_of(a))))}
% 145.14/36.70 === Backtracking. Learning clause 42:2:1:[37.2,16.2,15.2]:Top: father(x0) -> child_with_parent(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 748
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 771
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 793
% 145.14/36.70 === Conflict found: 41:6:3:[21.1,10.4]:TopTopTop: child(x0,x1),parent(x1),person(x0),child(x0,x2),person(x2) -> grandparent(x0) {x0 -> child_of2(child_of1(child_of2(sex_of3(a)))), x1 -> child_of2(child_of2(child_of1(child_of2(sex_of3(a))))), x2 -> child_of2(child_of2(child_of1(child_of2(sex_of3(a)))))}
% 145.14/36.70 === Backtracking. Learning clause 43:7:4:[41.3,6.3]:TopTopTopTop: child(x0,x1),parent(x1),child(x0,x2),person(x2),sex(x0,x3),female(x3) -> grandparent(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 820
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 846
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 870
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 891
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 918
% 145.14/36.70 === Conflict found: 41:6:3:[21.1,10.4]:TopTopTop: child(x0,x1),parent(x1),person(x0),child(x0,x2),person(x2) -> grandparent(x0) {x0 -> child_of1(child_of2(female_child_of(a))), x1 -> child_of2(a), x2 -> child_of2(a)}
% 145.14/36.70 === Backtracking. Learning clause 44:6:3:[41.6,20.1]:TopTopTop: child(x0,x1),parent(x1),person(x0),child(x0,x2),person(x2) -> parent(child_of2(x0))
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 951
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 979
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1000
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1023
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1041
% 145.14/36.70 === Backtracking. Learning clause 45:3:2:[1.2,27.2,34.3]:TopTop: child_with_parent(x0),sex(x1,sex_of3(x0)) -> child_with_parent(x1)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1068
% 145.14/36.70 === Backtracking. Learning clause 46:5:4:[17.2,13.1,35.4]:TopTopTopTop: child(x0,x1),sex(x1,x2),sex(x0,x3) -> father(x0),female(sex_of2(x0))
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1095
% 145.14/36.70 === Backtracking. Learning clause 47:4:3:[26.2,35.2]:TopTopTop: child_with_parent(x0),child(x1,x0),sex(x1,x2) -> parent(x1)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1124
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1147
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1171
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1196
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1216
% 145.14/36.70 === Backtracking. Learning clause 48:4:3:[26.2,35.3]:TopTopTop: child_with_parent(x0),child(x0,x1),sex(x1,x2) -> parent(x0)
% 145.14/36.70 === Backtracking. Learning clause 49:2:1:[8.2,23.2,22.2]:Top: parent_with_sons_only(x0) -> child_with_parent(child_of1(x0))
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1241
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1269
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1294
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1314
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1329
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1343
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1352
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1364
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1382
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1391
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1399
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1408
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1420
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1426
% 145.14/36.70 === Backtracking. Learning clause 50:4:2:[2.2,14.3]:TopTop: parent(x0),sex(x0,x1) -> male(x1),mother(x0)
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1457
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1485
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1512
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1533
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1547
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1555
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1564
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1571
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1582
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1593
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1600
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1609
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1619
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1627
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1638
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1652
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1657
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1664
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1671
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1677
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1683
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1689
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1693
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1697
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1701
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1704
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1710
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1716
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1720
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1723
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1727
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1732
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1734
% 145.14/36.70 === Clause set with instances from active satisfied. Growing active. New size: 1736
% 145.14/36.70
% 145.14/36.70 Linear Model Building succeeded.
% 145.14/36.70 SZS status Satisfiable
% 145.14/36.70
% 145.14/36.70 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 145.14/36.70
% 145.14/36.70 SPASS-SCL-FOL Statistics:
% 145.14/36.70 Number of learned clauses: 20
% 145.14/36.70 Number of propagations: 6608
% 145.14/36.70 Number of decisions: 5563
% 145.14/36.70 Number of resolutions: 30
% 145.14/36.70 Number of condensations: 2
% 145.14/36.70 Number of sub resolutions: 2
% 145.14/36.70 Number of input literals (deduplicated): 22
% 145.14/36.70 Number of grows: 115
% 145.14/36.70 Number of considered ground atoms: 1736
% 145.14/36.70
% 145.14/36.70 Needed: 0:0:36.14
% 145.14/36.70
%------------------------------------------------------------------------------