%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN718-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 : n008.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:11 PM UTC 2026
% Result : Unsatisfiable 83.18s 21.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN718-1 : TPTP v9.2.1. Released v2.5.0.
% 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n008.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:44 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.21/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 83.18/21.32 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32 Execution resolution_3 ended with status: unsatisfiable
% 83.18/21.32 Used heuristic: resolution_3
% 83.18/21.32
% 83.18/21.32 Input Clauses:
% 83.18/21.32
% 83.18/21.32 Predicates: p11 p9 p7 p6 p58 p54 p52 p50 p49 p47 p45 p43 p41 p4 p39 p37 p35 p33 p31 p3 p29 p27 p25 p23 p21 p20 p2 p18 p16 p15 p14 p12 p60 p55 p59 p57 p62 p56 p61
% 83.18/21.32 Fol Constants: c77 c70 c63 c64 c74 c75 c78 c84 c72 c73 c76 c68 c69 c66 c83 c85 c71 c81 c82 c79 c80 c65 c67 c92 c88 c89 c86 c87 c93 c90 c91
% 83.18/21.32 Fol Functions: f28 f10 f17 f5 f19 f30 f26 f24 f22 f13 f8 f32 f53 f51 f48 f46 f38 f42 f40 f44 f36 f34
% 83.18/21.32 Problem Properties:
% 83.18/21.32 This is a full first-order problem without equality.
% 83.18/21.32
% 83.18/21.32 After reduction: Problem Properties:
% 83.18/21.32 This is a full first-order problem without equality.
% 83.18/21.32
% 83.18/21.32
% 83.18/21.32 Reduced Input Clauses:
% 83.18/21.32
% 83.18/21.32 Most General Atoms: p11(x1,x2) p7(x1,x2) p58(x1,x2) p54(x1,x2) p52(x1,x2) p50(x1,x2) p20(x1,x2) p2(x1,x2) p16(x1,x2) p14(x1,x2) p18(x2,x3) p62(x1,x3) p12(x2,x3) p55(x1,x3) p56(x2,x3) p21(x2,x3) p57(x1,x3) p25(x2,x3) p59(x1,x3) p15(x2,x3) p60(x3,x1) p61(x1,x3) p31(x2,x3) p6(x2,x3) p49(x2,x3) p47(x2,x3) p45(x2,x3) p37(x2,x3) p41(x2,x3) p39(x2,x3) p43(x2,x3) p35(x2,x3) p4(x2,x3) p9(x2,x3) p27(x2,x3) p23(x2,x3) p33(x2,x3) p29(x2,x3) p3(x1,x5)
% 83.18/21.32
% 83.18/21.32 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_3 ===
% 83.18/21.32
% 83.18/21.32 === Backtracking. Learning clause 119:3:2:[74.2,34.1]:TopTop: p54(c63,x0),p12(c64,x1) -> p55(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 120:2:1:[58.2,36.1]:Top: p3(c84,x0) -> p3(x0,f10(c72,c73))
% 83.18/21.32 === Backtracking. Learning clause 121:2:1:[67.2,38.1]:Top: p16(f17(c68,c69),x0) -> p16(x0,c70)
% 83.18/21.32 === Backtracking. Learning clause 122:3:2:[77.2,35.1]:TopTop: p58(c74,x0),p25(f28(c75,c78),x1) -> p59(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 123:3:2:[77.2,37.1]:TopTop: p58(c74,x0),p25(f28(c75,c76),x1) -> p59(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 124:4:5:[76.2,72.2]:TopTopTopTopTop: p25(f26(f30(c85,x0),x1),x2),p21(x3,x4),p57(f26(x0,x1),x3) -> p57(x2,x4)
% 83.18/21.32 === Backtracking. Learning clause 125:2:1:[58.3,71.1]:Top: p3(x0,f19(f5(c66,f10(c72,c73)),c83)),p3(x0,f10(c72,c73)) ->
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 119
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Backtracking. Learning clause 126:2:2:[40.2,2.1]:TopTop: p9(x0,x1) -> p9(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 127:2:2:[41.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 128:2:2:[42.2,4.1]:TopTop: p6(x0,x1) -> p6(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 129:2:2:[45.2,7.1]:TopTop: p52(x0,x1) -> p52(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 130:2:2:[46.2,8.1]:TopTop: p50(x0,x1) -> p50(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 131:2:2:[49.2,11.1]:TopTop: p45(x0,x1) -> p45(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 132:2:2:[50.2,12.1]:TopTop: p43(x0,x1) -> p43(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 133:2:2:[52.2,14.1]:TopTop: p4(x0,x1) -> p4(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 134:2:2:[53.2,15.1]:TopTop: p39(x0,x1) -> p39(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 135:2:2:[54.2,16.1]:TopTop: p37(x0,x1) -> p37(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 136:2:2:[56.2,18.1]:TopTop: p33(x0,x1) -> p33(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 138:2:2:[67.2,29.1]:TopTop: p16(x0,x1) -> p16(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 139:3:2:[76.2,80.1]:TopTop: p25(f26(c70,f22(f24(c71,c81),c82)),x0),p21(f22(f24(c71,c83),c84),x1) -> p57(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 140:3:2:[76.2,81.1]:TopTop: p25(f26(c70,f22(f24(c71,c79),c80)),x0),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 141:3:3:[75.1,82.1]:TopTopTop: p7(f8(f13(c65,c64),f5(c66,f10(c67,x0))),x1),p4(f5(c66,x0),x2) -> p56(x1,x2)
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 184
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Backtracking. Learning clause 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f26(f30(c85,c77),c77)}
% 83.18/21.32 === Backtracking. Learning clause 143:4:5:[142.2,124.1]:TopTopTopTopTop: p25(x0,f26(f30(c85,x1),x2)),p21(x3,x4),p57(f26(x1,x2),x3) -> p57(x0,x4)
% 83.18/21.32 === Backtracking. Learning clause 144:2:2:[63.2,25.1]:TopTop: p21(x0,x1) -> p21(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 145:2:2:[64.2,26.1]:TopTop: p20(x0,x1) -> p20(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 146:2:2:[66.2,28.1]:TopTop: p18(x0,x1) -> p18(x1,x0)
% 83.18/21.32 === Backtracking. Learning clause 147:2:0:[108.2,80.1]:: p3(f19(f5(c66,c82),c81),f10(c72,c73)) -> p18(c81,c83)
% 83.18/21.32 === Backtracking. Learning clause 148:2:0:[106.1,80.1]:: -> p18(c81,c83),p62(f53(c64,c81),c83)
% 83.18/21.32 === Conflict found: 143:4:5:[142.2,124.1]:TopTopTopTopTop: p25(x0,f26(f30(c85,x1),x2)),p21(x3,x4),p57(f26(x1,x2),x3) -> p57(x0,x4) {x0 -> c77, x1 -> c70, x2 -> f22(f24(c71,c79),c80), x3 -> f22(f24(c71,c81),c82), x4 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 149:3:2:[143.3,81.1]:TopTop: p25(x0,f26(f30(c85,c70),f22(f24(c71,c79),c80))),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 150:2:0:[108.2,81.1]:: p3(f19(f5(c66,c80),c79),f10(c72,c73)) -> p18(c79,c81)
% 83.18/21.32 === Backtracking. Learning clause 151:2:0:[106.1,81.1]:: -> p18(c79,c81),p62(f53(c64,c79),c81)
% 83.18/21.32 === Backtracking. Learning clause 152:5:6:[110.3,79.2]:TopTopTopTopTopTop: p57(f26(c70,f22(f24(c71,x0),x1)),f22(f24(c71,x2),x3)),p50(f51(c92,f19(f5(c66,x1),x2)),x4),p3(f19(f5(c66,x3),x2),x5) -> p62(f53(c64,x0),x2),p61(x4,x5)
% 83.18/21.32 === Backtracking. Learning clause 153:1:0:[72.2,105.1]:: p57(f26(c70,f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73))) ->
% 83.18/21.32 === Backtracking. Learning clause 154:2:1:[107.3,105.1]:Top: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p57(f26(f30(c85,c70),x0),f22(f24(c71,c83),f10(c72,c73))) ->
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 256
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f28(c75,c78)}
% 83.18/21.32 === Backtracking. Learning clause 155:3:2:[142.2,122.2]:TopTop: p25(x0,f28(c75,c78)),p58(c74,x1) -> p59(x1,x0)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f28(c75,c76)}
% 83.18/21.32 === Backtracking. Learning clause 156:3:2:[142.2,123.2]:TopTop: p25(x0,f28(c75,c76)),p58(c74,x1) -> p59(x1,x0)
% 83.18/21.32 === Conflict found: 138:2:2:[67.2,29.1]:TopTop: p16(x0,x1) -> p16(x1,x0) {x0 -> c77, x1 -> f17(c68,c69)}
% 83.18/21.32 === Backtracking. Learning clause 157:2:1:[138.2,121.1]:Top: p16(x0,f17(c68,c69)) -> p16(x0,c70)
% 83.18/21.32 === Conflict found: 138:2:2:[67.2,29.1]:TopTop: p16(x0,x1) -> p16(x1,x0) {x0 -> f17(c68,c69), x1 -> c70}
% 83.18/21.32 === Backtracking. Learning clause 158:1:0:[138.1,38.1]:: -> p16(c70,f17(c68,c69))
% 83.18/21.32 === Backtracking. Learning clause 159:2:1:[77.3,23.1,35.1]:Top: p58(c74,x0) -> p59(x0,f28(c75,c78))
% 83.18/21.32 === Backtracking. Learning clause 160:2:1:[77.3,23.1,37.1]:Top: p58(c74,x0) -> p59(x0,f28(c75,c76))
% 83.18/21.32 === Backtracking. Learning clause 161:3:2:[67.1,83.3,38.1]:TopTop: p14(c68,x0),p15(c69,x1) -> p16(f17(x0,x1),c70)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f26(c70,f22(f24(c71,c81),c82))}
% 83.18/21.32 === Backtracking. Learning clause 162:3:2:[142.2,139.1]:TopTop: p25(x0,f26(c70,f22(f24(c71,c81),c82))),p21(f22(f24(c71,c83),c84),x1) -> p57(x0,x1)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f26(c70,f22(f24(c71,c79),c80))}
% 83.18/21.32 === Backtracking. Learning clause 163:3:2:[142.2,140.1]:TopTop: p25(x0,f26(c70,f22(f24(c71,c79),c80))),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 164:4:5:[63.1,101.3]:TopTopTopTopTop: p21(f22(x0,x1),x2),p20(x0,x3),p3(x1,x4) -> p21(f22(x3,x4),x2)
% 83.18/21.32 === Conflict found: 125:2:1:[58.3,71.1]:Top: p3(x0,f19(f5(c66,f10(c72,c73)),c83)),p3(x0,f10(c72,c73)) -> {x0 -> f19(c77,c77)}
% 83.18/21.32 === Backtracking. Learning clause 165:3:2:[125.1,97.3]:TopTop: p3(f19(x0,x1),f10(c72,c73)),p18(x1,c83),p4(x0,f5(c66,f10(c72,c73))) ->
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(f5(c66,f10(c72,c73)),c83)}
% 83.18/21.32 === Backtracking. Learning clause 166:1:0:[137.2,71.1]:: p3(f10(c72,c73),f19(f5(c66,f10(c72,c73)),c83)) ->
% 83.18/21.32 === Conflict found: 139:3:2:[76.2,80.1]:TopTop: p25(f26(c70,f22(f24(c71,c81),c82)),x0),p21(f22(f24(c71,c83),c84),x1) -> p57(x0,x1) {x0 -> c77, x1 -> f22(f24(c71,c83),c84)}
% 83.18/21.32 === Backtracking. Learning clause 167:2:1:[139.2,25.1,142.2]:Top: p25(x0,f26(c70,f22(f24(c71,c81),c82))) -> p57(x0,f22(f24(c71,c83),c84))
% 83.18/21.32 === Conflict found: 124:4:5:[76.2,72.2]:TopTopTopTopTop: p25(f26(f30(c85,x0),x1),x2),p21(x3,x4),p57(f26(x0,x1),x3) -> p57(x2,x4) {x0 -> c77, x1 -> c77, x2 -> f26(c70,f22(f24(c71,c77),c77)), x3 -> c77, x4 -> f22(f24(c71,c77),c77)}
% 83.18/21.32 === Backtracking. Learning clause 168:7:9:[124.4,152.1]:TopTopTopTopTopTopTopTopTop: p25(f26(f30(c85,x0),x1),f26(c70,f22(f24(c71,x2),x3))),p21(x4,f22(f24(c71,x5),x6)),p57(f26(x0,x1),x4),p50(f51(c92,f19(f5(c66,x3),x5)),x7),p3(f19(f5(c66,x6),x5),x8) -> p62(f53(c64,x2),x5),p61(x7,x8)
% 83.18/21.32 === Conflict found: 124:4:5:[76.2,72.2]:TopTopTopTopTop: p25(f26(f30(c85,x0),x1),x2),p21(x3,x4),p57(f26(x0,x1),x3) -> p57(x2,x4) {x0 -> c70, x1 -> f22(f24(c71,c81),c82), x2 -> c77, x3 -> f22(f24(c71,c83),c84), x4 -> f22(f24(c71,c83),c84)}
% 83.18/21.32 === Backtracking. Learning clause 169:2:1:[124.3,80.1,25.1]:Top: p25(f26(f30(c85,c70),f22(f24(c71,c81),c82)),x0) -> p57(x0,f22(f24(c71,c83),c84))
% 83.18/21.32 === Backtracking. Learning clause 170:2:1:[76.1,23.1,81.1]:Top: p21(f22(f24(c71,c81),c82),x0) -> p57(f26(c70,f22(f24(c71,c79),c80)),x0)
% 83.18/21.32 === Conflict found: 140:3:2:[76.2,81.1]:TopTop: p25(f26(c70,f22(f24(c71,c79),c80)),x0),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1) {x0 -> f26(c70,f22(f24(c71,c79),c80)), x1 -> f22(f24(c71,c83),f10(c72,c73))}
% 83.18/21.32 === Backtracking. Learning clause 171:1:0:[140.3,153.1,23.1]:: p21(f22(f24(c71,c81),c82),f22(f24(c71,c83),f10(c72,c73))) ->
% 83.18/21.32 === Backtracking. Learning clause 172:2:1:[76.4,153.1,23.1,170.2]:Top: p21(x0,f22(f24(c71,c83),f10(c72,c73))),p21(f22(f24(c71,c81),c82),x0) ->
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 320
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Conflict found: 138:2:2:[67.2,29.1]:TopTop: p16(x0,x1) -> p16(x1,x0) {x0 -> f17(c77,c77), x1 -> c70}
% 83.18/21.32 === Backtracking. Learning clause 173:3:2:[138.1,161.3]:TopTop: p14(c68,x0),p15(c69,x1) -> p16(c70,f17(x0,x1))
% 83.18/21.32 === Backtracking. Learning clause 174:4:2:[73.2,148.2]:TopTop: p52(f53(c64,c81),x0),p18(c83,x1) -> p62(x0,x1),p18(c81,c83)
% 83.18/21.32 === Backtracking. Learning clause 175:4:2:[73.2,151.2]:TopTop: p52(f53(c64,c79),x0),p18(c81,x1) -> p62(x0,x1),p18(c79,c81)
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(f5(c66,c82),c81)}
% 83.18/21.32 === Backtracking. Learning clause 176:3:1:[137.2,147.1,58.3]:Top: p3(x0,f10(c72,c73)),p3(x0,f19(f5(c66,c82),c81)) -> p18(c81,c83)
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(f5(c66,c82),c81)}
% 83.18/21.32 === Backtracking. Learning clause 177:2:0:[137.2,147.1]:: p3(f10(c72,c73),f19(f5(c66,c82),c81)) -> p18(c81,c83)
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(f5(c66,c80),c79)}
% 83.18/21.32 === Backtracking. Learning clause 178:3:1:[137.2,150.1,58.3]:Top: p3(x0,f10(c72,c73)),p3(x0,f19(f5(c66,c80),c79)) -> p18(c79,c81)
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(f5(c66,c80),c79)}
% 83.18/21.32 === Backtracking. Learning clause 179:2:0:[137.2,150.1]:: p3(f10(c72,c73),f19(f5(c66,c80),c79)) -> p18(c79,c81)
% 83.18/21.32 === Conflict found: 127:2:2:[41.2,3.1]:TopTop: p7(x0,x1) -> p7(x1,x0) {x0 -> c77, x1 -> f8(f13(c65,c64),f5(c66,f10(c67,c77)))}
% 83.18/21.32 === Backtracking. Learning clause 180:3:3:[127.2,141.1]:TopTopTop: p7(x0,f8(f13(c65,c64),f5(c66,f10(c67,x1)))),p4(f5(c66,x1),x2) -> p56(x0,x2)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> c77, x1 -> f26(f30(c85,c70),f22(f24(c71,c81),c82))}
% 83.18/21.32 === Backtracking. Learning clause 181:2:1:[142.2,169.1]:Top: p25(x0,f26(f30(c85,c70),f22(f24(c71,c81),c82))) -> p57(x0,f22(f24(c71,c83),c84))
% 83.18/21.32 === Conflict found: 154:2:1:[107.3,105.1]:Top: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p57(f26(f30(c85,c70),x0),f22(f24(c71,c83),f10(c72,c73))) -> {x0 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 182:2:1:[154.2,72.2,72.2]:Top: p57(f26(c70,x0),f22(f24(c71,c83),f10(c72,c73))),p57(f26(c70,f22(f24(c71,c79),c80)),x0) ->
% 83.18/21.32 === Backtracking. Learning clause 183:2:2:[75.2,3.1,82.1]:TopTop: p4(f5(c66,x0),x1) -> p56(f8(f13(c65,c64),f5(c66,f10(c67,x0))),x1)
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 371
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Backtracking. Learning clause 184:4:5:[45.2,87.3,129.2]:TopTopTopTopTop: p12(x0,x1),p18(x2,x3),p52(x4,f53(x0,x2)) -> p52(x4,f53(x1,x3))
% 83.18/21.32 === Conflict found: 137:2:2:[58.2,20.1]:TopTop: p3(x0,x1) -> p3(x1,x0) {x0 -> f10(c72,c73), x1 -> f19(c77,c77)}
% 83.18/21.32 === Backtracking. Learning clause 185:3:2:[137.2,165.1]:TopTop: p3(f10(c72,c73),f19(x0,x1)),p18(x1,c83),p4(x0,f5(c66,f10(c72,c73))) ->
% 83.18/21.32 === Backtracking. Learning clause 186:6:5:[76.4,182.1,101.3,170.2,63.3]:TopTopTopTopTop: p25(x0,f26(c70,x1)),p57(x0,f22(x2,x3)),p20(x2,f24(c71,c83)),p3(x3,f10(c72,c73)),p21(x4,f22(f24(c71,c81),c82)),p21(x4,x1) ->
% 83.18/21.32 === Conflict found: 172:2:1:[76.4,153.1,23.1,170.2]:Top: p21(x0,f22(f24(c71,c83),f10(c72,c73))),p21(f22(f24(c71,c81),c82),x0) -> {x0 -> f22(c77,c77)}
% 83.18/21.32 === Backtracking. Learning clause 187:3:2:[172.1,101.3]:TopTop: p21(f22(f24(c71,c81),c82),f22(x0,x1)),p20(x0,f24(c71,c83)),p3(x1,f10(c72,c73)) ->
% 83.18/21.32 === Conflict found: 186:6:5:[76.4,182.1,101.3,170.2,63.3]:TopTopTopTopTop: p25(x0,f26(c70,x1)),p57(x0,f22(x2,x3)),p20(x2,f24(c71,c83)),p3(x3,f10(c72,c73)),p21(x4,f22(f24(c71,c81),c82)),p21(x4,x1) -> {x0 -> c77, x1 -> f22(f24(c71,c77),c77), x2 -> c77, x3 -> c77, x4 -> f22(f24(c71,c81),c82)}
% 83.18/21.32 === Backtracking. Learning clause 188:5:4:[186.5,25.1]:TopTopTopTop: p25(x0,f26(c70,x1)),p57(x0,f22(x2,x3)),p20(x2,f24(c71,c83)),p3(x3,f10(c72,c73)),p21(f22(f24(c71,c81),c82),x1) ->
% 83.18/21.32 === Conflict found: 187:3:2:[172.1,101.3]:TopTop: p21(f22(f24(c71,c81),c82),f22(x0,x1)),p20(x0,f24(c71,c83)),p3(x1,f10(c72,c73)) -> {x0 -> f24(c71,c81), x1 -> c82}
% 83.18/21.32 === Backtracking. Learning clause 189:3:1:[187.1,25.1,64.3]:Top: p3(c82,f10(c72,c73)),p20(x0,f24(c71,c81)),p20(x0,f24(c71,c83)) ->
% 83.18/21.32 === Conflict found: 187:3:2:[172.1,101.3]:TopTop: p21(f22(f24(c71,c81),c82),f22(x0,x1)),p20(x0,f24(c71,c83)),p3(x1,f10(c72,c73)) -> {x0 -> f24(c71,c81), x1 -> c82}
% 83.18/21.32 === Backtracking. Learning clause 190:2:0:[187.1,25.1]:: p20(f24(c71,c81),f24(c71,c83)),p3(c82,f10(c72,c73)) ->
% 83.18/21.32 === Conflict found: 140:3:2:[76.2,81.1]:TopTop: p25(f26(c70,f22(f24(c71,c79),c80)),x0),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1) {x0 -> c77, x1 -> f22(f24(c71,c81),c82)}
% 83.18/21.32 === Backtracking. Learning clause 191:2:1:[140.2,25.1,142.2]:Top: p25(x0,f26(c70,f22(f24(c71,c79),c80))) -> p57(x0,f22(f24(c71,c81),c82))
% 83.18/21.32 === Conflict found: 149:3:2:[143.3,81.1]:TopTop: p25(x0,f26(f30(c85,c70),f22(f24(c71,c79),c80))),p21(f22(f24(c71,c81),c82),x1) -> p57(x0,x1) {x0 -> c77, x1 -> f22(f24(c71,c81),c82)}
% 83.18/21.32 === Backtracking. Learning clause 192:2:1:[149.2,25.1]:Top: p25(x0,f26(f30(c85,c70),f22(f24(c71,c79),c80))) -> p57(x0,f22(f24(c71,c81),c82))
% 83.18/21.32 === Conflict found: 154:2:1:[107.3,105.1]:Top: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p57(f26(f30(c85,c70),x0),f22(f24(c71,c83),f10(c72,c73))) -> {x0 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 193:4:4:[154.2,124.4]:TopTopTopTop: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p25(f26(f30(c85,x1),x2),f26(f30(c85,c70),x0)),p21(x3,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x1,x2),x3) ->
% 83.18/21.32 === Backtracking. Learning clause 194:7:7:[76.1,100.3,193.1]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p25(f26(f30(c85,x4),x5),f26(f30(c85,c70),x3)),p21(x6,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x4,x5),x6) ->
% 83.18/21.32 === Conflict found: 154:2:1:[107.3,105.1]:Top: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p57(f26(f30(c85,c70),x0),f22(f24(c71,c83),f10(c72,c73))) -> {x0 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 195:4:3:[154.2,76.4]:TopTopTop: p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),x0),p25(x1,f26(f30(c85,c70),x0)),p57(x1,x2),p21(x2,f22(f24(c71,c83),f10(c72,c73))) ->
% 83.18/21.32 === Backtracking. Learning clause 196:8:7:[76.1,100.3,195.1,101.3]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p25(x4,f26(f30(c85,c70),x3)),p57(x4,f22(x5,x6)),p20(x5,f24(c71,c83)),p3(x6,f10(c72,c73)) ->
% 83.18/21.32 === Conflict found: 152:5:6:[110.3,79.2]:TopTopTopTopTopTop: p57(f26(c70,f22(f24(c71,x0),x1)),f22(f24(c71,x2),x3)),p50(f51(c92,f19(f5(c66,x1),x2)),x4),p3(f19(f5(c66,x3),x2),x5) -> p62(f53(c64,x0),x2),p61(x4,x5) {x0 -> c81, x1 -> c82, x2 -> c83, x3 -> c84, x4 -> c77, x5 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 197:4:2:[152.1,80.1]:TopTop: p50(f51(c92,f19(f5(c66,c82),c83)),x0),p3(f19(f5(c66,c84),c83),x1) -> p62(f53(c64,c81),c83),p61(x0,x1)
% 83.18/21.32 === Conflict found: 152:5:6:[110.3,79.2]:TopTopTopTopTopTop: p57(f26(c70,f22(f24(c71,x0),x1)),f22(f24(c71,x2),x3)),p50(f51(c92,f19(f5(c66,x1),x2)),x4),p3(f19(f5(c66,x3),x2),x5) -> p62(f53(c64,x0),x2),p61(x4,x5) {x0 -> c79, x1 -> c80, x2 -> c81, x3 -> c82, x4 -> c77, x5 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 198:4:2:[152.1,81.1]:TopTop: p50(f51(c92,f19(f5(c66,c80),c81)),x0),p3(f19(f5(c66,c82),c81),x1) -> p62(f53(c64,c79),c81),p61(x0,x1)
% 83.18/21.32 === Conflict found: 162:3:2:[142.2,139.1]:TopTop: p25(x0,f26(c70,f22(f24(c71,c81),c82))),p21(f22(f24(c71,c83),c84),x1) -> p57(x0,x1) {x0 -> f26(c70,f22(f24(c71,c79),c80)), x1 -> f22(f24(c71,c83),f10(c72,c73))}
% 83.18/21.32 === Backtracking. Learning clause 199:2:0:[162.3,153.1,142.2]:: p21(f22(f24(c71,c83),c84),f22(f24(c71,c83),f10(c72,c73))),p25(f26(c70,f22(f24(c71,c81),c82)),f26(c70,f22(f24(c71,c79),c80))) ->
% 83.18/21.32 === Backtracking. Learning clause 200:4:4:[61.2,61.3,142.2]:TopTopTopTop: p25(x0,x1),p25(x0,x2),p25(x3,x1) -> p25(x3,x2)
% 83.18/21.32 === Conflict found: 142:2:2:[61.2,23.1]:TopTop: p25(x0,x1) -> p25(x1,x0) {x0 -> f26(c70,c77), x1 -> f26(f30(c85,c77),c77)}
% 83.18/21.32 === Backtracking. Learning clause 201:4:4:[142.2,200.3]:TopTopTopTop: p25(x0,x1),p25(x2,x0),p25(x2,x3) -> p25(x1,x3)
% 83.18/21.32 === Conflict found: 162:3:2:[142.2,139.1]:TopTop: p25(x0,f26(c70,f22(f24(c71,c81),c82))),p21(f22(f24(c71,c83),c84),x1) -> p57(x0,x1) {x0 -> f26(f30(c85,c70),f22(f24(c71,c79),c80)), x1 -> f22(f24(c71,c83),f10(c72,c73))}
% 83.18/21.32 === Backtracking. Learning clause 202:4:2:[162.3,105.1,201.4]:TopTop: p21(f22(f24(c71,c83),c84),f22(f24(c71,c83),f10(c72,c73))),p25(x0,f26(f30(c85,c70),f22(f24(c71,c79),c80))),p25(x1,x0),p25(x1,f26(c70,f22(f24(c71,c81),c82))) ->
% 83.18/21.32 === Clause set with instances from active satisfied. Growing active. New size: 435
% 83.18/21.32 === Restarting.
% 83.18/21.32 === Conflict found: 189:3:1:[187.1,25.1,64.3]:Top: p3(c82,f10(c72,c73)),p20(x0,f24(c71,c81)),p20(x0,f24(c71,c83)) -> {x0 -> f24(c77,c77)}
% 83.18/21.32 === Backtracking. Learning clause 203:4:2:[189.2,102.3,102.3]:TopTop: p3(c82,f10(c72,c73)),p18(x0,c81),p18(x0,c83),p23(x1,c71) ->
% 83.18/21.32 === Conflict found: 130:2:2:[46.2,8.1]:TopTop: p50(x0,x1) -> p50(x1,x0) {x0 -> c77, x1 -> f51(c92,f19(f5(c66,c82),c83))}
% 83.18/21.32 === Backtracking. Learning clause 204:4:2:[130.2,197.1]:TopTop: p50(x0,f51(c92,f19(f5(c66,c82),c83))),p3(f19(f5(c66,c84),c83),x1) -> p62(f53(c64,c81),c83),p61(x0,x1)
% 83.18/21.32 === Backtracking. Learning clause 205:5:4:[58.2,97.3,120.2,185.1]:TopTopTopTop: p18(x0,x1),p4(x2,x3),p3(c84,f19(x2,x0)),p18(x1,c83),p4(x3,f5(c66,f10(c72,c73))) ->
% 83.18/21.32 === Backtracking. Learning clause 206:4:5:[58.2,97.3]:TopTopTopTopTop: p3(f19(x0,x1),x2),p18(x1,x3),p4(x0,x4) -> p3(x2,f19(x4,x3))
% 83.18/21.32 === Backtracking. Learning clause 207:5:6:[58.3,206.1]:TopTopTopTopTopTop: p3(x0,f19(x1,x2)),p3(x0,x3),p18(x2,x4),p4(x1,x5) -> p3(x3,f19(x5,x4))
% 83.18/21.32 === Conflict found: 196:8:7:[76.1,100.3,195.1,101.3]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p25(x4,f26(f30(c85,c70),x3)),p57(x4,f22(x5,x6)),p20(x5,f24(c71,c83)),p3(x6,f10(c72,c73)) -> {x0 -> c70, x1 -> c77, x2 -> c77, x3 -> c77, x4 -> f26(c77,c77), x5 -> c77, x6 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 208:9:8:[196.5,100.3]:TopTopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p57(f26(x4,x5),f22(x6,x7)),p20(x6,f24(c71,c83)),p3(x7,f10(c72,c73)),p16(x4,f30(c85,c70)),p21(x5,x3) ->
% 83.18/21.32 === Backtracking. Learning clause 209:4:5:[46.2,88.3,130.2]:TopTopTopTopTop: p3(x0,x1),p49(x2,x3),p50(x4,f51(x2,x0)) -> p50(x4,f51(x3,x1))
% 83.18/21.32 === Conflict found: 194:7:7:[76.1,100.3,193.1]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p25(f26(f30(c85,x4),x5),f26(f30(c85,c70),x3)),p21(x6,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x4,x5),x6) -> {x0 -> c77, x1 -> f22(c77,c77), x2 -> c77, x3 -> c77, x4 -> c77, x5 -> c77, x6 -> c77}
% 83.18/21.32 === Backtracking. Learning clause 210:8:7:[194.5,100.3]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p21(x4,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x5,x6),x4),p16(f30(c85,x5),f30(c85,c70)),p21(x6,x3) ->
% 83.18/21.32 === Conflict found: 200:4:4:[61.2,61.3,142.2]:TopTopTopTop: p25(x0,x1),p25(x0,x2),p25(x3,x1) -> p25(x3,x2) {x0 -> f26(c70,f22(f24(c71,c77),c77)), x1 -> f26(c70,c77), x2 -> c77, x3 -> f26(c70,f22(f24(c71,c79),c80))}
% 83.18/21.32 === Backtracking. Learning clause 211:9:8:[200.3,100.3,201.4,142.1,201.4,191.1]:TopTopTopTopTopTopTopTop: p16(c70,x0),p21(f22(f24(c71,c79),c80),x1),p25(x2,x3),p25(x4,x2),p25(x4,f26(x0,x1)),p25(x5,x3),p25(x6,x5),p25(x6,x7) -> p57(x7,f22(f24(c71,c81),c82))
% 83.18/21.32 === Backtracking. Learning clause 212:11:10:[76.4,208.5,101.3,26.1]:TopTopTopTopTopTopTopTopTopTop: p25(x0,f26(x1,x2)),p57(x0,f22(x3,x4)),p57(f26(x5,x6),x7),p21(x7,x8),p16(x5,f30(c85,c70)),p21(x6,f22(f24(c71,c79),c80)),p3(x9,f10(c72,c73)),p16(x1,f30(c85,c70)),p21(x2,x8),p20(x3,f24(c71,c83)),p3(x4,x9) ->
% 83.18/21.32 === Conflict found: 212:11:10:[76.4,208.5,101.3,26.1]:TopTopTopTopTopTopTopTopTopTop: p25(x0,f26(x1,x2)),p57(x0,f22(x3,x4)),p57(f26(x5,x6),x7),p21(x7,x8),p16(x5,f30(c85,c70)),p21(x6,f22(f24(c71,c79),c80)),p3(x9,f10(c72,c73)),p16(x1,f30(c85,c70)),p21(x2,x8),p20(x3,f24(c71,c83)),p3(x4,x9) -> {x0 -> f26(f30(c85,c70),c77), x1 -> f30(c85,c70), x2 -> c77, x3 -> c77, x4 -> c77, x5 -> c77, x6 -> f22(f24(c71,c79),c80), x7 -> c77, x8 -> c77, x9 -> f19(f5(c66,c82),c81)}
% 83.18/21.32 === Backtracking. Learning clause 213:9:8:[212.6,25.1,23.1]:TopTopTopTopTopTopTopTop: p57(f26(x0,x1),f22(x2,x3)),p57(f26(x4,f22(f24(c71,c79),c80)),x5),p21(x5,x6),p16(x4,f30(c85,c70)),p3(x7,f10(c72,c73)),p16(x0,f30(c85,c70)),p21(x1,x6),p20(x2,f24(c71,c83)),p3(x3,x7) ->
% 83.18/21.32 === Conflict found: 208:9:8:[196.5,100.3]:TopTopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p57(f26(x4,x5),f22(x6,x7)),p20(x6,f24(c71,c83)),p3(x7,f10(c72,c73)),p16(x4,f30(c85,c70)),p21(x5,x3) -> {x0 -> c70, x1 -> f22(f24(c71,c81),c82), x2 -> f22(f24(c71,c83),c84), x3 -> f22(f24(c71,c83),f10(c72,c73)), x4 -> f30(c85,c70), x5 -> c77, x6 -> f24(c71,c83), x7 -> f10(c72,c73)}
% 83.18/21.32 === Backtracking. Learning clause 214:11:8:[208.1,80.1,76.4,101.3]:TopTopTopTopTopTopTopTop: p16(c70,f30(c85,c70)),p21(f22(f24(c71,c81),c82),f22(f24(c71,c79),c80)),p20(x0,f24(c71,c83)),p3(x1,f10(c72,c73)),p16(x2,f30(c85,c70)),p21(x3,f22(x4,x5)),p25(x6,f26(x2,x3)),p57(x6,x7),p21(x7,f22(x0,x1)),p20(f24(c71,c83),x4),p3(c84,x5) ->
% 83.18/21.32 === Conflict found: 210:8:7:[194.5,100.3]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p21(x4,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x5,x6),x4),p16(f30(c85,x5),f30(c85,c70)),p21(x6,x3) -> {x0 -> c70, x1 -> f22(f24(c71,c79),c80), x2 -> f22(f24(c71,c81),c82), x3 -> f22(f24(c71,c81),c82), x4 -> f22(f24(c71,c83),c84), x5 -> c70, x6 -> f22(f24(c71,c81),c82)}
% 83.18/21.32 === Backtracking. Learning clause 216:1:0:[36.0,215.1,210.1,81.1,80.1,101.3,25.1,25.1,29.1,26.1]:: p16(c70,f30(c85,c70)) ->
% 83.18/21.32 === Conflict found: 210:8:7:[194.5,100.3]:TopTopTopTopTopTopTop: p57(f26(x0,x1),x2),p21(x2,x3),p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p21(x4,f22(f24(c71,c83),f10(c72,c73))),p57(f26(x5,x6),x4),p16(f30(c85,x5),f30(c85,c70)),p21(x6,x3) -> {x0 -> f30(c85,c70), x1 -> c77, x2 -> f22(f24(c71,c77),c77), x3 -> f22(f24(c71,c79),c80), x4 -> f22(c77,c77), x5 -> c70, x6 -> f22(f24(c71,c79),c80)}
% 83.18/21.32 === Backtracking. Learning clause 217:14:13:[210.6,76.4,76.4,25.1,63.3,101.3,100.3]:TopTopTopTopTopTopTopTopTopTopTopTopTop: p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p16(f30(c85,x2),f30(c85,c70)),p25(x3,f26(x2,x4)),p57(x3,x5),p21(x5,f22(x6,x7)),p57(f26(x8,x9),x10),p21(x10,x11),p21(x12,x11),p21(x12,x4),p20(x6,f24(c71,c83)),p3(x7,f10(c72,c73)),p16(x8,x0),p21(x9,x1) ->
% 83.18/21.32 === Conflict found: 217:14:13:[210.6,76.4,76.4,25.1,63.3,101.3,100.3]:TopTopTopTopTopTopTopTopTopTopTopTopTop: p16(x0,f30(c85,c70)),p21(x1,f22(f24(c71,c79),c80)),p16(f30(c85,x2),f30(c85,c70)),p25(x3,f26(x2,x4)),p57(x3,x5),p21(x5,f22(x6,x7)),p57(f26(x8,x9),x10),p21(x10,x11),p21(x12,x11),p21(x12,x4),p20(x6,f24(c71,c83)),p3(x7,f10(c72,c73)),p16(x8,x0),p21(x9,x1) -> {x0 -> f30(c85,c77), x1 -> c77, x2 -> c70, x3 -> c77, x4 -> c77, x5 -> f22(c77,c77), x6 -> c77, x7 -> c77, x8 -> c77, x9 -> c77, x10 -> c77, x11 -> c77, x12 -> f22(f24(c71,c79),c80)}
% 83.18/21.32 === Backtracking. Learning clause 218:11:10:[217.3,29.1,67.3,63.3,25.1]:TopTopTopTopTopTopTopTopTopTop: p21(x0,f22(f24(c71,c79),c80)),p25(x1,f26(c70,x2)),p57(x1,f22(x3,x4)),p57(f26(x5,x6),x7),p21(x7,x2),p20(x3,f24(c71,c83)),p3(x4,f10(c72,c73)),p16(x5,x8),p21(x6,x0),p16(x9,x8),p16(x9,f30(c85,c70)) ->
% 83.18/21.32 === Conflict found: 186:6:5:[76.4,182.1,101.3,170.2,63.3]:TopTopTopTopTop: p25(x0,f26(c70,x1)),p57(x0,f22(x2,x3)),p20(x2,f24(c71,c83)),p3(x3,f10(c72,c73)),p21(x4,f22(f24(c71,c81),c82)),p21(x4,x1) -> {x0 -> f26(c70,f22(f24(c71,c81),c82)), x1 -> f22(f24(c71,c81),c82), x2 -> f24(c71,c83), x3 -> c84, x4 -> f22(f24(c71,c81),c82)}
% 83.18/21.32
% 83.18/21.32 SZS status Unsatisfiable
% 83.18/21.32
% 83.18/21.32 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.18/21.32
% 83.18/21.32 SPASS-SCL-FOL Statistics:
% 83.18/21.32 Number of learned clauses: 99
% 83.18/21.32 Number of propagations: 7145
% 83.18/21.32 Number of decisions: 4055
% 83.18/21.32 Number of resolutions: 156
% 83.18/21.32 Number of condensations: 1
% 83.18/21.32 Number of sub resolutions: 1
% 83.18/21.32 Number of input literals (deduplicated): 118
% 83.18/21.32 Number of grows: 6
% 83.18/21.32 Number of considered ground atoms: 435
% 83.18/21.32
% 83.18/21.32 Needed: 0:0:20.70
% 83.18/21.32
%------------------------------------------------------------------------------