%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN353+1 : TPTP v9.2.1. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:39:39 PM UTC 2026
% Result : Theorem 237.88s 48.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN353+1 : TPTP v9.2.1. Released v2.0.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 : n007.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 13:40:24 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]
% 237.88/48.12 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12 Execution lmodel_grow ended with status: unsatisfiable
% 237.88/48.12 Used heuristic: lmodel_grow
% 237.88/48.12
% 237.88/48.12 Input Clauses:
% 237.88/48.12
% 237.88/48.12 Predicates: big_f ren1 ren2 ren3
% 237.88/48.12 Fol Constants: skc1
% 237.88/48.12 Fol Functions: skf2
% 237.88/48.12 Problem Properties:
% 237.88/48.12 This is a full first-order problem without equality.
% 237.88/48.12
% 237.88/48.12 After reduction: Problem Properties:
% 237.88/48.12 This is a full first-order problem without equality.
% 237.88/48.12
% 237.88/48.12
% 237.88/48.12 Reduced Input Clauses:
% 237.88/48.12
% 237.88/48.12 Most General Atoms: ren2(x0,x1,x2) big_f(x2,x1,x0) ren1(x1,x0,x2) ren3(x2,x0,x1)
% 237.88/48.12
% 237.88/48.12 === Starting SPASS-SCL-FOL A Little Less Naive, considering 54 atoms initially, heuristics mode: lmodel_grow ===
% 237.88/48.12
% 237.88/48.12 === Backtracking. Learning clause 24:1:1:[3.1,11.1,12.1]:Top: -> big_f(x0,x0,skf2(x0,x0,x0))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 78
% 237.88/48.12 === Backtracking. Learning clause 26:2:3:[8.0,25.0,9.1,6.2]:TopTopTop: -> ren3(x0,x1,x2),ren2(x0,x1,x2)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 94
% 237.88/48.12 === Backtracking. Learning clause 27:3:3:[3.2,9.1]:TopTopTop: big_f(x0,x1,x2) -> ren1(x0,x1,x2),ren3(x2,x0,x1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 125
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 158
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 190
% 237.88/48.12 === Backtracking. Learning clause 28:3:1:[10.3,16.1,11.2,11.2,19.1,8.2,5.1]:Top: big_f(skc1,x0,skc1) -> big_f(skc1,skc1,x0),big_f(x0,skc1,skc1)
% 237.88/48.12 === Backtracking. Learning clause 29:4:3:[10.4,6.2,16.2]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,x1,x2),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 230
% 237.88/48.12 === Backtracking. Learning clause 31:2:3:[1.1,30.1,7.2,2.2]:TopTopTop: ren3(x0,x1,x2),ren1(x2,x0,x1) ->
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 266
% 237.88/48.12 === Conflict found: 27:3:3:[3.2,9.1]:TopTopTop: big_f(x0,x1,x2) -> ren1(x0,x1,x2),ren3(x2,x0,x1) {x0 -> skc1, x1 -> skc1, x2 -> skf2(skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 32:3:3:[27.2,12.1]:TopTopTop: big_f(x0,x1,x2) -> ren3(x2,x0,x1),big_f(x1,x0,skf2(x0,x1,x2))
% 237.88/48.12 === Backtracking. Learning clause 33:3:3:[3.3,12.1,4.2,16.3,3.1]:TopTopTop: big_f(x0,x1,x2),big_f(x2,skf2(x2,x0,x1),x0) -> ren1(x0,x2,skf2(x2,x0,x1))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 303
% 237.88/48.12 === Backtracking. Learning clause 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2)
% 237.88/48.12 === Backtracking. Learning clause 35:3:3:[2.1,13.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)),big_f(x2,x1,x0) -> big_f(x0,x2,x1)
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skc1, x1 -> skc1, x2 -> skf2(skc1,skc1,skf2(skc1,skf2(skc1,skc1,skc1),skc1))}
% 237.88/48.12 === Backtracking. Learning clause 37:3:1:[18.1,36.0,34.4,5.1,11.2,19.1,10.1,35.2,9.2]:Top: big_f(skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0)),skc1),big_f(skc1,skc1,skf2(skc1,skc1,x0)) -> big_f(skc1,x0,skc1)
% 237.88/48.12 === Conflict found: 35:3:3:[2.1,13.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)),big_f(x2,x1,x0) -> big_f(x0,x2,x1) {x0 -> skc1, x1 -> skc1, x2 -> skf2(skc1,skc1,skf2(skc1,skf2(skc1,skc1,skc1),skc1))}
% 237.88/48.12 === Backtracking. Learning clause 38:4:3:[35.3,34.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,skf2(x0,x1,x2))),big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)) -> ren2(x0,x1,x2)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 346
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 387
% 237.88/48.12 === Backtracking. Learning clause 39:3:1:[19.1,28.3,9.2,14.2,35.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0),big_f(skc1,x0,skc1)
% 237.88/48.12 === Conflict found: 35:3:3:[2.1,13.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)),big_f(x2,x1,x0) -> big_f(x0,x2,x1) {x0 -> skc1, x1 -> skc1, x2 -> skf2(skc1,skf2(skc1,skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 40:3:1:[35.2,10.4,1.2,13.3,18.2]:Top: big_f(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0))),big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1)
% 237.88/48.12 === Conflict found: 39:3:1:[19.1,28.3,9.2,14.2,35.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0),big_f(skc1,x0,skc1) {x0 -> skf2(skc1,skc1,skf2(skc1,skc1,skf2(skf2(skc1,skc1,skf2(skc1,skc1,skc1)),skc1,skc1)))}
% 237.88/48.12 === Backtracking. Learning clause 42:3:1:[4.0,41.2,39.3,16.2,11.1,39.3]:Top: big_f(skf2(skc1,skc1,x0),skc1,skc1) -> big_f(skc1,skc1,x0),big_f(skc1,skc1,skf2(skc1,skc1,x0))
% 237.88/48.12 === Backtracking. Learning clause 43:3:1:[7.3,39.3]:Top: ren3(x0,skc1,skc1),big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0)
% 237.88/48.12 === Backtracking. Learning clause 44:4:3:[20.2,15.2,12.2,3.3,6.3,18.2]:TopTopTop: big_f(skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2))),big_f(x0,x2,x1),big_f(x2,x1,x0),big_f(x1,x0,x2) ->
% 237.88/48.12 === Backtracking. Learning clause 45:3:1:[11.2,10.2]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1),big_f(x0,skc1,skc1)
% 237.88/48.12 === Backtracking. Learning clause 47:3:3:[17.1,46.1,7.2,32.3]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2) -> ren3(x2,x1,x0)
% 237.88/48.12 === Backtracking. Learning clause 48:2:1:[17.2,42.1,43.1,13.1,1.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0)
% 237.88/48.12 === Conflict found: 48:2:1:[17.2,42.1,43.1,13.1,1.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0) {x0 -> skf2(skc1,skc1,skf2(skf2(skc1,skc1,skc1),skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 49:1:1:[48.1,11.1,18.1,48.1]:Top: -> big_f(skc1,skc1,skf2(skc1,skc1,x0))
% 237.88/48.12 === Conflict found: 40:3:1:[35.2,10.4,1.2,13.3,18.2]:Top: big_f(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0))),big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skf2(skc1,skc1,skc1),skc1)))}
% 237.88/48.12 === Backtracking. Learning clause 51:2:1:[49.0,50.1,40.1,49.1,37.1,28.1,18.1,38.2,5.1]:Top: big_f(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0))) -> big_f(x0,skc1,skc1)
% 237.88/48.12 === Conflict found: 51:2:1:[49.0,50.1,40.1,49.1,37.1,28.1,18.1,38.2,5.1]:Top: big_f(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0))) -> big_f(x0,skc1,skc1) {x0 -> skf2(skc1,skf2(skc1,skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 52:1:1:[51.1,49.1]:Top: -> big_f(x0,skc1,skc1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 431
% 237.88/48.12 === Conflict found: 33:3:3:[3.3,12.1,4.2,16.3,3.1]:TopTopTop: big_f(x0,x1,x2),big_f(x2,skf2(x2,x0,x1),x0) -> ren1(x0,x2,skf2(x2,x0,x1)) {x0 -> skc1, x1 -> skf2(skc1,skc1,skf2(skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1),skc1)), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 53:3:3:[33.2,15.2]:TopTopTop: big_f(x0,x1,x2),ren2(x2,x0,x1) -> ren1(x0,x2,skf2(x2,x0,x1))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 491
% 237.88/48.12 === Conflict found: 40:3:1:[35.2,10.4,1.2,13.3,18.2]:Top: big_f(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,x0))),big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skc1,skf2(skc1,skf2(skc1,skc1,skc1),skc1))))))}
% 237.88/48.12 === Backtracking. Learning clause 54:2:1:[40.1,49.1]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1)
% 237.88/48.12 === Conflict found: 54:2:1:[40.1,49.1]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skf2(skc1,skc1,skf2(skc1,skc1,skc1)),skf2(skc1,skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 55:2:1:[54.2,3.2]:Top: big_f(skc1,skc1,x0) -> ren1(skc1,skc1,x0)
% 237.88/48.12 === Backtracking. Learning clause 56:3:3:[20.2,2.2,1.2]:TopTopTop: big_f(x0,x1,x2),big_f(skf2(x1,x2,x0),skf2(x1,x2,x0),skf2(x1,x2,x0)),ren1(x1,x2,x0) ->
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 551
% 237.88/48.12 === Conflict found: 48:2:1:[17.2,42.1,43.1,13.1,1.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0) {x0 -> skf2(skc1,skf2(skf2(skc1,skf2(skc1,skc1,skc1),skc1),skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 57:2:1:[48.1,52.1,33.1]:Top: big_f(x0,skf2(x0,skc1,skc1),skc1) -> ren1(skc1,x0,skf2(x0,skc1,skc1))
% 237.88/48.12 === Conflict found: 47:3:3:[17.1,46.1,7.2,32.3]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2) -> ren3(x2,x1,x0) {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 58:4:3:[47.3,7.1]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2),big_f(x2,x1,x0),big_f(x0,x2,x1) ->
% 237.88/48.12 === Conflict found: 58:4:3:[47.3,7.1]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2),big_f(x2,x1,x0),big_f(x0,x2,x1) -> {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 59:1:0:[58.3,54.2,52.1,24.1]:: ren3(skc1,skf2(skc1,skc1,skc1),skf2(skf2(skc1,skc1,skc1),skc1,skc1)) ->
% 237.88/48.12 === Conflict found: 32:3:3:[27.2,12.1]:TopTopTop: big_f(x0,x1,x2) -> ren3(x2,x0,x1),big_f(x1,x0,skf2(x0,x1,x2)) {x0 -> skc1, x1 -> skf2(skc1,skc1,skf2(skc1,skc1,skc1)), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 63:2:1:[48.1,60.0,52.0,61.1,49.0,62.3,32.2,58.1,54.2]:Top: big_f(skc1,x0,skc1) -> big_f(skf2(skc1,skc1,x0),skc1,skf2(skc1,skf2(skc1,skc1,x0),skc1))
% 237.88/48.12 === Backtracking. Learning clause 65:1:1:[52.0,64.1,7.2,48.2]:Top: ren3(skc1,skc1,x0) ->
% 237.88/48.12 === Backtracking. Learning clause 67:2:3:[9.0,66.0,3.2,8.1]:TopTopTop: -> ren1(x0,x1,x2),ren3(x1,x2,x0)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 604
% 237.88/48.12 === Backtracking. Learning clause 68:3:3:[3.2,18.2]:TopTopTop: big_f(x0,skf2(x0,x1,x2),x1),big_f(x0,x1,x2) -> ren1(x0,skf2(x0,x1,x2),x1)
% 237.88/48.12 === Backtracking. Learning clause 69:2:1:[20.1,22.1,49.1,52.1]:Top: big_f(skf2(skc1,skf2(skc1,skc1,x0),skc1),skf2(skc1,skf2(skc1,skc1,x0),skc1),skf2(skc1,skf2(skc1,skc1,x0),skc1)) -> big_f(skf2(skc1,skc1,skf2(skc1,skc1,x0)),skf2(skc1,skc1,skf2(skc1,skc1,x0)),skf2(skc1,skc1,skf2(skc1,skc1,x0)))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 662
% 237.88/48.12 === Backtracking. Learning clause 70:3:3:[15.1,6.3]:TopTopTop: big_f(x0,x1,x2),big_f(x2,x0,x1) -> big_f(x0,skf2(x0,x1,x2),x1)
% 237.88/48.12 === Conflict found: 48:2:1:[17.2,42.1,43.1,13.1,1.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0) {x0 -> skf2(skf2(skc1,skc1,skf2(skc1,skc1,skc1)),skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 71:1:1:[48.2,6.1,52.1]:Top: -> ren2(skc1,skc1,x0)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 728
% 237.88/48.12 === Backtracking. Learning clause 73:2:1:[52.0,72.0,20.3,54.2]:Top: big_f(skf2(x0,skc1,skc1),skf2(x0,skc1,skc1),skf2(x0,skc1,skc1)),big_f(skc1,skc1,x0) ->
% 237.88/48.12 === Backtracking. Learning clause 74:2:1:[6.1,52.1]:Top: big_f(skc1,x0,skc1) -> ren2(x0,skc1,skc1)
% 237.88/48.12 === Conflict found: 54:2:1:[40.1,49.1]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skf2(skc1,skf2(skc1,skc1,skc1),skc1),skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 76:1:1:[52.0,75.0,54.2,74.1,48.2]:Top: -> ren2(x0,skc1,skc1)
% 237.88/48.12 === Backtracking. Learning clause 77:4:3:[10.4,7.3]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),ren3(x0,x1,x2),big_f(x0,x1,x2) -> big_f(x1,x2,x0)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 789
% 237.88/48.12 === Conflict found: 48:2:1:[17.2,42.1,43.1,13.1,1.1]:Top: big_f(x0,skc1,skc1) -> big_f(skc1,skc1,x0) {x0 -> skf2(skc1,skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1)),skf2(skc1,skc1,skf2(skc1,skc1,skc1)))}
% 237.88/48.12 === Backtracking. Learning clause 78:1:1:[48.1,52.1]:Top: -> big_f(skc1,skc1,x0)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 843
% 237.88/48.12 === Conflict found: 27:3:3:[3.2,9.1]:TopTopTop: big_f(x0,x1,x2) -> ren1(x0,x1,x2),ren3(x2,x0,x1) {x0 -> skc1, x1 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skf2(skc1,skc1,skc1),skc1,skc1)), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 80:1:1:[78.0,79.0,27.1,54.2,12.1,65.1]:Top: -> big_f(x0,skc1,skf2(skc1,x0,skc1))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 901
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 964
% 237.88/48.12 === Backtracking. Learning clause 83:1:1:[52.0,81.0,78.0,82.1,3.1,54.2,31.2]:Top: ren3(x0,skc1,skc1) ->
% 237.88/48.12 === Backtracking. Learning clause 84:4:3:[14.2,29.3,3.2,11.1]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)) -> ren2(x0,x1,x2),ren1(x0,x1,x2),big_f(x2,x1,skf2(x1,x2,x0))
% 237.88/48.12 === Backtracking. Learning clause 85:2:3:[6.1,2.2,1.2]:TopTopTop: ren1(x0,x1,x2) -> ren2(x1,x2,x0)
% 237.88/48.12 === Backtracking. Learning clause 86:2:3:[18.2,7.3,9.1,12.2,67.1]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)) -> ren3(x0,x2,x1)
% 237.88/48.12 === Conflict found: 54:2:1:[40.1,49.1]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skf2(skc1,skc1,skc1),skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 87:1:1:[54.2,6.1,78.1]:Top: -> ren2(skc1,x0,skc1)
% 237.88/48.12 === Conflict found: 54:2:1:[40.1,49.1]:Top: big_f(skc1,skc1,x0) -> big_f(skc1,x0,skc1) {x0 -> skf2(skc1,skc1,skf2(skc1,skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1)))}
% 237.88/48.12 === Backtracking. Learning clause 88:1:1:[54.1,49.1]:Top: -> big_f(skc1,skf2(skc1,skc1,x0),skc1)
% 237.88/48.12 === Conflict found: 58:4:3:[47.3,7.1]:TopTopTop: ren3(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2),big_f(x2,x1,x0),big_f(x0,x2,x1) -> {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skc1,skf2(skc1,skc1,skc1),skc1)}
% 237.88/48.12 === Backtracking. Learning clause 90:2:1:[78.0,89.0,58.2,80.1,70.3,9.2,18.2]:Top: big_f(skc1,x0,skc1) -> big_f(skf2(x0,skc1,skf2(skc1,x0,skc1)),skc1,x0)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1032
% 237.88/48.12 === Backtracking. Learning clause 92:4:3:[14.1,91.3,4.2,77.3,34.4]:TopTopTop: ren3(x0,x1,x2),big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)) -> big_f(x1,x2,x0)
% 237.88/48.12 === Conflict found: 77:4:3:[10.4,7.3]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),ren3(x0,x1,x2),big_f(x0,x1,x2) -> big_f(x1,x2,x0) {x0 -> skf2(skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1),skc1), x1 -> skf2(skc1,skc1,skc1), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 93:3:3:[77.4,18.1,17.1]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,x1,x2) -> big_f(skf2(x1,x2,x0),x2,x1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1093
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1160
% 237.88/48.12 === Backtracking. Learning clause 94:3:3:[11.1,3.1]:TopTopTop: big_f(x0,x1,x2) -> big_f(x1,x0,skf2(x0,x1,x2)),ren1(x2,x0,x1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1232
% 237.88/48.12 === Backtracking. Learning clause 95:3:3:[8.1,35.1]:TopTopTop: big_f(x0,x1,x2) -> ren3(x2,x1,skf2(x1,x2,x0)),big_f(x2,x0,x1)
% 237.88/48.12 === Backtracking. Learning clause 96:3:3:[7.3,35.3,5.2]:TopTopTop: ren3(x0,x1,x2),big_f(x2,x1,skf2(x1,x2,x0)),ren2(x1,x2,x0) ->
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skc1,skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 97:5:3:[34.3,14.2,5.1,77.3,13.2,67.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(skc1,skc1,skf2(x1,x2,x0)),big_f(x1,x0,skf2(x0,x1,x2)) -> ren1(x0,x1,x2)
% 237.88/48.12 === Conflict found: 44:4:3:[20.2,15.2,12.2,3.3,6.3,18.2]:TopTopTop: big_f(skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2))),big_f(x0,x2,x1),big_f(x2,x1,x0),big_f(x1,x0,x2) -> {x0 -> skc1, x1 -> skc1, x2 -> skf2(skc1,skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 100:1:1:[54.1,98.1,78.0,99.2,44.3,52.1]:Top: big_f(skf2(skc1,skc1,skf2(skc1,skc1,x0)),skf2(skc1,skc1,skf2(skc1,skc1,x0)),skf2(skc1,skc1,skf2(skc1,skc1,x0))) ->
% 237.88/48.12 === Backtracking. Learning clause 101:1:1:[20.2,9.1,78.1,52.1,83.1]:Top: big_f(skf2(skc1,skc1,x0),skf2(skc1,skc1,x0),skf2(skc1,skc1,x0)) ->
% 237.88/48.12 === Backtracking. Learning clause 102:2:3:[3.2,23.1,22.1]:TopTopTop: -> ren1(x0,x1,x2),big_f(skf2(x2,x0,x1),skf2(x2,x0,x1),skf2(x2,x0,x1))
% 237.88/48.12 === Backtracking. Learning clause 103:3:3:[4.2,3.1,16.3]:TopTopTop: big_f(x2,skf2(x2,x0,x1),x0),big_f(x0,x1,x2) -> ren1(x2,x0,x1)
% 237.88/48.12 === Conflict found: 103:3:3:[4.2,3.1,16.3]:TopTopTop: big_f(x2,skf2(x2,x0,x1),x0),big_f(x0,x1,x2) -> ren1(x2,x0,x1) {x0 -> skc1, x1 -> skf2(skc1,skf2(skc1,skc1,skc1),skc1), x2 -> skf2(skc1,skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 104:2:3:[103.2,22.1,70.3,23.1,21.1]:TopTopTop: -> ren1(x0,x1,x2),big_f(skf2(x0,x1,x2),skf2(x0,x1,x2),skf2(x0,x1,x2))
% 237.88/48.12 === Conflict found: 38:4:3:[35.3,34.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,skf2(x0,x1,x2))),big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)) -> ren2(x0,x1,x2) {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 105:5:3:[38.4,5.1,18.2,70.1,14.1,3.1,93.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,skf2(x0,x1,x2))),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(skc1,skc1,skf2(x1,x2,x0)),big_f(x1,x2,x0) -> ren1(x2,skf2(x2,x0,x1),x0)
% 237.88/48.12 === Conflict found: 96:3:3:[7.3,35.3,5.2]:TopTopTop: ren3(x0,x1,x2),big_f(x2,x1,skf2(x1,x2,x0)),ren2(x1,x2,x0) -> {x0 -> skf2(skc1,skc1,skc1), x1 -> skf2(skc1,skf2(skc1,skc1,skc1),skc1), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 107:3:3:[22.0,106.2,96.2,21.1,34.4,23.1]:TopTopTop: ren3(x0,x1,x2),big_f(skc1,skc1,skf2(x1,x2,x0)) -> big_f(skf2(x2,x1,skf2(x1,x2,x0)),skf2(x2,x1,skf2(x1,x2,x0)),skf2(x2,x1,skf2(x1,x2,x0)))
% 237.88/48.12 === Backtracking. Learning clause 108:3:3:[10.2,78.1,18.1]:TopTopTop: big_f(x0,x1,x2) -> big_f(x2,x0,x1),big_f(skf2(x1,x2,x0),x2,x1)
% 237.88/48.12 === Backtracking. Learning clause 109:2:3:[7.2,4.2,5.2]:TopTopTop: ren3(x0,x1,x2),ren2(x0,x1,x2) ->
% 237.88/48.12 === Conflict found: 73:2:1:[52.0,72.0,20.3,54.2]:Top: big_f(skf2(x0,skc1,skc1),skf2(x0,skc1,skc1),skf2(x0,skc1,skc1)),big_f(skc1,skc1,x0) -> {x0 -> skf2(skc1,skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1)),skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 110:1:1:[73.2,78.1]:Top: big_f(skf2(x0,skc1,skc1),skf2(x0,skc1,skc1),skf2(x0,skc1,skc1)) ->
% 237.88/48.12 === Backtracking. Learning clause 111:3:3:[12.1,53.3]:TopTopTop: big_f(x0,x1,x2),ren2(x2,x0,x1) -> big_f(x2,x0,skf2(x0,x2,skf2(x2,x0,x1)))
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1305
% 237.88/48.12 === Conflict found: 56:3:3:[20.2,2.2,1.2]:TopTopTop: big_f(x0,x1,x2),big_f(skf2(x1,x2,x0),skf2(x1,x2,x0),skf2(x1,x2,x0)),ren1(x1,x2,x0) -> {x0 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1))), x1 -> skc1, x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 112:3:3:[56.1,18.2]:TopTopTop: big_f(skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2))),ren1(x0,x1,skf2(x1,x0,x2)),big_f(x1,x0,x2) ->
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1384
% 237.88/48.12 === Backtracking. Learning clause 113:4:3:[7.2,93.3]:TopTopTop: ren3(skf2(x0,x1,x2),x1,x0),big_f(x0,skf2(x0,x1,x2),x1),big_f(skc1,skc1,skf2(x2,x0,x1)),big_f(x2,x0,x1) ->
% 237.88/48.12 === Conflict found: 33:3:3:[3.3,12.1,4.2,16.3,3.1]:TopTopTop: big_f(x0,x1,x2),big_f(x2,skf2(x2,x0,x1),x0) -> ren1(x0,x2,skf2(x2,x0,x1)) {x0 -> skc1, x1 -> skf2(skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1),skc1), x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 114:3:3:[33.2,10.4,1.1,9.1,13.1,8.1,17.2]:TopTopTop: big_f(skc1,skc1,skf2(skf2(x0,x1,x2),x1,x0)) -> ren1(x0,x1,x2),ren3(x2,x0,x1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1471
% 237.88/48.12 === Backtracking. Learning clause 115:3:3:[3.2,14.2]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)) -> ren1(x0,x1,skf2(x1,x0,x2)),big_f(x0,x2,x1)
% 237.88/48.12 === Backtracking. Learning clause 117:2:3:[14.0,116.0,7.2,11.1,17.1,18.1,108.1]:TopTopTop: -> big_f(x0,skf2(x0,x1,x2),x1),big_f(skf2(x1,x0,skf2(x0,x1,x2)),x0,x1)
% 237.88/48.12 === Clause set with instances from active satisfied. Growing active. New size: 1565
% 237.88/48.12 === Conflict found: 56:3:3:[20.2,2.2,1.2]:TopTopTop: big_f(x0,x1,x2),big_f(skf2(x1,x2,x0),skf2(x1,x2,x0),skf2(x1,x2,x0)),ren1(x1,x2,x0) -> {x0 -> skf2(skf2(skc1,skc1,skc1),skc1,skc1), x1 -> skc1, x2 -> skf2(skc1,skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 118:3:3:[56.1,5.2]:TopTopTop: big_f(skf2(x0,x1,x2),skf2(x0,x1,x2),skf2(x0,x1,x2)),ren1(x0,x1,x2),ren2(x0,x1,x2) ->
% 237.88/48.12 === Conflict found: 95:3:3:[8.1,35.1]:TopTopTop: big_f(x0,x1,x2) -> ren3(x2,x1,skf2(x1,x2,x0)),big_f(x2,x0,x1) {x0 -> skf2(skc1,skf2(skc1,skc1,skc1),skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1))), x1 -> skf2(skc1,skc1,skc1), x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 120:3:3:[18.0,119.3,95.1,18.2,16.1,11.2,5.1,14.2,10.1,78.1]:TopTopTop: -> ren3(x0,x1,skf2(x1,x0,skf2(x0,x1,skf2(x1,x0,x2)))),big_f(skf2(x1,x0,x2),x0,x1),big_f(x2,x1,x0)
% 237.88/48.12 === Conflict found: 38:4:3:[35.3,34.3]:TopTopTop: big_f(x0,x1,skf2(x1,x0,skf2(x0,x1,x2))),big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)) -> ren2(x0,x1,x2) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 122:4:3:[85.0,121.3,38.2,9.1,12.2,5.1,115.2,29.2,14.2,13.2,8.1]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(skc1,skc1,skf2(x1,x2,x0)) -> ren2(x1,x2,x0),ren3(x1,x0,skf2(x0,x1,x2))
% 237.88/48.12 === Conflict found: 122:4:3:[85.0,121.3,38.2,9.1,12.2,5.1,115.2,29.2,14.2,13.2,8.1]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(skc1,skc1,skf2(x1,x2,x0)) -> ren2(x1,x2,x0),ren3(x1,x0,skf2(x0,x1,x2)) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 123:3:3:[122.1,78.1,15.1]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)) -> ren3(x0,x2,skf2(x2,x0,x1)),big_f(x0,skf2(x0,x1,x2),x1)
% 237.88/48.12 === Backtracking. Learning clause 124:3:3:[13.3,85.1]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)),big_f(x2,x1,x0) -> ren2(x0,x2,x1)
% 237.88/48.12 === Conflict found: 124:3:3:[13.3,85.1]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)),big_f(x2,x1,x0) -> ren2(x0,x2,x1) {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 125:2:3:[124.3,15.1,14.1]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)) -> big_f(x0,skf2(x0,x2,x1),x2)
% 237.88/48.12 === Conflict found: 125:2:3:[124.3,15.1,14.1]:TopTopTop: big_f(x0,x1,skf2(x1,x0,x2)) -> big_f(x0,skf2(x0,x2,x1),x2) {x0 -> skf2(skf2(skc1,skc1,skc1),skc1,skc1), x1 -> skc1, x2 -> skc1}
% 237.88/48.12 === Backtracking. Learning clause 126:1:1:[125.1,80.1]:Top: -> big_f(x0,skf2(x0,skc1,skc1),skc1)
% 237.88/48.12 === Backtracking. Learning clause 127:1:1:[18.1,52.1]:Top: -> big_f(skf2(x0,skc1,skc1),skc1,x0)
% 237.88/48.12 === Backtracking. Learning clause 128:3:3:[17.2,13.2,109.1,1.1,124.1,5.1,3.2,4.2]:TopTopTop: big_f(x0,x1,skf2(x1,x0,skf2(x0,x1,x2))),ren2(x2,x0,x1) -> ren1(x2,x0,x1)
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skc1,skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 130:4:3:[4.0,129.3,34.4,4.1,14.2,124.1,5.1,117.2,16.1,10.4]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,skf2(x1,x0,x2))),big_f(x2,x1,x0),big_f(skc1,skc1,skf2(x2,x1,x0)) -> big_f(x1,x0,x2)
% 237.88/48.12 === Conflict found: 44:4:3:[20.2,15.2,12.2,3.3,6.3,18.2]:TopTopTop: big_f(skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2)),skf2(x0,x1,skf2(x1,x0,x2))),big_f(x0,x2,x1),big_f(x2,x1,x0),big_f(x1,x0,x2) -> {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skc1,skf2(skc1,skc1,skc1),skf2(skf2(skc1,skc1,skc1),skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 134:2:1:[8.0,131.1,127.0,132.2,78.0,133.3,44.3,18.2,102.2,56.3,111.3,126.1,70.3,111.3,26.2,76.1]:Top: big_f(skf2(x0,skf2(x0,skc1,skf2(skc1,x0,skf2(x0,skc1,skc1))),skc1),skf2(x0,skf2(x0,skc1,skf2(skc1,x0,skf2(x0,skc1,skc1))),skc1),skf2(x0,skf2(x0,skc1,skf2(skc1,x0,skf2(x0,skc1,skc1))),skc1)) -> ren3(skc1,x0,skf2(x0,skc1,skc1))
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skc1,skf2(skc1,skc1,skc1),skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 135:4:3:[34.2,78.1,14.2,16.1]:TopTopTop: big_f(skf2(x0,x1,skf2(x1,x0,x2)),x1,x0),big_f(x0,x2,x1) -> ren2(x0,x1,skf2(x1,x0,x2)),ren2(x1,x0,x2)
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skc1, x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 136:5:3:[34.1,108.3,14.2,135.2]:TopTopTop: big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x2,x0,x1),big_f(skf2(x1,x0,skf2(x0,x1,x2)),x0,x1) -> ren2(x1,x0,skf2(x0,x1,x2)),ren2(x0,x1,x2)
% 237.88/48.12 === Conflict found: 108:3:3:[10.2,78.1,18.1]:TopTopTop: big_f(x0,x1,x2) -> big_f(x2,x0,x1),big_f(skf2(x1,x2,x0),x2,x1) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 137:4:3:[108.3,34.1,16.2,117.1,136.3,4.1,124.1]:TopTopTop: big_f(skc1,skc1,skf2(x1,x2,x0)),big_f(x0,x1,x2) -> ren2(x1,x2,x0),ren2(x2,x0,x1)
% 237.88/48.12 === Backtracking. Learning clause 138:1:1:[3.2,49.1,52.1]:Top: -> ren1(skf2(skc1,skc1,x0),skc1,skc1)
% 237.88/48.12 === Conflict found: 137:4:3:[108.3,34.1,16.2,117.1,136.3,4.1,124.1]:TopTopTop: big_f(skc1,skc1,skf2(x1,x2,x0)),big_f(x0,x1,x2) -> ren2(x1,x2,x0),ren2(x2,x0,x1) {x0 -> skf2(skc1,skc1,skc1), x1 -> skc1, x2 -> skf2(skf2(skc1,skc1,skc1),skc1,skf2(skc1,skc1,skc1))}
% 237.88/48.12 === Backtracking. Learning clause 139:1:3:[137.2,4.2,5.1,78.1,53.1,1.1,137.3,78.1,15.1,14.1,125.1]:TopTopTop: -> big_f(x0,skf2(x0,x1,x2),x1)
% 237.88/48.12 === Conflict found: 102:2:3:[3.2,23.1,22.1]:TopTopTop: -> ren1(x0,x1,x2),big_f(skf2(x2,x0,x1),skf2(x2,x0,x1),skf2(x2,x0,x1)) {x0 -> skc1, x1 -> skf2(skc1,skf2(skf2(skc1,skc1,skc1),skc1,skc1),skc1), x2 -> skf2(skf2(skc1,skc1,skc1),skc1,skc1)}
% 237.88/48.12 === Backtracking. Learning clause 140:4:3:[102.2,44.1,12.1]:TopTopTop: big_f(x0,x1,x2),big_f(x1,x2,x0),big_f(x2,x0,x1) -> big_f(skf2(x2,x0,x1),x2,skf2(x2,skf2(x2,x0,x1),x0))
% 237.88/48.12 === Conflict found: 34:4:3:[19.2,9.2,29.2,16.2]:TopTopTop: big_f(skf2(x0,x1,x2),x1,x0),big_f(skc1,skc1,skf2(x0,x1,x2)),big_f(x0,skf2(x0,x1,x2),x1) -> ren2(x0,x1,x2) {x0 -> skf2(skc1,skc1,skc1), x1 -> skf2(skc1,skc1,skc1), x2 -> skf2(skc1,skc1,skc1)}
% 237.88/48.12
% 237.88/48.12 SZS status Unsatisfiable
% 237.88/48.12
% 237.88/48.12 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 237.88/48.12
% 237.88/48.12 SPASS-SCL-FOL Statistics:
% 237.88/48.12 Number of learned clauses: 89
% 237.88/48.12 Number of propagations: 35744
% 237.88/48.12 Number of decisions: 3922
% 237.88/48.12 Number of resolutions: 244
% 237.88/48.12 Number of condensations: 0
% 237.88/48.12 Number of sub resolutions: 28
% 237.88/48.12 Number of input literals (deduplicated): 9
% 237.88/48.12 Number of grows: 28
% 237.88/48.12 Number of considered ground atoms: 1565
% 237.88/48.12
% 237.88/48.12 Needed: 0:0:47.51
% 237.88/48.12
%------------------------------------------------------------------------------