%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN632-1 : TPTP v9.2.1. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n021.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:40:06 PM UTC 2026
% Result : Unsatisfiable 188.87s 38.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : SYN632-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.36 % Computer : n021.cluster.edu
% 0.18/0.36 % Model : x86_64 x86_64
% 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36 % Memory : 8042.1875MB
% 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36 % CPULimit : 300
% 0.18/0.36 % WCLimit : 300
% 0.18/0.36 % DateTime : Thu May 7 13:47:13 EDT 2026
% 0.18/0.36 % CPUTime :
% 0.18/0.36 SPASS-SCL-FOL version:
% 0.25/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 188.87/38.48 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48 Execution resolution_2 ended with status: unsatisfiable
% 188.87/38.48 Used heuristic: resolution_2
% 188.87/38.48
% 188.87/38.48 Input Clauses:
% 188.87/38.48
% 188.87/38.48 Predicates: p11 p9 p8 p6 p4 p3 p2 p19 p17 p15 p13 p21
% 188.87/38.48 Fol Constants: c24 c28 c25 c26 c22 c23 c27 c29
% 188.87/38.48 Fol Functions: f12 f10 f7 f5 f16 f18 f20 f14
% 188.87/38.48 Problem Properties:
% 188.87/38.48 This is a full first-order problem without equality.
% 188.87/38.48
% 188.87/38.48 After reduction: Problem Properties:
% 188.87/38.48 This is a full first-order problem without equality.
% 188.87/38.48
% 188.87/38.48
% 188.87/38.48 Reduced Input Clauses:
% 188.87/38.48
% 188.87/38.48 Most General Atoms: p11(x1,x2) p8(x1,x2) p19(x1,x2) p17(x1,x2) p15(x1,x2) p13(x1,x2) p4(x2,x3) p21(x3,x1) p9(x2,x3) p2(x2,x3) p3(x2,x3) p6(x2,x3)
% 188.87/38.48
% 188.87/38.48 === Starting SPASS-SCL-FOL A Little Less Naive, considering 79 atoms initially, heuristics mode: resolution_2 ===
% 188.87/38.48
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 79
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 79
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 79
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 79
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 143
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 143
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 143
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 39:1:2:[34.1,6.1]:TopTop: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),x1),x1)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 143
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 143
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 207
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 207
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 207
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 207
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 213
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 40:3:2:[23.3,24.1]:TopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c23),x1) -> p21(x1,x0)
% 188.87/38.48 === Backtracking. Learning clause 41:2:2:[37.1,24.1]:TopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c23) -> p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c27)
% 188.87/38.48 === Backtracking. Learning clause 42:1:0:[36.1,24.1]:: -> p21(f5(c22,f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c27)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 277
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 283
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 43:3:4:[23.3,39.1]:TopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x0),x3) -> p21(x3,x1)
% 188.87/38.48 === Backtracking. Learning clause 44:2:3:[37.2,39.1]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),x1),x2)
% 188.87/38.48 === Backtracking. Learning clause 45:1:0:[35.2,39.1]:: p21(f5(c22,c23),c27) ->
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 287
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 46:3:2:[23.3,42.1]:TopTop: p3(c27,x0),p4(f5(c22,f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x1) -> p21(x1,x0)
% 188.87/38.48 === Backtracking. Learning clause 47:2:2:[37.1,42.1]:TopTop: p21(f5(f7(f10(c24,x0),c22),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)) -> p21(f5(f7(f10(c24,f12(c28,x0)),c22),x1),c27)
% 188.87/38.48 === Conflict found: 44:2:3:[37.2,39.1]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),x1),x2) {x0 -> c22, x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27), x2 -> c27}
% 188.87/38.48 === Backtracking. Learning clause 48:1:0:[44.1,42.1]:: -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c27)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 292
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) ->
% 188.87/38.48 === Conflict found: 40:3:2:[23.3,24.1]:TopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c23),x1) -> p21(x1,x0) {x0 -> c27, x1 -> f5(c22,c23)}
% 188.87/38.48 === Backtracking. Learning clause 50:2:0:[40.3,45.1]:: p3(c27,c27),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c23),f5(c22,c23)) ->
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 298
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 51:3:2:[23.3,48.1]:TopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 51:3:2:[23.3,48.1]:TopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x1) -> p21(x1,x0) {x0 -> c27, x1 -> f5(c22,c23)}
% 188.87/38.48 === Backtracking. Learning clause 52:2:0:[51.3,45.1]:: p3(c27,c27),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),f5(c22,c23)) ->
% 188.87/38.48 === Backtracking. Learning clause 53:1:0:[38.1,48.1]:: -> p21(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 362
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 368
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 54:3:2:[23.3,53.1]:TopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),x0),p4(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 54:3:2:[23.3,53.1]:TopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),x0),p4(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x1) -> p21(x1,x0) {x0 -> c27, x1 -> f5(c22,c23)}
% 188.87/38.48 === Backtracking. Learning clause 55:2:0:[54.3,45.1]:: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),f5(c22,c23)) ->
% 188.87/38.48 === Backtracking. Learning clause 56:1:0:[33.1,53.1]:: -> p3(f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 376
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 57:1:1:[34.1,56.1]:Top: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 380
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 58:3:3:[23.3,57.1]:TopTopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),x0),p4(f5(f7(f10(c24,f12(c25,c26)),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x2) -> p21(x2,x0)
% 188.87/38.48 === Conflict found: 58:3:3:[23.3,57.1]:TopTopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),x0),p4(f5(f7(f10(c24,f12(c25,c26)),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x2) -> p21(x2,x0) {x0 -> c27, x1 -> c24, x2 -> f5(c22,c23)}
% 188.87/38.48 === Backtracking. Learning clause 59:2:1:[58.3,45.1]:Top: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),f5(c22,c23)) ->
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 389
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 60:4:5:[23.3,34.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x3),x4),p3(x3,x0) -> p21(x4,x1)
% 188.87/38.48 === Conflict found: 41:2:2:[37.1,24.1]:TopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c23) -> p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c27) {x0 -> f12(c25,c26), x1 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 61:2:1:[41.1,34.2]:Top: p3(x0,c23) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x0),c27)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 453
% 188.87/38.48 === Conflict found: 60:4:5:[23.3,34.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x3),x4),p3(x3,x0) -> p21(x4,x1) {x0 -> c27, x1 -> c27, x2 -> c22, x3 -> c27, x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 62:5:5:[60.4,49.3]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x3),x4),p3(x3,x0),p3(x1,c27),p4(x4,f5(c22,c23)) ->
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 463
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 63:2:4:[33.1,36.2]:TopTopTopTop: p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c25,c26)),x1)),x2),x3) -> p3(f14(f16(f18(f20(c29,x0),x2),f7(f10(c24,f12(c25,c26)),x1)),x3),x3)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 467
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 64:4:6:[23.3,38.2]:TopTopTopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),x4),p4(f5(f7(f10(c24,x0),x2),x1),x5),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> p21(x5,x4)
% 188.87/38.48 === Conflict found: 64:4:6:[23.3,38.2]:TopTopTopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),x4),p4(f5(f7(f10(c24,x0),x2),x1),x5),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> p21(x5,x4) {x0 -> f12(c25,c26), x1 -> c23, x2 -> c22, x3 -> c27, x4 -> c27, x5 -> f5(c22,c23)}
% 188.87/38.48 === Backtracking. Learning clause 65:3:4:[64.4,45.1]:TopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),c27),p4(f5(f7(f10(c24,x0),x2),x1),f5(c22,c23)),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) ->
% 188.87/38.48 === Backtracking. Learning clause 66:3:5:[37.2,38.2]:TopTopTopTopTop: p21(f5(x0,f14(f16(f18(f20(c29,x1),x2),x0),x3)),x4),p21(f5(f7(f10(c24,f12(c28,x1)),x0),x2),x3) -> p21(f5(f7(f10(c24,f12(c28,x1)),x0),x2),x4)
% 188.87/38.48 === Conflict found: 44:2:3:[37.2,39.1]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),x1),x2) {x0 -> f7(f10(c24,f12(c25,c26)),c22), x1 -> c23, x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 67:2:4:[44.1,38.2]:TopTopTopTop: p21(f5(f7(f10(c24,f12(c28,x0)),x1),x2),x3) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,x0),x1)),x2),f14(f16(f18(f20(c29,x0),x2),x1),x3))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 482
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 68:4:4:[23.3,41.2]:TopTopTopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,x1)),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x2),x3),p21(f5(f7(f10(c24,x1),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x2),c23) -> p21(x3,x0)
% 188.87/38.48 === Backtracking. Learning clause 69:2:2:[38.1,41.2,44.1]:TopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c23) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),c22))),x1),f14(f16(f18(f20(c29,x0),x1),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 497
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1)
% 188.87/38.48 === Backtracking. Learning clause 71:2:3:[36.1,44.2]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(x0,f14(f16(f18(f20(c29,f12(c25,c26)),x1),x0),x2)),x2)
% 188.87/38.48 === Backtracking. Learning clause 72:1:0:[38.1,24.1]:: -> p21(f5(f7(f10(c24,f12(c25,c26)),c22),c23),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 561
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 562
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 73:4:6:[23.3,67.2]:TopTopTopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),x4),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,x0),x2)),x1),x5),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> p21(x5,x4)
% 188.87/38.48 === Conflict found: 71:2:3:[36.1,44.2]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(x0,f14(f16(f18(f20(c29,f12(c25,c26)),x1),x0),x2)),x2) {x0 -> f7(f10(c24,f12(c25,c26)),c22), x1 -> c23, x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 74:1:0:[71.1,72.1]:: -> p21(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 569
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 75:2:1:[37.2,74.1]:Top: p21(f5(c22,f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)),x0) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x0)
% 188.87/38.48 === Conflict found: 47:2:2:[37.1,42.1]:TopTop: p21(f5(f7(f10(c24,x0),c22),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)) -> p21(f5(f7(f10(c24,f12(c28,x0)),c22),x1),c27) {x0 -> f12(c25,c26), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))}
% 188.87/38.48 === Backtracking. Learning clause 76:1:0:[47.1,74.1]:: -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c27)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 581
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 77:2:2:[37.1,76.1]:TopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))) -> p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),x1),c27)
% 188.87/38.48 === Conflict found: 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) -> {x0 -> c27, x1 -> f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)))}
% 188.87/38.48 === Backtracking. Learning clause 78:2:0:[49.3,76.1]:: p3(c27,c27),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Conflict found: 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1) {x0 -> c27, x1 -> c24, x2 -> f7(f10(c24,f12(c28,f12(c25,c26))),c22), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 79:3:2:[70.3,76.1]:TopTop: p3(c27,x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c28,f12(c25,c26))),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 64:4:6:[23.3,38.2]:TopTopTopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),x4),p4(f5(f7(f10(c24,x0),x2),x1),x5),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> p21(x5,x4) {x0 -> f12(c25,c26), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x2 -> c22, x3 -> c27, x4 -> c24, x5 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 80:3:2:[64.3,76.1]:TopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),x0),p4(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 65:3:4:[64.4,45.1]:TopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),c27),p4(f5(f7(f10(c24,x0),x2),x1),f5(c22,c23)),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> {x0 -> f12(c25,c26), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x2 -> c22, x3 -> c27}
% 188.87/38.48 === Backtracking. Learning clause 81:2:0:[65.3,76.1]:: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Conflict found: 67:2:4:[44.1,38.2]:TopTopTopTop: p21(f5(f7(f10(c24,f12(c28,x0)),x1),x2),x3) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,x0),x1)),x2),f14(f16(f18(f20(c29,x0),x2),x1),x3)) {x0 -> f12(c25,c26), x1 -> c22, x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x3 -> c27}
% 188.87/38.48 === Backtracking. Learning clause 82:1:0:[67.1,76.1]:: -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 598
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 83:2:2:[37.1,82.1]:TopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22))),x1),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))) -> p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22))),x1),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Conflict found: 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) -> {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)))}
% 188.87/38.48 === Backtracking. Learning clause 84:2:0:[49.3,82.1]:: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),c27),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Conflict found: 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> c24, x2 -> f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22)), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 85:3:2:[70.3,82.1]:TopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22))),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 64:4:6:[23.3,38.2]:TopTopTopTopTopTop: p3(f14(f16(f18(f20(c29,x0),x1),x2),x3),x4),p4(f5(f7(f10(c24,x0),x2),x1),x5),p21(f5(f7(f10(c24,f12(c28,x0)),x2),x1),x3) -> p21(x5,x4) {x0 -> f12(c25,c26), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x2 -> f7(f10(c24,f12(c25,c26)),c22), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x4 -> c24, x5 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 86:3:2:[64.3,82.1]:TopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)),x0),p4(f5(f7(f10(c24,f12(c25,c26)),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x1) -> p21(x1,x0)
% 188.87/38.48 === Conflict found: 66:3:5:[37.2,38.2]:TopTopTopTopTop: p21(f5(x0,f14(f16(f18(f20(c29,x1),x2),x0),x3)),x4),p21(f5(f7(f10(c24,f12(c28,x1)),x0),x2),x3) -> p21(f5(f7(f10(c24,f12(c28,x1)),x0),x2),x4) {x0 -> f7(f10(c24,f12(c25,c26)),c22), x1 -> f12(c25,c26), x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 87:2:1:[66.2,82.1]:Top: p21(f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x0) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),x0)
% 188.87/38.48 === Conflict found: 63:2:4:[33.1,36.2]:TopTopTopTop: p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c25,c26)),x1)),x2),x3) -> p3(f14(f16(f18(f20(c29,x0),x2),f7(f10(c24,f12(c25,c26)),x1)),x3),x3) {x0 -> f12(c25,c26), x1 -> c22, x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 88:1:0:[63.1,82.1]:: -> p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 662
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 669
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 89:1:1:[34.1,88.1]:Top: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 675
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Conflict found: 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) -> {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> f5(f7(f10(c24,f12(c25,c26)),c22),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)))}
% 188.87/38.48 === Backtracking. Learning clause 90:2:1:[49.3,89.1]:Top: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Backtracking. Learning clause 91:2:2:[37.2,89.1]:TopTop: p21(f5(x0,f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)),x1) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x1)
% 188.87/38.48 === Conflict found: 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> c24, x2 -> f7(f10(c24,f12(c25,c26)),c22), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 92:3:3:[70.3,89.1]:TopTopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x2) -> p21(x2,x0)
% 188.87/38.48 === Conflict found: 71:2:3:[36.1,44.2]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(x0,f14(f16(f18(f20(c29,f12(c25,c26)),x1),x0),x2)),x2) {x0 -> f7(f10(c24,f12(c25,c26)),c22), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 93:1:1:[71.1,89.1]:Top: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 685
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Conflict found: 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) -> {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> f5(f7(f10(c24,f12(c25,c26)),c24),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)))}
% 188.87/38.48 === Backtracking. Learning clause 94:2:1:[49.3,93.1]:Top: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Backtracking. Learning clause 95:2:2:[37.2,93.1]:TopTop: p21(f5(x0,f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)),x1) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x1)
% 188.87/38.48 === Conflict found: 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> c24, x2 -> f7(f10(c24,f12(c25,c26)),c24), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 96:3:3:[70.3,93.1]:TopTopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x2) -> p21(x2,x0)
% 188.87/38.48 === Conflict found: 44:2:3:[37.2,39.1]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),x1),x2) {x0 -> f7(f10(c24,f12(c25,c26)),c24), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 97:1:1:[44.1,93.1,36.1]:Top: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 693
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Conflict found: 49:3:2:[23.4,45.1]:TopTop: p3(x0,c27),p4(x1,f5(c22,c23)),p21(x1,x0) -> {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> f5(f7(f10(c24,f12(c25,c26)),c24),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)))}
% 188.87/38.48 === Backtracking. Learning clause 98:2:1:[49.3,97.1]:Top: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),c27),p4(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f5(c22,c23)) ->
% 188.87/38.48 === Conflict found: 70:4:5:[23.3,44.2]:TopTopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x2),x3),x4),p21(f5(x2,x3),x0) -> p21(x4,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x1 -> c24, x2 -> f7(f10(c24,f12(c25,c26)),c24), x3 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x4 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 99:3:3:[70.3,97.1]:TopTopTop: p3(f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27),x0),p4(f5(f7(f10(c24,f12(c28,f12(c25,c26))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),x2) -> p21(x2,x0)
% 188.87/38.48 === Backtracking. Learning clause 100:2:3:[37.1,97.1]:TopTopTop: p21(f5(f7(f10(c24,x0),f7(f10(c24,f12(c25,c26)),x1)),x2),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x1)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))) -> p21(f5(f7(f10(c24,f12(c28,x0)),f7(f10(c24,f12(c25,c26)),x1)),x2),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Conflict found: 44:2:3:[37.2,39.1]:TopTopTop: p21(f5(x0,x1),x2) -> p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),x0),x1),x2) {x0 -> f7(f10(c24,f12(c25,c26)),c24), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x2 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)}
% 188.87/38.48 === Backtracking. Learning clause 101:1:1:[44.1,97.1,36.1]:Top: -> p21(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),x0)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 757
% 188.87/38.48 === Conflict found: 43:3:4:[23.3,39.1]:TopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x0),x3) -> p21(x3,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27)), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x2 -> c22, x3 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 102:3:5:[43.1,33.2]:TopTopTopTopTop: p4(f5(f7(f10(c24,f12(c25,c26)),x0),x1),x2),p21(f5(f7(f10(c24,f12(c25,c26)),x3),x1),x4) -> p21(x2,x4)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 761
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Conflict found: 43:3:4:[23.3,39.1]:TopTopTopTop: p3(x0,x1),p4(f5(f7(f10(c24,f12(c25,c26)),x2),x0),x3) -> p21(x3,x1) {x0 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27))),f7(f10(c24,f12(c25,c26)),c24)),f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27)), x1 -> f14(f16(f18(f20(c29,f12(c25,c26)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),f7(f10(c24,f12(c25,c26)),c22)),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),c22),c27), x2 -> c24, x3 -> c24}
% 188.87/38.48 === Backtracking. Learning clause 103:3:6:[43.1,63.2]:TopTopTopTopTopTop: p4(f5(f7(f10(c24,f12(c25,c26)),x0),f14(f16(f18(f20(c29,x1),x2),f7(f10(c24,f12(c25,c26)),x3)),x4)),x5),p21(f5(f7(f10(c24,f12(c28,x1)),f7(f10(c24,f12(c25,c26)),x3)),x2),x4) -> p21(x5,x4)
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 763
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 104:2:0:[31.3,50.2,6.1]:: p2(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c22),p3(c27,c27) ->
% 188.87/38.48 === Backtracking. Learning clause 105:2:3:[30.1,11.1]:TopTopTop: p3(x0,x1) -> p3(f14(x2,x0),f14(x2,x1))
% 188.87/38.48 === Clause set with instances from active satisfied. Growing active. New size: 765
% 188.87/38.48 === Restarting.
% 188.87/38.48 === Backtracking. Learning clause 106:3:1:[16.3,52.2]:Top: p4(x0,f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),f14(f16(f18(f20(c29,f12(c25,c26)),c23),c22),c27))),p4(x0,f5(c22,c23)),p3(c27,c27) ->
% 188.87/38.48
% 188.87/38.48 SZS status Unsatisfiable
% 188.87/38.48
% 188.87/38.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 188.87/38.48
% 188.87/38.48 SPASS-SCL-FOL Statistics:
% 188.87/38.48 Number of learned clauses: 68
% 188.87/38.48 Number of propagations: 10601
% 188.87/38.48 Number of decisions: 4891
% 188.87/38.48 Number of resolutions: 80
% 188.87/38.48 Number of condensations: 0
% 188.87/38.48 Number of sub resolutions: 0
% 188.87/38.48 Number of input literals (deduplicated): 40
% 188.87/38.48 Number of grows: 43
% 188.87/38.48 Number of considered ground atoms: 765
% 188.87/38.48
% 188.87/38.48 Needed: 0:0:37.88
% 188.87/38.48
%------------------------------------------------------------------------------