%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GEO254+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 : n029.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:13 PM UTC 2026
% Result : Theorem 5.17s 1.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GEO254+1 : TPTP v9.2.1. Bugfixed v6.4.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n029.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.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 5.17/1.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57 Execution resolution_2 ended with status: unsatisfiable
% 5.17/1.57 Used heuristic: resolution_2
% 5.17/1.57
% 5.17/1.57 Input Clauses:
% 5.17/1.57
% 5.17/1.57 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
% 5.17/1.57 Fol Constants: skc1 skc2 skc3
% 5.17/1.57 Fol Functions: reverse_line line_connecting intersection_point parallel_through_point
% 5.17/1.57 Problem Properties:
% 5.17/1.57 This is a full first-order problem without equality.
% 5.17/1.57
% 5.17/1.57 After reduction: Problem Properties:
% 5.17/1.57 This is a full first-order problem without equality.
% 5.17/1.57
% 5.17/1.57
% 5.17/1.57 Reduced Input Clauses:
% 5.17/1.57 77:1:2:[49.0,1.1,49.0,76.2]:TopTop: apart_point_and_line(x0,x1) ->
% 5.17/1.57 78:1:3:[49.0,7.1]:TopTopTop: ren1(x0,x1,x2) ->
% 5.17/1.57 79:1:3:[49.0,10.1]:TopTopTop: ren2(x0,x1,x2) ->
% 5.17/1.57 97:2:4:[49.0,67.2,49.0,90.3,49.0,91.4,49.0,92.5,49.0,93.6,49.0,94.7,49.0,95.8,49.0,96.9]:TopTopTopTop: distinct_points(x0,x1),distinct_lines(x2,x3) ->
% 5.17/1.57 81:1:3:[78.0,13.1,79.0,80.2]:TopTopTop: divides_points(x0,x1,x2) ->
% 5.17/1.57 83:1:2:[49.0,16.1,49.0,82.2]:TopTop: ren3(x0,x1) ->
% 5.17/1.57 85:1:2:[49.0,19.1,49.0,84.2]:TopTop: ren4(x0,x1) ->
% 5.17/1.57 87:3:3:[83.0,26.1,85.0,86.2]:TopTopTop: distinct_points(x0,x1) -> unequally_directed_lines(x2,line_connecting(x0,x1)),before_on_line(x2,x0,x1)
% 5.17/1.57 89:2:2:[51.0,48.2,51.0,88.3]:TopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x0,reverse_line(x1)) ->
% 5.17/1.57
% 5.17/1.57 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) ren9(x0,x1) left_convergent_lines(x0,x1) point(x1)
% 5.17/1.57
% 5.17/1.57 === Starting SPASS-SCL-FOL A Little Less Naive, considering 83 atoms initially, heuristics mode: resolution_2 ===
% 5.17/1.57
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 83
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 98:1:2:[22.2,36.1]:TopTop: before_on_line(x0,x1,x1) ->
% 5.17/1.57 === Conflict found: 89:2:2:[51.0,48.2,51.0,88.3]:TopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x0,reverse_line(x1)) -> {x0 -> skc1, x1 -> skc2}
% 5.17/1.57 === Backtracking. Learning clause 99:1:2:[89.1,4.2,5.2]:TopTop: convergent_lines(x0,x1) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 83
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 102:1:2:[43.1,100.1,99.0,101.2,42.2,6.1]:TopTop: ren7(x0,x1) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 92
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 103:2:2:[41.2,40.1]:TopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x1,x0)
% 5.17/1.57 === Backtracking. Learning clause 104:1:1:[45.2,40.1]:Top: ren8(reverse_line(x0),x0) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 92
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 156
% 5.17/1.57 === Backtracking. Learning clause 105:2:1:[47.3,40.1]:Top: line(x0) -> unequally_directed_lines(x0,reverse_line(x0))
% 5.17/1.57 === Backtracking. Learning clause 107:1:2:[99.0,106.1,6.2,45.2,44.2]:TopTop: ren8(x0,x1) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 157
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 108:2:3:[41.3,65.1,89.2]:TopTopTop: unequally_directed_lines(x0,line_connecting(x1,x2)),unequally_directed_lines(x0,line_connecting(x2,x1)) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 168
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 109:3:2:[47.4,66.1]:TopTop: line(parallel_through_point(reverse_line(x0),x1)),line(x0) -> unequally_directed_lines(parallel_through_point(reverse_line(x0),x1),x0)
% 5.17/1.57 === Backtracking. Learning clause 110:1:2:[41.3,66.1,40.1]:TopTop: unequally_directed_lines(x0,parallel_through_point(x0,x1)) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 168
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 111:3:0:[53.3,72.1]:: point(skc1),point(skc2) -> line(line_connecting(skc1,skc2))
% 5.17/1.57 === Conflict found: 87:3:3:[83.0,26.1,85.0,86.2]:TopTopTop: distinct_points(x0,x1) -> unequally_directed_lines(x2,line_connecting(x0,x1)),before_on_line(x2,x0,x1) {x0 -> skc1, x1 -> skc2, x2 -> skc1}
% 5.17/1.57 === Backtracking. Learning clause 112:2:1:[87.1,72.1]:Top: -> unequally_directed_lines(x0,line_connecting(skc1,skc2)),before_on_line(x0,skc1,skc2)
% 5.17/1.57 === Backtracking. Learning clause 113:2:1:[37.1,72.1]:Top: -> distinct_points(skc1,x0),distinct_points(skc2,x0)
% 5.17/1.57 === Backtracking. Learning clause 114:1:0:[59.1,72.1]:: -> ren9(skc1,skc2)
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 168
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 115:1:3:[30.2,98.1]:TopTopTop: ren6(x0,x1,x1,x2) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 232
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 232
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Conflict found: 103:2:2:[41.2,40.1]:TopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x1,x0) {x0 -> skc1, x1 -> parallel_through_point(reverse_line(skc1),skc1)}
% 5.17/1.57 === Backtracking. Learning clause 116:3:3:[103.1,41.2]:TopTopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x2,x0),unequally_directed_lines(x1,x2)
% 5.17/1.57 === Backtracking. Learning clause 119:4:4:[102.0,117.2,107.0,118.3,46.2,116.3,116.3]:TopTopTopTop: unequally_directed_lines(x0,x1),unequally_directed_lines(x2,x1) -> unequally_directed_lines(reverse_line(x3),x0),unequally_directed_lines(x3,x2)
% 5.17/1.57 === Backtracking. Learning clause 120:4:4:[41.3,116.1,89.2,116.3]:TopTopTopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x2,x3),unequally_directed_lines(reverse_line(x3),x2),unequally_directed_lines(x3,x0)
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 232
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 121:2:3:[41.3,108.1]:TopTopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x0,line_connecting(x2,x2))
% 5.17/1.57 === Conflict found: 121:2:3:[41.3,108.1]:TopTopTop: unequally_directed_lines(x0,x1) -> unequally_directed_lines(x0,line_connecting(x2,x2)) {x0 -> skc1, x1 -> reverse_line(skc1), x2 -> skc1}
% 5.17/1.57 === Backtracking. Learning clause 122:1:2:[121.2,108.1]:TopTop: unequally_directed_lines(x0,x1) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 233
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 233
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 297
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 299
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 123:2:2:[47.3,110.1,122.1]:TopTop: line(x0),line(parallel_through_point(x0,x1)) ->
% 5.17/1.57 === Conflict found: 105:2:1:[47.3,40.1]:Top: line(x0) -> unequally_directed_lines(x0,reverse_line(x0)) {x0 -> reverse_line(skc1)}
% 5.17/1.57 === Backtracking. Learning clause 124:1:1:[105.2,122.1]:Top: line(x0) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 299
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 299
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 125:2:3:[33.3,115.1,27.1]:TopTopTop: between_on_line(x0,x1,x2,x2) -> before_on_line(x0,x1,x2)
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 299
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 363
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 363
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 126:1:3:[27.2,98.1]:TopTopTop: ren5(x0,x1,x1,x2) ->
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 363
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 363
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 363
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 427
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 439
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 127:4:4:[29.1,87.3]:TopTopTopTop: before_on_line(x0,x1,x2),distinct_points(x3,x1) -> ren5(x0,x3,x1,x2),unequally_directed_lines(x0,line_connecting(x3,x1))
% 5.17/1.57 === Backtracking. Learning clause 128:4:4:[32.1,87.3,87.3,122.1]:TopTopTopTop: distinct_points(x0,x1),distinct_points(x1,x2) -> ren6(x3,x0,x1,x2),unequally_directed_lines(x3,line_connecting(x0,x1))
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 439
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 439
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 439
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 503
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 503
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 129:4:4:[31.1,128.3]:TopTopTopTop: distinct_points(x0,x1),distinct_points(x1,x2) -> before_on_line(x3,x1,x2),unequally_directed_lines(x3,line_connecting(x0,x1))
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 503
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 130:5:5:[29.2,129.3]:TopTopTopTopTop: before_on_line(x0,x1,x2),distinct_points(x3,x2),distinct_points(x2,x4) -> ren5(x0,x1,x2,x4),unequally_directed_lines(x0,line_connecting(x3,x2))
% 5.17/1.57 === Clause set with instances from active satisfied. Growing active. New size: 503
% 5.17/1.57 === Restarting.
% 5.17/1.57 === Backtracking. Learning clause 131:1:0:[37.2,36.1,72.1]:: -> distinct_points(skc2,skc1)
% 5.17/1.57 === Conflict found: 129:4:4:[31.1,128.3]:TopTopTopTop: distinct_points(x0,x1),distinct_points(x1,x2) -> before_on_line(x3,x1,x2),unequally_directed_lines(x3,line_connecting(x0,x1)) {x0 -> skc2, x1 -> skc1, x2 -> skc2, x3 -> skc1}
% 5.17/1.57 === Backtracking. Learning clause 132:3:4:[129.4,122.1]:TopTopTopTop: distinct_points(x0,x1),distinct_points(x1,x2) -> before_on_line(x3,x1,x2)
% 5.17/1.57
% 5.17/1.57 SZS status Unsatisfiable
% 5.17/1.57
% 5.17/1.57 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.17/1.57
% 5.17/1.57 SPASS-SCL-FOL Statistics:
% 5.17/1.57 Number of learned clauses: 30
% 5.17/1.57 Number of propagations: 9601
% 5.17/1.57 Number of decisions: 950
% 5.17/1.57 Number of resolutions: 46
% 5.17/1.57 Number of condensations: 0
% 5.17/1.57 Number of sub resolutions: 27
% 5.17/1.57 Number of input literals (deduplicated): 44
% 5.17/1.57 Number of grows: 33
% 5.17/1.57 Number of considered ground atoms: 503
% 5.17/1.57
% 5.17/1.57 Needed: 0:00:01.05
% 5.17/1.57
%------------------------------------------------------------------------------