%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP019_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n029.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 : Tue May 5 07:12:53 PM UTC 2026 % Result : Theorem 0.48s 0.64s % Output : Refutation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP019_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : run_ksp %s % 0.17/0.34 % Computer : n029.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Mon May 4 16:09:44 EDT 2026 % 0.17/0.34 % CPUTime : % 0.36/0.61 ----KSP format--- % 0.36/0.61 usable(formulas). % 0.36/0.61 true. % 0.36/0.61 end_of_list. % 0.36/0.61 sos(formulas). % 0.36/0.61 ~ ([] ( p1 ) | [] ( p2 ) | [] ( p3 ) | [] ( p5 ) | <> ( ~ ( p1 ) & [] ( p3 ) ) | <> ( ~ ( p1 ) & [] ( p5 ) ) | $false | <> ( ~ ( p2 ) & [] ( p1 ) ) | $false | <> ( ~ ( p3 ) & [] ( p3 ) ) | <> ( ~ ( p3 ) & [] ( p5 ) ) | $false | $false | $false | <> ( ~ ( p5 ) & [] ( p3 ) ) | <> ( ~ ( p5 ) & [] ( p5 ) ) | $false | $false | $false | <> ( <> ( ~ ( p1 ) & [] ( p1 ) ) ) | <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) | <> ( <> ( ~ ( p1 ) & [] ( p6 ) ) ) | <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) | $false | $false | <> ( ~ ( p4 ) & [] ( p2 ) ) | <> ( ~ ( p6 ) & [] ( p2 ) ) | <> ( <> ( ~ ( p3 ) & [] ( p1 ) ) ) | <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) | <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) | $false | $false | <> ( ~ ( p4 ) & [] ( p4 ) ) | <> ( ~ ( p6 ) & [] ( p4 ) ) | <> ( <> ( ~ ( p5 ) & [] ( p1 ) ) ) | <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) | <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) | $false | $false | <> ( ~ ( p4 ) & [] ( p6 ) ) | <> ( ~ ( p6 ) & [] ( p6 ) ) | <> ( <> ( <> ( ~ ( p1 ) & [] ( p1 ) ) ) ) | <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) | $false | $false | <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) | <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) | <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) | <> ( <> ( <> ( ~ ( p3 ) & [] ( p1 ) ) ) ) | <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) | $false | $false | <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) | <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) | <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) | <> ( <> ( <> ( ~ ( p5 ) & [] ( p1 ) ) ) ) | <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) | $false | <> ( <> ( <> ( ~ ( p6 ) & [] ( p5 ) ) ) ) | <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) | <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) | <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) | <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p1 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) | $false | $false | <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) | <> ( <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p1 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) | $false | $false | <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) | <> ( <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p1 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p4 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) | $false | $false | <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) | <> ( <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) ) | $false | <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p1 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) ) ) | <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p1 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p4 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p1 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p1 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) ) ) ) | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p1 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p1 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p4 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p1 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p1 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p3 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) & [] ( p5 ) ) ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p3 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p3 ) & [] ( p5 ) ) ) ) ) ) ) ) ) ) | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p1 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p3 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p5 ) & [] ( p5 ) ) ) ) ) ) ) ) ) ) | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p1 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) ) ) ) ) ) ) ) ) ) ) ). % 0.36/0.61 end_of_list. % 0.36/0.61 ----------------- % 0.36/0.61 ksp -tstp -pproof -early_ple -mlple -ord -snf++ -unit -lhs_unit -fsub -bsub -limited_reuse_renaming -bnfsimp -maxproof 1 -populate_max_lit_positive -short -global2local -i /export/starexec/sandbox/tmp/tmp.Gm7WKtaIrb/theBenchmark.ksp % 0.48/0.64 % 0.48/0.64 % SZS status Theorem % 0.48/0.64 % 0.48/0.64 ***************** % 0.48/0.64 FOUND PROOF 1 % 0.48/0.64 ***************** % 0.48/0.64 % SZS output start Refutation % 0.48/0.64 % 0.48/0.64 (1,1) [1,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.48/0.64 (1,1) [41,0]. _t0 => box 1 _t32 [ SNF ] [ Backward Subsumption, 1414 ] % 0.48/0.64 (1,1) [52,0]. _t0 => box 1 _t42 [ SNF ] [ Backward Subsumption, 1413 ] % 0.48/0.64 (1,1) [327,0]. _t0 => box 1 _t223 [ SNF ] [ Backward Subsumption, 1400 ] % 0.48/0.64 (1,1) [363,0]. _t0 => box 1 _t44 [ SNF ] [ Backward Subsumption, 1396 ] % 0.48/0.64 (1,1) [582,0]. _t0 => box 1 _t225 [ SNF ] [ Backward Subsumption, 1383 ] % 0.48/0.64 (1,1) [610,0]. _t0 => box 1 _t46 [ SNF ] [ Backward Subsumption, 1379 ] % 0.48/0.64 (1,1) [725,0]. _t0 => box 1 _t241 [ SNF ] [ Backward Subsumption, 1372 ] % 0.48/0.64 (1,1) [808,0]. _t0 => box 1 _t246 [ SNF ] [ Backward Subsumption, 1362 ] % 0.48/0.64 (1,1) [900,0]. _t0 => box 1 _t250 [ SNF ] [ Backward Subsumption, 1349 ] % 0.48/0.64 (1,1) [937,0]. _t0 => box 1 _t253 [ SNF ] [ Backward Subsumption, 1341 ] % 0.48/0.64 (289,1) [944,0]. _t0 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 1336 ] % 0.48/0.64 (289,1) [1336,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 1, 944, _t0 ] [ SNF++, 2247, ~p2 ] % 0.48/0.64 (1,1) [1341,0]. true => box 1 _t253 [ LHS Unit Resolution, 1, 937, _t0 ] [ SNF++, 2237, _t253 ] % 0.48/0.64 (1,1) [1349,0]. true => box 1 _t250 [ LHS Unit Resolution, 1, 900, _t0 ] [ SNF++, 2221, _t250 ] % 0.48/0.64 (1,1) [1362,0]. true => box 1 _t246 [ LHS Unit Resolution, 1, 808, _t0 ] [ SNF++, 2195, _t246 ] % 0.48/0.64 (1,1) [1372,0]. true => box 1 _t241 [ LHS Unit Resolution, 1, 725, _t0 ] [ SNF++, 2175, _t241 ] % 0.48/0.64 (1,1) [1379,0]. true => box 1 _t46 [ LHS Unit Resolution, 1, 610, _t0 ] [ SNF++, 2161, _t46 ] % 0.48/0.64 (1,1) [1383,0]. true => box 1 _t225 [ LHS Unit Resolution, 1, 582, _t0 ] [ SNF++, 2153, _t225 ] % 0.48/0.64 (1,1) [1396,0]. true => box 1 _t44 [ LHS Unit Resolution, 1, 363, _t0 ] [ SNF++, 2127, _t44 ] % 0.48/0.64 (1,1) [1400,0]. true => box 1 _t223 [ LHS Unit Resolution, 1, 327, _t0 ] [ SNF++, 2119, _t223 ] % 0.48/0.64 (1,1) [1413,0]. true => box 1 _t42 [ LHS Unit Resolution, 1, 52, _t0 ] [ SNF++, 2093, _t42 ] % 0.48/0.64 (1,1) [1414,0]. true => box 1 _t32 [ LHS Unit Resolution, 1, 41, _t0 ] [ SNF++, 2091, _t32 ] % 0.48/0.64 (1,1) [2091,0]. true => box 1 _t359 [ SNF++, 1414 ] % 0.48/0.64 (1,1) [2093,0]. true => box 1 _t360 [ SNF++, 1413 ] % 0.48/0.64 (1,1) [2119,0]. true => box 1 _t369 [ SNF++, 1400 ] % 0.48/0.64 (1,1) [2127,0]. true => box 1 _t330 [ SNF++, 1396 ] % 0.48/0.64 (1,1) [2153,0]. true => box 1 _t339 [ SNF++, 1383 ] % 0.48/0.64 (1,1) [2161,0]. true => box 1 _t305 [ SNF++, 1379 ] % 0.48/0.64 (1,1) [2175,0]. true => box 1 _t371 [ SNF++, 1372 ] % 0.48/0.64 (1,1) [2195,0]. true => box 1 _t372 [ SNF++, 1362 ] % 0.48/0.64 (1,1) [2221,0]. true => box 1 _t373 [ SNF++, 1349 ] % 0.48/0.64 (1,1) [2237,0]. true => box 1 _t374 [ SNF++, 1341 ] % 0.48/0.64 (289,1) [2247,0]. true => ~box 1~ _t375 [ SNF++, 1336 ] % 0.48/0.64 (289,1) [2416,0]. true => false [ GEN1, 2237, 2195, 2119, 2091, 2127, 2161, 2153, 2093, 2175, 2221, 2247, 2415, _t374, _t372, _t369, _t359, _t330, _t305, _t339, _t360, _t371, _t373, _t375 ] % 0.48/0.64 (1,1) [40,1]. _t32 => box 1 _t33 [ SNF ] [ SNF++, 1947, _t33 ] % 0.48/0.64 (1,1) [51,1]. _t42 => box 1 _t43 [ SNF ] [ SNF++, 1949, _t43 ] % 0.48/0.64 (1,1) [326,1]. _t223 => box 1 _t224 [ SNF ] [ SNF++, 1975, _t224 ] % 0.48/0.64 (1,1) [362,1]. _t44 => box 1 _t45 [ SNF ] [ SNF++, 1983, _t45 ] % 0.48/0.64 (1,1) [581,1]. _t225 => box 1 _t226 [ SNF ] [ SNF++, 2009, _t226 ] % 0.48/0.64 (1,1) [609,1]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 2017, _t47 ] % 0.48/0.64 (1,1) [724,1]. _t241 => box 1 _t242 [ SNF ] [ SNF++, 2031, _t242 ] % 0.48/0.64 (1,1) [807,1]. _t246 => box 1 _t247 [ SNF ] [ SNF++, 2051, _t247 ] % 0.48/0.64 (1,1) [899,1]. _t250 => box 1 _t251 [ SNF ] [ SNF++, 2077, _t251 ] % 0.48/0.64 (279,1) [935,1]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 2089, ~p1 ] % 0.48/0.64 (1,1) [936,1]. true => ~_t253 | _t51 | p2 [ SNF ] % 0.48/0.64 (1,1) [1947,1]. _t32 => box 1 _t344 [ SNF++, 40 ] % 0.48/0.64 (1,1) [1949,1]. _t42 => box 1 _t345 [ SNF++, 51 ] % 0.48/0.64 (1,1) [1975,1]. _t223 => box 1 _t354 [ SNF++, 326 ] % 0.48/0.64 (1,1) [1983,1]. _t44 => box 1 _t317 [ SNF++, 362 ] % 0.48/0.64 (1,1) [2009,1]. _t225 => box 1 _t326 [ SNF++, 581 ] % 0.48/0.64 (1,1) [2017,1]. _t46 => box 1 _t293 [ SNF++, 609 ] % 0.48/0.64 (1,1) [2031,1]. _t241 => box 1 _t356 [ SNF++, 724 ] % 0.48/0.64 (1,1) [2051,1]. _t246 => box 1 _t357 [ SNF++, 807 ] % 0.48/0.64 (1,1) [2077,1]. _t250 => box 1 _t358 [ SNF++, 899 ] % 0.48/0.64 (279,1) [2089,1]. _t51 => ~box 1~ _t256 [ SNF++, 935 ] % 0.48/0.64 (1,1) [2092,1]. true => ~_t359 | _t32 [ SNF++, 1414 ] % 0.48/0.64 (1,1) [2094,1]. true => ~_t360 | _t42 [ SNF++, 1413 ] % 0.48/0.64 (1,1) [2120,1]. true => ~_t369 | _t223 [ SNF++, 1400 ] % 0.48/0.64 (1,1) [2128,1]. true => ~_t330 | _t44 [ SNF++, 1396 ] % 0.48/0.64 (1,1) [2154,1]. true => ~_t339 | _t225 [ SNF++, 1383 ] % 0.48/0.64 (1,1) [2162,1]. true => ~_t305 | _t46 [ SNF++, 1379 ] % 0.48/0.64 (1,1) [2176,1]. true => ~_t371 | _t241 [ SNF++, 1372 ] % 0.48/0.64 (1,1) [2196,1]. true => ~_t372 | _t246 [ SNF++, 1362 ] % 0.48/0.64 (1,1) [2222,1]. true => ~_t373 | _t250 [ SNF++, 1349 ] % 0.48/0.64 (1,1) [2238,1]. true => ~_t374 | _t253 [ SNF++, 1341 ] % 0.48/0.64 (289,1) [2248,1]. true => ~_t375 | ~p2 [ SNF++, 1336 ] % 0.48/0.64 (289,1) [2317,1]. true => ~_t375 | ~_t253 | _t51 [ LRES, 2248, 936, ~p2 ] % 0.48/0.64 (279,1) [2404,1]. true => ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 | ~_t42 | ~_t32 [ GEN1, 2077, 2031, 1949, 2009, 2017, 1983, 1947, 1975, 2051, 2089, 2403, _t358, _t356, _t345, _t326, _t293, _t317, _t344, _t354, _t357, _t256 ] % 0.48/0.64 (279,1) [2405,1]. true => ~_t359 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 | ~_t42 [ LRES, 2404, 2092, ~_t32 ] % 0.48/0.64 (279,1) [2406,1]. true => ~_t360 | ~_t359 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 [ LRES, 2405, 2094, ~_t42 ] % 0.48/0.64 (279,1) [2407,1]. true => ~_t360 | ~_t359 | ~_t330 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 [ LRES, 2406, 2128, ~_t44 ] % 0.48/0.64 (279,1) [2408,1]. true => ~_t360 | ~_t359 | ~_t330 | ~_t305 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 [ LRES, 2407, 2162, ~_t46 ] % 0.48/0.64 (289,1) [2409,1]. true => ~_t375 | ~_t360 | ~_t359 | ~_t330 | ~_t305 | ~_t253 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 [ LRES, 2408, 2317, ~_t51 ] % 0.48/0.64 (289,1) [2410,1]. true => ~_t375 | ~_t369 | ~_t360 | ~_t359 | ~_t330 | ~_t305 | ~_t253 | ~_t250 | ~_t246 | ~_t241 | ~_t225 [ LRES, 2409, 2120, ~_t223 ] % 0.48/0.64 (289,1) [2411,1]. true => ~_t375 | ~_t369 | ~_t360 | ~_t359 | ~_t339 | ~_t330 | ~_t305 | ~_t253 | ~_t250 | ~_t246 | ~_t241 [ LRES, 2410, 2154, ~_t225 ] % 0.48/0.64 (289,1) [2412,1]. true => ~_t375 | ~_t371 | ~_t369 | ~_t360 | ~_t359 | ~_t339 | ~_t330 | ~_t305 | ~_t253 | ~_t250 | ~_t246 [ LRES, 2411, 2176, ~_t241 ] % 0.48/0.64 (289,1) [2413,1]. true => ~_t375 | ~_t372 | ~_t371 | ~_t369 | ~_t360 | ~_t359 | ~_t339 | ~_t330 | ~_t305 | ~_t253 | ~_t250 [ LRES, 2412, 2196, ~_t246 ] % 0.48/0.64 (289,1) [2414,1]. true => ~_t375 | ~_t373 | ~_t372 | ~_t371 | ~_t369 | ~_t360 | ~_t359 | ~_t339 | ~_t330 | ~_t305 | ~_t253 [ LRES, 2413, 2222, ~_t250 ] % 0.48/0.64 (289,1) [2415,1]. true => ~_t375 | ~_t374 | ~_t373 | ~_t372 | ~_t371 | ~_t369 | ~_t360 | ~_t359 | ~_t339 | ~_t330 | ~_t305 [ LRES, 2414, 2238, ~_t253 ] % 0.48/0.64 (1,1) [39,2]. _t33 => box 1 _t34 [ SNF ] [ SNF++, 1821, _t34 ] % 0.48/0.64 (1,1) [50,2]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 1823, _t44 ] % 0.48/0.64 (1,1) [325,2]. _t224 => box 1 _t225 [ SNF ] [ SNF++, 1849, _t225 ] % 0.48/0.64 (1,1) [361,2]. _t45 => box 1 _t46 [ SNF ] [ SNF++, 1857, _t46 ] % 0.48/0.64 (1,1) [580,2]. _t226 => box 1 _t227 [ SNF ] [ SNF++, 1883, _t227 ] % 0.48/0.64 (1,1) [608,2]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 1891, _t48 ] % 0.48/0.64 (1,1) [723,2]. _t242 => box 1 _t243 [ SNF ] [ SNF++, 1905, _t243 ] % 0.48/0.64 (1,1) [806,2]. _t247 => box 1 _t248 [ SNF ] [ SNF++, 1925, _t248 ] % 0.48/0.64 (223,1) [851,2]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 1939, ~p6 ] % 0.48/0.64 (1,1) [898,2]. true => ~_t251 | _t73 | p1 [ SNF ] % 0.48/0.64 (1,1) [1821,2]. _t33 => box 1 _t329 [ SNF++, 39 ] % 0.48/0.64 (1,1) [1823,2]. _t43 => box 1 _t330 [ SNF++, 50 ] % 0.48/0.64 (1,1) [1849,2]. _t224 => box 1 _t339 [ SNF++, 325 ] % 0.48/0.64 (1,1) [1857,2]. _t45 => box 1 _t305 [ SNF++, 361 ] % 0.48/0.64 (1,1) [1883,2]. _t226 => box 1 _t314 [ SNF++, 580 ] % 0.48/0.64 (1,1) [1891,2]. _t47 => box 1 _t281 [ SNF++, 608 ] % 0.48/0.64 (1,1) [1905,2]. _t242 => box 1 _t341 [ SNF++, 723 ] % 0.48/0.64 (1,1) [1925,2]. _t247 => box 1 _t342 [ SNF++, 806 ] % 0.48/0.64 (223,1) [1939,2]. _t73 => ~box 1~ _t343 [ SNF++, 851 ] % 0.48/0.64 (1,1) [1948,2]. true => ~_t344 | _t33 [ SNF++, 40 ] % 0.48/0.64 (1,1) [1950,2]. true => ~_t345 | _t43 [ SNF++, 51 ] % 0.48/0.64 (1,1) [1976,2]. true => ~_t354 | _t224 [ SNF++, 326 ] % 0.48/0.64 (1,1) [1984,2]. true => ~_t317 | _t45 [ SNF++, 362 ] % 0.48/0.64 (1,1) [2010,2]. true => ~_t326 | _t226 [ SNF++, 581 ] % 0.48/0.64 (1,1) [2018,2]. true => ~_t293 | _t47 [ SNF++, 609 ] % 0.48/0.64 (1,1) [2032,2]. true => ~_t356 | _t242 [ SNF++, 724 ] % 0.48/0.64 (1,1) [2052,2]. true => ~_t357 | _t247 [ SNF++, 807 ] % 0.48/0.64 (1,1) [2078,2]. true => ~_t358 | _t251 [ SNF++, 899 ] % 0.48/0.64 (279,1) [2090,2]. true => ~_t256 | ~p1 [ SNF++, 935 ] % 0.48/0.64 (279,1) [2313,2]. true => ~_t256 | ~_t251 | _t73 [ LRES, 2090, 898, ~p1 ] % 0.48/0.64 (223,1) [2393,2]. true => ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 | ~_t43 | ~_t33 [ GEN1, 1925, 1849, 1821, 1857, 1891, 1883, 1823, 1905, 1939, 2392, _t342, _t339, _t329, _t305, _t281, _t314, _t330, _t341, _t343 ] % 0.48/0.64 (223,1) [2394,2]. true => ~_t344 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 | ~_t43 [ LRES, 2393, 1948, ~_t33 ] % 0.48/0.64 (223,1) [2395,2]. true => ~_t345 | ~_t344 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 [ LRES, 2394, 1950, ~_t43 ] % 0.48/0.64 (223,1) [2396,2]. true => ~_t345 | ~_t344 | ~_t317 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 [ LRES, 2395, 1984, ~_t45 ] % 0.48/0.64 (223,1) [2397,2]. true => ~_t345 | ~_t344 | ~_t317 | ~_t293 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 [ LRES, 2396, 2018, ~_t47 ] % 0.48/0.64 (279,1) [2398,2]. true => ~_t345 | ~_t344 | ~_t317 | ~_t293 | ~_t256 | ~_t251 | ~_t247 | ~_t242 | ~_t226 | ~_t224 [ LRES, 2397, 2313, ~_t73 ] % 0.48/0.64 (279,1) [2399,2]. true => ~_t354 | ~_t345 | ~_t344 | ~_t317 | ~_t293 | ~_t256 | ~_t251 | ~_t247 | ~_t242 | ~_t226 [ LRES, 2398, 1976, ~_t224 ] % 0.48/0.64 (279,1) [2400,2]. true => ~_t354 | ~_t345 | ~_t344 | ~_t326 | ~_t317 | ~_t293 | ~_t256 | ~_t251 | ~_t247 | ~_t242 [ LRES, 2399, 2010, ~_t226 ] % 0.48/0.64 (279,1) [2401,2]. true => ~_t356 | ~_t354 | ~_t345 | ~_t344 | ~_t326 | ~_t317 | ~_t293 | ~_t256 | ~_t251 | ~_t247 [ LRES, 2400, 2032, ~_t242 ] % 0.48/0.64 (279,1) [2402,2]. true => ~_t357 | ~_t356 | ~_t354 | ~_t345 | ~_t344 | ~_t326 | ~_t317 | ~_t293 | ~_t256 | ~_t251 [ LRES, 2401, 2052, ~_t247 ] % 0.48/0.64 (279,1) [2403,2]. true => ~_t358 | ~_t357 | ~_t356 | ~_t354 | ~_t345 | ~_t344 | ~_t326 | ~_t317 | ~_t293 | ~_t256 [ LRES, 2402, 2078, ~_t251 ] % 0.48/0.64 (1,1) [38,3]. _t34 => box 1 _t35 [ SNF ] [ SNF++, 1711, _t35 ] % 0.48/0.64 (1,1) [49,3]. _t44 => box 1 _t45 [ SNF ] [ SNF++, 1713, _t45 ] % 0.48/0.64 (1,1) [324,3]. _t225 => box 1 _t226 [ SNF ] [ SNF++, 1739, _t226 ] % 0.48/0.64 (1,1) [360,3]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 1747, _t47 ] % 0.48/0.64 (1,1) [579,3]. _t227 => box 1 _t228 [ SNF ] [ SNF++, 1773, _t228 ] % 0.48/0.64 (1,1) [607,3]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 1781, _t49 ] % 0.48/0.64 (1,1) [722,3]. _t243 => box 1 _t244 [ SNF ] [ SNF++, 1795, _t244 ] % 0.48/0.64 (201,1) [804,3]. _t95 => ~box 1~ ~p5 [ SNF ] [ SNF++, 1815, ~p5 ] % 0.48/0.64 (1,1) [805,3]. true => ~_t248 | _t95 | p6 [ SNF ] % 0.48/0.64 (1,1) [1711,3]. _t34 => box 1 _t316 [ SNF++, 38 ] % 0.48/0.64 (1,1) [1713,3]. _t44 => box 1 _t317 [ SNF++, 49 ] % 0.48/0.64 (1,1) [1739,3]. _t225 => box 1 _t326 [ SNF++, 324 ] % 0.48/0.64 (1,1) [1747,3]. _t46 => box 1 _t293 [ SNF++, 360 ] % 0.48/0.64 (1,1) [1773,3]. _t227 => box 1 _t302 [ SNF++, 579 ] % 0.48/0.64 (1,1) [1781,3]. _t48 => box 1 _t269 [ SNF++, 607 ] % 0.48/0.64 (1,1) [1795,3]. _t243 => box 1 _t328 [ SNF++, 722 ] % 0.48/0.64 (201,1) [1815,3]. _t95 => ~box 1~ _t266 [ SNF++, 804 ] % 0.48/0.64 (1,1) [1822,3]. true => ~_t329 | _t34 [ SNF++, 39 ] % 0.48/0.64 (1,1) [1824,3]. true => ~_t330 | _t44 [ SNF++, 50 ] % 0.48/0.64 (1,1) [1850,3]. true => ~_t339 | _t225 [ SNF++, 325 ] % 0.48/0.64 (1,1) [1858,3]. true => ~_t305 | _t46 [ SNF++, 361 ] % 0.48/0.64 (1,1) [1884,3]. true => ~_t314 | _t227 [ SNF++, 580 ] % 0.48/0.64 (1,1) [1892,3]. true => ~_t281 | _t48 [ SNF++, 608 ] % 0.48/0.64 (1,1) [1906,3]. true => ~_t341 | _t243 [ SNF++, 723 ] % 0.48/0.64 (1,1) [1926,3]. true => ~_t342 | _t248 [ SNF++, 806 ] % 0.48/0.64 (223,1) [1940,3]. true => ~_t343 | ~p6 [ SNF++, 851 ] % 0.48/0.64 (223,1) [2266,3]. true => ~_t343 | ~_t248 | _t95 [ LRES, 1940, 805, ~p6 ] % 0.48/0.64 (201,1) [2383,3]. true => ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 | ~_t44 | ~_t34 [ GEN1, 1795, 1713, 1773, 1781, 1747, 1711, 1739, 1815, 2382, _t328, _t317, _t302, _t269, _t293, _t316, _t326, _t266 ] % 0.48/0.64 (201,1) [2384,3]. true => ~_t329 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 | ~_t44 [ LRES, 2383, 1822, ~_t34 ] % 0.48/0.64 (201,1) [2385,3]. true => ~_t330 | ~_t329 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 [ LRES, 2384, 1824, ~_t44 ] % 0.48/0.64 (201,1) [2386,3]. true => ~_t330 | ~_t329 | ~_t305 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 [ LRES, 2385, 1858, ~_t46 ] % 0.48/0.64 (201,1) [2387,3]. true => ~_t330 | ~_t329 | ~_t305 | ~_t281 | ~_t243 | ~_t227 | ~_t225 | ~_t95 [ LRES, 2386, 1892, ~_t48 ] % 0.48/0.64 (223,1) [2388,3]. true => ~_t343 | ~_t330 | ~_t329 | ~_t305 | ~_t281 | ~_t248 | ~_t243 | ~_t227 | ~_t225 [ LRES, 2387, 2266, ~_t95 ] % 0.48/0.64 (223,1) [2389,3]. true => ~_t343 | ~_t339 | ~_t330 | ~_t329 | ~_t305 | ~_t281 | ~_t248 | ~_t243 | ~_t227 [ LRES, 2388, 1850, ~_t225 ] % 0.48/0.64 (223,1) [2390,3]. true => ~_t343 | ~_t339 | ~_t330 | ~_t329 | ~_t314 | ~_t305 | ~_t281 | ~_t248 | ~_t243 [ LRES, 2389, 1884, ~_t227 ] % 0.48/0.64 (223,1) [2391,3]. true => ~_t343 | ~_t341 | ~_t339 | ~_t330 | ~_t329 | ~_t314 | ~_t305 | ~_t281 | ~_t248 [ LRES, 2390, 1906, ~_t243 ] % 0.48/0.64 (223,1) [2392,3]. true => ~_t343 | ~_t342 | ~_t341 | ~_t339 | ~_t330 | ~_t329 | ~_t314 | ~_t305 | ~_t281 [ LRES, 2391, 1926, ~_t248 ] % 0.48/0.64 (1,1) [37,4]. _t35 => box 1 _t36 [ SNF ] [ SNF++, 1619, _t36 ] % 0.48/0.64 (1,1) [48,4]. _t45 => box 1 _t46 [ SNF ] [ SNF++, 1621, _t46 ] % 0.48/0.64 (1,1) [323,4]. _t226 => box 1 _t227 [ SNF ] [ SNF++, 1647, _t227 ] % 0.48/0.64 (1,1) [359,4]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 1655, _t48 ] % 0.48/0.64 (1,1) [578,4]. _t228 => box 1 _t229 [ SNF ] [ SNF++, 1681, _t229 ] % 0.48/0.64 (1,1) [606,4]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 1689, _t50 ] % 0.48/0.64 (157,1) [688,4]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 1703, ~p4 ] % 0.48/0.64 (1,1) [721,4]. true => ~_t244 | _t62 | p5 [ SNF ] % 0.48/0.64 (1,1) [1619,4]. _t35 => box 1 _t304 [ SNF++, 37 ] % 0.48/0.64 (1,1) [1621,4]. _t45 => box 1 _t305 [ SNF++, 48 ] % 0.48/0.64 (1,1) [1647,4]. _t226 => box 1 _t314 [ SNF++, 323 ] % 0.48/0.64 (1,1) [1655,4]. _t47 => box 1 _t281 [ SNF++, 359 ] % 0.48/0.64 (1,1) [1681,4]. _t228 => box 1 _t290 [ SNF++, 578 ] % 0.48/0.64 (1,1) [1689,4]. _t49 => box 1 _t258 [ SNF++, 606 ] % 0.48/0.64 (157,1) [1703,4]. _t62 => ~box 1~ _t265 [ SNF++, 688 ] % 0.48/0.64 (1,1) [1712,4]. true => ~_t316 | _t35 [ SNF++, 38 ] % 0.48/0.64 (1,1) [1714,4]. true => ~_t317 | _t45 [ SNF++, 49 ] % 0.48/0.64 (1,1) [1740,4]. true => ~_t326 | _t226 [ SNF++, 324 ] % 0.48/0.64 (1,1) [1748,4]. true => ~_t293 | _t47 [ SNF++, 360 ] % 0.48/0.64 (1,1) [1774,4]. true => ~_t302 | _t228 [ SNF++, 579 ] % 0.48/0.64 (1,1) [1782,4]. true => ~_t269 | _t49 [ SNF++, 607 ] % 0.48/0.64 (1,1) [1796,4]. true => ~_t328 | _t244 [ SNF++, 722 ] % 0.48/0.64 (201,1) [1816,4]. true => ~_t266 | ~p5 [ SNF++, 804 ] % 0.48/0.64 (201,1) [2262,4]. true => ~_t266 | ~_t244 | _t62 [ LRES, 1816, 721, ~p5 ] % 0.48/0.64 (157,1) [2374,4]. true => ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 | ~_t45 | ~_t35 [ GEN1, 1647, 1619, 1655, 1689, 1681, 1621, 1703, 2373, _t314, _t304, _t281, _t258, _t290, _t305, _t265 ] % 0.48/0.64 (157,1) [2375,4]. true => ~_t316 | ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 | ~_t45 [ LRES, 2374, 1712, ~_t35 ] % 0.48/0.64 (157,1) [2376,4]. true => ~_t317 | ~_t316 | ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 [ LRES, 2375, 1714, ~_t45 ] % 0.48/0.64 (157,1) [2377,4]. true => ~_t317 | ~_t316 | ~_t293 | ~_t228 | ~_t226 | ~_t62 | ~_t49 [ LRES, 2376, 1748, ~_t47 ] % 0.48/0.64 (157,1) [2378,4]. true => ~_t317 | ~_t316 | ~_t293 | ~_t269 | ~_t228 | ~_t226 | ~_t62 [ LRES, 2377, 1782, ~_t49 ] % 0.48/0.64 (201,1) [2379,4]. true => ~_t317 | ~_t316 | ~_t293 | ~_t269 | ~_t266 | ~_t244 | ~_t228 | ~_t226 [ LRES, 2378, 2262, ~_t62 ] % 0.48/0.64 (201,1) [2380,4]. true => ~_t326 | ~_t317 | ~_t316 | ~_t293 | ~_t269 | ~_t266 | ~_t244 | ~_t228 [ LRES, 2379, 1740, ~_t226 ] % 0.48/0.64 (201,1) [2381,4]. true => ~_t326 | ~_t317 | ~_t316 | ~_t302 | ~_t293 | ~_t269 | ~_t266 | ~_t244 [ LRES, 2380, 1774, ~_t228 ] % 0.48/0.64 (201,1) [2382,4]. true => ~_t328 | ~_t326 | ~_t317 | ~_t316 | ~_t302 | ~_t293 | ~_t269 | ~_t266 [ LRES, 2381, 1796, ~_t244 ] % 0.48/0.64 (1,1) [36,5]. _t36 => box 1 _t37 [ SNF ] [ SNF++, 1543, _t37 ] % 0.48/0.64 (1,1) [47,5]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 1545, _t47 ] % 0.48/0.64 (1,1) [322,5]. _t227 => box 1 _t228 [ SNF ] [ SNF++, 1571, _t228 ] % 0.48/0.64 (1,1) [358,5]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 1579, _t49 ] % 0.48/0.64 (1,1) [577,5]. _t229 => box 1 _t230 [ SNF ] [ SNF++, 1605, _t230 ] % 0.48/0.64 (131,1) [604,5]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 1613, ~p1 ] % 0.48/0.64 (1,1) [605,5]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.48/0.64 (1,1) [1543,5]. _t36 => box 1 _t292 [ SNF++, 36 ] % 0.48/0.64 (1,1) [1545,5]. _t46 => box 1 _t293 [ SNF++, 47 ] % 0.48/0.64 (1,1) [1571,5]. _t227 => box 1 _t302 [ SNF++, 322 ] % 0.48/0.64 (1,1) [1579,5]. _t48 => box 1 _t269 [ SNF++, 358 ] % 0.48/0.64 (1,1) [1605,5]. _t229 => box 1 _t278 [ SNF++, 577 ] % 0.48/0.64 (131,1) [1613,5]. _t51 => ~box 1~ _t256 [ SNF++, 604 ] % 0.48/0.64 (1,1) [1620,5]. true => ~_t304 | _t36 [ SNF++, 37 ] % 0.48/0.64 (1,1) [1622,5]. true => ~_t305 | _t46 [ SNF++, 48 ] % 0.48/0.64 (1,1) [1648,5]. true => ~_t314 | _t227 [ SNF++, 323 ] % 0.48/0.64 (1,1) [1656,5]. true => ~_t281 | _t48 [ SNF++, 359 ] % 0.48/0.64 (1,1) [1682,5]. true => ~_t290 | _t229 [ SNF++, 578 ] % 0.48/0.64 (1,1) [1690,5]. true => ~_t258 | _t50 [ SNF++, 606 ] % 0.48/0.64 (157,1) [1704,5]. true => ~_t265 | ~p4 [ SNF++, 688 ] % 0.48/0.64 (157,1) [2261,5]. true => ~_t265 | _t51 | ~_t50 [ LRES, 1704, 605, ~p4 ] % 0.48/0.64 (157,1) [2331,5]. true => ~_t265 | ~_t258 | _t51 [ LRES, 2261, 1690, ~_t50 ] % 0.48/0.64 (131,1) [2367,5]. true => ~_t229 | ~_t227 | ~_t51 | ~_t48 | ~_t46 | ~_t36 [ GEN1, 1571, 1543, 1579, 1605, 1545, 1613, 2366, _t302, _t292, _t269, _t278, _t293, _t256 ] % 0.48/0.64 (131,1) [2368,5]. true => ~_t304 | ~_t229 | ~_t227 | ~_t51 | ~_t48 | ~_t46 [ LRES, 2367, 1620, ~_t36 ] % 0.48/0.64 (131,1) [2369,5]. true => ~_t305 | ~_t304 | ~_t229 | ~_t227 | ~_t51 | ~_t48 [ LRES, 2368, 1622, ~_t46 ] % 0.48/0.64 (131,1) [2370,5]. true => ~_t305 | ~_t304 | ~_t281 | ~_t229 | ~_t227 | ~_t51 [ LRES, 2369, 1656, ~_t48 ] % 0.48/0.64 (157,1) [2371,5]. true => ~_t305 | ~_t304 | ~_t281 | ~_t265 | ~_t258 | ~_t229 | ~_t227 [ LRES, 2370, 2331, ~_t51 ] % 0.48/0.64 (157,1) [2372,5]. true => ~_t314 | ~_t305 | ~_t304 | ~_t281 | ~_t265 | ~_t258 | ~_t229 [ LRES, 2371, 1648, ~_t227 ] % 0.48/0.64 (157,1) [2373,5]. true => ~_t314 | ~_t305 | ~_t304 | ~_t290 | ~_t281 | ~_t265 | ~_t258 [ LRES, 2372, 1682, ~_t229 ] % 0.48/0.64 (1,1) [35,6]. _t37 => box 1 _t38 [ SNF ] [ SNF++, 1485, _t38 ] % 0.48/0.64 (1,1) [46,6]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 1487, _t48 ] % 0.48/0.64 (1,1) [321,6]. _t228 => box 1 _t229 [ SNF ] [ SNF++, 1513, _t229 ] % 0.48/0.64 (1,1) [357,6]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 1521, _t50 ] % 0.48/0.64 (93,1) [465,6]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 1535, ~p4 ] % 0.48/0.64 (1,1) [576,6]. true => ~_t230 | _t62 | p1 [ SNF ] % 0.48/0.64 (1,1) [1485,6]. _t37 => box 1 _t280 [ SNF++, 35 ] % 0.48/0.64 (1,1) [1487,6]. _t47 => box 1 _t281 [ SNF++, 46 ] % 0.48/0.64 (1,1) [1513,6]. _t228 => box 1 _t290 [ SNF++, 321 ] % 0.48/0.64 (1,1) [1521,6]. _t49 => box 1 _t258 [ SNF++, 357 ] % 0.48/0.64 (93,1) [1535,6]. _t62 => ~box 1~ _t265 [ SNF++, 465 ] % 0.48/0.64 (1,1) [1544,6]. true => ~_t292 | _t37 [ SNF++, 36 ] % 0.48/0.64 (1,1) [1546,6]. true => ~_t293 | _t47 [ SNF++, 47 ] % 0.48/0.64 (1,1) [1572,6]. true => ~_t302 | _t228 [ SNF++, 322 ] % 0.48/0.64 (1,1) [1580,6]. true => ~_t269 | _t49 [ SNF++, 358 ] % 0.48/0.64 (1,1) [1606,6]. true => ~_t278 | _t230 [ SNF++, 577 ] % 0.48/0.64 (131,1) [1614,6]. true => ~_t256 | ~p1 [ SNF++, 604 ] % 0.48/0.64 (131,1) [2257,6]. true => ~_t256 | ~_t230 | _t62 [ LRES, 1614, 576, ~p1 ] % 0.48/0.64 (93,1) [2360,6]. true => ~_t228 | ~_t62 | ~_t49 | ~_t47 | ~_t37 [ GEN1, 1513, 1485, 1521, 1487, 1535, 2359, _t290, _t280, _t258, _t281, _t265 ] % 0.48/0.64 (93,1) [2361,6]. true => ~_t292 | ~_t228 | ~_t62 | ~_t49 | ~_t47 [ LRES, 2360, 1544, ~_t37 ] % 0.48/0.64 (93,1) [2362,6]. true => ~_t293 | ~_t292 | ~_t228 | ~_t62 | ~_t49 [ LRES, 2361, 1546, ~_t47 ] % 0.48/0.64 (93,1) [2363,6]. true => ~_t293 | ~_t292 | ~_t269 | ~_t228 | ~_t62 [ LRES, 2362, 1580, ~_t49 ] % 0.48/0.64 (131,1) [2364,6]. true => ~_t293 | ~_t292 | ~_t269 | ~_t256 | ~_t230 | ~_t228 [ LRES, 2363, 2257, ~_t62 ] % 0.48/0.64 (131,1) [2365,6]. true => ~_t302 | ~_t293 | ~_t292 | ~_t269 | ~_t256 | ~_t230 [ LRES, 2364, 1572, ~_t228 ] % 0.48/0.64 (131,1) [2366,6]. true => ~_t302 | ~_t293 | ~_t292 | ~_t278 | ~_t269 | ~_t256 [ LRES, 2365, 1606, ~_t230 ] % 0.48/0.64 (1,1) [34,7]. _t38 => box 1 _t39 [ SNF ] [ SNF++, 1443, _t39 ] % 0.48/0.64 (1,1) [45,7]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 1445, _t49 ] % 0.48/0.64 (1,1) [320,7]. _t229 => box 1 _t230 [ SNF ] [ SNF++, 1471, _t230 ] % 0.48/0.64 (67,1) [355,7]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 1479, ~p1 ] % 0.48/0.64 (1,1) [356,7]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.48/0.64 (1,1) [1443,7]. _t38 => box 1 _t268 [ SNF++, 34 ] % 0.48/0.64 (1,1) [1445,7]. _t48 => box 1 _t269 [ SNF++, 45 ] % 0.48/0.64 (1,1) [1471,7]. _t229 => box 1 _t278 [ SNF++, 320 ] % 0.48/0.64 (67,1) [1479,7]. _t51 => ~box 1~ _t256 [ SNF++, 355 ] % 0.48/0.64 (1,1) [1486,7]. true => ~_t280 | _t38 [ SNF++, 35 ] % 0.48/0.64 (1,1) [1488,7]. true => ~_t281 | _t48 [ SNF++, 46 ] % 0.48/0.64 (1,1) [1514,7]. true => ~_t290 | _t229 [ SNF++, 321 ] % 0.48/0.64 (1,1) [1522,7]. true => ~_t258 | _t50 [ SNF++, 357 ] % 0.48/0.64 (93,1) [1536,7]. true => ~_t265 | ~p4 [ SNF++, 465 ] % 0.48/0.64 (93,1) [2256,7]. true => ~_t265 | _t51 | ~_t50 [ LRES, 1536, 356, ~p4 ] % 0.48/0.65 (93,1) [2330,7]. true => ~_t265 | ~_t258 | _t51 [ LRES, 2256, 1522, ~_t50 ] % 0.48/0.65 (67,1) [2355,7]. true => ~_t229 | ~_t51 | ~_t48 | ~_t38 [ GEN1, 1471, 1443, 1445, 1479, 2354, _t278, _t268, _t269, _t256 ] % 0.48/0.65 (67,1) [2356,7]. true => ~_t280 | ~_t229 | ~_t51 | ~_t48 [ LRES, 2355, 1486, ~_t38 ] % 0.48/0.65 (67,1) [2357,7]. true => ~_t281 | ~_t280 | ~_t229 | ~_t51 [ LRES, 2356, 1488, ~_t48 ] % 0.48/0.65 (93,1) [2358,7]. true => ~_t281 | ~_t280 | ~_t265 | ~_t258 | ~_t229 [ LRES, 2357, 2330, ~_t51 ] % 0.48/0.65 (93,1) [2359,7]. true => ~_t290 | ~_t281 | ~_t280 | ~_t265 | ~_t258 [ LRES, 2358, 1514, ~_t229 ] % 0.48/0.65 (1,1) [33,8]. _t39 => box 1 _t40 [ SNF ] [ SNF++, 1419, _t40 ] % 0.48/0.65 (1,1) [44,8]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 1421, _t50 ] % 0.48/0.65 (29,1) [178,8]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 1435, ~p4 ] % 0.48/0.65 (1,1) [319,8]. true => ~_t230 | _t62 | p1 [ SNF ] % 0.48/0.65 (1,1) [1419,8]. _t39 => box 1 _t257 [ SNF++, 33 ] % 0.48/0.65 (1,1) [1421,8]. _t49 => box 1 _t258 [ SNF++, 44 ] % 0.48/0.65 (29,1) [1435,8]. _t62 => ~box 1~ _t265 [ SNF++, 178 ] % 0.48/0.65 (1,1) [1444,8]. true => ~_t268 | _t39 [ SNF++, 34 ] % 0.48/0.65 (1,1) [1446,8]. true => ~_t269 | _t49 [ SNF++, 45 ] % 0.48/0.65 (1,1) [1472,8]. true => ~_t278 | _t230 [ SNF++, 320 ] % 0.48/0.65 (67,1) [1480,8]. true => ~_t256 | ~p1 [ SNF++, 355 ] % 0.48/0.65 (67,1) [2252,8]. true => ~_t256 | ~_t230 | _t62 [ LRES, 1480, 319, ~p1 ] % 0.48/0.65 (29,1) [2350,8]. true => ~_t62 | ~_t49 | ~_t39 [ GEN1, 1421, 1419, 1435, 2349, _t258, _t257, _t265 ] % 0.48/0.65 (29,1) [2351,8]. true => ~_t268 | ~_t62 | ~_t49 [ LRES, 2350, 1444, ~_t39 ] % 0.48/0.65 (29,1) [2352,8]. true => ~_t269 | ~_t268 | ~_t62 [ LRES, 2351, 1446, ~_t49 ] % 0.48/0.65 (67,1) [2353,8]. true => ~_t269 | ~_t268 | ~_t256 | ~_t230 [ LRES, 2352, 2252, ~_t62 ] % 0.48/0.65 (67,1) [2354,8]. true => ~_t278 | ~_t269 | ~_t268 | ~_t256 [ LRES, 2353, 1472, ~_t230 ] % 0.48/0.65 (1,1) [32,9]. _t40 => box 1 p1 [ SNF ] [ SNF++, 1415, p1 ] % 0.48/0.65 (3,1) [42,9]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 1417, ~p1 ] % 0.48/0.65 (1,1) [43,9]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.48/0.65 (1,1) [1415,9]. _t40 => box 1 _t255 [ SNF++, 32 ] % 0.48/0.65 (3,1) [1417,9]. _t51 => ~box 1~ _t256 [ SNF++, 42 ] % 0.48/0.65 (1,1) [1420,9]. true => ~_t257 | _t40 [ SNF++, 33 ] % 0.48/0.65 (1,1) [1422,9]. true => ~_t258 | _t50 [ SNF++, 44 ] % 0.48/0.65 (29,1) [1436,9]. true => ~_t265 | ~p4 [ SNF++, 178 ] % 0.48/0.65 (29,1) [2251,9]. true => ~_t265 | _t51 | ~_t50 [ LRES, 1436, 43, ~p4 ] % 0.48/0.65 (3,1) [2295,9]. true => ~_t51 | ~_t40 [ GEN1, 1415, 1417, 2272, _t255, _t256 ] % 0.48/0.65 (3,1) [2329,9]. true => ~_t257 | ~_t51 [ LRES, 2295, 1420, ~_t40 ] % 0.48/0.65 (29,1) [2340,9]. true => ~_t265 | ~_t258 | _t51 [ LRES, 2251, 1422, ~_t50 ] % 0.48/0.65 (29,1) [2349,9]. true => ~_t265 | ~_t258 | ~_t257 [ LRES, 2340, 2329, _t51 ] % 0.48/0.65 (1,1) [1416,10]. true => ~_t255 | p1 [ SNF++, 32 ] % 0.48/0.65 (3,1) [1418,10]. true => ~_t256 | ~p1 [ SNF++, 42 ] % 0.48/0.65 (3,1) [2272,10]. true => ~_t256 | ~_t255 [ LRES, 1418, 1416, ~p1 ] % 0.48/0.65 % SZS output end Refutation % 0.48/0.65 % KSP exiting %------------------------------------------------------------------------------