%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRA017+1 : TPTP v9.2.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.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:22:36 PM UTC 2026
% Result : CounterSatisfiable 139.31s 28.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA017+1 : TPTP v9.2.1. Released v3.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.34 % Computer : n028.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Thu May 7 11:59:16 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 139.31/28.32 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32 Execution lmodel_grow ended with status: satisfiable
% 139.31/28.32 Used heuristic: lmodel_grow
% 139.31/28.32
% 139.31/28.32 Input Clauses:
% 139.31/28.32
% 139.31/28.32 Predicates: less_than red goal green
% 139.31/28.32 Fol Constants: n1 n2 n3 n4 n5 n6 n7 n8 n9 n10 n11 n12 n13
% 139.31/28.32 Fol Functions:
% 139.31/28.32 Problem Properties:
% 139.31/28.32 This is a Bernays Schoenfinkel problem.
% 139.31/28.32
% 139.31/28.32 After reduction: Problem Properties:
% 139.31/28.32 This is a Bernays Schoenfinkel problem.
% 139.31/28.32
% 139.31/28.32
% 139.31/28.32 Reduced Input Clauses:
% 139.31/28.32 19:6:4:[18.0,13.6]:TopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x0,x3),red(x1,x3),red(x2,x3) ->
% 139.31/28.32 20:6:4:[18.0,14.6]:TopTopTopTop: green(x0,x1),green(x0,x2),green(x1,x2),green(x0,x3),green(x1,x3),green(x2,x3) ->
% 139.31/28.32 21:2:2:[18.0,15.2]:TopTop: red(x0,x1),green(x0,x1) ->
% 139.31/28.32
% 139.31/28.32 Most General Atoms: red(x2,x3) green(x2,x3) less_than(x0,x2) goal
% 139.31/28.32
% 139.31/28.32 === Starting SPASS-SCL-FOL A Little Less Naive, considering 508 atoms initially, heuristics mode: lmodel_grow ===
% 139.31/28.32
% 139.31/28.32 === Conflict found: 19:6:4:[18.0,13.6]:TopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x0,x3),red(x1,x3),red(x2,x3) -> {x0 -> n1, x1 -> n3, x2 -> n6, x3 -> n13}
% 139.31/28.32 === Backtracking. Learning clause 22:25:11:[19.6,17.2,17.2,20.1,20.4,17.3,19.3,17.2,20.1]:TopTopTopTopTopTopTopTopTopTopTop: red(x0,x1),red(x1,x2),red(x0,x3),red(x1,x3),less_than(x2,x3),less_than(x0,x2),green(x0,x4),green(x0,x5),green(x2,x5),green(x4,x5),green(x2,x6),green(x4,x6),green(x4,x3),green(x6,x3),less_than(x2,x4),red(x7,x2),red(x7,x4),red(x7,x8),red(x2,x8),less_than(x4,x8),green(x4,x9),green(x8,x9),green(x4,x10),green(x8,x10),green(x9,x10) ->
% 139.31/28.32 === Conflict found: 19:6:4:[18.0,13.6]:TopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x0,x3),red(x1,x3),red(x2,x3) -> {x0 -> n1, x1 -> n3, x2 -> n10, x3 -> n13}
% 139.31/28.32 === Backtracking. Learning clause 23:16:8:[19.2,17.2,17.2,20.2,20.2]:TopTopTopTopTopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x3,x2),less_than(x0,x3),less_than(x1,x3),green(x1,x4),green(x4,x3),green(x1,x5),green(x4,x5),green(x3,x5),green(x0,x6),green(x6,x3),green(x0,x7),green(x6,x7),green(x3,x7) ->
% 139.31/28.32 === Backtracking. Learning clause 24:58:23:[17.2,19.2,20.1,17.2,20.4,17.3,19.3,17.2,23.8,17.2,22.24]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: less_than(x0,x1),red(x0,x2),red(x2,x1),red(x0,x3),red(x2,x3),green(x0,x4),green(x0,x5),green(x1,x5),green(x4,x5),less_than(x1,x3),green(x1,x6),green(x4,x6),green(x4,x3),green(x6,x3),less_than(x1,x4),red(x7,x1),red(x7,x4),red(x7,x8),red(x1,x8),less_than(x4,x8),red(x9,x10),red(x9,x11),red(x10,x11),less_than(x9,x8),less_than(x10,x8),green(x10,x4),green(x10,x12),green(x4,x12),green(x8,x12),green(x9,x4),green(x9,x13),green(x4,x13),green(x8,x13),less_than(x8,x11),red(x14,x15),red(x15,x16),red(x14,x17),red(x15,x17),less_than(x16,x17),less_than(x14,x16),green(x14,x18),green(x14,x19),green(x16,x19),green(x18,x19),green(x16,x20),green(x18,x20),green(x18,x17),green(x20,x17),less_than(x16,x18),red(x21,x16),red(x21,x18),red(x21,x8),red(x16,x8),less_than(x18,x8),green(x18,x22),green(x8,x22),green(x18,x11),green(x22,x11) ->
% 139.31/28.32 === Backtracking. Learning clause 25:11:6:[17.2,19.4,20.2]:TopTopTopTopTopTop: less_than(x0,x1),red(x0,x2),red(x0,x3),red(x2,x3),red(x2,x1),red(x3,x1),green(x0,x4),green(x4,x1),green(x0,x5),green(x4,x5),green(x1,x5) ->
% 139.31/28.32 === Conflict found: 19:6:4:[18.0,13.6]:TopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x0,x3),red(x1,x3),red(x2,x3) -> {x0 -> n9, x1 -> n2, x2 -> n11, x3 -> n12}
% 139.31/28.32 === Backtracking. Learning clause 26:20:9:[19.5,17.2,17.2,20.6,20.4,17.3,19.5]:TopTopTopTopTopTopTopTopTop: red(x0,x1),red(x0,x2),red(x1,x2),red(x0,x3),less_than(x1,x3),less_than(x2,x3),green(x4,x5),green(x4,x2),green(x5,x2),green(x4,x3),green(x1,x6),green(x1,x5),green(x6,x5),green(x6,x3),less_than(x5,x3),red(x7,x5),red(x7,x8),red(x5,x8),red(x7,x3),red(x8,x3) ->
% 139.31/28.32
% 139.31/28.32 Linear Model Building succeeded.
% 139.31/28.32 SZS status Satisfiable
% 139.31/28.32
% 139.31/28.32 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 139.31/28.32
% 139.31/28.32 SPASS-SCL-FOL Statistics:
% 139.31/28.32 Number of learned clauses: 5
% 139.31/28.32 Number of propagations: 498
% 139.31/28.32 Number of decisions: 147
% 139.31/28.32 Number of resolutions: 30
% 139.31/28.32 Number of condensations: 0
% 139.31/28.32 Number of sub resolutions: 3
% 139.31/28.32 Number of input literals (deduplicated): 16
% 139.31/28.32 Number of grows: 0
% 139.31/28.32 Number of considered ground atoms: 508
% 139.31/28.32
% 139.31/28.32 Needed: 0:0:27.80
% 139.31/28.32
%------------------------------------------------------------------------------