%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN421+1 : TPTP v9.2.1. Released v2.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:39:46 PM UTC 2026 % Result : CounterSatisfiable 16.54s 4.63s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SYN421+1 : TPTP v9.2.1. Released v2.1.0. % 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.35 % Computer : n025.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Thu May 7 13:41:59 EDT 2026 % 0.16/0.35 % CPUTime : % 0.16/0.35 SPASS-SCL-FOL version: % 0.18/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 16.54/4.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.62 Execution lmodel_grow ended with status: satisfiable % 16.54/4.62 Used heuristic: lmodel_grow % 16.54/4.62 % 16.54/4.62 Input Clauses: % 16.54/4.63 % 16.54/4.63 Predicates: ndr1_0 c3_1 c8_1 ndr1_1 c9_2 c4_2 c8_2 c6_2 c5_1 c1_1 c6_0 c9_0 c2_0 c7_2 c2_2 c1_2 c7_0 c4_0 c4_1 c9_1 c2_1 c10_2 c10_1 c3_2 c7_1 c6_1 c1_0 c3_0 c5_0 c5_2 c10_0 c8_0 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 % 16.54/4.63 Fol Constants: a449 a450 a451 a452 a453 a454 a455 a456 a457 a458 a459 a460 a461 a462 a463 a464 a465 a466 a467 a468 a469 a470 a471 a472 a473 a474 a475 a476 a477 a478 a479 a480 a481 a482 a483 a484 a485 a486 a487 a488 a489 a490 a491 a492 a493 a494 a495 a496 a497 a498 a499 a500 a501 a502 a503 a504 a505 a506 a507 a508 a509 a510 a511 a512 a513 a514 a515 a516 a517 a518 a519 a520 a521 a522 a523 a524 a525 a526 a527 a528 a529 a530 a531 a532 a533 a534 a535 a536 a537 a538 a539 a540 a541 a542 a543 a544 a545 a546 a547 a548 a549 a550 a551 a552 a553 a554 a555 a556 a557 a558 a559 a560 a561 a562 a563 a564 a565 a566 a567 a568 a569 a570 a571 a572 a573 a574 a575 a576 a577 a578 a579 a580 a581 a582 a583 a584 a585 a586 a587 a588 a589 a590 a591 a592 a593 a594 a595 a596 a597 a598 a599 a600 a601 a602 a603 a604 a605 a606 a607 % 16.54/4.63 Fol Functions: % 16.54/4.63 Problem Properties: % 16.54/4.63 This is a Bernays Schoenfinkel problem. % 16.54/4.63 % 16.54/4.63 After reduction: Problem Properties: % 16.54/4.63 This is a Bernays Schoenfinkel problem. % 16.54/4.63 % 16.54/4.63 % 16.54/4.63 Reduced Input Clauses: % 16.54/4.63 662:4:1:[116.1,115.1]:Top: ren24,c7_2(a481,x0),c3_2(a481,x0),c5_2(a481,x0) -> % 16.54/4.63 663:3:1:[127.1,125.1]:Top: ren25,c5_2(a484,x0) -> c7_2(a484,x0) % 16.54/4.63 664:3:1:[127.1,126.1]:Top: ren25 -> c10_2(a484,x0),c8_2(a484,x0) % 16.54/4.63 665:4:1:[149.1,153.1]:Top: ren30,c4_2(a491,x0),c9_2(a491,x0) -> c10_2(a491,x0) % 16.54/4.63 666:4:1:[195.1,194.1]:Top: ren38,c9_2(a504,x0) -> c1_2(a504,x0),c7_2(a504,x0) % 16.54/4.63 667:4:1:[234.1,238.1]:Top: ren47,c10_2(a515,x0),c1_2(a515,x0) -> c5_2(a515,x0) % 16.54/4.63 668:3:1:[242.1,240.1]:Top: ren48,c10_2(a517,x0) -> c4_2(a517,x0) % 16.54/4.63 669:4:1:[319.1,318.1]:Top: ren63,c2_2(a538,x0) -> c10_2(a538,x0),c9_2(a538,x0) % 16.54/4.63 670:4:1:[402.1,401.1]:Top: ren82,c8_2(a560,x0) -> c10_2(a560,x0),c3_2(a560,x0) % 16.54/4.63 671:3:1:[406.1,410.1]:Top: ren83 -> c9_2(a562,x0),c6_2(a562,x0) % 16.54/4.63 672:4:1:[527.1,532.1]:Top: ren108,c1_2(a597,x0),c3_2(a597,x0) -> c7_2(a597,x0) % 16.54/4.63 673:4:1:[546.1,544.1]:Top: ren111,c2_2(a602,x0),c4_2(a602,x0) -> c7_2(a602,x0) % 16.54/4.63 674:2:0:[607.0,627.0]:: c3_0 -> c4_0 % 16.54/4.63 675:2:0:[582.0,648.1]:: c8_0 -> ren97 % 16.54/4.63 % 16.54/4.63 Most General Atoms: ren1 ndr1_0 ren2(x0) ren3(x0) ren4(x0) ren5(x0) ren6 ren7 ren8(x0) ren9 ren10(x0) ren11 ren12(x0) ren13 ren14 c2_0 c10_1(x0) c10_0 ren15 ren16 ren17 ren18 ren19 ren20(x0) ren21 ren22 ren23 c7_0 c5_1(x1) ren24 c9_0 c4_0 ren25 ren26(x0) ren27(x0) ren28 ren29 ren30 ren31 ren32 ren33(x0) ren36 ren113 c1_1(x0) ren37 ren38 ren39(x0) ren42 ren43(x0) ren44(x0) ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53(x0) ren54(x0) ren56(x0) ren57(x0) ren58(x0) ren59(x0) ren60 ren110 ren111 ren112(x0) ren61(x0) ren62 ren63 ren108 ren109 ren64 ren65(x0) ren66(x0) ren67(x0) ren69(x0) ren70 ren71(x0) ren72 ren73 ren74 ren75(x0) ren76 ren77(x0) ren78 ren79(x0) ren80(x0) ren82 ren83 ren86 ren87(x0) ren88(x0) ren89 ren90 ren91 c1_0 ren107 ren92(x0) ren93 ren94 ren95 ren96(x0) ren97 ren98 ren99 ren100 ren101 c9_1(x0) ren104(x0) ren105 ren102(x0) ren106(x0) c3_0 ren103(x2) ren114(x0) c6_0 c3_1(x0) c5_0 c7_2(x0,x2) c8_1(x0) c8_0 ren34(x1) ren35(x1) c8_2(x1,x2) ndr1_1(x2) c6_2(x2,x3) ren40(x2) ren41(x2) c9_2(x0,x2) c2_1(x1) ren55(x1) ren68(x1) c3_2(x2,x4) c2_2(x2,x3) c4_2(x2,x4) c1_2(x2,x4) ren81(x3) c7_1(x3) c10_2(x0,x2) ren84(x3) ren85(x3) c5_2(x1,x2) c4_1(x1) c6_1(x1) % 16.54/4.63 % 16.54/4.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 651 atoms initially, heuristics mode: lmodel_grow === % 16.54/4.63 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 681 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 701 % 16.54/4.63 === Backtracking. Learning clause 676:6:1:[644.5,446.1]:Top: c4_0,ndr1_0,c6_1(x0),c8_1(x0) -> c2_0,ndr1_1(x0) % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 729 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 750 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 771 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 789 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 800 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 816 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 828 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 854 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 875 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 913 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 943 % 16.54/4.63 === Backtracking. Learning clause 679:8:2:[346.1,677.4,349.1,678.8,660.9,348.2]:TopTop: c6_1(x0),c7_1(x0),c7_0,ndr1_0,c5_1(x1),ren69(x1) -> c2_1(x0),ren114(x1) % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 964 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 983 % 16.54/4.63 === Backtracking. Learning clause 681:10:2:[221.1,680.0,653.2,223.2,503.1,676.4]:TopTop: c3_2(x0,a512),ren44(x0),c4_0,ndr1_0,c6_1(x1) -> c3_0,ren102(x0),c10_1(x0),c2_0,ndr1_1(x1) % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1010 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1030 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1059 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1071 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1081 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1093 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1099 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1103 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1108 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1120 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1130 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1135 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1144 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1148 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1152 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1155 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1160 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1163 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1167 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1178 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1185 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1197 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1207 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1213 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1217 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1221 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1225 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1228 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1231 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1233 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1240 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1244 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1247 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1254 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1259 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1263 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1267 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1270 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1272 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1276 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1277 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1281 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1284 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1286 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1293 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1296 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1299 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1302 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1306 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1309 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1312 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1315 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1318 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1320 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1327 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1331 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1335 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1339 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1342 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1346 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1350 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1353 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1357 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1361 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1363 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1367 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1370 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1374 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1376 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1384 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1387 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1390 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1393 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1395 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1399 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1402 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1409 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1415 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1421 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1423 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1430 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1437 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1440 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1443 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1450 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1454 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1465 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1470 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1472 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1474 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1484 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1491 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1503 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1527 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1545 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1559 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1574 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1590 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1608 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1614 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1621 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1623 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1630 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1633 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1637 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1640 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1643 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1646 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1653 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1655 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1663 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1666 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1670 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1677 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1680 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1685 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1688 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1692 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1695 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1702 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1708 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1717 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1721 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1729 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1735 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1744 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1749 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1752 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1756 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1759 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1763 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1765 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1772 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1775 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1778 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1780 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1784 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1787 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1794 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1798 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1806 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1809 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1816 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1821 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1824 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1828 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1830 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1837 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1839 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1847 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1850 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1853 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1856 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1859 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1862 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1865 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1872 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1876 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1879 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1882 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1885 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1887 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1891 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1895 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1897 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1904 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1907 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1911 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1914 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1917 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1924 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1928 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1931 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1934 % 16.54/4.63 === Clause set with instances from active satisfied. Growing active. New size: 1935 % 16.54/4.63 % 16.54/4.63 Linear Model Building succeeded. % 16.54/4.63 SZS status Satisfiable % 16.54/4.63 % 16.54/4.63 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 16.54/4.63 % 16.54/4.63 SPASS-SCL-FOL Statistics: % 16.54/4.63 Number of learned clauses: 3 % 16.54/4.63 Number of propagations: 668 % 16.54/4.63 Number of decisions: 1802 % 16.54/4.63 Number of resolutions: 5 % 16.54/4.63 Number of condensations: 0 % 16.54/4.63 Number of sub resolutions: 17 % 16.54/4.63 Number of input literals (deduplicated): 651 % 16.54/4.63 Number of grows: 190 % 16.54/4.63 Number of considered ground atoms: 1935 % 16.54/4.63 % 16.54/4.63 Needed: 0:00:04.04 % 16.54/4.63 %------------------------------------------------------------------------------