%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN656-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 : n004.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:07 PM UTC 2026
% Result : Unsatisfiable 21.07s 5.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN656-1 : TPTP v9.2.1. Released v2.5.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n004.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:47:03 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 21.07/5.73 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73 Execution resolution_2 ended with status: unsatisfiable
% 21.07/5.73 Used heuristic: resolution_2
% 21.07/5.73
% 21.07/5.73 Input Clauses:
% 21.07/5.73
% 21.07/5.73 Predicates: p11 p9 p8 p6 p4 p3 p22 p20 p2 p18 p16 p14 p12 p24 p25
% 21.07/5.73 Fol Constants: c26 c27 c30 c31 c28 c29 c32 c33 c34 c35 c36
% 21.07/5.73 Fol Functions: f13 f10 f7 f5 f15 f17 f21 f23 f19
% 21.07/5.73 Problem Properties:
% 21.07/5.73 This is a full first-order problem without equality.
% 21.07/5.73
% 21.07/5.73 After reduction: Problem Properties:
% 21.07/5.73 This is a full first-order problem without equality.
% 21.07/5.73
% 21.07/5.73
% 21.07/5.73 Reduced Input Clauses:
% 21.07/5.73
% 21.07/5.73 Most General Atoms: p11(x1,x2) p20(x1,x2) p2(x1,x2) p18(x1,x2) p9(x2,x3) p24(x3,x1) p4(x2,x3) p25(x3,x1) p8(x2,x3) p14(x2,x3) p16(x2,x3) p3(x2,x3) p6(x2,x3) p22(x2,x3) p12(x2,x3)
% 21.07/5.73
% 21.07/5.73 === Starting SPASS-SCL-FOL A Little Less Naive, considering 50 atoms initially, heuristics mode: resolution_2 ===
% 21.07/5.73
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 50
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 50
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 50
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 50
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 114
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 178
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 242
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 242
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 242
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 50:3:2:[34.3,14.1]:TopTop: p4(c27,x0),p9(c26,x1) -> p24(x1,x0)
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 243
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 51:3:3:[34.3,15.1]:TopTopTop: p4(c27,x0),p9(f10(c30,f13(c31,x1)),x2) -> p24(x2,x0)
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 247
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 52:3:3:[35.4,16.1]:TopTopTop: p3(x0,x1),p4(x2,f5(f7(c28,c29),x1)),p25(x2,x0) ->
% 21.07/5.73 === Backtracking. Learning clause 53:2:1:[48.2,16.1]:Top: p25(f5(f7(c28,f7(c28,c29)),x0),x0) -> p25(f5(f7(c28,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),x0),x0)),x0)
% 21.07/5.73 === Backtracking. Learning clause 54:1:1:[33.2,16.1]:Top: p25(f5(c29,x0),x0) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 311
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 316
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 55:3:3:[35.3,31.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),x2) -> p25(x2,x1)
% 21.07/5.73 === Backtracking. Learning clause 56:2:2:[46.1,31.1]:TopTop: p25(f5(f7(c28,c29),f13(c31,x0)),x1) -> p25(f5(f7(c28,c29),f13(c31,f15(c32,x0))),x1)
% 21.07/5.73 === Backtracking. Learning clause 57:1:1:[33.1,31.1]:Top: -> p25(f5(f7(c28,c29),f13(c31,f15(c32,x0))),f13(c31,x0))
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 326
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 58:3:2:[35.4,45.1]:TopTop: p3(x0,f13(c31,c34)),p4(x1,f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35))))),p25(x1,x0) ->
% 21.07/5.73 === Conflict found: 58:3:2:[35.4,45.1]:TopTop: p3(x0,f13(c31,c34)),p4(x1,f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35))))),p25(x1,x0) -> {x0 -> f13(c31,c26), x1 -> f5(c29,f13(c31,f15(c32,c26)))}
% 21.07/5.73 === Backtracking. Learning clause 59:2:1:[58.3,31.1]:Top: p3(f13(c31,x0),f13(c31,c34)),p4(f5(c29,f13(c31,f15(c32,x0))),f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35))))) ->
% 21.07/5.73 === Backtracking. Learning clause 60:2:0:[47.2,45.1]:: p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) -> p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))
% 21.07/5.73 === Backtracking. Learning clause 61:2:1:[46.3,45.1]:Top: p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),x0),p25(f5(f7(c28,c29),x0),f13(c31,c34)) ->
% 21.07/5.73 === Conflict found: 56:2:2:[46.1,31.1]:TopTop: p25(f5(f7(c28,c29),f13(c31,x0)),x1) -> p25(f5(f7(c28,c29),f13(c31,f15(c32,x0))),x1) {x0 -> f15(f17(c33,c34),c35), x1 -> f13(c31,c34)}
% 21.07/5.73 === Backtracking. Learning clause 62:1:0:[56.2,45.1]:: p25(f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35))),f13(c31,c34)) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 330
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 63:3:3:[35.4,54.1]:TopTopTop: p3(x0,x1),p4(x2,f5(c29,x1)),p25(x2,x0) ->
% 21.07/5.73 === Conflict found: 63:3:3:[35.4,54.1]:TopTopTop: p3(x0,x1),p4(x2,f5(c29,x1)),p25(x2,x0) -> {x0 -> f13(c31,c26), x1 -> c26, x2 -> f5(c29,f13(c31,f15(c32,c26)))}
% 21.07/5.73 === Backtracking. Learning clause 64:2:2:[63.3,31.1]:TopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),f5(c29,x1)) ->
% 21.07/5.73 === Backtracking. Learning clause 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5)
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 346
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Conflict found: 63:3:3:[35.4,54.1]:TopTopTop: p3(x0,x1),p4(x2,f5(c29,x1)),p25(x2,x0) -> {x0 -> f13(c31,c34), x1 -> c26, x2 -> f5(f7(c28,c29),f13(c31,f15(c32,c34)))}
% 21.07/5.73 === Backtracking. Learning clause 66:2:2:[63.3,57.1]:TopTop: p3(f13(c31,x0),x1),p4(f5(f7(c28,c29),f13(c31,f15(c32,x0))),f5(c29,x1)) ->
% 21.07/5.73 === Backtracking. Learning clause 67:1:0:[46.2,57.1,45.1]:: p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 410
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 418
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 68:2:0:[48.2,62.1]:: p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(f17(c33,c34),c35))),f13(c31,c34)) -> p25(f5(f7(c28,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(f17(c33,c34),c35))),f13(c31,c34))),f13(c31,c34))
% 21.07/5.73 === Backtracking. Learning clause 69:2:1:[46.3,62.1]:Top: p25(f5(c29,f13(c31,f15(f17(c33,c34),c35))),x0),p25(f5(f7(c28,c29),x0),f13(c31,c34)) ->
% 21.07/5.73 === Conflict found: 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5) {x0 -> c26, x1 -> c26, x2 -> c26, x3 -> f13(c31,c34), x4 -> f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35))), x5 -> c26, x6 -> c26}
% 21.07/5.73 === Backtracking. Learning clause 70:6:5:[65.6,62.1]:TopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(x2,x3),p4(f5(x0,x1),x4) -> p25(x4,x3)
% 21.07/5.73 === Conflict found: 55:3:3:[35.3,31.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),x2) -> p25(x2,x1) {x0 -> c26, x1 -> f13(c31,c34), x2 -> f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))}
% 21.07/5.73 === Backtracking. Learning clause 71:2:1:[55.3,62.1]:Top: p3(f13(c31,x0),f13(c31,c34)),p4(f5(c29,f13(c31,f15(c32,x0))),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))) ->
% 21.07/5.73 === Backtracking. Learning clause 72:1:0:[49.2,62.1]:: -> p3(f13(c31,c34),f13(c31,f15(f17(c33,c34),c35)))
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 426
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Conflict found: 55:3:3:[35.3,31.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),x2) -> p25(x2,x1) {x0 -> c26, x1 -> f13(c31,f15(c32,c34)), x2 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73 === Backtracking. Learning clause 73:2:1:[55.3,67.1]:Top: p3(f13(c31,x0),f13(c31,f15(c32,c34))),p4(f5(c29,f13(c31,f15(c32,x0))),f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))) ->
% 21.07/5.73 === Backtracking. Learning clause 74:2:0:[47.2,67.1]:: p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))) -> p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))))
% 21.07/5.73 === Conflict found: 70:6:5:[65.6,62.1]:TopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(x2,x3),p4(f5(x0,x1),x4) -> p25(x4,x3) {x0 -> c26, x1 -> c26, x2 -> c26, x3 -> f13(c31,f15(c32,c34)), x4 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73 === Backtracking. Learning clause 75:5:3:[70.6,67.1]:TopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(x2,f13(c31,f15(c32,c34))),p4(f5(x0,x1),f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 439
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Conflict found: 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5) {x0 -> c26, x1 -> c26, x2 -> f13(c31,c34), x3 -> f13(c31,f15(f17(c33,c34),c35)), x4 -> c26, x5 -> f13(c31,f15(f17(c33,c34),c35)), x6 -> c26}
% 21.07/5.73 === Backtracking. Learning clause 76:5:4:[65.2,72.1]:TopTopTopTop: p25(f5(f7(c28,x0),x1),f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),f13(c31,c34))),x2),p4(f5(x0,x1),x3) -> p25(x2,f13(c31,f15(f17(c33,c34),c35))),p25(x3,f13(c31,f15(f17(c33,c34),c35)))
% 21.07/5.73 === Backtracking. Learning clause 77:2:1:[35.4,62.1,6.1]:Top: p4(x0,f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p25(x0,f13(c31,c34)) ->
% 21.07/5.73 === Backtracking. Learning clause 78:2:2:[44.2,72.1]:TopTop: p2(x0,x1) -> p4(f5(x0,f13(c31,c34)),f5(x1,f13(c31,f15(f17(c33,c34),c35))))
% 21.07/5.73 === Backtracking. Learning clause 79:2:2:[43.2,72.1]:TopTop: p18(x0,x1) -> p3(f19(x0,f13(c31,c34)),f19(x1,f13(c31,f15(f17(c33,c34),c35))))
% 21.07/5.73 === Backtracking. Learning clause 80:2:2:[39.2,72.1]:TopTop: p20(x0,x1) -> p18(f21(x0,f13(c31,c34)),f21(x1,f13(c31,f15(f17(c33,c34),c35))))
% 21.07/5.73 === Backtracking. Learning clause 81:2:2:[36.1,72.1]:TopTop: p8(x0,x1) -> p9(f10(x0,f13(c31,c34)),f10(x1,f13(c31,f15(f17(c33,c34),c35))))
% 21.07/5.73 === Backtracking. Learning clause 82:2:1:[22.1,72.1]:Top: p3(f13(c31,c34),x0) -> p3(f13(c31,f15(f17(c33,c34),c35)),x0)
% 21.07/5.73 === Conflict found: 64:2:2:[63.3,31.1]:TopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),f5(c29,x1)) -> {x0 -> c34, x1 -> f13(c31,f15(f17(c33,c34),c35))}
% 21.07/5.73 === Backtracking. Learning clause 83:1:0:[64.1,72.1]:: p4(f5(c29,f13(c31,f15(c32,c34))),f5(c29,f13(c31,f15(f17(c33,c34),c35)))) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 442
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 84:2:0:[44.3,83.1]:: p2(c29,c29),p3(f13(c31,f15(c32,c34)),f13(c31,f15(f17(c33,c34),c35))) ->
% 21.07/5.73 === Backtracking. Learning clause 85:2:1:[21.3,83.1]:Top: p4(x0,f5(c29,f13(c31,f15(c32,c34)))),p4(x0,f5(c29,f13(c31,f15(f17(c33,c34),c35)))) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 506
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 511
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Conflict found: 55:3:3:[35.3,31.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),x2) -> p25(x2,x1) {x0 -> c26, x1 -> f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))), x2 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73 === Backtracking. Learning clause 86:3:3:[55.3,30.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),f5(c29,x2)) -> p24(f10(c30,x1),c27)
% 21.07/5.73 === Backtracking. Learning clause 87:3:2:[48.2,30.1]:TopTop: p25(f5(f7(c28,c29),x0),x1) -> p25(f5(f7(c28,c29),f19(f21(f23(c36,c29),x0),x1)),x1),p24(f10(c30,x1),c27)
% 21.07/5.73 === Conflict found: 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5) {x0 -> c26, x1 -> c26, x2 -> c26, x3 -> f13(c31,c34), x4 -> f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35))), x5 -> f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))), x6 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73 === Backtracking. Learning clause 88:6:5:[65.7,30.1,62.1]:TopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(x2,x3),p4(f5(x0,x1),f5(c29,x4)) -> p24(f10(c30,x3),c27)
% 21.07/5.73 === Conflict found: 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5) {x0 -> c26, x1 -> c26, x2 -> c26, x3 -> c26, x4 -> c26, x5 -> f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))), x6 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73 === Backtracking. Learning clause 89:7:7:[65.7,30.1]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),f5(c29,x6)) -> p25(x4,x3),p24(f10(c30,x5),c27)
% 21.07/5.73 === Conflict found: 74:2:0:[47.2,67.1]:: p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))) -> p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34)))) {}
% 21.07/5.73 === Backtracking. Learning clause 90:2:0:[74.2,30.1]:: p25(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34))) -> p24(f10(c30,f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,f15(c32,c34)))),c27)
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 530
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 91:4:3:[35.3,53.2]:TopTopTop: p3(x0,x1),p4(f5(f7(c28,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),x0),x0)),x2),p25(f5(f7(c28,f7(c28,c29)),x0),x0) -> p25(x2,x1)
% 21.07/5.73 === Backtracking. Learning clause 92:3:1:[47.1,53.2]:Top: p25(f5(f7(c28,f7(c28,c29)),x0),x0) -> p25(f5(f7(c28,c29),f19(f21(f23(c36,f7(c28,c29)),x0),x0)),x0),p25(f5(f7(c28,c29),f19(f21(f23(c36,f7(c28,c29)),x0),x0)),f19(f21(f23(c36,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),x0),x0)),x0))
% 21.07/5.73 === Conflict found: 52:3:3:[35.4,16.1]:TopTopTop: p3(x0,x1),p4(x2,f5(f7(c28,c29),x1)),p25(x2,x0) -> {x0 -> f13(c31,c34), x1 -> f13(c31,f15(f17(c33,c34),c35)), x2 -> f5(f7(c28,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),f13(c31,c34)),f13(c31,c34)))}
% 21.07/5.73 === Backtracking. Learning clause 93:2:0:[52.3,53.2,72.1]:: p4(f5(f7(c28,f7(c28,c29)),f19(f21(f23(c36,f7(c28,c29)),f13(c31,c34)),f13(c31,c34))),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p25(f5(f7(c28,f7(c28,c29)),f13(c31,c34)),f13(c31,c34)) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 533
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 94:3:1:[44.3,59.2]:Top: p2(c29,f7(c28,c29)),p3(f13(c31,f15(c32,x0)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),p3(f13(c31,x0),f13(c31,c34)) ->
% 21.07/5.73 === Backtracking. Learning clause 95:3:2:[21.3,59.2]:TopTop: p4(x0,f5(c29,f13(c31,f15(c32,x1)))),p4(x0,f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35))))),p3(f13(c31,x1),f13(c31,c34)) ->
% 21.07/5.73 === Clause set with instances from active satisfied. Growing active. New size: 552
% 21.07/5.73 === Restarting.
% 21.07/5.73 === Backtracking. Learning clause 96:4:2:[35.3,60.2]:TopTop: p3(f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),x0),p4(f5(f7(c28,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),x1),p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) -> p25(x1,x0)
% 21.07/5.73 === Conflict found: 65:7:7:[48.3,35.3,35.3]:TopTopTopTopTopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,x3),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),x4),p3(x2,x5),p4(f5(x0,x1),x6) -> p25(x4,x3),p25(x6,x5) {x0 -> c29, x1 -> f13(c31,f15(c32,f15(f17(c33,c34),c35))), x2 -> f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)), x3 -> f13(c31,c34), x4 -> f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35))), x5 -> c26, x6 -> c26}
% 21.07/5.73 === Backtracking. Learning clause 97:6:2:[65.1,60.2,62.1]:TopTop: p3(f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),f13(c31,c34)),p4(f5(f7(c28,c29),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),x0),p4(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),x1),p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) -> p25(x1,x0)
% 21.07/5.73 === Conflict found: 75:5:3:[70.6,67.1]:TopTopTop: p25(f5(f7(c28,x0),x1),x2),p3(x2,f13(c31,c34)),p4(f5(f7(c28,x0),f19(f21(f23(c36,x0),x1),x2)),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(x2,f13(c31,f15(c32,c34))),p4(f5(x0,x1),f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))) -> {x0 -> c29, x1 -> f13(c31,f15(c32,f15(f17(c33,c34),c35))), x2 -> f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))}
% 21.07/5.73 === Backtracking. Learning clause 98:4:0:[75.1,60.2,5.1]:: p3(f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),f13(c31,c34)),p4(f5(f7(c28,c29),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))),f5(f7(c28,c29),f13(c31,f15(f17(c33,c34),c35)))),p3(f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)),f13(c31,f15(c32,c34))),p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) ->
% 21.07/5.73 === Conflict found: 87:3:2:[48.2,30.1]:TopTop: p25(f5(f7(c28,c29),x0),x1) -> p25(f5(f7(c28,c29),f19(f21(f23(c36,c29),x0),x1)),x1),p24(f10(c30,x1),c27) {x0 -> f13(c31,f15(c32,f15(f17(c33,c34),c35))), x1 -> f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))}
% 21.07/5.73 === Backtracking. Learning clause 99:3:0:[87.1,60.2]:: p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) -> p25(f5(f7(c28,c29),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),p24(f10(c30,f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),c27)
% 21.07/5.73 === Backtracking. Learning clause 100:3:0:[48.1,60.2]:: p25(f5(f7(c28,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)) -> p25(f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34))),p25(f5(f7(c28,c29),f19(f21(f23(c36,c29),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))),f19(f21(f23(c36,f7(c28,c29)),f13(c31,f15(c32,f15(f17(c33,c34),c35)))),f13(c31,c34)))
% 21.07/5.73 === Conflict found: 55:3:3:[35.3,31.1]:TopTopTop: p3(f13(c31,x0),x1),p4(f5(c29,f13(c31,f15(c32,x0))),x2) -> p25(x2,x1) {x0 -> f15(f17(c33,c34),c35), x1 -> f13(c31,c34), x2 -> f5(c29,f13(c31,f15(c32,f15(f17(c33,c34),c35))))}
% 21.07/5.73
% 21.07/5.73 SZS status Unsatisfiable
% 21.07/5.73
% 21.07/5.73 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.07/5.73
% 21.07/5.73 SPASS-SCL-FOL Statistics:
% 21.07/5.73 Number of learned clauses: 51
% 21.07/5.73 Number of propagations: 5276
% 21.07/5.73 Number of decisions: 2650
% 21.07/5.73 Number of resolutions: 64
% 21.07/5.73 Number of condensations: 0
% 21.07/5.73 Number of sub resolutions: 0
% 21.07/5.73 Number of input literals (deduplicated): 50
% 21.07/5.73 Number of grows: 34
% 21.07/5.73 Number of considered ground atoms: 552
% 21.07/5.73
% 21.07/5.73 Needed: 0:00:05.17
% 21.07/5.73
%------------------------------------------------------------------------------