%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYO604+1 : TPTP v9.2.1. Released v7.0.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:41:11 PM UTC 2026
% Result : Theorem 33.97s 7.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : SYO604+1 : TPTP v9.2.1. Released v7.0.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.35 % Computer : n028.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Thu May 7 13:55:01 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 SPASS-SCL-FOL version:
% 0.21/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 33.97/7.34 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34 Execution normal ended with status: unsatisfiable
% 33.97/7.34 Used heuristic: normal
% 33.97/7.34
% 33.97/7.34 Input Clauses:
% 33.97/7.34
% 33.97/7.34 Predicates: g_true_only g_both g_false_only g_true g_false ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18
% 33.97/7.34 Fol Constants: skc10 skc15
% 33.97/7.34 Fol Functions: skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf11 skf12 skf13 skf14
% 33.97/7.34 Problem Properties:
% 33.97/7.34 This is a full first-order problem without equality.
% 33.97/7.34
% 33.97/7.34 After reduction: Problem Properties:
% 33.97/7.34 This is a full first-order problem without equality.
% 33.97/7.34
% 33.97/7.34
% 33.97/7.34 Reduced Input Clauses:
% 33.97/7.34
% 33.97/7.34 Most General Atoms: g_both(x0,x1) ren1(x1,x0) ren2(x0,x1) g_true_only(x1,x0) ren3(x0) ren4(x0) ren5(x1,x0) ren6(x0,x1) ren7(x0) ren9(x0,x1) ren10(x0) ren11(x0,x1) ren12(x0,x1) ren13(x0,x1) ren14(x0,x1) g_false_only(x2,x0) ren15(x0) ren16(x0,x1) ren17(x0,x1) ren18(x0,x1) ren8(x0,x2) g_true(x0,x1) g_false(x0,x1)
% 33.97/7.34
% 33.97/7.34 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: normal ===
% 33.97/7.34
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 114
% 33.97/7.34 === Backtracking. Learning clause 58:2:2:[6.1,3.2,4.2]:TopTop: ren2(x0,x1) -> ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 60:1:1:[29.1,59.0,6.3,44.2,30.2]:Top: ren13(skc10,x0) ->
% 33.97/7.34 === Backtracking. Learning clause 61:3:2:[53.1,56.2]:TopTop: g_false(x0,x1) -> g_both(x0,x1),g_false_only(x0,x1)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 178
% 33.97/7.34 === Backtracking. Learning clause 62:2:2:[40.2,14.1,15.1]:TopTop: ren17(x0,x1) -> ren7(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 242
% 33.97/7.34 === Backtracking. Learning clause 63:3:1:[57.1,6.1,1.1,57.1,2.1,5.1,14.1,15.1,46.2]:Top: g_false_only(x0,skc10) -> ren2(x0,skf1(x0)),ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 64:2:0:[1.1,57.2,5.1,6.1,63.1]:: -> ren2(skc10,skf1(skc10)),ren3(skc10)
% 33.97/7.34 === Backtracking. Learning clause 65:5:2:[9.1,12.2,13.2,16.4,11.2,57.2]:TopTop: -> ren4(x0),g_false_only(x0,x1),ren7(x0),g_true_only(x1,x0),g_false_only(x1,x0)
% 33.97/7.34 === Backtracking. Learning clause 66:4:2:[9.2,13.2,12.2,16.4,10.2,57.2,9.1,65.4]:TopTop: -> ren4(x0),g_false_only(x0,x1),ren7(x0),g_false_only(x1,x0)
% 33.97/7.34 === Backtracking. Learning clause 67:4:1:[44.2,6.3,13.2,12.2,16.4,11.2,57.2]:Top: -> g_false_only(skc10,x0),ren7(skc10),g_true_only(x0,skc10),g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 68:3:1:[16.3,15.1,14.1]:Top: ren5(x0,skf3(x0)) -> ren6(x0,skf4(x0)),ren7(x0)
% 33.97/7.34 === Backtracking. Learning clause 69:3:1:[57.3,15.1,11.1,68.1]:Top: -> g_true_only(skf3(x0),x0),ren6(x0,skf4(x0)),ren7(x0)
% 33.97/7.34 === Conflict found: 67:4:1:[44.2,6.3,13.2,12.2,16.4,11.2,57.2]:Top: -> g_false_only(skc10,x0),ren7(skc10),g_true_only(x0,skc10),g_false_only(x0,skc10) {x0 -> skf3(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 70:2:0:[67.1,14.1,15.1]:: -> g_true_only(skf3(skc10),skc10),ren7(skc10)
% 33.97/7.34 === Backtracking. Learning clause 71:2:0:[6.3,44.2,12.2,13.2,68.2]:: ren5(skc10,skf3(skc10)) -> ren7(skc10)
% 33.97/7.34 === Backtracking. Learning clause 72:1:0:[6.3,44.2,57.1,10.1,14.1,70.1,71.1,46.2]:: g_false_only(skc10,skc10) ->
% 33.97/7.34 === Conflict found: 58:2:2:[6.1,3.2,4.2]:TopTop: ren2(x0,x1) -> ren3(x0) {x0 -> skc10, x1 -> skf1(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 73:4:2:[58.1,5.4]:TopTop: ren1(x0,x1) -> g_false_only(x0,x1),g_false_only(x1,x0),ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 74:2:2:[9.1,3.2,4.2]:TopTop: ren2(x0,x1) -> ren4(x0)
% 33.97/7.34 === Backtracking. Learning clause 75:2:1:[45.2,9.3,57.2,44.1,6.3,39.2]:Top: ren17(x0,x0) -> g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 76:2:2:[57.2,45.1,44.1,74.2,58.2]:TopTop: ren2(x0,x1) -> g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 77:1:1:[46.2,62.2,75.2]:Top: ren17(x0,x0) ->
% 33.97/7.34 === Conflict found: 76:2:2:[57.2,45.1,44.1,74.2,58.2]:TopTop: ren2(x0,x1) -> g_false_only(x0,skc10) {x0 -> skc10, x1 -> skf1(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 78:1:1:[76.2,72.1]:Top: ren2(skc10,x0) ->
% 33.97/7.34 === Backtracking. Learning clause 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 81:2:1:[72.0,80.0,57.1,79.1,2.1,57.1,1.1,5.1,63.1,58.1]:Top: -> g_false_only(skc10,x0),ren3(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 306
% 33.97/7.34 === Conflict found: 66:4:2:[9.2,13.2,12.2,16.4,10.2,57.2,9.1,65.4]:TopTop: -> ren4(x0),g_false_only(x0,x1),ren7(x0),g_false_only(x1,x0) {x0 -> skf3(skc10), x1 -> skc10}
% 33.97/7.34 === Backtracking. Learning clause 82:4:2:[66.1,45.2]:TopTop: g_both(x0,skc10) -> g_false_only(x0,x1),ren7(x0),g_false_only(x1,x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 370
% 33.97/7.34 === Backtracking. Learning clause 83:2:2:[9.2,26.2,25.2]:TopTop: ren11(x0,x1) -> ren4(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 434
% 33.97/7.34 === Backtracking. Learning clause 84:2:2:[52.2,49.2]:TopTop: g_both(x0,x1),g_true_only(x0,x1) ->
% 33.97/7.34 === Backtracking. Learning clause 85:2:2:[6.1,42.2,43.2]:TopTop: ren18(x0,x1) -> ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 86:3:1:[5.1,2.2,55.1,51.2,31.2]:Top: ren14(x0,x0) -> ren2(x0,skf1(x0)),ren3(x0)
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skf5(skc10), x1 -> skc10}
% 33.97/7.34 === Backtracking. Learning clause 87:1:1:[79.2,12.2,54.1,49.2,13.2]:Top: ren6(skc10,x0) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 498
% 33.97/7.34 === Backtracking. Learning clause 88:3:1:[6.2,57.1,57.1,1.1,2.1,73.1,7.1,8.1,45.2,57.2]:Top: -> ren3(x0),g_true_only(x0,skc10),g_false_only(x0,skc10)
% 33.97/7.34 === Conflict found: 66:4:2:[9.2,13.2,12.2,16.4,10.2,57.2,9.1,65.4]:TopTop: -> ren4(x0),g_false_only(x0,x1),ren7(x0),g_false_only(x1,x0) {x0 -> skc15, x1 -> skf2(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 89:2:1:[66.2,7.1,8.1]:Top: -> ren7(x0),ren4(x0)
% 33.97/7.34 === Conflict found: 66:4:2:[9.2,13.2,12.2,16.4,10.2,57.2,9.1,65.4]:TopTop: -> ren4(x0),g_false_only(x0,x1),ren7(x0),g_false_only(x1,x0) {x0 -> skc15, x1 -> skf2(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 90:2:1:[66.3,46.2,8.1,7.1]:Top: g_false_only(x0,skc10) -> ren4(x0)
% 33.97/7.34 === Conflict found: 58:2:2:[6.1,3.2,4.2]:TopTop: ren2(x0,x1) -> ren3(x0) {x0 -> skc15, x1 -> skf1(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 91:2:1:[58.1,63.2]:Top: g_false_only(x0,skc10) -> ren3(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 562
% 33.97/7.34 === Backtracking. Learning clause 92:2:2:[51.2,55.2]:TopTop: g_both(x0,x1),g_false_only(x0,x1) ->
% 33.97/7.34 === Backtracking. Learning clause 93:2:2:[9.1,19.2,20.2]:TopTop: ren9(x0,x1) -> ren4(x0)
% 33.97/7.34 === Backtracking. Learning clause 94:2:2:[9.1,42.2,43.2]:TopTop: ren18(x0,x1) -> ren4(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 626
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 690
% 33.97/7.34 === Backtracking. Learning clause 95:2:1:[44.2,91.2]:Top: g_true_only(x0,skc10),g_false_only(x0,skc10) ->
% 33.97/7.34 === Backtracking. Learning clause 96:2:2:[9.1,20.2,19.2]:TopTop: ren9(x0,x1) -> ren4(x1)
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skc10, x1 -> skf4(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 97:2:2:[79.1,26.2,25.2]:TopTop: ren11(x0,x1) -> g_false_only(x1,skc10)
% 33.97/7.34 === Backtracking. Learning clause 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 99:2:2:[48.2,55.2]:TopTop: g_true_only(x0,x1),g_false_only(x0,x1) ->
% 33.97/7.34 === Conflict found: 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0) {x0 -> skc15, x1 -> skf3(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 100:3:1:[98.1,14.1,15.1]:Top: -> ren2(x0,skf1(x0)),ren3(x0),ren7(x0)
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skc10, x1 -> skf1(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 101:2:2:[79.1,13.2,12.2]:TopTop: ren6(x0,x1) -> g_false_only(x1,skc10)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 754
% 33.97/7.34 === Backtracking. Learning clause 102:2:2:[27.2,84.2]:TopTop: ren12(x0,x1),g_both(x0,x1) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 818
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 882
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 946
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1010
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1074
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1138
% 33.97/7.34 === Backtracking. Learning clause 103:2:2:[6.1,29.2,30.2]:TopTop: ren13(x0,x1) -> ren3(x0)
% 33.97/7.34 === Conflict found: 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0) {x0 -> skf8(skc10), x1 -> skf8(skf8(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 104:3:1:[98.1,34.2,35.2]:Top: ren15(x0) -> ren2(x0,skf1(x0)),ren3(x0)
% 33.97/7.34 === Conflict found: 104:3:1:[98.1,34.2,35.2]:Top: ren15(x0) -> ren2(x0,skf1(x0)),ren3(x0) {x0 -> skf8(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 105:2:1:[104.2,76.1,44.2,99.2]:Top: ren15(x0),g_true_only(x0,skc10) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1202
% 33.97/7.34 === Conflict found: 99:2:2:[48.2,55.2]:TopTop: g_true_only(x0,x1),g_false_only(x0,x1) -> {x0 -> skf5(skf1(skc10)), x1 -> skf1(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 106:3:2:[99.1,20.2,98.2,58.1,44.2]:TopTop: ren9(x0,x1),g_true_only(x0,skc10) -> g_false_only(x0,x1)
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skf6(skc10), x1 -> skf11(skf6(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 107:2:2:[79.2,20.2,19.2]:TopTop: ren9(x0,x1) -> g_false_only(x0,skc10)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1266
% 33.97/7.34 === Backtracking. Learning clause 108:3:1:[57.1,44.1]:Top: ren3(x0) -> g_both(x0,skc10),g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 109:2:2:[9.2,29.2,30.2]:TopTop: ren13(x0,x1) -> ren4(x1)
% 33.97/7.34 === Backtracking. Learning clause 110:2:2:[9.2,30.2,29.2]:TopTop: ren13(x0,x1) -> ren4(x0)
% 33.97/7.34 === Backtracking. Learning clause 111:2:2:[57.3,54.1,52.1]:TopTop: -> g_true_only(x0,x1),g_false(x0,x1)
% 33.97/7.34 === Conflict found: 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0) {x0 -> skf8(skc10), x1 -> skf5(skf8(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 112:4:2:[98.2,23.2,22.2,28.2]:TopTop: ren12(x0,x1) -> ren2(x0,skf1(x0)),ren3(x0),ren11(x0,skf6(x0))
% 33.97/7.34 === Backtracking. Learning clause 113:2:2:[36.2,42.2,43.2]:TopTop: ren15(x0),ren18(x0,x1) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1330
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1394
% 33.97/7.34 === Conflict found: 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0) {x0 -> skf12(skc10), x1 -> skf2(skf12(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 114:2:1:[98.3,58.1,7.1,8.1]:Top: -> ren3(x0),ren4(x0)
% 33.97/7.34 === Backtracking. Learning clause 115:2:2:[45.1,108.2,94.2,85.2]:TopTop: ren18(x0,x1) -> g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 116:1:1:[32.2,7.1,110.1,8.1,45.2,31.2]:Top: ren14(x0,skc10) ->
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skf4(skc10), x1 -> skf9(skf4(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 117:2:2:[79.1,4.2,3.2]:TopTop: ren2(x0,x1) -> g_false_only(x1,skc10)
% 33.97/7.34 === Backtracking. Learning clause 118:2:2:[40.3,8.1,7.1,45.2,61.2,46.1,62.2]:TopTop: g_false(x0,skc10),ren17(x0,x1) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1458
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1522
% 33.97/7.34 === Backtracking. Learning clause 119:3:3:[40.2,99.2,99.2]:TopTopTop: ren17(x0,x1),g_true_only(x0,x2),g_true_only(x2,x0) ->
% 33.97/7.34 === Backtracking. Learning clause 120:1:1:[14.1,41.2,46.2,115.2]:Top: ren18(x0,skf3(x0)) ->
% 33.97/7.34 === Conflict found: 98:4:2:[57.1,6.1,1.1,57.1,2.1,5.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),ren2(x0,skf1(x0)),ren3(x0) {x0 -> skf9(skc10), x1 -> skf3(skf9(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 121:4:2:[98.4,108.1,76.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),g_both(x0,skc10),g_false_only(x0,skc10)
% 33.97/7.34 === Backtracking. Learning clause 122:3:3:[38.4,36.1,14.1,15.1,46.2,108.3,30.2,29.2,103.2]:TopTopTop: ren16(x0,x1),ren13(x0,x2) -> g_both(x0,skc10)
% 33.97/7.34 === Conflict found: 121:4:2:[98.4,108.1,76.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf3(skc15), x1 -> skc15}
% 33.97/7.34 === Backtracking. Learning clause 123:3:2:[121.3,84.1,99.2]:TopTop: g_true_only(x0,skc10) -> g_false_only(x0,x1),g_false_only(x1,x0)
% 33.97/7.34 === Backtracking. Learning clause 124:3:2:[27.2,79.2]:TopTop: ren12(x0,x1),g_true_only(x1,x0) -> g_false_only(x1,skc10)
% 33.97/7.34 === Backtracking. Learning clause 125:2:2:[57.2,51.1,48.1]:TopTop: -> g_false_only(x0,x1),g_true(x0,x1)
% 33.97/7.34 === Conflict found: 123:3:2:[121.3,84.1,99.2]:TopTop: g_true_only(x0,skc10) -> g_false_only(x0,x1),g_false_only(x1,x0) {x0 -> skf3(skc15), x1 -> skc15}
% 33.97/7.34 === Backtracking. Learning clause 126:3:2:[123.2,15.1,14.1,46.2,79.3]:TopTop: g_true_only(skf3(x0),skc10),g_true_only(x0,x1),g_true_only(x1,x0) ->
% 33.97/7.34 === Conflict found: 121:4:2:[98.4,108.1,76.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf9(skc10), x1 -> skf5(skf9(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 127:3:1:[121.1,22.2,23.2]:Top: ren10(x0) -> g_both(x0,skc10),g_false_only(x0,skc10)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1586
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1650
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1714
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1778
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1842
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1906
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 1970
% 33.97/7.34 === Backtracking. Learning clause 128:2:2:[36.2,13.2,12.2]:TopTop: ren15(x0),ren6(x1,x0) ->
% 33.97/7.34 === Backtracking. Learning clause 131:3:1:[14.0,129.2,15.0,130.3,57.2,10.1,9.2,69.1,16.1,128.2]:Top: ren15(skf4(x0)) -> ren4(skf3(x0)),ren7(x0)
% 33.97/7.34 === Conflict found: 121:4:2:[98.4,108.1,76.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf11(skf6(skc10)), x1 -> skf3(skf11(skf6(skc10)))}
% 33.97/7.34 === Backtracking. Learning clause 132:2:1:[121.2,15.1,45.1,89.2,14.1]:Top: -> g_false_only(x0,skc10),ren7(x0)
% 33.97/7.34 === Backtracking. Learning clause 133:2:1:[32.4,60.1,7.1,8.1,45.2]:Top: ren14(skc10,x0),g_both(skc10,skc10) ->
% 33.97/7.34 === Conflict found: 121:4:2:[98.4,108.1,76.1]:TopTop: -> g_false_only(x0,x1),g_false_only(x1,x0),g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf5(skc10), x1 -> skc10}
% 33.97/7.34 === Backtracking. Learning clause 134:3:1:[121.2,22.2,23.2,28.2]:Top: ren12(skc10,x0) -> g_both(skf5(skc10),skc10),ren11(skc10,skf6(skc10))
% 33.97/7.34 === Backtracking. Learning clause 135:4:2:[16.1,11.2,92.2]:TopTop: g_both(x0,x1) -> g_false_only(x1,x0),ren6(x1,skf4(x1)),ren7(x1)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2034
% 33.97/7.34 === Backtracking. Learning clause 136:2:2:[24.2,42.2,43.2]:TopTop: ren10(x0),ren18(x0,x1) ->
% 33.97/7.34 === Backtracking. Learning clause 137:5:4:[38.4,36.1]:TopTopTopTop: ren16(x0,x1),g_true_only(x0,x2),g_true_only(x2,x0) -> g_false_only(x0,x3),g_false_only(x3,x0)
% 33.97/7.34 === Backtracking. Learning clause 138:3:1:[14.2,46.2,37.2,38.2]:Top: ren16(x0,skf3(x0)) -> g_false_only(skc10,x0),ren15(x0)
% 33.97/7.34 === Conflict found: 88:3:1:[6.2,57.1,57.1,1.1,2.1,73.1,7.1,8.1,45.2,57.2]:Top: -> ren3(x0),g_true_only(x0,skc10),g_false_only(x0,skc10) {x0 -> skf11(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 139:2:1:[88.3,91.1]:Top: -> g_true_only(x0,skc10),ren3(x0)
% 33.97/7.34 === Conflict found: 79:3:2:[57.2,45.1,44.1,9.3,6.3]:TopTop: g_true_only(x0,x1),g_true_only(x1,x0) -> g_false_only(x0,skc10) {x0 -> skf7(skc15), x1 -> skc15}
% 33.97/7.34 === Backtracking. Learning clause 140:2:2:[79.1,30.2,29.2]:TopTop: ren13(x0,x1) -> g_false_only(x1,skc10)
% 33.97/7.34 === Backtracking. Learning clause 141:2:1:[57.1,36.2,10.1,68.1,69.1,38.4,14.1,15.1,46.2,37.2]:Top: ren16(x0,skc10) -> ren6(x0,skf4(x0))
% 33.97/7.34 === Backtracking. Learning clause 142:2:1:[38.2,14.1,15.1,46.2,37.2]:Top: ren16(x0,skc10) -> ren15(x0)
% 33.97/7.34 === Conflict found: 137:5:4:[38.4,36.1]:TopTopTopTop: ren16(x0,x1),g_true_only(x0,x2),g_true_only(x2,x0) -> g_false_only(x0,x3),g_false_only(x3,x0) {x0 -> skf13(skc10), x1 -> skf2(skf13(skc10)), x2 -> skf9(skf13(skc10)), x3 -> skf3(skf13(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 143:2:3:[137.5,15.1,14.1,46.2,42.2,115.2,43.2]:TopTopTop: ren16(x0,x1),ren18(x0,x2) ->
% 33.97/7.34 === Backtracking. Learning clause 144:2:2:[6.2,19.2,20.2]:TopTop: ren9(x0,x1) -> ren3(x1)
% 33.97/7.34 === Conflict found: 127:3:1:[121.1,22.2,23.2]:Top: ren10(x0) -> g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf5(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 145:2:1:[127.3,99.2,84.1]:Top: ren10(x0),g_true_only(x0,skc10) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2098
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2162
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2226
% 33.97/7.34 === Backtracking. Learning clause 146:2:2:[41.2,99.2]:TopTop: ren18(x0,x1),g_true_only(x0,x1) ->
% 33.97/7.34 === Backtracking. Learning clause 147:2:2:[36.2,3.2,4.2]:TopTop: ren15(x0),ren2(x0,x1) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2290
% 33.97/7.34 === Backtracking. Learning clause 148:2:2:[40.3,35.2,34.2]:TopTop: ren17(x0,x1),ren15(x0) ->
% 33.97/7.34 === Backtracking. Learning clause 149:2:2:[31.2,84.1]:TopTop: ren14(x0,x1),g_true_only(x0,x1) ->
% 33.97/7.34 === Conflict found: 108:3:1:[57.1,44.1]:Top: ren3(x0) -> g_both(x0,skc10),g_false_only(x0,skc10) {x0 -> skf12(skc15)}
% 33.97/7.34 === Backtracking. Learning clause 150:2:1:[108.1,114.1,90.1]:Top: -> g_both(x0,skc10),ren4(x0)
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2354
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2418
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2482
% 33.97/7.34 === Backtracking. Learning clause 151:10:4:[36.2,12.2,13.2,141.2,142.2,47.8,27.1,44.1,81.2,119.1,92.2]:TopTopTopTop: g_both(x0,skc10),ren8(x0,x1),g_true_only(x2,x3),g_true_only(x3,x2),g_both(skc10,skf12(skc10)) -> g_false_only(x0,x1),g_false_only(x1,x0),ren9(x0,skf11(x0)),ren14(skf13(skc10),skc10),ren18(x2,skc15)
% 33.97/7.34 === Conflict found: 123:3:2:[121.3,84.1,99.2]:TopTop: g_true_only(x0,skc10) -> g_false_only(x0,x1),g_false_only(x1,x0) {x0 -> skf3(skf6(skc10)), x1 -> skf6(skc10)}
% 33.97/7.34 === Backtracking. Learning clause 152:4:3:[123.2,15.1,14.1,46.2,108.3,45.1,110.2,32.4,139.2,123.1,99.2]:TopTopTop: g_true_only(skf3(x0),skc10),ren14(x0,x1),g_true_only(x2,x0) -> g_false_only(x0,x2)
% 33.97/7.34 === Backtracking. Learning clause 153:2:2:[32.3,8.1,7.1,110.1,45.2]:TopTop: ren14(x0,x1),g_both(x0,skc10) ->
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2546
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2610
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2674
% 33.97/7.34 === Clause set with instances from active satisfied. Growing active. New size: 2738
% 33.97/7.34 === Backtracking. Learning clause 154:9:3:[6.1,25.2,26.2,112.4,58.1,44.2,27.2,47.6,37.1,92.2,94.1]:TopTopTop: g_both(x0,skc10),ren8(x0,x1),g_both(skf14(skc10),skc10) -> g_false_only(x0,x1),g_false_only(x1,x0),ren9(x0,skf11(x0)),ren14(skf13(skc10),skc10),ren17(x2,skc15),ren4(x2)
% 33.97/7.34 === Backtracking. Learning clause 155:3:2:[6.1,25.2,26.2,112.4]:TopTop: ren12(x0,x1) -> ren2(x0,skf1(x0)),ren3(x0)
% 33.97/7.34 === Backtracking. Learning clause 156:9:3:[36.2,12.2,13.2,141.2,142.2,47.8,155.1,58.1,44.2]:TopTopTop: g_both(x0,skc10),ren8(x0,x1),g_true_only(skf12(skc10),skc10) -> g_false_only(x0,x1),g_false_only(x1,x0),ren9(x0,skf11(x0)),ren14(skf13(skc10),skc10),ren17(x2,skc15),ren18(x2,skc15)
% 33.97/7.34 === Backtracking. Learning clause 157:1:0:[36.1,142.2,13.2,12.2,141.2,47.8,27.1,156.3,18.2,116.1,40.1,41.1,107.1,121.3,8.1,7.1,45.2,121.3,72.1,15.1,14.1]:: -> ren7(skc15)
% 33.97/7.34 === Conflict found: 58:2:2:[6.1,3.2,4.2]:TopTop: ren2(x0,x1) -> ren3(x0) {x0 -> skf12(skc10), x1 -> skf1(skf12(skc10))}
% 33.97/7.34 === Backtracking. Learning clause 158:1:1:[58.1,155.2,44.2,27.2]:Top: ren12(x0,skc10) ->
% 33.97/7.34 === Conflict found: 156:9:3:[36.2,12.2,13.2,141.2,142.2,47.8,155.1,58.1,44.2]:TopTopTop: g_both(x0,skc10),ren8(x0,x1),g_true_only(skf12(skc10),skc10) -> g_false_only(x0,x1),g_false_only(x1,x0),ren9(x0,skf11(x0)),ren14(skf13(skc10),skc10),ren17(x2,skc15),ren18(x2,skc15) {x0 -> skc10, x1 -> skf2(skc10), x2 -> skc15}
% 33.97/7.34 === Backtracking. Learning clause 159:1:0:[156.9,115.1,77.1,107.1,116.1,18.2,121.3,7.1,8.1,45.2,121.3,72.1,46.1,157.1]:: g_true_only(skf12(skc10),skc10) ->
% 33.97/7.34 === Backtracking. Learning clause 162:1:0:[157.0,160.0,158.0,161.1,47.10,115.1,77.1,18.2,116.1,107.1,121.3,8.1,7.1,45.2,121.3,72.1,46.1]:: -> ren16(skf14(skc10),skc10)
% 33.97/7.34
% 33.97/7.34 SZS status Unsatisfiable
% 33.97/7.34
% 33.97/7.34 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.97/7.34
% 33.97/7.34 SPASS-SCL-FOL Statistics:
% 33.97/7.34 Number of learned clauses: 99
% 33.97/7.34 Number of propagations: 43917
% 33.97/7.34 Number of decisions: 8268
% 33.97/7.34 Number of resolutions: 359
% 33.97/7.34 Number of condensations: 17
% 33.97/7.34 Number of sub resolutions: 6
% 33.97/7.34 Number of input literals (deduplicated): 50
% 33.97/7.34 Number of grows: 42
% 33.97/7.34 Number of considered ground atoms: 2738
% 33.97/7.34
% 33.97/7.34 Needed: 0:00:06.76
% 33.97/7.34
%------------------------------------------------------------------------------