%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GEO259+1 : TPTP v9.2.1. Bugfixed v6.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:14 PM UTC 2026
% Result : Theorem 0.61s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO259+1 : TPTP v9.2.1. Bugfixed v6.4.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n019.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 11:57:15 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.61/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60 Execution resolution_2 ended with status: unsatisfiable
% 0.61/0.60 Used heuristic: resolution_2
% 0.61/0.60
% 0.61/0.60 Input Clauses:
% 0.61/0.60
% 0.61/0.60 Predicates: apart_point_and_line left_apart_point convergent_lines unequally_directed_lines divides_points before_on_line distinct_points between_on_line distinct_lines line left_convergent_lines point ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10
% 0.61/0.60 Fol Constants: skc1 skc2 skc3 skc4
% 0.61/0.60 Fol Functions: reverse_line line_connecting intersection_point parallel_through_point
% 0.61/0.60 Problem Properties:
% 0.61/0.60 This is a full first-order problem without equality.
% 0.61/0.60
% 0.61/0.60 After reduction: Problem Properties:
% 0.61/0.60 This is a full first-order problem without equality.
% 0.61/0.60
% 0.61/0.60
% 0.61/0.60 Reduced Input Clauses:
% 0.61/0.60 79:1:2:[49.0,1.1,49.0,78.2]:TopTop: apart_point_and_line(x0,x1) ->
% 0.61/0.60 80:1:3:[49.0,7.1]:TopTopTop: ren1(x0,x1,x2) ->
% 0.61/0.60 81:1:3:[49.0,10.1]:TopTopTop: ren2(x0,x1,x2) ->
% 0.61/0.60 83:1:3:[80.0,13.1,81.0,82.2]:TopTopTop: divides_points(x0,x1,x2) ->
% 0.61/0.60 99:2:4:[49.0,67.2,49.0,92.3,49.0,93.4,49.0,94.5,49.0,95.6,49.0,96.7,49.0,97.8,49.0,98.9]:TopTopTopTop: distinct_points(x0,x1),distinct_lines(x2,x3) ->
% 0.61/0.60 85:1:2:[49.0,16.1,49.0,84.2]:TopTop: ren3(x0,x1) ->
% 0.61/0.60 87:1:2:[49.0,19.1,49.0,86.2]:TopTop: ren4(x0,x1) ->
% 0.61/0.60 89:3:3:[85.0,26.1,87.0,88.2]:TopTopTop: distinct_points(x0,x1) -> unequally_directed_lines(x2,line_connecting(x0,x1)),before_on_line(x2,x0,x1)
% 0.61/0.60 91:2:2:[51.0,48.2,51.0,90.3]:TopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x0,reverse_line(x1)) ->
% 0.61/0.60
% 0.61/0.60 Most General Atoms: apart_point_and_line(x0,x1) convergent_lines(x0,x1) ren1(x0,x1,x2) ren2(x0,x1,x2) divides_points(x0,x1,x2) ren10(x0,x1) ren3(x1,x0) ren4(x2,x0) ren5(x0,x1,x2,x3) before_on_line(x0,x2,x3) ren6(x0,x3,x2,x1) between_on_line(x0,x3,x2,x1) distinct_points(x0,x2) distinct_lines(x1,x2) unequally_directed_lines(x1,x2) ren7(x0,x2) ren8(x1,x2) line(x1) left_apart_point(x0,x1) left_convergent_lines(x0,x1) point(x1) ren9(x0,x1)
% 0.61/0.60
% 0.61/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 84 atoms initially, heuristics mode: resolution_2 ===
% 0.61/0.60
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 84
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 100:1:2:[22.2,36.1]:TopTop: before_on_line(x0,x1,x1) ->
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 84
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 101:1:3:[30.2,100.1]:TopTopTop: ren6(x0,x1,x1,x2) ->
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 102:2:2:[41.2,40.1]:TopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x1,x0)
% 0.61/0.60 === Backtracking. Learning clause 103:1:1:[45.2,40.1]:Top: ren8(reverse_line(x0),x0) ->
% 0.61/0.60 === Conflict found: 91:2:2:[51.0,48.2,51.0,90.3]:TopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x0,reverse_line(x1)) -> {x0 -> skc1, x1 -> skc2}
% 0.61/0.60 === Backtracking. Learning clause 104:1:2:[91.2,45.2,44.2]:TopTop: ren8(x0,x1) ->
% 0.61/0.60 === Conflict found: 91:2:2:[51.0,48.2,51.0,90.3]:TopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x0,reverse_line(x1)) -> {x0 -> skc1, x1 -> skc2}
% 0.61/0.60 === Backtracking. Learning clause 105:1:2:[91.1,4.2,5.2]:TopTop: convergent_lines(x0,x1) ->
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 93
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Conflict found: 99:2:4:[49.0,67.2,49.0,92.3,49.0,93.4,49.0,94.5,49.0,95.6,49.0,96.7,49.0,97.8,49.0,98.9]:TopTopTopTop: distinct_points(x0,x1),distinct_lines(x2,x3) -> {x0 -> skc3, x1 -> skc4, x2 -> skc1, x3 -> skc2}
% 0.61/0.60 === Backtracking. Learning clause 106:1:2:[99.1,74.1]:TopTop: distinct_lines(x0,x1) ->
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 157
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 160
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 107:2:3:[41.3,65.1,91.2]:TopTopTop: unequally_directed_lines(x0,line_connecting(x1,x2)),unequally_directed_lines(x0,line_connecting(x2,x1)) ->
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 171
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 108:2:3:[41.3,66.1]:TopTopTop: unequally_directed_lines(x0,parallel_through_point(x1,x2)) -> unequally_directed_lines(x0,x1)
% 0.61/0.60 === Conflict found: 102:2:2:[41.2,40.1]:TopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x1,x0) {x0 -> reverse_line(skc1), x1 -> parallel_through_point(reverse_line(skc1),skc1)}
% 0.61/0.60 === Backtracking. Learning clause 109:1:2:[102.2,66.1]:TopTop: unequally_directed_lines(x0,parallel_through_point(x0,x1)) ->
% 0.61/0.60 === Backtracking. Learning clause 110:1:0:[47.1,72.1,40.1]:: -> unequally_directed_lines(skc1,reverse_line(skc1))
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 178
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 111:3:0:[53.3,73.1]:: point(skc2),point(skc4) -> line(line_connecting(skc2,skc4))
% 0.61/0.60 === Conflict found: 89:3:3:[85.0,26.1,87.0,88.2]:TopTopTop: distinct_points(x0,x1) -> unequally_directed_lines(x2,line_connecting(x0,x1)),before_on_line(x2,x0,x1) {x0 -> skc2, x1 -> skc4, x2 -> skc1}
% 0.61/0.60 === Backtracking. Learning clause 112:2:1:[89.1,73.1]:Top: -> unequally_directed_lines(x0,line_connecting(skc2,skc4)),before_on_line(x0,skc2,skc4)
% 0.61/0.60 === Backtracking. Learning clause 113:2:1:[37.1,73.1]:Top: -> distinct_points(skc2,x0),distinct_points(skc4,x0)
% 0.61/0.60 === Backtracking. Learning clause 114:1:0:[59.1,73.1]:: -> ren9(skc2,skc4)
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 183
% 0.61/0.60 === Restarting.
% 0.61/0.60 === Backtracking. Learning clause 115:3:0:[53.3,75.1]:: point(skc2),point(skc3) -> line(line_connecting(skc2,skc3))
% 0.61/0.60 === Conflict found: 89:3:3:[85.0,26.1,87.0,88.2]:TopTopTop: distinct_points(x0,x1) -> unequally_directed_lines(x2,line_connecting(x0,x1)),before_on_line(x2,x0,x1) {x0 -> skc2, x1 -> skc3, x2 -> skc1}
% 0.61/0.60 === Backtracking. Learning clause 116:2:1:[89.1,75.1]:Top: -> unequally_directed_lines(x0,line_connecting(skc2,skc3)),before_on_line(x0,skc2,skc3)
% 0.61/0.60 === Backtracking. Learning clause 117:2:1:[37.1,75.1]:Top: -> distinct_points(skc2,x0),distinct_points(skc3,x0)
% 0.61/0.60 === Backtracking. Learning clause 118:1:0:[59.1,75.1]:: -> ren9(skc2,skc3)
% 0.61/0.60 === Clause set with instances from active satisfied. Growing active. New size: 247
% 0.61/0.60
% 0.61/0.60 SZS status Unsatisfiable
% 0.61/0.60
% 0.61/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.61/0.60
% 0.61/0.60 SPASS-SCL-FOL Statistics:
% 0.61/0.60 Number of learned clauses: 19
% 0.61/0.60 Number of propagations: 1382
% 0.61/0.60 Number of decisions: 282
% 0.61/0.60 Number of resolutions: 31
% 0.61/0.60 Number of condensations: 0
% 0.61/0.60 Number of sub resolutions: 22
% 0.61/0.60 Number of input literals (deduplicated): 45
% 0.61/0.60 Number of grows: 10
% 0.61/0.60 Number of considered ground atoms: 247
% 0.61/0.60
% 0.61/0.60 Needed: 0:00:00.07
% 0.61/0.60
%------------------------------------------------------------------------------