%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP037_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:54 PM UTC 2026 % Result : Theorem 83.15s 83.35s % Output : Refutation 87.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP037_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.18/0.33 % Computer : n029.cluster.edu % 0.18/0.33 % Model : x86_64 x86_64 % 0.18/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.33 % Memory : 8042.1875MB % 0.18/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.33 % CPULimit : 300 % 0.18/0.33 % WCLimit : 300 % 0.18/0.33 % DateTime : Mon May 4 16:19:59 EDT 2026 % 0.18/0.34 % CPUTime : % 0.35/0.61 ----KSP format--- % 0.35/0.61 set(box,TRANS). % 0.35/0.61 usable(formulas). % 0.35/0.61 true. % 0.35/0.61 end_of_list. % 0.35/0.61 sos(formulas). % 0.35/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.35/0.61 end_of_list. % 0.35/0.61 ----------------- % 0.35/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.Zo2a1unoF0/theBenchmark.ksp % 83.15/83.35 % 83.15/83.35 % SZS status Theorem % 83.15/83.35 % 83.15/83.35 ***************** % 83.15/83.35 FOUND PROOF 1 % 83.15/83.35 ***************** % 83.15/83.35 % SZS output start Refutation % 83.15/83.35 % 83.15/83.35 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 83.15/83.35 (1,1) [73474,0]. _t11 => box 1 _t12 [ SNF ] [ Backward Subsumption, 2297624 ] % 83.15/83.35 (1,1) [77495,0]. true => _t11 | ~_t0 [ SNF ] [ Backward Subsumption, 2297335 ] % 83.15/83.35 (1,1) [2238500,0]. _t249 => box 1 _t250 [ SNF ] [ Backward Subsumption, 2297466 ] % 83.15/83.35 (1,1) [2242521,0]. true => _t249 | ~_t0 [ SNF ] [ Backward Subsumption, 2297208 ] % 83.15/83.35 (1,1) [2269357,0]. _t71 => box 1 _t71 [ Axiom 4 ] [ Backward Subsumption, 2297471 ] % 83.15/83.35 (1,1) [2272038,0]. true => _t71 | ~_t0 [ SNF ] [ Backward Subsumption, 2297200 ] % 83.15/83.35 (1,1) [2285463,0]. _t252 => box 1 _t253 [ SNF ] [ Backward Subsumption, 2297477 ] % 83.15/83.35 (1,1) [2289484,0]. true => _t252 | ~_t0 [ SNF ] [ Backward Subsumption, 2297194 ] % 83.15/83.35 (289,1) [2294857,0]. _t84 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 2297482 ] % 83.15/83.35 (1,1) [2294858,0]. true => _t84 | ~_t0 [ SNF ] [ Backward Subsumption, 2297189 ] % 83.15/83.35 (1,1) [2297189,0]. true => _t84 [ Unit Resolution, 3, 2294858, _t0 ] [ Modal Level Pure Literal Elimination, _t84 ] % 83.15/83.35 (1,1) [2297194,0]. true => _t252 [ Unit Resolution, 3, 2289484, _t0 ] [ Modal Level Pure Literal Elimination, _t252 ] % 83.15/83.35 (1,1) [2297200,0]. true => _t71 [ Unit Resolution, 3, 2272038, _t0 ] [ Modal Level Pure Literal Elimination, _t71 ] % 83.15/83.35 (1,1) [2297208,0]. true => _t249 [ Unit Resolution, 3, 2242521, _t0 ] [ Modal Level Pure Literal Elimination, _t249 ] % 83.15/83.35 (1,1) [2297335,0]. true => _t11 [ Unit Resolution, 3, 77495, _t0 ] [ Modal Level Pure Literal Elimination, _t11 ] % 83.15/83.35 (1,1) [2297466,0]. true => box 1 _t250 [ LHS Unit Resolution, 2297208, 2238500, _t249 ] [ SNF++, 3504035, _t250 ] % 83.15/83.35 (1,1) [2297471,0]. true => box 1 _t71 [ LHS Unit Resolution, 2297200, 2269357, _t71 ] [ SNF++, 3504005, _t71 ] % 83.15/83.35 (1,1) [2297477,0]. true => box 1 _t253 [ LHS Unit Resolution, 2297194, 2285463, _t252 ] [ SNF++, 3504055, _t253 ] % 83.15/83.35 (289,1) [2297482,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 2297189, 2294857, _t84 ] [ SNF++, 3504067, ~p2 ] % 83.15/83.35 (1,1) [2297624,0]. true => box 1 _t12 [ LHS Unit Resolution, 2297335, 73474, _t11 ] [ SNF++, 3503691, _t12 ] % 83.15/83.35 (1,1) [3503691,0]. true => box 1 _t275 [ SNF++, 2297624 ] % 83.15/83.35 (1,1) [3504005,0]. true => box 1 _t320 [ SNF++, 2297471 ] % 83.15/83.35 (1,1) [3504035,0]. true => box 1 _t502 [ SNF++, 2297466 ] % 83.15/83.35 (1,1) [3504055,0]. true => box 1 _t504 [ SNF++, 2297477 ] % 83.15/83.35 (289,1) [3504067,0]. true => ~box 1~ _t509 [ SNF++, 2297482 ] % 83.15/83.35 (289,1) [4046047,0]. true => false [ GEN1, 3504055, 3504005, 3503691, 3504035, 3504067, 4040716, _t504, _t320, _t275, _t502, _t509 ] % 83.15/83.35 (1,1) [69456,1]. _t12 => box 1 _t13 [ SNF ] [ SNF++, 3502985, _t13 ] % 83.15/83.35 (1,1) [2175468,1]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3503635, _t71 ] % 83.15/83.35 (1,1) [2178151,1]. _t70 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3503633, _t71 ] % 83.15/83.35 (1,1) [2234482,1]. _t250 => box 1 _t251 [ SNF ] [ SNF++, 3503661, _t251 ] % 83.15/83.35 (279,1) [2285461,1]. _t51 => ~box 1~ ~p1 [ SNF ] [ SNF++, 3503685, ~p1 ] % 83.15/83.35 (1,1) [2285462,1]. true => ~_t253 | _t51 | p2 [ SNF ] % 83.15/83.35 (1,1) [3502985,1]. _t12 => box 1 _t274 [ SNF++, 69456 ] % 83.15/83.35 (1,1) [3503635,1]. _t71 => box 1 _t320 [ SNF++, 2175468 ] % 83.15/83.35 (1,1) [3503661,1]. _t250 => box 1 _t501 [ SNF++, 2234482 ] % 83.15/83.35 (279,1) [3503685,1]. _t51 => ~box 1~ _t506 [ SNF++, 2285461 ] % 83.15/83.35 (1,1) [3503692,1]. true => ~_t275 | _t12 [ SNF++, 2297624 ] % 83.15/83.35 (1,1) [3504006,1]. true => ~_t320 | _t71 [ SNF++, 2297471 ] % 83.15/83.35 (1,1) [3504036,1]. true => ~_t502 | _t250 [ SNF++, 2297466 ] % 83.15/83.35 (1,1) [3504056,1]. true => ~_t504 | _t253 [ SNF++, 2297477 ] % 83.15/83.35 (289,1) [3504068,1]. true => ~_t509 | ~p2 [ SNF++, 2297482 ] % 83.15/83.35 (289,1) [3525466,1]. true => ~_t509 | ~_t253 | _t51 [ LRES, 3504068, 2285462, ~p2 ] % 83.15/83.35 (279,1) [4007333,1]. true => ~_t250 | ~_t71 | ~_t51 | ~_t12 [ GEN1, 3503661, 3502985, 3503635, 3503685, 4003304, _t501, _t274, _t320, _t506 ] % 83.15/83.35 (279,1) [4008677,1]. true => ~_t275 | ~_t250 | ~_t71 | ~_t51 [ LRES, 4007333, 3503692, ~_t12 ] % 83.15/83.35 (289,1) [4012701,1]. true => ~_t509 | ~_t275 | ~_t253 | ~_t250 | ~_t71 [ LRES, 4008677, 3525466, ~_t51 ] % 83.15/83.35 (289,1) [4019380,1]. true => ~_t509 | ~_t320 | ~_t275 | ~_t253 | ~_t250 [ LRES, 4012701, 3504006, ~_t71 ] % 83.15/83.35 (289,1) [4024713,1]. true => ~_t509 | ~_t502 | ~_t320 | ~_t275 | ~_t253 [ LRES, 4019380, 3504036, ~_t250 ] % 83.15/83.35 (289,1) [4040716,1]. true => ~_t509 | ~_t504 | ~_t502 | ~_t320 | ~_t275 [ LRES, 4024713, 3504056, ~_t253 ] % 83.15/83.35 (1,1) [65441,2]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 3502239, _t14 ] % 83.15/83.35 (223,1) [2159370,2]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3502969, ~p6 ] % 83.15/83.35 (1,1) [2175470,2]. _t71 => box 1 _t72 [ Axiom 4 ] [ SNF++, 3502949, _t72 ] % 83.15/83.35 (1,1) [2175471,2]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3502843, _t71 ] % 83.15/83.35 (1,1) [2234481,2]. true => ~_t251 | _t73 | p1 [ SNF ] % 83.15/83.35 (1,1) [3502239,2]. _t13 => box 1 _t273 [ SNF++, 65441 ] % 83.15/83.35 (1,1) [3502843,2]. _t71 => box 1 _t320 [ SNF++, 2175471 ] % 83.15/83.35 (1,1) [3502949,2]. _t71 => box 1 _t319 [ SNF++, 2175470 ] % 83.15/83.35 (223,1) [3502969,2]. _t73 => ~box 1~ _t508 [ SNF++, 2159370 ] % 83.15/83.35 (1,1) [3502986,2]. true => ~_t274 | _t13 [ SNF++, 69456 ] % 83.15/83.35 (1,1) [3503634,2]. true => ~_t320 | _t71 [ SNF++, 2178151 ] % 83.15/83.35 (1,1) [3503662,2]. true => ~_t501 | _t251 [ SNF++, 2234482 ] % 83.15/83.35 (279,1) [3503686,2]. true => ~_t506 | ~p1 [ SNF++, 2285461 ] % 83.15/83.35 (279,1) [3525462,2]. true => ~_t506 | ~_t251 | _t73 [ LRES, 3503686, 2234481, ~p1 ] % 83.15/83.35 (223,1) [3995251,2]. true => ~_t73 | ~_t71 | ~_t13 [ GEN1, 3502843, 3502239, 3502949, 3502969, 3981854, _t320, _t273, _t319, _t508 ] % 83.15/83.35 (223,1) [3995252,2]. true => ~_t274 | ~_t73 | ~_t71 [ LRES, 3995251, 3502986, ~_t13 ] % 83.15/83.35 (223,1) [3996595,2]. true => ~_t320 | ~_t274 | ~_t73 [ LRES, 3995252, 3503634, ~_t71 ] % 83.15/83.35 (279,1) [3997936,2]. true => ~_t506 | ~_t320 | ~_t274 | ~_t251 [ LRES, 3996595, 3525462, ~_t73 ] % 83.15/83.35 (279,1) [4003304,2]. true => ~_t506 | ~_t501 | ~_t320 | ~_t274 [ LRES, 3997936, 3503662, ~_t251 ] % 83.15/83.35 (1,1) [61429,3]. _t14 => box 1 _t15 [ SNF ] [ SNF++, 3501447, _t15 ] % 83.15/83.35 (1,1) [1879305,3]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3502135, _t72 ] % 83.15/83.35 (1,1) [1879306,3]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3502071, _t71 ] % 83.15/83.35 (197,1) [2053482,3]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3502217, ~p6 ] % 83.15/83.35 (1,1) [2175469,3]. true => _t73 | ~_t72 | p6 [ Axiom 4 ] % 83.15/83.35 (1,1) [3501447,3]. _t14 => box 1 _t272 [ SNF++, 61429 ] % 83.15/83.35 (1,1) [3502071,3]. _t71 => box 1 _t320 [ SNF++, 1879306 ] % 83.15/83.35 (1,1) [3502135,3]. _t71 => box 1 _t319 [ SNF++, 1879305 ] % 83.15/83.35 (197,1) [3502217,3]. _t73 => ~box 1~ _t508 [ SNF++, 2053482 ] % 83.15/83.35 (1,1) [3502240,3]. true => ~_t273 | _t14 [ SNF++, 65441 ] % 83.15/83.35 (1,1) [3502844,3]. true => ~_t320 | _t71 [ SNF++, 2175471 ] % 83.15/83.35 (1,1) [3502950,3]. true => ~_t319 | _t72 [ SNF++, 2175470 ] % 83.15/83.35 (223,1) [3502970,3]. true => ~_t508 | ~p6 [ SNF++, 2159370 ] % 83.15/83.35 (223,1) [3512084,3]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3502970, 2175469, ~p6 ] % 83.15/83.35 (223,1) [3545521,3]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3512084, 3502950, ~_t72 ] % 83.15/83.35 (197,1) [3977832,3]. true => ~_t73 | ~_t71 | ~_t14 [ GEN1, 3502071, 3501447, 3502135, 3502217, 3975145, _t320, _t272, _t319, _t508 ] % 83.15/83.35 (197,1) [3979176,3]. true => ~_t273 | ~_t73 | ~_t71 [ LRES, 3977832, 3502240, ~_t14 ] % 83.15/83.35 (197,1) [3980515,3]. true => ~_t320 | ~_t273 | ~_t73 [ LRES, 3979176, 3502844, ~_t71 ] % 83.15/83.35 (223,1) [3981854,3]. true => ~_t508 | ~_t320 | ~_t319 | ~_t273 [ LRES, 3980515, 3545521, ~_t73 ] % 83.15/83.35 (1,1) [57420,4]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 3500631, _t16 ] % 83.15/83.35 (1,1) [1689103,4]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3501345, _t72 ] % 83.15/83.35 (1,1) [1689104,4]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3501263, _t71 ] % 83.15/83.35 (159,1) [1847140,4]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3501421, ~p6 ] % 83.15/83.35 (1,1) [1879304,4]. true => _t73 | ~_t72 | p6 [ SNF ] % 83.15/83.35 (1,1) [3500631,4]. _t15 => box 1 _t271 [ SNF++, 57420 ] % 83.15/83.35 (1,1) [3501263,4]. _t71 => box 1 _t320 [ SNF++, 1689104 ] % 83.15/83.35 (1,1) [3501345,4]. _t71 => box 1 _t319 [ SNF++, 1689103 ] % 83.15/83.35 (159,1) [3501421,4]. _t73 => ~box 1~ _t508 [ SNF++, 1847140 ] % 83.15/83.35 (1,1) [3501448,4]. true => ~_t272 | _t15 [ SNF++, 61429 ] % 83.15/83.35 (1,1) [3502072,4]. true => ~_t320 | _t71 [ SNF++, 1879306 ] % 83.15/83.35 (1,1) [3502136,4]. true => ~_t319 | _t72 [ SNF++, 1879305 ] % 83.15/83.35 (197,1) [3502218,4]. true => ~_t508 | ~p6 [ SNF++, 2053482 ] % 83.15/83.35 (197,1) [3518768,4]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3502218, 1879304, ~p6 ] % 83.15/83.35 (197,1) [3552186,4]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3518768, 3502136, ~_t72 ] % 83.15/83.35 (159,1) [3971126,4]. true => ~_t73 | ~_t71 | ~_t15 [ GEN1, 3501263, 3500631, 3501345, 3501421, 3957743, _t320, _t271, _t319, _t508 ] % 83.15/83.35 (159,1) [3972465,4]. true => ~_t272 | ~_t73 | ~_t71 [ LRES, 3971126, 3501448, ~_t15 ] % 83.15/83.35 (159,1) [3973804,4]. true => ~_t320 | ~_t272 | ~_t73 [ LRES, 3972465, 3502072, ~_t71 ] % 83.15/83.35 (197,1) [3975145,4]. true => ~_t508 | ~_t320 | ~_t319 | ~_t272 [ LRES, 3973804, 3552186, ~_t73 ] % 83.15/83.35 (1,1) [53414,5]. _t16 => box 1 _t17 [ SNF ] [ SNF++, 3499795, _t17 ] % 83.15/83.35 (1,1) [1421324,5]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3500511, _t72 ] % 83.15/83.35 (1,1) [1421325,5]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3500447, _t71 ] % 83.15/83.35 (135,1) [1689101,5]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3500603, ~p6 ] % 83.15/83.35 (1,1) [1689102,5]. true => _t73 | ~_t72 | p6 [ SNF ] % 83.15/83.35 (1,1) [3499795,5]. _t16 => box 1 _t270 [ SNF++, 53414 ] % 83.15/83.35 (1,1) [3500447,5]. _t71 => box 1 _t320 [ SNF++, 1421325 ] % 83.15/83.35 (1,1) [3500511,5]. _t71 => box 1 _t319 [ SNF++, 1421324 ] % 83.15/83.35 (135,1) [3500603,5]. _t73 => ~box 1~ _t508 [ SNF++, 1689101 ] % 83.15/83.35 (1,1) [3500632,5]. true => ~_t271 | _t16 [ SNF++, 57420 ] % 83.15/83.35 (1,1) [3501264,5]. true => ~_t320 | _t71 [ SNF++, 1689104 ] % 83.15/83.35 (1,1) [3501346,5]. true => ~_t319 | _t72 [ SNF++, 1689103 ] % 83.15/83.35 (159,1) [3501422,5]. true => ~_t508 | ~p6 [ SNF++, 1847140 ] % 83.15/83.35 (159,1) [3518764,5]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3501422, 1689102, ~p6 ] % 83.15/83.35 (159,1) [3552189,5]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3518764, 3501346, ~_t72 ] % 83.15/83.35 (135,1) [3955065,5]. true => ~_t73 | ~_t71 | ~_t16 [ GEN1, 3500447, 3499795, 3500511, 3500603, 3933677, _t320, _t270, _t319, _t508 ] % 83.15/83.35 (135,1) [3955067,5]. true => ~_t271 | ~_t73 | ~_t71 [ LRES, 3955065, 3500632, ~_t16 ] % 83.15/83.35 (135,1) [3956405,5]. true => ~_t320 | ~_t271 | ~_t73 [ LRES, 3955067, 3501264, ~_t71 ] % 83.15/83.35 (159,1) [3957743,5]. true => ~_t508 | ~_t320 | ~_t319 | ~_t271 [ LRES, 3956405, 3552189, ~_t73 ] % 83.15/83.35 (1,1) [49411,6]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 3498943, _t18 ] % 83.15/83.35 (1,1) [1150970,6]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3499683, _t72 ] % 83.15/83.35 (1,1) [1150971,6]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3499511, _t71 ] % 83.15/83.35 (95,1) [1373117,6]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3499761, ~p6 ] % 83.15/83.35 (1,1) [1421323,6]. true => _t73 | ~_t72 | p6 [ SNF ] % 83.15/83.35 (1,1) [3498943,6]. _t17 => box 1 _t269 [ SNF++, 49411 ] % 83.15/83.35 (1,1) [3499511,6]. _t71 => box 1 _t320 [ SNF++, 1150971 ] % 83.15/83.35 (1,1) [3499683,6]. _t71 => box 1 _t319 [ SNF++, 1150970 ] % 83.15/83.35 (95,1) [3499761,6]. _t73 => ~box 1~ _t508 [ SNF++, 1373117 ] % 83.15/83.35 (1,1) [3499796,6]. true => ~_t270 | _t17 [ SNF++, 53414 ] % 83.15/83.35 (1,1) [3500448,6]. true => ~_t320 | _t71 [ SNF++, 1421325 ] % 83.15/83.35 (1,1) [3500512,6]. true => ~_t319 | _t72 [ SNF++, 1421324 ] % 83.15/83.35 (135,1) [3500604,6]. true => ~_t508 | ~p6 [ SNF++, 1689101 ] % 83.15/83.35 (135,1) [3525448,6]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3500604, 1421323, ~p6 ] % 83.15/83.35 (135,1) [3557535,6]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3525448, 3500512, ~_t72 ] % 83.15/83.35 (95,1) [3929670,6]. true => ~_t73 | ~_t71 | ~_t17 [ GEN1, 3499511, 3498943, 3499683, 3499761, 3881537, _t320, _t269, _t319, _t508 ] % 83.15/83.35 (95,1) [3931004,6]. true => ~_t270 | ~_t73 | ~_t71 [ LRES, 3929670, 3499796, ~_t17 ] % 83.15/83.35 (95,1) [3932339,6]. true => ~_t320 | ~_t270 | ~_t73 [ LRES, 3931004, 3500448, ~_t71 ] % 83.15/83.35 (135,1) [3933677,6]. true => ~_t508 | ~_t320 | ~_t319 | ~_t270 [ LRES, 3932339, 3557535, ~_t73 ] % 83.15/83.35 (1,1) [45411,7]. _t18 => box 1 _t19 [ SNF ] [ SNF++, 3498075, _t19 ] % 83.15/83.35 (1,1) [749723,7]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3498711, _t72 ] % 83.15/83.35 (1,1) [749724,7]. _t71 => box 1 _t71 [ Axiom 4 ] [ SNF++, 3498239, _t71 ] % 83.15/83.35 (71,1) [1150968,7]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3498907, ~p6 ] % 83.15/83.35 (1,1) [1150969,7]. true => _t73 | ~_t72 | p6 [ SNF ] % 83.15/83.35 (1,1) [3498075,7]. _t18 => box 1 _t268 [ SNF++, 45411 ] % 83.15/83.35 (1,1) [3498239,7]. _t71 => box 1 _t320 [ SNF++, 749724 ] % 83.15/83.35 (1,1) [3498711,7]. _t71 => box 1 _t319 [ SNF++, 749723 ] % 83.15/83.35 (71,1) [3498907,7]. _t73 => ~box 1~ _t508 [ SNF++, 1150968 ] % 83.15/83.35 (1,1) [3498944,7]. true => ~_t269 | _t18 [ SNF++, 49411 ] % 83.15/83.35 (1,1) [3499512,7]. true => ~_t320 | _t71 [ SNF++, 1150971 ] % 83.15/83.35 (1,1) [3499684,7]. true => ~_t319 | _t72 [ SNF++, 1150970 ] % 83.15/83.35 (95,1) [3499762,7]. true => ~_t508 | ~p6 [ SNF++, 1373117 ] % 87.97/88.16 (95,1) [3518756,7]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3499762, 1150969, ~p6 ] % 87.97/88.16 (95,1) [3552192,7]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3518756, 3499684, ~_t72 ] % 87.97/88.16 (71,1) [3878867,7]. true => ~_t73 | ~_t71 | ~_t18 [ GEN1, 3498239, 3498075, 3498711, 3498907, 3656228, _t320, _t268, _t319, _t508 ] % 87.97/88.16 (71,1) [3878869,7]. true => ~_t269 | ~_t73 | ~_t71 [ LRES, 3878867, 3498944, ~_t18 ] % 87.97/88.16 (71,1) [3880203,7]. true => ~_t320 | ~_t269 | ~_t73 [ LRES, 3878869, 3499512, ~_t71 ] % 87.97/88.16 (95,1) [3881537,7]. true => ~_t508 | ~_t320 | ~_t319 | ~_t269 [ LRES, 3880203, 3552192, ~_t73 ] % 87.97/88.16 (1,1) [41414,8]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 3497191, _t20 ] % 87.97/88.16 (1,1) [229820,8]. _t71 => box 1 _t72 [ SNF ] [ SNF++, 3497371, _t72 ] % 87.97/88.16 (31,1) [664146,8]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 3498033, ~p6 ] % 87.97/88.16 (1,1) [749722,8]. true => _t73 | ~_t72 | p6 [ SNF ] % 87.97/88.16 (1,1) [3497191,8]. _t19 => box 1 _t267 [ SNF++, 41414 ] % 87.97/88.16 (1,1) [3497371,8]. _t71 => box 1 _t319 [ SNF++, 229820 ] % 87.97/88.16 (31,1) [3498033,8]. _t73 => ~box 1~ _t508 [ SNF++, 664146 ] % 87.97/88.16 (1,1) [3498076,8]. true => ~_t268 | _t19 [ SNF++, 45411 ] % 87.97/88.16 (1,1) [3498240,8]. true => ~_t320 | _t71 [ SNF++, 749724 ] % 87.97/88.16 (1,1) [3498712,8]. true => ~_t319 | _t72 [ SNF++, 749723 ] % 87.97/88.16 (71,1) [3498908,8]. true => ~_t508 | ~p6 [ SNF++, 1150968 ] % 87.97/88.16 (71,1) [3525440,8]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3498908, 749722, ~p6 ] % 87.97/88.16 (71,1) [3557534,8]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3525440, 3498712, ~_t72 ] % 87.97/88.16 (31,1) [3605517,8]. true => ~_t73 | ~_t71 | ~_t19 [ GEN1, 3497371, 3497191, 3498033, 3588176, _t319, _t267, _t508 ] % 87.97/88.16 (31,1) [3629527,8]. true => ~_t268 | ~_t73 | ~_t71 [ LRES, 3605517, 3498076, ~_t19 ] % 87.97/88.16 (31,1) [3654888,8]. true => ~_t320 | ~_t268 | ~_t73 [ LRES, 3629527, 3498240, ~_t71 ] % 87.97/88.16 (71,1) [3656228,8]. true => ~_t508 | ~_t320 | ~_t319 | ~_t268 [ LRES, 3654888, 3557534, ~_t73 ] % 87.97/88.16 (1,1) [38750,9]. _t20 => box 1 p6 [ SNF ] [ SNF++, 2297665, p6 ] % 87.97/88.16 (7,1) [229818,9]. _t73 => ~box 1~ ~p6 [ SNF ] [ SNF++, 2298521, ~p6 ] % 87.97/88.16 (1,1) [229819,9]. true => _t73 | ~_t72 | p6 [ SNF ] % 87.97/88.16 (1,1) [2297665,9]. _t20 => box 1 _t266 [ SNF++, 38750 ] % 87.97/88.16 (7,1) [2298521,9]. _t73 => ~box 1~ _t508 [ SNF++, 229818 ] % 87.97/88.16 (1,1) [3497192,9]. true => ~_t267 | _t20 [ SNF++, 41414 ] % 87.97/88.16 (1,1) [3497372,9]. true => ~_t319 | _t72 [ SNF++, 229820 ] % 87.97/88.16 (31,1) [3498034,9]. true => ~_t508 | ~p6 [ SNF++, 664146 ] % 87.97/88.16 (31,1) [3512093,9]. true => ~_t508 | _t73 | ~_t72 [ LRES, 3498034, 229819, ~p6 ] % 87.97/88.16 (7,1) [3544190,9]. true => ~_t73 | ~_t20 [ GEN1, 2297665, 2298521, 3518788, _t266, _t508 ] % 87.97/88.16 (7,1) [3546855,9]. true => ~_t267 | ~_t73 [ LRES, 3544190, 3497192, ~_t20 ] % 87.97/88.16 (31,1) [3554867,9]. true => ~_t508 | ~_t319 | _t73 [ LRES, 3512093, 3497372, ~_t72 ] % 87.97/88.16 (31,1) [3588176,9]. true => ~_t508 | ~_t319 | ~_t267 [ LRES, 3554867, 3546855, _t73 ] % 87.97/88.16 (1,1) [2297666,10]. true => ~_t266 | p6 [ SNF++, 38750 ] % 87.97/88.16 (7,1) [2298522,10]. true => ~_t508 | ~p6 [ SNF++, 229818 ] % 87.97/88.16 (7,1) [3518788,10]. true => ~_t508 | ~_t266 [ LRES, 2298522, 2297666, ~p6 ] % 87.97/88.16 % SZS output end Refutation % 0.48/88.31 % KSP exiting %------------------------------------------------------------------------------