%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP073_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n006.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:57 PM UTC 2026 % Result : Theorem 1.47s 1.65s % Output : Refutation 1.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP073_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_ksp %s % 0.16/0.33 % Computer : n006.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 17:10:46 EDT 2026 % 0.16/0.34 % CPUTime : % 0.37/0.62 ----KSP format--- % 0.37/0.62 set(box,SYM). % 0.37/0.62 usable(formulas). % 0.37/0.62 true. % 0.37/0.62 end_of_list. % 0.37/0.62 sos(formulas). % 0.37/0.62 ~ ([] ( 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.37/0.62 end_of_list. % 0.37/0.62 ----------------- % 0.37/0.62 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/sandbox2/tmp/tmp.i0r2ojZJ1i/theBenchmark.ksp % 1.47/1.65 % 1.47/1.65 % SZS status Theorem % 1.47/1.65 % 1.47/1.65 ***************** % 1.47/1.65 FOUND PROOF 1 % 1.47/1.65 ***************** % 1.47/1.65 % SZS output start Refutation % 1.47/1.65 % 1.47/1.65 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 1.47/1.65 (1,1) [218,0]. _t275 => box 1 ~_t28 [ Axiom SYM ] [ SNF++, 5593, ~_t28 ] % 1.47/1.65 (1,1) [219,0]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 5595, _t30 ] % 1.47/1.65 (1,1) [220,0]. true => _t275 | _t29 [ Axiom SYM ] [ Backward Subsumption, 26627 ] % 1.47/1.65 (1,1) [229,0]. _t277 => box 1 ~_t26 [ Axiom SYM ] [ SNF++, 5597, ~_t26 ] % 1.47/1.65 (1,1) [230,0]. _t27 => box 1 _t28 [ SNF ] [ SNF++, 5599, _t28 ] % 1.47/1.65 (1,1) [231,0]. true => _t277 | _t27 [ Axiom SYM ] [ Backward Subsumption, 26632 ] % 1.47/1.65 (1,1) [237,0]. _t279 => box 1 ~_t24 [ Axiom SYM ] [ SNF++, 5601, ~_t24 ] % 1.47/1.65 (1,1) [238,0]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 5603, _t26 ] % 1.47/1.65 (1,1) [239,0]. true => _t279 | _t25 [ Axiom SYM ] [ Backward Subsumption, 26637 ] % 1.47/1.65 (1,1) [242,0]. _t281 => box 1 ~_t22 [ Axiom SYM ] [ SNF++, 5605, ~_t22 ] % 1.47/1.65 (1,1) [243,0]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 5607, _t24 ] % 1.47/1.65 (1,1) [244,0]. true => _t281 | _t23 [ Axiom SYM ] [ Backward Subsumption, 26642 ] % 1.47/1.65 (1,1) [245,0]. _t21 => box 1 _t22 [ SNF ] [ Backward Subsumption, 2818 ] % 1.47/1.65 (1,1) [246,0]. true => _t21 | ~_t0 [ SNF ] [ Backward Subsumption, 2814 ] % 1.47/1.65 (1,1) [1110,0]. _t372 => box 1 ~_t154 [ Axiom SYM ] [ SNF++, 5737, ~_t154 ] % 1.47/1.65 (1,1) [1111,0]. _t155 => box 1 _t156 [ SNF ] [ SNF++, 5739, _t156 ] % 1.47/1.65 (1,1) [1112,0]. true => _t372 | _t155 [ Axiom SYM ] [ Backward Subsumption, 7406 ] % 1.47/1.65 (1,1) [1122,0]. _t153 => box 1 _t154 [ SNF ] [ Backward Subsumption, 2874 ] % 1.47/1.65 (33,1) [1441,0]. _t84 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 2841 ] % 1.47/1.65 (45,1) [1804,0]. _t51 => ~box 1~ ~p1 [ SNF ] [ Backward Subsumption, 2935 ] % 1.47/1.65 (1,1) [2564,0]. true => _t153 | ~_t0 [ SNF ] [ Backward Subsumption, 2706 ] % 1.47/1.65 (1,1) [2619,0]. true => _t84 | ~_t0 [ SNF ] [ Backward Subsumption, 2675 ] % 1.47/1.65 (1,1) [2620,0]. true => _t51 | ~_t0 [ SNF ] [ Backward Subsumption, 2674 ] % 1.47/1.65 (1,1) [2674,0]. true => _t51 [ Unit Resolution, 3, 2620, _t0 ] [ Modal Level Pure Literal Elimination, _t51 ] % 1.47/1.65 (1,1) [2675,0]. true => _t84 [ Unit Resolution, 3, 2619, _t0 ] [ Modal Level Pure Literal Elimination, _t84 ] % 1.47/1.65 (1,1) [2706,0]. true => _t153 [ Unit Resolution, 3, 2564, _t0 ] [ Modal Level Pure Literal Elimination, _t153 ] % 1.47/1.65 (1,1) [2814,0]. true => _t21 [ Unit Resolution, 3, 246, _t0 ] [ Modal Level Pure Literal Elimination, _t21 ] % 1.47/1.65 (1,1) [2818,0]. true => box 1 _t22 [ LHS Unit Resolution, 2814, 245, _t21 ] [ SNF++, 5609, _t22 ] % 1.47/1.65 (33,1) [2841,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 2675, 1441, _t84 ] [ SNF++, 5963, ~p2 ] % 1.47/1.65 (1,1) [2874,0]. true => box 1 _t154 [ LHS Unit Resolution, 2706, 1122, _t153 ] [ SNF++, 5741, _t154 ] % 1.47/1.65 (45,1) [2935,0]. true => ~box 1~ ~p1 [ LHS Unit Resolution, 2674, 1804, _t51 ] [ SNF++, 5969, ~p1 ] % 1.47/1.65 (1,1) [5593,0]. _t275 => box 1 _t526 [ SNF++, 218 ] [ Backward Subsumption, 26631 ] % 1.47/1.65 (1,1) [5595,0]. _t29 => box 1 _t463 [ SNF++, 219 ] [ Backward Subsumption, 26628 ] % 1.47/1.65 (1,1) [5597,0]. _t277 => box 1 _t622 [ SNF++, 229 ] [ Backward Subsumption, 26635 ] % 1.47/1.65 (1,1) [5599,0]. _t27 => box 1 _t527 [ SNF++, 230 ] [ Backward Subsumption, 26636 ] % 1.47/1.65 (1,1) [5601,0]. _t279 => box 1 _t719 [ SNF++, 237 ] [ Backward Subsumption, 26640 ] % 1.47/1.65 (1,1) [5603,0]. _t25 => box 1 _t623 [ SNF++, 238 ] [ Backward Subsumption, 26641 ] % 1.47/1.65 (1,1) [5605,0]. _t281 => box 1 _t822 [ SNF++, 242 ] % 1.47/1.65 (1,1) [5607,0]. _t23 => box 1 _t720 [ SNF++, 243 ] % 1.47/1.65 (1,1) [5609,0]. true => box 1 _t823 [ SNF++, 2818 ] % 1.47/1.65 (1,1) [5737,0]. _t372 => box 1 _t550 [ SNF++, 1110 ] [ Backward Subsumption, 7407 ] % 1.47/1.65 (1,1) [5739,0]. _t155 => box 1 _t476 [ SNF++, 1111 ] [ Backward Subsumption, 7408 ] % 1.47/1.65 (1,1) [5741,0]. true => box 1 _t551 [ SNF++, 2874 ] % 1.47/1.65 (33,1) [5963,0]. true => ~box 1~ _t457 [ SNF++, 2841 ] % 1.47/1.65 (45,1) [5969,0]. true => ~box 1~ _t454 [ SNF++, 2935 ] % 1.47/1.65 (1,1) [6803,0]. true => ~_t275 | ~_t27 [ GEN3, 5599, 5593, 6105, 5969, _t527, _t526, _t454 ] [ Backward Subsumption, 26630 ] % 1.47/1.65 (1,1) [6816,0]. true => _t277 | ~_t275 [ LRES, 6803, 231, ~_t27 ] [ Backward Subsumption, 26629 ] % 1.47/1.65 (1,1) [6837,0]. true => ~_t277 | ~_t25 [ GEN3, 5603, 5597, 6120, 5969, _t623, _t622, _t454 ] [ Backward Subsumption, 26634 ] % 1.47/1.67 (1,1) [6859,0]. true => _t279 | ~_t277 [ LRES, 6837, 239, ~_t25 ] [ Backward Subsumption, 26633 ] % 1.47/1.67 (1,1) [6872,0]. true => ~_t279 | ~_t23 [ GEN3, 5607, 5601, 6136, 5969, _t720, _t719, _t454 ] [ Backward Subsumption, 26639 ] % 1.47/1.67 (1,1) [6895,0]. true => ~_t281 [ GEN3, 5609, 5605, 6150, 5969, _t823, _t822, _t454 ] % 1.47/1.67 (1,1) [6915,0]. true => _t281 | ~_t279 [ LRES, 6872, 244, ~_t23 ] [ Backward Subsumption, 26638 ] % 1.47/1.67 (1,1) [7402,0]. true => ~_t372 [ GEN3, 5741, 5737, 6362, 5969, _t551, _t550, _t454 ] [ Modal Level Pure Literal Elimination, ~_t372 ] % 1.47/1.67 (1,1) [7406,0]. true => _t155 [ Unit Resolution, 7402, 1112, _t372 ] [ Modal Level Pure Literal Elimination, _t155 ] % 1.47/1.67 (1,1) [7408,0]. true => box 1 _t476 [ LHS Unit Resolution, 7406, 5739, _t155 ] % 1.47/1.67 (33,1) [26626,0]. true => ~_t29 [ GEN1, 7408, 5595, 5963, 13406, _t476, _t463, _t457 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 1.47/1.67 (33,1) [26627,0]. true => _t275 [ Unit Resolution, 26626, 220, _t29 ] [ Modal Level Pure Literal Elimination, _t275 ] % 1.47/1.67 (33,1) [26629,0]. true => _t277 [ Unit Resolution, 26627, 6816, _t275 ] [ Modal Level Pure Literal Elimination, _t277 ] % 1.47/1.67 (33,1) [26633,0]. true => _t279 [ Unit Resolution, 26629, 6859, _t277 ] [ Modal Level Pure Literal Elimination, _t279 ] % 1.47/1.67 (33,1) [26638,0]. true => _t281 [ Unit Resolution, 26633, 6915, _t279 ] % 1.47/1.67 (33,1) [26643,0]. true => false [ Unit Resolution, 26638, 6895, _t281 ] % 1.47/1.67 (1,1) [204,1]. _t30 => box 1 p2 [ SNF ] [ SNF++, 5017, p2 ] % 1.47/1.67 (9,1) [590,1]. _t84 => ~box 1~ ~p2 [ SNF ] [ SNF++, 5551, ~p2 ] % 1.47/1.67 (1,1) [1098,1]. true => ~_t156 | _t84 | p2 [ SNF ] % 1.47/1.67 (1,1) [5017,1]. _t30 => box 1 _t452 [ SNF++, 204 ] % 1.47/1.67 (9,1) [5551,1]. _t84 => ~box 1~ _t457 [ SNF++, 590 ] % 1.47/1.67 (1,1) [5594,1]. true => ~_t526 | ~_t28 [ SNF++, 218 ] % 1.47/1.67 (1,1) [5596,1]. true => ~_t463 | _t30 [ SNF++, 219 ] [ Modal Level Pure Literal Elimination, ~_t463 ] % 1.47/1.67 (1,1) [5598,1]. true => ~_t622 | ~_t26 [ SNF++, 229 ] % 1.47/1.67 (1,1) [5600,1]. true => ~_t527 | _t28 [ SNF++, 230 ] [ Modal Level Pure Literal Elimination, ~_t527 ] % 1.47/1.67 (1,1) [5602,1]. true => ~_t719 | ~_t24 [ SNF++, 237 ] % 1.47/1.67 (1,1) [5604,1]. true => ~_t623 | _t26 [ SNF++, 238 ] [ Modal Level Pure Literal Elimination, ~_t623 ] % 1.47/1.67 (1,1) [5606,1]. true => ~_t822 | ~_t22 [ SNF++, 242 ] % 1.47/1.67 (1,1) [5608,1]. true => ~_t720 | _t24 [ SNF++, 243 ] % 1.47/1.67 (1,1) [5610,1]. true => ~_t823 | _t22 [ SNF++, 2818 ] % 1.47/1.67 (1,1) [5738,1]. true => ~_t550 | ~_t154 [ SNF++, 1110 ] [ Modal Level Pure Literal Elimination, ~_t550 ] % 1.47/1.67 (1,1) [5740,1]. true => ~_t476 | _t156 [ SNF++, 1111 ] % 1.47/1.67 (1,1) [5742,1]. true => ~_t551 | _t154 [ SNF++, 2874 ] % 1.47/1.67 (33,1) [5964,1]. true => ~_t457 | ~p2 [ SNF++, 2841 ] % 1.47/1.67 (1,1) [6105,1]. true => ~_t527 | ~_t526 [ LRES, 5594, 5600, ~_t28 ] [ Modal Level Pure Literal Elimination, ~_t527 ] % 1.47/1.67 (1,1) [6120,1]. true => ~_t623 | ~_t622 [ LRES, 5598, 5604, ~_t26 ] [ Modal Level Pure Literal Elimination, ~_t623 ] % 1.47/1.67 (1,1) [6136,1]. true => ~_t720 | ~_t719 [ LRES, 5602, 5608, ~_t24 ] % 1.47/1.67 (1,1) [6150,1]. true => ~_t823 | ~_t822 [ LRES, 5606, 5610, ~_t22 ] % 1.47/1.67 (1,1) [6362,1]. true => ~_t551 | ~_t550 [ LRES, 5738, 5742, ~_t154 ] [ Modal Level Pure Literal Elimination, ~_t550 ] % 1.47/1.67 (33,1) [6504,1]. true => ~_t457 | ~_t156 | _t84 [ LRES, 5964, 1098, ~p2 ] % 1.47/1.67 (9,1) [12385,1]. true => ~_t84 | ~_t30 [ GEN1, 5017, 5551, 8355, _t452, _t457 ] % 1.47/1.67 (9,1) [12420,1]. true => ~_t463 | ~_t84 [ LRES, 12385, 5596, ~_t30 ] [ Modal Level Pure Literal Elimination, ~_t463 ] % 1.47/1.67 (33,1) [12429,1]. true => ~_t463 | ~_t457 | ~_t156 [ LRES, 12420, 6504, ~_t84 ] [ Modal Level Pure Literal Elimination, ~_t463 ] % 1.47/1.67 (33,1) [13406,1]. true => ~_t476 | ~_t463 | ~_t457 [ LRES, 12429, 5740, ~_t156 ] [ Modal Level Pure Literal Elimination, ~_t463 ] % 1.47/1.67 (1,1) [5018,2]. true => ~_t452 | p2 [ SNF++, 204 ] % 1.47/1.67 (9,1) [5552,2]. true => ~_t457 | ~p2 [ SNF++, 590 ] % 1.47/1.67 (9,1) [8355,2]. true => ~_t457 | ~_t452 [ LRES, 5552, 5018, ~p2 ] % 1.47/1.67 % SZS output end Refutation % 1.47/1.67 % KSP exiting %------------------------------------------------------------------------------