%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP091_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n017.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:58 PM UTC 2026 % Result : Theorem 0.47s 0.65s % Output : Refutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SYP091_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n017.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 4 17:25:12 EDT 2026 % 0.15/0.33 % CPUTime : % 0.42/0.59 ----KSP format--- % 0.42/0.60 set(box,SER). % 0.42/0.60 usable(formulas). % 0.42/0.60 true. % 0.42/0.60 end_of_list. % 0.42/0.60 sos(formulas). % 0.42/0.60 ~ ([] ( 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.42/0.60 end_of_list. % 0.42/0.60 ----------------- % 0.42/0.60 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.GXd1CcEBDK/theBenchmark.ksp % 0.47/0.65 % 0.47/0.65 % SZS status Theorem % 0.47/0.65 % 0.47/0.65 ***************** % 0.47/0.65 FOUND PROOF 1 % 0.47/0.65 ***************** % 0.47/0.65 % SZS output start Refutation % 0.47/0.65 % 0.47/0.65 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.47/0.65 (1,1) [85,0]. _t31 => box 1 _t32 [ SNF ] [ Backward Subsumption, 2439 ] % 0.47/0.65 (1,1) [87,0]. true => _t31 | ~_t0 [ SNF ] [ Backward Subsumption, 2150 ] % 0.47/0.65 (1,1) [106,0]. _t41 => box 1 _t42 [ SNF ] [ Backward Subsumption, 2159 ] % 0.47/0.65 (1,1) [108,0]. true => _t41 | ~_t0 [ SNF ] [ Backward Subsumption, 2149 ] % 0.47/0.65 (1,1) [645,0]. _t222 => box 1 _t223 [ SNF ] [ Backward Subsumption, 2187 ] % 0.47/0.65 (1,1) [647,0]. true => _t222 | ~_t0 [ SNF ] [ Backward Subsumption, 2121 ] % 0.47/0.65 (1,1) [716,0]. _t43 => box 1 _t44 [ SNF ] [ Backward Subsumption, 2191 ] % 0.47/0.65 (1,1) [718,0]. true => _t43 | ~_t0 [ SNF ] [ Backward Subsumption, 2117 ] % 0.47/0.65 (1,1) [1143,0]. _t224 => box 1 _t225 [ SNF ] [ Backward Subsumption, 2219 ] % 0.47/0.65 (1,1) [1145,0]. true => _t224 | ~_t0 [ SNF ] [ Backward Subsumption, 2089 ] % 0.47/0.65 (1,1) [1198,0]. _t45 => box 1 _t46 [ SNF ] [ Backward Subsumption, 2223 ] % 0.47/0.65 (1,1) [1200,0]. true => _t45 | ~_t0 [ SNF ] [ Backward Subsumption, 2085 ] % 0.47/0.65 (1,1) [1420,0]. _t240 => box 1 _t241 [ SNF ] [ Backward Subsumption, 2355 ] % 0.47/0.65 (1,1) [1422,0]. true => _t240 | ~_t0 [ SNF ] [ Backward Subsumption, 2066 ] % 0.47/0.65 (1,1) [1579,0]. _t245 => box 1 _t246 [ SNF ] [ Backward Subsumption, 2339 ] % 0.47/0.65 (1,1) [1581,0]. true => _t245 | ~_t0 [ SNF ] [ Backward Subsumption, 2050 ] % 0.47/0.65 (1,1) [1755,0]. _t249 => box 1 _t250 [ SNF ] [ Backward Subsumption, 2283 ] % 0.47/0.65 (1,1) [1757,0]. true => _t249 | ~_t0 [ SNF ] [ Backward Subsumption, 2025 ] % 0.47/0.65 (1,1) [1823,0]. _t252 => box 1 _t253 [ SNF ] [ Backward Subsumption, 2294 ] % 0.47/0.65 (1,1) [1825,0]. true => _t252 | ~_t0 [ SNF ] [ Backward Subsumption, 2011 ] % 0.47/0.65 (289,1) [1838,0]. _t84 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 2299 ] % 0.47/0.65 (1,1) [1839,0]. true => _t84 | ~_t0 [ SNF ] [ Backward Subsumption, 2006 ] % 0.47/0.65 (1,1) [2006,0]. true => _t84 [ Unit Resolution, 3, 1839, _t0 ] [ Modal Level Pure Literal Elimination, _t84 ] % 0.47/0.65 (1,1) [2011,0]. true => _t252 [ Unit Resolution, 3, 1825, _t0 ] [ Modal Level Pure Literal Elimination, _t252 ] % 0.47/0.65 (1,1) [2025,0]. true => _t249 [ Unit Resolution, 3, 1757, _t0 ] [ Modal Level Pure Literal Elimination, _t249 ] % 0.47/0.65 (1,1) [2050,0]. true => _t245 [ Unit Resolution, 3, 1581, _t0 ] [ Modal Level Pure Literal Elimination, _t245 ] % 0.47/0.65 (1,1) [2066,0]. true => _t240 [ Unit Resolution, 3, 1422, _t0 ] [ Modal Level Pure Literal Elimination, _t240 ] % 0.47/0.65 (1,1) [2085,0]. true => _t45 [ Unit Resolution, 3, 1200, _t0 ] [ Modal Level Pure Literal Elimination, _t45 ] % 0.47/0.65 (1,1) [2089,0]. true => _t224 [ Unit Resolution, 3, 1145, _t0 ] [ Modal Level Pure Literal Elimination, _t224 ] % 0.47/0.65 (1,1) [2117,0]. true => _t43 [ Unit Resolution, 3, 718, _t0 ] [ Modal Level Pure Literal Elimination, _t43 ] % 0.47/0.65 (1,1) [2121,0]. true => _t222 [ Unit Resolution, 3, 647, _t0 ] [ Modal Level Pure Literal Elimination, _t222 ] % 0.47/0.65 (1,1) [2149,0]. true => _t41 [ Unit Resolution, 3, 108, _t0 ] [ Modal Level Pure Literal Elimination, _t41 ] % 0.47/0.65 (1,1) [2150,0]. true => _t31 [ Unit Resolution, 3, 87, _t0 ] [ Modal Level Pure Literal Elimination, _t31 ] % 0.47/0.65 (1,1) [2159,0]. true => box 1 _t42 [ LHS Unit Resolution, 2149, 106, _t41 ] [ SNF++, 4656, _t42 ] % 0.47/0.65 (1,1) [2187,0]. true => box 1 _t223 [ LHS Unit Resolution, 2121, 645, _t222 ] [ SNF++, 4712, _t223 ] % 0.47/0.65 (1,1) [2191,0]. true => box 1 _t44 [ LHS Unit Resolution, 2117, 716, _t43 ] [ SNF++, 4720, _t44 ] % 0.47/0.65 (1,1) [2219,0]. true => box 1 _t225 [ LHS Unit Resolution, 2089, 1143, _t224 ] [ SNF++, 4776, _t225 ] % 0.47/0.65 (1,1) [2223,0]. true => box 1 _t46 [ LHS Unit Resolution, 2085, 1198, _t45 ] [ SNF++, 4784, _t46 ] % 0.47/0.65 (1,1) [2283,0]. true => box 1 _t250 [ LHS Unit Resolution, 2025, 1755, _t249 ] [ SNF++, 4904, _t250 ] % 0.47/0.65 (1,1) [2294,0]. true => box 1 _t253 [ LHS Unit Resolution, 2011, 1823, _t252 ] [ SNF++, 4920, _t253 ] % 0.47/0.65 (289,1) [2299,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 2006, 1838, _t84 ] [ SNF++, 5208, ~p2 ] % 0.47/0.65 (1,1) [2339,0]. true => box 1 _t246 [ LHS Unit Resolution, 2050, 1579, _t245 ] [ SNF++, 4854, _t246 ] % 0.47/0.65 (1,1) [2355,0]. true => box 1 _t241 [ LHS Unit Resolution, 2066, 1420, _t240 ] [ SNF++, 4822, _t241 ] % 0.47/0.65 (1,1) [2439,0]. true => box 1 _t32 [ LHS Unit Resolution, 2150, 85, _t31 ] [ SNF++, 4654, _t32 ] % 0.47/0.65 (1,1) [4654,0]. true => box 1 _t669 [ SNF++, 2439 ] % 0.47/0.65 (1,1) [4656,0]. true => box 1 _t670 [ SNF++, 2159 ] % 0.47/0.65 (1,1) [4712,0]. true => box 1 _t688 [ SNF++, 2187 ] % 0.47/0.65 (1,1) [4720,0]. true => box 1 _t616 [ SNF++, 2191 ] % 0.47/0.65 (1,1) [4776,0]. true => box 1 _t634 [ SNF++, 2219 ] % 0.47/0.65 (1,1) [4784,0]. true => box 1 _t567 [ SNF++, 2223 ] % 0.47/0.65 (1,1) [4822,0]. true => box 1 _t690 [ SNF++, 2355 ] % 0.47/0.65 (1,1) [4854,0]. true => box 1 _t691 [ SNF++, 2339 ] % 0.47/0.65 (1,1) [4904,0]. true => box 1 _t692 [ SNF++, 2283 ] % 0.47/0.65 (1,1) [4920,0]. true => box 1 _t693 [ SNF++, 2294 ] % 0.47/0.65 (289,1) [5208,0]. true => ~box 1~ _t694 [ SNF++, 2299 ] % 0.47/0.65 (289,1) [5377,0]. true => false [ GEN1, 4920, 4854, 4712, 4654, 4720, 4784, 4776, 4656, 4822, 4904, 5208, 5376, _t693, _t691, _t688, _t669, _t616, _t567, _t634, _t670, _t690, _t692, _t694 ] % 0.47/0.65 (1,1) [83,1]. _t32 => box 1 _t33 [ SNF ] [ SNF++, 4156, _t33 ] % 0.47/0.65 (1,1) [104,1]. _t42 => box 1 _t43 [ SNF ] [ SNF++, 4158, _t43 ] % 0.47/0.65 (1,1) [643,1]. _t223 => box 1 _t224 [ SNF ] [ SNF++, 4214, _t224 ] % 0.47/0.65 (1,1) [714,1]. _t44 => box 1 _t45 [ SNF ] [ SNF++, 4222, _t45 ] % 0.47/0.65 (1,1) [1141,1]. _t225 => box 1 _t226 [ SNF ] [ SNF++, 4278, _t226 ] % 0.47/0.65 (1,1) [1196,1]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 4286, _t47 ] % 0.47/0.65 (1,1) [1418,1]. _t241 => box 1 _t242 [ SNF ] [ SNF++, 4324, _t242 ] % 0.47/0.65 (1,1) [1577,1]. _t246 => box 1 _t247 [ SNF ] [ SNF++, 4356, _t247 ] % 0.47/0.65 (1,1) [1753,1]. _t250 => box 1 _t251 [ SNF ] [ SNF++, 4388, _t251 ] % 0.47/0.65 (279,1) [1821,1]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 4646, ~p1 ] % 0.47/0.65 (1,1) [1822,1]. true => ~_t253 | _t51 | p2 [ SNF ] % 0.47/0.65 (1,1) [4156,1]. _t32 => box 1 _t642 [ SNF++, 83 ] % 0.47/0.65 (1,1) [4158,1]. _t42 => box 1 _t643 [ SNF++, 104 ] % 0.47/0.65 (1,1) [4214,1]. _t223 => box 1 _t661 [ SNF++, 643 ] % 0.47/0.65 (1,1) [4222,1]. _t44 => box 1 _t591 [ SNF++, 714 ] % 0.47/0.65 (1,1) [4278,1]. _t225 => box 1 _t609 [ SNF++, 1141 ] % 0.47/0.65 (1,1) [4286,1]. _t46 => box 1 _t543 [ SNF++, 1196 ] % 0.47/0.65 (1,1) [4324,1]. _t241 => box 1 _t663 [ SNF++, 1418 ] % 0.47/0.65 (1,1) [4356,1]. _t246 => box 1 _t664 [ SNF++, 1577 ] % 0.47/0.65 (1,1) [4388,1]. _t250 => box 1 _t665 [ SNF++, 1753 ] % 0.47/0.65 (279,1) [4646,1]. _t51 => ~box 1~ _t479 [ SNF++, 1821 ] % 0.47/0.65 (1,1) [4655,1]. true => ~_t669 | _t32 [ SNF++, 2439 ] % 0.47/0.65 (1,1) [4657,1]. true => ~_t670 | _t42 [ SNF++, 2159 ] % 0.47/0.65 (1,1) [4713,1]. true => ~_t688 | _t223 [ SNF++, 2187 ] % 0.47/0.65 (1,1) [4721,1]. true => ~_t616 | _t44 [ SNF++, 2191 ] % 0.47/0.65 (1,1) [4777,1]. true => ~_t634 | _t225 [ SNF++, 2219 ] % 0.47/0.65 (1,1) [4785,1]. true => ~_t567 | _t46 [ SNF++, 2223 ] % 0.47/0.65 (1,1) [4823,1]. true => ~_t690 | _t241 [ SNF++, 2355 ] % 0.47/0.65 (1,1) [4855,1]. true => ~_t691 | _t246 [ SNF++, 2339 ] % 0.47/0.65 (1,1) [4905,1]. true => ~_t692 | _t250 [ SNF++, 2283 ] % 0.47/0.65 (1,1) [4921,1]. true => ~_t693 | _t253 [ SNF++, 2294 ] % 0.47/0.65 (289,1) [5209,1]. true => ~_t694 | ~p2 [ SNF++, 2299 ] % 0.47/0.65 (289,1) [5278,1]. true => ~_t694 | ~_t253 | _t51 [ LRES, 5209, 1822, ~p2 ] % 0.47/0.65 (279,1) [5365,1]. true => ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 | ~_t42 | ~_t32 [ GEN1, 4388, 4324, 4158, 4278, 4286, 4222, 4156, 4214, 4356, 4646, 5364, _t665, _t663, _t643, _t609, _t543, _t591, _t642, _t661, _t664, _t479 ] % 0.47/0.65 (279,1) [5366,1]. true => ~_t669 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 | ~_t42 [ LRES, 5365, 4655, ~_t32 ] % 0.47/0.65 (279,1) [5367,1]. true => ~_t670 | ~_t669 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 | ~_t44 [ LRES, 5366, 4657, ~_t42 ] % 0.47/0.65 (279,1) [5368,1]. true => ~_t670 | ~_t669 | ~_t616 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 | ~_t46 [ LRES, 5367, 4721, ~_t44 ] % 0.47/0.65 (279,1) [5369,1]. true => ~_t670 | ~_t669 | ~_t616 | ~_t567 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 | ~_t51 [ LRES, 5368, 4785, ~_t46 ] % 0.47/0.65 (289,1) [5370,1]. true => ~_t694 | ~_t670 | ~_t669 | ~_t616 | ~_t567 | ~_t253 | ~_t250 | ~_t246 | ~_t241 | ~_t225 | ~_t223 [ LRES, 5369, 5278, ~_t51 ] % 0.47/0.65 (289,1) [5371,1]. true => ~_t694 | ~_t688 | ~_t670 | ~_t669 | ~_t616 | ~_t567 | ~_t253 | ~_t250 | ~_t246 | ~_t241 | ~_t225 [ LRES, 5370, 4713, ~_t223 ] % 0.47/0.65 (289,1) [5372,1]. true => ~_t694 | ~_t688 | ~_t670 | ~_t669 | ~_t634 | ~_t616 | ~_t567 | ~_t253 | ~_t250 | ~_t246 | ~_t241 [ LRES, 5371, 4777, ~_t225 ] % 0.47/0.65 (289,1) [5373,1]. true => ~_t694 | ~_t690 | ~_t688 | ~_t670 | ~_t669 | ~_t634 | ~_t616 | ~_t567 | ~_t253 | ~_t250 | ~_t246 [ LRES, 5372, 4823, ~_t241 ] % 0.47/0.65 (289,1) [5374,1]. true => ~_t694 | ~_t691 | ~_t690 | ~_t688 | ~_t670 | ~_t669 | ~_t634 | ~_t616 | ~_t567 | ~_t253 | ~_t250 [ LRES, 5373, 4855, ~_t246 ] % 0.47/0.65 (289,1) [5375,1]. true => ~_t694 | ~_t692 | ~_t691 | ~_t690 | ~_t688 | ~_t670 | ~_t669 | ~_t634 | ~_t616 | ~_t567 | ~_t253 [ LRES, 5374, 4905, ~_t250 ] % 0.47/0.65 (289,1) [5376,1]. true => ~_t694 | ~_t693 | ~_t692 | ~_t691 | ~_t690 | ~_t688 | ~_t670 | ~_t669 | ~_t634 | ~_t616 | ~_t567 [ LRES, 5375, 4921, ~_t253 ] % 0.47/0.65 (1,1) [81,2]. _t33 => box 1 _t34 [ SNF ] [ SNF++, 3720, _t34 ] % 0.47/0.65 (1,1) [102,2]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 3722, _t44 ] % 0.47/0.65 (1,1) [641,2]. _t224 => box 1 _t225 [ SNF ] [ SNF++, 3778, _t225 ] % 0.47/0.65 (1,1) [712,2]. _t45 => box 1 _t46 [ SNF ] [ SNF++, 3786, _t46 ] % 0.47/0.65 (1,1) [1139,2]. _t226 => box 1 _t227 [ SNF ] [ SNF++, 3842, _t227 ] % 0.47/0.65 (1,1) [1194,2]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 3850, _t48 ] % 0.47/0.65 (1,1) [1416,2]. _t242 => box 1 _t243 [ SNF ] [ SNF++, 3888, _t243 ] % 0.47/0.65 (1,1) [1575,2]. _t247 => box 1 _t248 [ SNF ] [ SNF++, 3914, _t248 ] % 0.47/0.65 (223,1) [1663,2]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 4142, ~p6 ] % 0.47/0.65 (1,1) [1752,2]. true => ~_t251 | _t73 | p1 [ SNF ] % 0.47/0.65 (1,1) [3720,2]. _t33 => box 1 _t615 [ SNF++, 81 ] % 0.47/0.65 (1,1) [3722,2]. _t43 => box 1 _t616 [ SNF++, 102 ] % 0.47/0.65 (1,1) [3778,2]. _t224 => box 1 _t634 [ SNF++, 641 ] % 0.47/0.65 (1,1) [3786,2]. _t45 => box 1 _t567 [ SNF++, 712 ] % 0.47/0.65 (1,1) [3842,2]. _t226 => box 1 _t585 [ SNF++, 1139 ] % 0.47/0.65 (1,1) [3850,2]. _t47 => box 1 _t519 [ SNF++, 1194 ] % 0.47/0.65 (1,1) [3888,2]. _t242 => box 1 _t636 [ SNF++, 1416 ] % 0.47/0.65 (1,1) [3914,2]. _t247 => box 1 _t637 [ SNF++, 1575 ] % 0.47/0.65 (223,1) [4142,2]. _t73 => ~box 1~ _t638 [ SNF++, 1663 ] % 0.47/0.65 (1,1) [4157,2]. true => ~_t642 | _t33 [ SNF++, 83 ] % 0.47/0.65 (1,1) [4159,2]. true => ~_t643 | _t43 [ SNF++, 104 ] % 0.47/0.65 (1,1) [4215,2]. true => ~_t661 | _t224 [ SNF++, 643 ] % 0.47/0.65 (1,1) [4223,2]. true => ~_t591 | _t45 [ SNF++, 714 ] % 0.47/0.65 (1,1) [4279,2]. true => ~_t609 | _t226 [ SNF++, 1141 ] % 0.47/0.65 (1,1) [4287,2]. true => ~_t543 | _t47 [ SNF++, 1196 ] % 0.47/0.65 (1,1) [4325,2]. true => ~_t663 | _t242 [ SNF++, 1418 ] % 0.47/0.65 (1,1) [4357,2]. true => ~_t664 | _t247 [ SNF++, 1577 ] % 0.47/0.65 (1,1) [4389,2]. true => ~_t665 | _t251 [ SNF++, 1753 ] % 0.47/0.65 (279,1) [4647,2]. true => ~_t479 | ~p1 [ SNF++, 1821 ] % 0.47/0.65 (279,1) [5274,2]. true => ~_t479 | ~_t251 | _t73 [ LRES, 4647, 1752, ~p1 ] % 0.47/0.65 (223,1) [5354,2]. true => ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 | ~_t43 | ~_t33 [ GEN1, 3914, 3778, 3720, 3786, 3850, 3842, 3722, 3888, 4142, 5353, _t637, _t634, _t615, _t567, _t519, _t585, _t616, _t636, _t638 ] % 0.47/0.65 (223,1) [5355,2]. true => ~_t642 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 | ~_t43 [ LRES, 5354, 4157, ~_t33 ] % 0.47/0.65 (223,1) [5356,2]. true => ~_t643 | ~_t642 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 | ~_t45 [ LRES, 5355, 4159, ~_t43 ] % 0.47/0.65 (223,1) [5357,2]. true => ~_t643 | ~_t642 | ~_t591 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 | ~_t47 [ LRES, 5356, 4223, ~_t45 ] % 0.47/0.65 (223,1) [5358,2]. true => ~_t643 | ~_t642 | ~_t591 | ~_t543 | ~_t247 | ~_t242 | ~_t226 | ~_t224 | ~_t73 [ LRES, 5357, 4287, ~_t47 ] % 0.47/0.65 (279,1) [5359,2]. true => ~_t643 | ~_t642 | ~_t591 | ~_t543 | ~_t479 | ~_t251 | ~_t247 | ~_t242 | ~_t226 | ~_t224 [ LRES, 5358, 5274, ~_t73 ] % 0.47/0.65 (279,1) [5360,2]. true => ~_t661 | ~_t643 | ~_t642 | ~_t591 | ~_t543 | ~_t479 | ~_t251 | ~_t247 | ~_t242 | ~_t226 [ LRES, 5359, 4215, ~_t224 ] % 0.47/0.65 (279,1) [5361,2]. true => ~_t661 | ~_t643 | ~_t642 | ~_t609 | ~_t591 | ~_t543 | ~_t479 | ~_t251 | ~_t247 | ~_t242 [ LRES, 5360, 4279, ~_t226 ] % 0.47/0.65 (279,1) [5362,2]. true => ~_t663 | ~_t661 | ~_t643 | ~_t642 | ~_t609 | ~_t591 | ~_t543 | ~_t479 | ~_t251 | ~_t247 [ LRES, 5361, 4325, ~_t242 ] % 0.47/0.65 (279,1) [5363,2]. true => ~_t664 | ~_t663 | ~_t661 | ~_t643 | ~_t642 | ~_t609 | ~_t591 | ~_t543 | ~_t479 | ~_t251 [ LRES, 5362, 4357, ~_t247 ] % 0.47/0.65 (279,1) [5364,2]. true => ~_t665 | ~_t664 | ~_t663 | ~_t661 | ~_t643 | ~_t642 | ~_t609 | ~_t591 | ~_t543 | ~_t479 [ LRES, 5363, 4389, ~_t251 ] % 0.47/0.65 (1,1) [79,3]. _t34 => box 1 _t35 [ SNF ] [ SNF++, 3350, _t35 ] % 0.47/0.65 (1,1) [100,3]. _t44 => box 1 _t45 [ SNF ] [ SNF++, 3352, _t45 ] % 0.47/0.65 (1,1) [639,3]. _t225 => box 1 _t226 [ SNF ] [ SNF++, 3408, _t226 ] % 0.47/0.65 (1,1) [710,3]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 3416, _t47 ] % 0.47/0.65 (1,1) [1137,3]. _t227 => box 1 _t228 [ SNF ] [ SNF++, 3472, _t228 ] % 0.47/0.65 (1,1) [1192,3]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 3480, _t49 ] % 0.47/0.65 (1,1) [1414,3]. _t243 => box 1 _t244 [ SNF ] [ SNF++, 3506, _t244 ] % 0.47/0.65 (201,1) [1573,3]. _t95 => ~box 1~ ~p5 [ SNF ] [ SNF++, 3708, ~p5 ] % 0.47/0.65 (1,1) [1574,3]. true => ~_t248 | _t95 | p6 [ SNF ] % 0.47/0.65 (1,1) [3350,3]. _t34 => box 1 _t590 [ SNF++, 79 ] % 0.47/0.65 (1,1) [3352,3]. _t44 => box 1 _t591 [ SNF++, 100 ] % 0.47/0.65 (1,1) [3408,3]. _t225 => box 1 _t609 [ SNF++, 639 ] % 0.47/0.65 (1,1) [3416,3]. _t46 => box 1 _t543 [ SNF++, 710 ] % 0.47/0.65 (1,1) [3472,3]. _t227 => box 1 _t561 [ SNF++, 1137 ] % 0.47/0.65 (1,1) [3480,3]. _t48 => box 1 _t498 [ SNF++, 1192 ] % 0.47/0.65 (1,1) [3506,3]. _t243 => box 1 _t611 [ SNF++, 1414 ] % 0.47/0.65 (201,1) [3708,3]. _t95 => ~box 1~ _t492 [ SNF++, 1573 ] % 0.47/0.65 (1,1) [3721,3]. true => ~_t615 | _t34 [ SNF++, 81 ] % 0.47/0.65 (1,1) [3723,3]. true => ~_t616 | _t44 [ SNF++, 102 ] % 0.47/0.65 (1,1) [3779,3]. true => ~_t634 | _t225 [ SNF++, 641 ] % 0.47/0.65 (1,1) [3787,3]. true => ~_t567 | _t46 [ SNF++, 712 ] % 0.47/0.65 (1,1) [3843,3]. true => ~_t585 | _t227 [ SNF++, 1139 ] % 0.47/0.65 (1,1) [3851,3]. true => ~_t519 | _t48 [ SNF++, 1194 ] % 0.47/0.65 (1,1) [3889,3]. true => ~_t636 | _t243 [ SNF++, 1416 ] % 0.47/0.65 (1,1) [3915,3]. true => ~_t637 | _t248 [ SNF++, 1575 ] % 0.47/0.65 (223,1) [4143,3]. true => ~_t638 | ~p6 [ SNF++, 1663 ] % 0.47/0.65 (223,1) [5227,3]. true => ~_t638 | ~_t248 | _t95 [ LRES, 4143, 1574, ~p6 ] % 0.47/0.65 (201,1) [5344,3]. true => ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 | ~_t44 | ~_t34 [ GEN1, 3506, 3352, 3472, 3480, 3416, 3350, 3408, 3708, 5343, _t611, _t591, _t561, _t498, _t543, _t590, _t609, _t492 ] % 0.47/0.65 (201,1) [5345,3]. true => ~_t615 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 | ~_t44 [ LRES, 5344, 3721, ~_t34 ] % 0.47/0.65 (201,1) [5346,3]. true => ~_t616 | ~_t615 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 | ~_t46 [ LRES, 5345, 3723, ~_t44 ] % 0.47/0.65 (201,1) [5347,3]. true => ~_t616 | ~_t615 | ~_t567 | ~_t243 | ~_t227 | ~_t225 | ~_t95 | ~_t48 [ LRES, 5346, 3787, ~_t46 ] % 0.47/0.65 (201,1) [5348,3]. true => ~_t616 | ~_t615 | ~_t567 | ~_t519 | ~_t243 | ~_t227 | ~_t225 | ~_t95 [ LRES, 5347, 3851, ~_t48 ] % 0.47/0.65 (223,1) [5349,3]. true => ~_t638 | ~_t616 | ~_t615 | ~_t567 | ~_t519 | ~_t248 | ~_t243 | ~_t227 | ~_t225 [ LRES, 5348, 5227, ~_t95 ] % 0.47/0.65 (223,1) [5350,3]. true => ~_t638 | ~_t634 | ~_t616 | ~_t615 | ~_t567 | ~_t519 | ~_t248 | ~_t243 | ~_t227 [ LRES, 5349, 3779, ~_t225 ] % 0.47/0.65 (223,1) [5351,3]. true => ~_t638 | ~_t634 | ~_t616 | ~_t615 | ~_t585 | ~_t567 | ~_t519 | ~_t248 | ~_t243 [ LRES, 5350, 3843, ~_t227 ] % 0.47/0.65 (223,1) [5352,3]. true => ~_t638 | ~_t636 | ~_t634 | ~_t616 | ~_t615 | ~_t585 | ~_t567 | ~_t519 | ~_t248 [ LRES, 5351, 3889, ~_t243 ] % 0.47/0.65 (223,1) [5353,3]. true => ~_t638 | ~_t637 | ~_t636 | ~_t634 | ~_t616 | ~_t615 | ~_t585 | ~_t567 | ~_t519 [ LRES, 5352, 3915, ~_t248 ] % 0.47/0.65 (1,1) [77,4]. _t35 => box 1 _t36 [ SNF ] [ SNF++, 3042, _t36 ] % 0.47/0.65 (1,1) [98,4]. _t45 => box 1 _t46 [ SNF ] [ SNF++, 3044, _t46 ] % 0.47/0.65 (1,1) [637,4]. _t226 => box 1 _t227 [ SNF ] [ SNF++, 3100, _t227 ] % 0.47/0.65 (1,1) [708,4]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 3108, _t48 ] % 0.47/0.65 (1,1) [1135,4]. _t228 => box 1 _t229 [ SNF ] [ SNF++, 3164, _t229 ] % 0.47/0.65 (1,1) [1190,4]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 3172, _t50 ] % 0.47/0.65 (157,1) [1350,4]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 3336, ~p4 ] % 0.47/0.65 (1,1) [1413,4]. true => ~_t244 | _t62 | p5 [ SNF ] % 0.47/0.65 (1,1) [3042,4]. _t35 => box 1 _t566 [ SNF++, 77 ] % 0.47/0.65 (1,1) [3044,4]. _t45 => box 1 _t567 [ SNF++, 98 ] % 0.47/0.65 (1,1) [3100,4]. _t226 => box 1 _t585 [ SNF++, 637 ] % 0.47/0.65 (1,1) [3108,4]. _t47 => box 1 _t519 [ SNF++, 708 ] % 0.47/0.65 (1,1) [3164,4]. _t228 => box 1 _t537 [ SNF++, 1135 ] % 0.47/0.65 (1,1) [3172,4]. _t49 => box 1 _t484 [ SNF++, 1190 ] % 0.47/0.65 (157,1) [3336,4]. _t62 => ~box 1~ _t491 [ SNF++, 1350 ] % 0.47/0.65 (1,1) [3351,4]. true => ~_t590 | _t35 [ SNF++, 79 ] % 0.47/0.65 (1,1) [3353,4]. true => ~_t591 | _t45 [ SNF++, 100 ] % 0.47/0.65 (1,1) [3409,4]. true => ~_t609 | _t226 [ SNF++, 639 ] % 0.47/0.65 (1,1) [3417,4]. true => ~_t543 | _t47 [ SNF++, 710 ] % 0.47/0.65 (1,1) [3473,4]. true => ~_t561 | _t228 [ SNF++, 1137 ] % 0.47/0.65 (1,1) [3481,4]. true => ~_t498 | _t49 [ SNF++, 1192 ] % 0.47/0.65 (1,1) [3507,4]. true => ~_t611 | _t244 [ SNF++, 1414 ] % 0.47/0.65 (201,1) [3709,4]. true => ~_t492 | ~p5 [ SNF++, 1573 ] % 0.47/0.65 (201,1) [5223,4]. true => ~_t492 | ~_t244 | _t62 [ LRES, 3709, 1413, ~p5 ] % 0.47/0.65 (157,1) [5335,4]. true => ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 | ~_t45 | ~_t35 [ GEN1, 3100, 3042, 3108, 3172, 3164, 3044, 3336, 5334, _t585, _t566, _t519, _t484, _t537, _t567, _t491 ] % 0.47/0.65 (157,1) [5336,4]. true => ~_t590 | ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 | ~_t45 [ LRES, 5335, 3351, ~_t35 ] % 0.47/0.65 (157,1) [5337,4]. true => ~_t591 | ~_t590 | ~_t228 | ~_t226 | ~_t62 | ~_t49 | ~_t47 [ LRES, 5336, 3353, ~_t45 ] % 0.47/0.65 (157,1) [5338,4]. true => ~_t591 | ~_t590 | ~_t543 | ~_t228 | ~_t226 | ~_t62 | ~_t49 [ LRES, 5337, 3417, ~_t47 ] % 0.47/0.65 (157,1) [5339,4]. true => ~_t591 | ~_t590 | ~_t543 | ~_t498 | ~_t228 | ~_t226 | ~_t62 [ LRES, 5338, 3481, ~_t49 ] % 0.47/0.65 (201,1) [5340,4]. true => ~_t591 | ~_t590 | ~_t543 | ~_t498 | ~_t492 | ~_t244 | ~_t228 | ~_t226 [ LRES, 5339, 5223, ~_t62 ] % 0.47/0.65 (201,1) [5341,4]. true => ~_t609 | ~_t591 | ~_t590 | ~_t543 | ~_t498 | ~_t492 | ~_t244 | ~_t228 [ LRES, 5340, 3409, ~_t226 ] % 0.47/0.65 (201,1) [5342,4]. true => ~_t609 | ~_t591 | ~_t590 | ~_t561 | ~_t543 | ~_t498 | ~_t492 | ~_t244 [ LRES, 5341, 3473, ~_t228 ] % 0.47/0.65 (201,1) [5343,4]. true => ~_t611 | ~_t609 | ~_t591 | ~_t590 | ~_t561 | ~_t543 | ~_t498 | ~_t492 [ LRES, 5342, 3507, ~_t244 ] % 0.47/0.65 (1,1) [75,5]. _t36 => box 1 _t37 [ SNF ] [ SNF++, 2800, _t37 ] % 0.47/0.65 (1,1) [96,5]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 2802, _t47 ] % 0.47/0.65 (1,1) [635,5]. _t227 => box 1 _t228 [ SNF ] [ SNF++, 2858, _t228 ] % 0.47/0.65 (1,1) [706,5]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 2866, _t49 ] % 0.47/0.65 (1,1) [1133,5]. _t229 => box 1 _t230 [ SNF ] [ SNF++, 2904, _t230 ] % 0.47/0.65 (131,1) [1188,5]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 3030, ~p1 ] % 0.47/0.65 (1,1) [1189,5]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.47/0.65 (1,1) [2800,5]. _t36 => box 1 _t542 [ SNF++, 75 ] % 0.47/0.65 (1,1) [2802,5]. _t46 => box 1 _t543 [ SNF++, 96 ] % 0.47/0.65 (1,1) [2858,5]. _t227 => box 1 _t561 [ SNF++, 635 ] % 0.47/0.65 (1,1) [2866,5]. _t48 => box 1 _t498 [ SNF++, 706 ] % 0.47/0.65 (1,1) [2904,5]. _t229 => box 1 _t513 [ SNF++, 1133 ] % 0.47/0.65 (131,1) [3030,5]. _t51 => ~box 1~ _t479 [ SNF++, 1188 ] % 0.47/0.65 (1,1) [3043,5]. true => ~_t566 | _t36 [ SNF++, 77 ] % 0.47/0.65 (1,1) [3045,5]. true => ~_t567 | _t46 [ SNF++, 98 ] % 0.47/0.65 (1,1) [3101,5]. true => ~_t585 | _t227 [ SNF++, 637 ] % 0.47/0.65 (1,1) [3109,5]. true => ~_t519 | _t48 [ SNF++, 708 ] % 0.47/0.65 (1,1) [3165,5]. true => ~_t537 | _t229 [ SNF++, 1135 ] % 0.47/0.65 (1,1) [3173,5]. true => ~_t484 | _t50 [ SNF++, 1190 ] % 0.47/0.65 (157,1) [3337,5]. true => ~_t491 | ~p4 [ SNF++, 1350 ] % 0.47/0.65 (157,1) [5222,5]. true => ~_t491 | _t51 | ~_t50 [ LRES, 3337, 1189, ~p4 ] % 0.47/0.65 (157,1) [5292,5]. true => ~_t491 | ~_t484 | _t51 [ LRES, 5222, 3173, ~_t50 ] % 0.47/0.65 (131,1) [5328,5]. true => ~_t229 | ~_t227 | ~_t51 | ~_t48 | ~_t46 | ~_t36 [ GEN1, 2858, 2800, 2866, 2904, 2802, 3030, 5327, _t561, _t542, _t498, _t513, _t543, _t479 ] % 0.47/0.65 (131,1) [5329,5]. true => ~_t566 | ~_t229 | ~_t227 | ~_t51 | ~_t48 | ~_t46 [ LRES, 5328, 3043, ~_t36 ] % 0.47/0.65 (131,1) [5330,5]. true => ~_t567 | ~_t566 | ~_t229 | ~_t227 | ~_t51 | ~_t48 [ LRES, 5329, 3045, ~_t46 ] % 0.47/0.65 (131,1) [5331,5]. true => ~_t567 | ~_t566 | ~_t519 | ~_t229 | ~_t227 | ~_t51 [ LRES, 5330, 3109, ~_t48 ] % 0.47/0.65 (157,1) [5332,5]. true => ~_t567 | ~_t566 | ~_t519 | ~_t491 | ~_t484 | ~_t229 | ~_t227 [ LRES, 5331, 5292, ~_t51 ] % 0.47/0.65 (157,1) [5333,5]. true => ~_t585 | ~_t567 | ~_t566 | ~_t519 | ~_t491 | ~_t484 | ~_t229 [ LRES, 5332, 3101, ~_t227 ] % 0.47/0.65 (157,1) [5334,5]. true => ~_t585 | ~_t567 | ~_t566 | ~_t537 | ~_t519 | ~_t491 | ~_t484 [ LRES, 5333, 3165, ~_t229 ] % 0.47/0.65 (1,1) [73,6]. _t37 => box 1 _t38 [ SNF ] [ SNF++, 2620, _t38 ] % 0.47/0.65 (1,1) [94,6]. _t47 => box 1 _t48 [ SNF ] [ SNF++, 2622, _t48 ] % 0.47/0.65 (1,1) [633,6]. _t228 => box 1 _t229 [ SNF ] [ SNF++, 2678, _t229 ] % 0.47/0.65 (1,1) [704,6]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 2686, _t50 ] % 0.47/0.65 (93,1) [916,6]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 2786, ~p4 ] % 0.47/0.65 (1,1) [1132,6]. true => ~_t230 | _t62 | p1 [ SNF ] % 0.47/0.65 (1,1) [2620,6]. _t37 => box 1 _t518 [ SNF++, 73 ] % 0.47/0.65 (1,1) [2622,6]. _t47 => box 1 _t519 [ SNF++, 94 ] % 0.47/0.65 (1,1) [2678,6]. _t228 => box 1 _t537 [ SNF++, 633 ] % 0.47/0.65 (1,1) [2686,6]. _t49 => box 1 _t484 [ SNF++, 704 ] % 0.47/0.65 (93,1) [2786,6]. _t62 => ~box 1~ _t491 [ SNF++, 916 ] % 0.47/0.65 (1,1) [2801,6]. true => ~_t542 | _t37 [ SNF++, 75 ] % 0.47/0.65 (1,1) [2803,6]. true => ~_t543 | _t47 [ SNF++, 96 ] % 0.47/0.65 (1,1) [2859,6]. true => ~_t561 | _t228 [ SNF++, 635 ] % 0.47/0.65 (1,1) [2867,6]. true => ~_t498 | _t49 [ SNF++, 706 ] % 0.47/0.65 (1,1) [2905,6]. true => ~_t513 | _t230 [ SNF++, 1133 ] % 0.47/0.65 (131,1) [3031,6]. true => ~_t479 | ~p1 [ SNF++, 1188 ] % 0.47/0.65 (131,1) [5218,6]. true => ~_t479 | ~_t230 | _t62 [ LRES, 3031, 1132, ~p1 ] % 0.47/0.65 (93,1) [5321,6]. true => ~_t228 | ~_t62 | ~_t49 | ~_t47 | ~_t37 [ GEN1, 2678, 2620, 2686, 2622, 2786, 5320, _t537, _t518, _t484, _t519, _t491 ] % 0.47/0.65 (93,1) [5322,6]. true => ~_t542 | ~_t228 | ~_t62 | ~_t49 | ~_t47 [ LRES, 5321, 2801, ~_t37 ] % 0.47/0.65 (93,1) [5323,6]. true => ~_t543 | ~_t542 | ~_t228 | ~_t62 | ~_t49 [ LRES, 5322, 2803, ~_t47 ] % 0.47/0.65 (93,1) [5324,6]. true => ~_t543 | ~_t542 | ~_t498 | ~_t228 | ~_t62 [ LRES, 5323, 2867, ~_t49 ] % 0.47/0.65 (131,1) [5325,6]. true => ~_t543 | ~_t542 | ~_t498 | ~_t479 | ~_t230 | ~_t228 [ LRES, 5324, 5218, ~_t62 ] % 0.47/0.65 (131,1) [5326,6]. true => ~_t561 | ~_t543 | ~_t542 | ~_t498 | ~_t479 | ~_t230 [ LRES, 5325, 2859, ~_t228 ] % 0.47/0.65 (131,1) [5327,6]. true => ~_t561 | ~_t543 | ~_t542 | ~_t513 | ~_t498 | ~_t479 [ LRES, 5326, 2905, ~_t230 ] % 0.47/0.65 (1,1) [71,7]. _t38 => box 1 _t39 [ SNF ] [ SNF++, 2506, _t39 ] % 0.47/0.65 (1,1) [92,7]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 2508, _t49 ] % 0.47/0.65 (1,1) [631,7]. _t229 => box 1 _t230 [ SNF ] [ SNF++, 2546, _t230 ] % 0.47/0.65 (67,1) [702,7]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 2608, ~p1 ] % 0.47/0.65 (1,1) [703,7]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.47/0.65 (1,1) [2506,7]. _t38 => box 1 _t497 [ SNF++, 71 ] % 0.47/0.65 (1,1) [2508,7]. _t48 => box 1 _t498 [ SNF++, 92 ] % 0.47/0.65 (1,1) [2546,7]. _t229 => box 1 _t513 [ SNF++, 631 ] % 0.47/0.65 (67,1) [2608,7]. _t51 => ~box 1~ _t479 [ SNF++, 702 ] % 0.47/0.65 (1,1) [2621,7]. true => ~_t518 | _t38 [ SNF++, 73 ] % 0.47/0.65 (1,1) [2623,7]. true => ~_t519 | _t48 [ SNF++, 94 ] % 0.47/0.65 (1,1) [2679,7]. true => ~_t537 | _t229 [ SNF++, 633 ] % 0.47/0.65 (1,1) [2687,7]. true => ~_t484 | _t50 [ SNF++, 704 ] % 0.47/0.65 (93,1) [2787,7]. true => ~_t491 | ~p4 [ SNF++, 916 ] % 0.47/0.65 (93,1) [5217,7]. true => ~_t491 | _t51 | ~_t50 [ LRES, 2787, 703, ~p4 ] % 0.47/0.65 (93,1) [5291,7]. true => ~_t491 | ~_t484 | _t51 [ LRES, 5217, 2687, ~_t50 ] % 0.47/0.65 (67,1) [5316,7]. true => ~_t229 | ~_t51 | ~_t48 | ~_t38 [ GEN1, 2546, 2506, 2508, 2608, 5315, _t513, _t497, _t498, _t479 ] % 0.47/0.65 (67,1) [5317,7]. true => ~_t518 | ~_t229 | ~_t51 | ~_t48 [ LRES, 5316, 2621, ~_t38 ] % 0.47/0.65 (67,1) [5318,7]. true => ~_t519 | ~_t518 | ~_t229 | ~_t51 [ LRES, 5317, 2623, ~_t48 ] % 0.47/0.65 (93,1) [5319,7]. true => ~_t519 | ~_t518 | ~_t491 | ~_t484 | ~_t229 [ LRES, 5318, 5291, ~_t51 ] % 0.47/0.65 (93,1) [5320,7]. true => ~_t537 | ~_t519 | ~_t518 | ~_t491 | ~_t484 [ LRES, 5319, 2679, ~_t229 ] % 0.47/0.65 (1,1) [69,8]. _t39 => box 1 _t40 [ SNF ] [ SNF++, 2454, _t40 ] % 0.47/0.65 (1,1) [90,8]. _t49 => box 1 _t50 [ SNF ] [ SNF++, 2456, _t50 ] % 0.47/0.65 (29,1) [354,8]. _t62 => ~box 1~ ~p4 [ SNF ] [ SNF++, 2492, ~p4 ] % 0.47/0.65 (1,1) [630,8]. true => ~_t230 | _t62 | p1 [ SNF ] % 0.47/0.65 (1,1) [2454,8]. _t39 => box 1 _t483 [ SNF++, 69 ] % 0.47/0.65 (1,1) [2456,8]. _t49 => box 1 _t484 [ SNF++, 90 ] % 0.47/0.65 (29,1) [2492,8]. _t62 => ~box 1~ _t491 [ SNF++, 354 ] % 0.47/0.65 (1,1) [2507,8]. true => ~_t497 | _t39 [ SNF++, 71 ] % 0.47/0.65 (1,1) [2509,8]. true => ~_t498 | _t49 [ SNF++, 92 ] % 0.47/0.65 (1,1) [2547,8]. true => ~_t513 | _t230 [ SNF++, 631 ] % 0.47/0.65 (67,1) [2609,8]. true => ~_t479 | ~p1 [ SNF++, 702 ] % 0.47/0.65 (67,1) [5213,8]. true => ~_t479 | ~_t230 | _t62 [ LRES, 2609, 630, ~p1 ] % 0.47/0.65 (29,1) [5311,8]. true => ~_t62 | ~_t49 | ~_t39 [ GEN1, 2456, 2454, 2492, 5310, _t484, _t483, _t491 ] % 0.47/0.65 (29,1) [5312,8]. true => ~_t497 | ~_t62 | ~_t49 [ LRES, 5311, 2507, ~_t39 ] % 0.47/0.65 (29,1) [5313,8]. true => ~_t498 | ~_t497 | ~_t62 [ LRES, 5312, 2509, ~_t49 ] % 0.47/0.65 (67,1) [5314,8]. true => ~_t498 | ~_t497 | ~_t479 | ~_t230 [ LRES, 5313, 5213, ~_t62 ] % 0.47/0.65 (67,1) [5315,8]. true => ~_t513 | ~_t498 | ~_t497 | ~_t479 [ LRES, 5314, 2547, ~_t230 ] % 0.47/0.65 (1,1) [67,9]. _t40 => box 1 p1 [ SNF ] [ SNF++, 2442, p1 ] % 0.47/0.65 (3,1) [88,9]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 2446, ~p1 ] % 0.47/0.65 (1,1) [89,9]. true => _t51 | ~_t50 | p4 [ SNF ] % 0.47/0.65 (1,1) [2442,9]. _t40 => box 1 _t478 [ SNF++, 67 ] % 0.47/0.65 (3,1) [2446,9]. _t51 => ~box 1~ _t479 [ SNF++, 88 ] % 0.47/0.65 (1,1) [2455,9]. true => ~_t483 | _t40 [ SNF++, 69 ] % 0.47/0.65 (1,1) [2457,9]. true => ~_t484 | _t50 [ SNF++, 90 ] % 0.47/0.65 (29,1) [2493,9]. true => ~_t491 | ~p4 [ SNF++, 354 ] % 0.47/0.65 (29,1) [5212,9]. true => ~_t491 | _t51 | ~_t50 [ LRES, 2493, 89, ~p4 ] % 0.47/0.65 (3,1) [5256,9]. true => ~_t51 | ~_t40 [ GEN1, 2442, 2446, 5233, _t478, _t479 ] % 0.47/0.65 (3,1) [5290,9]. true => ~_t483 | ~_t51 [ LRES, 5256, 2455, ~_t40 ] % 0.47/0.65 (29,1) [5301,9]. true => ~_t491 | ~_t484 | _t51 [ LRES, 5212, 2457, ~_t50 ] % 0.47/0.65 (29,1) [5310,9]. true => ~_t491 | ~_t484 | ~_t483 [ LRES, 5301, 5290, _t51 ] % 0.47/0.65 (1,1) [2443,10]. true => ~_t478 | p1 [ SNF++, 67 ] % 0.47/0.65 (3,1) [2447,10]. true => ~_t479 | ~p1 [ SNF++, 88 ] % 0.47/0.65 (3,1) [5233,10]. true => ~_t479 | ~_t478 [ LRES, 2447, 2443, ~p1 ] % 0.47/0.65 % SZS output end Refutation % 0.47/0.66 % KSP exiting %------------------------------------------------------------------------------