nohup: ignoring input 10pipe_k.cnf 13pipe_k.cnf 14pipe_q0_k.cnf 20-100-frag12-0_sat.cnf 20-100-frag12-14_sat.cnf 20-100-frag12-32_sat.cnf 20-100-frag12-53_sat.cnf 20-100-lambda100-14_sat.cnf 20-100-lambda100-14_unsat.cnf 20-100-lambda100-47_unsat.cnf 20-100-lambda100-49_sat.cnf 20-100-lambda100-65_sat.cnf 20-100-lambda100-89_sat.cnf 20-100-lambda100-89_unsat.cnf 20-100-p100-55_sat.cnf 20-100-p100-55_unsat.cnf 2bitcomp_5.hg_20.cnf 51.smt2.cnf 73.smt2.cnf 9dlx_vliw_at_b_iq5.cnf 9dlx_vliw_at_b_iq8.cnf ACG-15-10p1.cnf ak016modbtsimpbisc.cnf ak032modbtmodbtisc.cnf ak128paralparalisc.cnf assoc_mult_err_3.c.cnf at-least-two-aaai10-planning-ipc5-pathways-17-step20.cnf at-least-two-aaai10-planning-ipc5-pipesworld-12-step15.cnf at-least-two-hwmcc10-timeframe-expansion-k50-pdtviseisenberg2-tseitin.cnf at-least-two-ibm-2004-23-k100.cnf at-least-two-maris-s03-gripper11.cnf at-least-two-smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf at-least-two-sokoban-sequential-p145-microban-sequential.030-NOTKNOWN.cnf at-least-two-traffic_b_unsat.cnf at-least-two-traffic_f_unknown.cnf at-least-two-traffic_kkb_unknown.cnf at-least-two-traffic_pcb_unknown.cnf vmpc_26.cnf at-least-two-vmpc_28.cnf b04_s_unknown_pre.cnf b2005-p3-12x12c10h7-Ser7-0.cnf barman-pfile10-039.sas.ex.15.cnf barman-pfile10-040.sas.ex.15.cnf battleship-12-12-unsat.cnf battleship-14-26-sat.cnf blocks-blocks-36-0.180-SAT.cnf blocks-blocks-37-1.120-NOTKNOWN.cnf blocks-blocks-37-1.130-NOTKNOWN.cnf bvsdiv_19.smt2.cnf bvsmod_18.smt2.cnf bvsmod_19.smt2.cnf bvsub_08985.smt2.cnf bvsub_12973.smt2.cnf bvsub_19952.smt2.cnf bv-term-small-rw_1492.smt2.cnf bvurem_20.smt2.cnf Circuit_multiplier18.cnf Circuit_multiplier22.cnf Circuit_multiplier24.cnf Circuit_multiplier25.cnf Circuit_multiplier26.cnf Circuit_multiplier29.cnf Circuit_multiplier33.cnf Circuit_multiplier34.cnf Circuit_multiplier35.cnf Circuit_multiplier36.cnf Circuit_multiplier37.cnf Circuit_multiplier45.cnf Circuit_multiplier53.cnf crafted_n10_d6_c4_num15.cnf crafted_n10_d6_c4_num21.cnf crafted_n11_d6_c4_num14.cnf crafted_n12_d6_c3_num18.cnf crafted_n12_d6_c3_num28.cnf crafted_n12_d6_c4_num17.cnf ctl_4201_555_unsat.cnf ctl_4291_567_1_unsat.cnf ctl_4291_567_11_unsat.cnf ctl_4291_567_6_unsat_pre.cnf ctl_4291_567_9_unsat.cnf dist10.c.cnf dist4.c.cnf E00X23.cnf E02F17.cnf ecarev-110-1031-23-40-8.cnf ecarev-110-4099-22-30-4.cnf edit_distance007_85.cnf edit_distance019_312.cnf edit_distance023_281.cnf edit_distance023_282.cnf edit_distance023_283.cnf edit_distance025_448.cnf edit_distance025_449.cnf edit_distance025_450.cnf edit_distance031_283.cnf edit_distance031_284.cnf edit_distance035_393.cnf edit_distance041_182.cnf edit_distance041_183.cnf ER_500_40_2.apx_0.cnf erin2_0x0_n207-379.cnf erin2_0x0-379.cnf erin2_0x1e3-216.cnf ex045_7.cnf ex065_25.cnf ex095_8.cnf ex175_20.cnf HCP-424-60.cnf HCP-446-105.cnf HCP-446-420.cnf HCP-446-60.cnf HCP-470-105.cnf HCP-470-420.cnf HCP-470-60.cnf HCP-506-60.cnf HCP-522-105.cnf HCP-526-105.cnf HCP-526-420.cnf HCP-529-420.cnf HCP-529-60.cnf huck.col.11.cnf IBM_FV_2004_rule_batch_30_SAT_dat.k75.cnf k2fix_gr_rcs_w8.shuffled.cnf Kakuro-easy-045-ext.xml.hg_4.cnf Kakuro-easy-051-ext.xml.hg_4.cnf Kakuro-easy-089-ext.xml.hg_4.cnf Kakuro-easy-104-ext.xml.hg_6.cnf Kakuro-easy-112-ext.xml.hg_7.cnf Kakuro-easy-115-ext.xml.hg_5.cnf Kakuro-easy-118-ext.xml.hg_4.cnf Kakuro-easy-127-ext.xml.hg_7.cnf Kakuro-easy-132-ext.xml.hg_8.cnf Kakuro-easy-142-ext.xml.hg_8.cnf Kakuro-easy-150-ext.xml.hg_9.cnf Kakuro-easy-156-ext.xml.hg_7.cnf ktf_TF-1.tf_4_0.06_101.cnf ktf_TF-3.tf_2_0.02_24.cnf ktf_TF-3.tf_3_0.02_24.cnf ktf_TF-4.tf_2_0.02_18.cnf ktf_TF-4.tf_4_0.04_35.cnf ktf_TF-4.tf_4_0.06_52.cnf ktf_TF-6.tf_4_0.06_77.cnf ktf_TF-7.tf_3_0.06_113.cnf ktf_TF-8.tf_4_0.06_109.cnf LABS_n041_goal003.cnf LABS_n068_goal001.cnf LABS_n069_goal001.cnf LABS_n072_goal006.cnf LABS_n089_goal008.cnf maximum_constrained_partition_14_bits_n200.cnf maximum_constrained_partition_18_bits_n200.cnf maxor128.cnf mp1-blockpuzzle_5x10_s5_free3.cnf mp1-blockpuzzle_5x12_s6_free3.cnf mp1-blockpuzzle_9x9_s1_free8.cnf mp1-blockpuzzle_9x9_s5_free3.cnf mp1-bsat00_322_20.cnf rbsat-v760c43649g8.cnf schur-triples-7-60.cnf schur-triples-7-90.cnf sgp_5-6-8.sat05-2669.reshuffled-07.cnf size_5_5_5_i003_r12.cnf size_5_5_5_i019_r12.cnf size_5_5_5_i041_r12.cnf size_5_5_5_i053_r12.cnf size_5_5_5_i058_r12.cnf size_5_5_5_i059_r12.cnf size_5_5_5_i092_r12.cnf size_5_5_5_i131_r12.cnf size_5_5_5_i235_r12.cnf size_5_5_5_i260_r12.cnf sqrt_ineq_3.c.cnf ssAES_4-4-8_round_7-10_faultAt_8_fault_injections_2_seed_1579630418.cnf ssAES_4-4-8_round_8-10_faultAt_8_fault_injections_2_seed_1579630418.cnf ssAES_4-4-8_round_8-10_faultAt_8_fault_injections_2_seed_31944661.cnf ssp-0.046166496845693274.cnf ssp-0.497665446947731.cnf stable-300-0.1-20-98765432130020.cnf sted1_0x0_n438-636.cnf sted1_0x0-649.cnf sted2_0x0_n219-342.cnf sted3_0x1e3-147.cnf sted4_0x1e3-124.cnf sted5_0x0-157.cnf sted6_0x0-135.cnf Steiner-135-32-bce.cnf Steiner-243-45-bce.cnf sv-comp19_prop-reachsafety.queue_longer_false-unreach-call.i-witness.cnf Timetable_C_241_E_45_Cl_16_S_16.cnf Timetable_C_392_E_50_Cl_26_S_26.cnf Timetable_C_392_E_50_Cl_26_S_28.cnf Timetable_C_392_E_62_Cl_26_S_28.cnf Timetable_C_437_E_62_Cl_29_S_28.cnf Timetable_C_466_E_50_Cl_31_S_28.cnf Timetable_C_497_E_62_Cl_33_S_30.cnf TT7F-33-24A.cnf TT7F-33-24B.cnf TT7F-33-24C.cnf TT7F-33-24D.cnf TT7F-33-24E.cnf TT7F-33-25.cnf TT7F-33-26.cnf unsat-set-a-clqcolor-16-10-11.sat05-1253.reshuffled-07.cnf vlsat2_16676_1598591.dimacs.cnf vlsat2_24450_2770239.dimacs.cnf vlsat2_30744_3925645.dimacs.cnf vlsat2_34161_4607712.dimacs.cnf vlsat2_37758_5364539.dimacs.cnf vlsat2_40170_5970608.dimacs.cnf vlsat2_57038_10572502.dimacs.cnf 22930-0426-195.smt2.cnf 22930-0601-11.smt2.cnf 3bitadd_32.cnf.gz.CP3-cnfmiter.cnf 6s153.cnf 6s20.cnf abw-I-ash85.mtx-w24.cnf abw-I-ash85.mtx-w25.cnf abw-K-dwt__234.mtx-w55.cnf abw-N-bcsstk07.mtx-w44.cnf abw-Q-494_bus.mtx-w242.cnf baseballcover12with22_and2positions.cnf baseballcover12with25_and5positions.cnf baseballcover13with25_and3positions.cnf baseballcover14with25.cnf baseballcover14with25_and1positions.cnf baseballcover14with25_and2positions.cnf baseballcover15with25.cnf beempgsol5b1.cnf bivium-39-200-0s0-0x5fa955de2b4f64d00226837d226c955de4566ce95f660180d7-30.cnf bivium-40-200-0s0-0x92fc13b11169afbb2ef11a684d9fe9a19e743cd6aa5ce23fb5-19.cnf bv-term-small-rw_1159.smt2.cnf bv-term-small-rw_503.smt2.cnf bv-term-small-rw_848.smt2.cnf ccp-s8-facto4.cnf contest03-SGI_30_50_30_20_3-dir.sat05-440.reshuffled-07.cnf crafted_n10_d6_c3_num18.cnf crafted_n11_d6_c4_num19.cnf crafted_n12_d6_c4_num9.cnf ctl_429sp4-33-one-nons-flat-noid.cnf sp4-33-one-stri-tree-noid.cnf sp4-33-una-stri-flat-noid.cnf sp5-21-15-bin-stri-flat-noid.cnf sp5-21-15-bin-stri-tree-noid.cnf sp5-21-15-one-nons-tree-noid.cnf sp5-21-15-one-stri-tree-noid.cnf sp5-21-15-una-nons-tree-noid.cnf sp5-21-15-una-stri-flat-noid.cnf sp5-26-19-bin-nons-tree-noid.cnf sp5-26-19-bin-stri-flat-noid.cnf sp5-26-19-una-nons-tree-noid.cnf spg_200_300.cnf spg_200_301.cnf spg_200_307.cnf spg_200_316.cnf spg_200_317.cnf spg_200_321.cnf spg_300_300.cnf spg_300_301.cnf spg_300_312.cnf spg_330_400.cnf spg_400_281.cnf spg_420_280.cnf spg_420_350.cnf stb_531_83.apx_0.cnf stb_792_333.apx_0.cnf sted1_0x0-637.cnf sted1_0x1e3-393.cnf sted12a_0x1e1-67.cnf sted2_0x0-343.cnf sted2_0x1e3-216.cnf sted3_0x0_n201-239.cnf sted4_0x0_n159-185.cnf sted5_0x0_n90-157.cnf sted5_0x1e3-120.cnf sted5_0x1e3-20.cnf sted6_0x1e3-97.cnf string_compare_safety_cbmc_unwinding_600.cnf string_compare_safety_cbmc_unwinding_630.cnf string_compare_safety_cbmc_unwinding_670.cnf string_compare_safety_cbmc_unwinding_680.cnf string_compare_safety_cbmc_unwinding_690.cnf string_compare_safety_cbmc_unwinding_700.cnf string_compare_safety_cbmc_unwinding_730.cnf string_compare_safety_cbmc_unwinding_780.cnf string_compare_safety_cbmc_unwinding_800.cnf string_compare_safety_cbmc_unwinding_870.cnf string_compare_safety_cbmc_unwinding_900.cnf string_compare_safety_cbmc_unwinding_930.cnf string_compare_safety_cbmc_unwinding_940.cnf sum_of_3_cubes_37_bits_87.cnf sum_of_3_cubes_42_bits_96.cnf sum_of_3_cubes_50_bits_91.cnf sum_of_3_cubes_51_bits_80.cnf sum_of_3_cubes_52_bits_39mp1-rubikcube312.cnf mp1-squ_any_s09x07_c27_bail_UNS.cnf Nb51T6-sc2018.cnf ncc_none_12477_5_3_3_0_0_435991723.cnf ncc_none_2_17_4_3_0_0_435991723.cnf ncc_none_2_18_9_3_0_0_435991723.cnf ncc_none_21015_5_3_3_0_0_11.cnf ncc_none_3_16_3_3_0_0_435991723.cnf ncc_none_5047_6_3_3_0_0_41.cnf ncc_none_7047_6_3_3_0_0_420.cnf newpol29-4.cnf newpol34-4.cnf newpol36-4.cnf newpol4-6.cnf newpol6-6.cnf newpol6-7.cnf newpol7-6.cnf post-cbmc-aes-ee-r2.cnf problem_19.smt2.cnf problem_21.smt2.cnf problem_23.smt2.cnf ps_200_300_70.cnf ps_200_301_70.cnf ps_200_305_70.cnf ps_200_306_70.cnf ps_200_316_70.cnf ps_200_317_70.cnf ps_200_323_70.cnf QG7a-gensys-ukn009.sat05-3849.reshuffled-07.cnf rbcl_xits_08_UNSAT.cnf rook-42-0-1.cnf rphp4_090_shuffled.cnf SAT_dat.k80.cnf schup-l2s-bc56s-1-k391.cnf sgen4-unsat-89-1.cnf SGI_30_70_20_60_10-dir.shuffled-as.sat03-144.cnf simon03:sat02bis:k2fix_gr_2pinvar_w8.used-as.sat04-349.cnf simon-mixed-s02bis-05.cnf size_4_4_4_i4096_r8.cnf size_4_5_5_i000_w31_r9.cnf size_4_5_5_i003_w31_r9.cnf size_4_5_5_i028_w31_r9.cnf size_4_5_5_i031_w31_r9.cnf size_4_5_5_i032_w31_r9.cnf size_4_5_5_i035_w31_r9.cnf size_4_5_5_i037_w31_r9.cnf SocialGolfers-6-6-6-cp_c18.cnf Steiner-15-7-bce.cnf Steiner-27-10-bce.cnf Steiner-45-16-bce.cnf Steiner-9-5-bce.cnf sv-comp19_prop-reachsafety.newton_2_2_true-unreach-call_true-termination.i-witness.cnf traffic_kkb_unknown.cnf tseitingrid7x165_shuffled.cnf tseitingrid7x185_shuffled.cnf uum12.smt2.cnf VanDerWaerden_pd_2-3-26_635.cnf velev-dlx-uns-1.0-05.cnf velev-pipe-uns-1.0-9.cnf w15.cnf w16-5.cnf w16-6a.cnf w19-2.0.cnf w19-20.0.cnf w19-20.1.cnf w19-49.0.cnf w19-5.1.cnf w19-8.0.cnf real 4m28.224s user 142m31.949s sys 0m6.455s real 4m25.993s user 141m25.341s sys 0m5.995s real 4m12.815s user 134m15.685s sys 0m6.587s real 4m8.870s user 132m20.894s sys 0m5.232s