%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GEO002-4 : TPTP v9.2.1. Released v1.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/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:21:37 PM UTC 2026
% Result : Unsatisfiable 5.00s 1.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO002-4 : TPTP v9.2.1. Released v1.1.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.33 % Computer : n028.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Thu May 7 11:54:16 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]
% 5.00/1.73 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73 Execution normal ended with status: unsatisfiable
% 5.00/1.73 Used heuristic: normal
% 5.00/1.73
% 5.00/1.73 Input Clauses:
% 5.00/1.73
% 5.00/1.73 Predicates: between equidistant equalish
% 5.00/1.73 Fol Constants: a b
% 5.00/1.73 Fol Functions: outer_pasch extension
% 5.00/1.73 Problem Properties:
% 5.00/1.73 This is a full first-order problem without equality.
% 5.00/1.73
% 5.00/1.73 After reduction: Problem Properties:
% 5.00/1.73 This is a full first-order problem without equality.
% 5.00/1.73
% 5.00/1.73
% 5.00/1.73 Reduced Input Clauses:
% 5.00/1.73
% 5.00/1.73 Most General Atoms: equidistant(x0,x1,x2,x2) equalish(x0,x1) equidistant(x0,extension(x1,x0,x2,x3),x2,x3) between(x2,x3,x1)
% 5.00/1.73
% 5.00/1.73 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: normal ===
% 5.00/1.73
% 5.00/1.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 5.00/1.73 === Backtracking. Learning clause 9:4:5:[7.3,1.1]:TopTopTopTopTop: equalish(x0,x1),between(x2,x3,x0),between(x3,x4,x1) -> between(x2,x3,x4)
% 5.00/1.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 5.00/1.73 === Clause set with instances from active satisfied. Growing active. New size: 242
% 5.00/1.73 === Backtracking. Learning clause 10:4:6:[7.3,1.2,2.2]:TopTopTopTopTopTop: between(x0,x1,x2),between(x3,x0,x4),equidistant(x2,x4,x5,x5) -> between(x3,x0,x1)
% 5.00/1.73 === Conflict found: 10:4:6:[7.3,1.2,2.2]:TopTopTopTopTopTop: between(x0,x1,x2),between(x3,x0,x4),equidistant(x2,x4,x5,x5) -> between(x3,x0,x1) {x0 -> b, x1 -> b, x2 -> b, x3 -> a, x4 -> extension(a,b,b,b), x5 -> b}
% 5.00/1.73 === Backtracking. Learning clause 11:4:6:[10.2,5.1,1.1,1.2,8.1]:TopTopTopTopTopTop: between(b,x0,x1),equidistant(x1,extension(a,b,x2,x3),x4,x4),between(b,x5,x0),between(a,a,x5) ->
% 5.00/1.73 === Conflict found: 9:4:5:[7.3,1.1]:TopTopTopTopTop: equalish(x0,x1),between(x2,x3,x0),between(x3,x4,x1) -> between(x2,x3,x4) {x0 -> extension(a,b,a,b), x1 -> extension(b,a,a,a), x2 -> a, x3 -> b, x4 -> a}
% 5.00/1.73 === Backtracking. Learning clause 12:3:6:[9.3,5.1]:TopTopTopTopTopTop: equalish(x0,extension(x1,x2,x3,x4)),between(x5,x1,x0) -> between(x5,x1,x2)
% 5.00/1.73 === Conflict found: 11:4:6:[10.2,5.1,1.1,1.2,8.1]:TopTopTopTopTopTop: between(b,x0,x1),equidistant(x1,extension(a,b,x2,x3),x4,x4),between(b,x5,x0),between(a,a,x5) -> {x0 -> a, x1 -> b, x2 -> b, x3 -> b, x4 -> b, x5 -> a}
% 5.00/1.73 === Backtracking. Learning clause 13:5:5:[11.2,6.1,10.4]:TopTopTopTopTop: between(b,x0,b),between(a,a,x1),between(x1,x0,x2),between(b,x1,x3),equidistant(x2,x3,x4,x4) ->
% 5.00/1.73 === Clause set with instances from active satisfied. Growing active. New size: 306
% 5.00/1.73 === Conflict found: 11:4:6:[10.2,5.1,1.1,1.2,8.1]:TopTopTopTopTopTop: between(b,x0,x1),equidistant(x1,extension(a,b,x2,x3),x4,x4),between(b,x5,x0),between(a,a,x5) -> {x0 -> b, x1 -> b, x2 -> b, x3 -> b, x4 -> b, x5 -> outer_pasch(a,b,b,a,a)}
% 5.00/1.73
% 5.00/1.73 SZS status Unsatisfiable
% 5.00/1.73
% 5.00/1.73 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.00/1.73
% 5.00/1.73 SPASS-SCL-FOL Statistics:
% 5.00/1.73 Number of learned clauses: 5
% 5.00/1.73 Number of propagations: 598
% 5.00/1.73 Number of decisions: 115
% 5.00/1.73 Number of resolutions: 20
% 5.00/1.73 Number of condensations: 0
% 5.00/1.73 Number of sub resolutions: 0
% 5.00/1.73 Number of input literals (deduplicated): 8
% 5.00/1.73 Number of grows: 4
% 5.00/1.73 Number of considered ground atoms: 306
% 5.00/1.73
% 5.00/1.73 Needed: 0:00:01.18
% 5.00/1.73
%------------------------------------------------------------------------------