%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP055_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n003.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:56 PM UTC 2026 % Result : Theorem 6.27s 6.43s % Output : Refutation 7.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP055_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : run_ksp %s % 0.15/0.33 % Computer : n003.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 16:43:26 EDT 2026 % 0.15/0.33 % CPUTime : % 0.38/0.60 ----KSP format--- % 0.38/0.60 set(box,FIVE). % 0.38/0.60 usable(formulas). % 0.38/0.60 true. % 0.38/0.60 end_of_list. % 0.38/0.60 sos(formulas). % 0.38/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.38/0.60 end_of_list. % 0.38/0.60 ----------------- % 0.38/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.QvaaO4jY8d/theBenchmark.ksp % 6.27/6.43 % 6.27/6.43 % SZS status Theorem % 6.27/6.43 % 6.27/6.43 ***************** % 6.27/6.43 FOUND PROOF 1 % 6.27/6.43 ***************** % 6.27/6.43 % SZS output start Refutation % 6.27/6.43 % 6.27/6.43 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 6.27/6.43 (1,1) [1037,0]. _t30 => box 1 p2 [ Axiom 5 ] [ SNF++, 17753, p2 ] % 6.27/6.43 (1,1) [1039,0]. ~_t275 => box 1 ~_t30 [ Axiom 5 ] [ SNF++, 17755, ~_t30 ] % 6.27/6.43 (1,1) [1041,0]. true => ~_t275 | _t30 [ Axiom 5 ] [ Modal Level Pure Literal Elimination, ~_t275 ] % 6.27/6.43 (1,1) [1084,0]. _t29 => box 1 _t30 [ Axiom 5 ] [ SNF++, 17759, _t30 ] % 6.27/6.43 (1,1) [1086,0]. ~_t276 => box 1 ~_t29 [ Axiom 5 ] [ SNF++, 17761, ~_t29 ] % 6.27/6.43 (1,1) [1088,0]. true => ~_t276 | _t29 [ Axiom 5 ] [ Backward Subsumption, 850986 ] % 6.27/6.43 (1,1) [1137,0]. _t28 => box 1 _t29 [ Axiom 5 ] [ SNF++, 17765, _t29 ] % 6.27/6.43 (1,1) [1139,0]. ~_t277 => box 1 ~_t28 [ Axiom 5 ] [ SNF++, 17767, ~_t28 ] % 6.27/6.43 (1,1) [1141,0]. true => ~_t277 | _t28 [ Axiom 5 ] [ Backward Subsumption, 851213 ] % 6.27/6.43 (1,1) [1189,0]. _t27 => box 1 _t28 [ Axiom 5 ] [ SNF++, 17771, _t28 ] % 6.27/6.43 (1,1) [1191,0]. ~_t278 => box 1 ~_t27 [ Axiom 5 ] [ SNF++, 17773, ~_t27 ] % 6.27/6.43 (1,1) [1193,0]. true => ~_t278 | _t27 [ Axiom 5 ] [ Backward Subsumption, 851439 ] % 6.27/6.43 (1,1) [1241,0]. _t26 => box 1 _t27 [ Axiom 5 ] [ SNF++, 17777, _t27 ] % 6.27/6.43 (1,1) [1243,0]. ~_t279 => box 1 ~_t26 [ Axiom 5 ] [ SNF++, 17779, ~_t26 ] % 6.27/6.43 (1,1) [1245,0]. true => ~_t279 | _t26 [ Axiom 5 ] [ Backward Subsumption, 851664 ] % 6.27/6.43 (1,1) [1293,0]. _t25 => box 1 _t26 [ Axiom 5 ] [ SNF++, 17783, _t26 ] % 6.27/6.43 (1,1) [1295,0]. ~_t280 => box 1 ~_t25 [ Axiom 5 ] [ SNF++, 17785, ~_t25 ] % 6.27/6.43 (1,1) [1297,0]. true => ~_t280 | _t25 [ Axiom 5 ] [ Backward Subsumption, 851888 ] % 6.27/6.43 (1,1) [1345,0]. _t24 => box 1 _t25 [ Axiom 5 ] [ SNF++, 17789, _t25 ] % 6.27/6.43 (1,1) [1347,0]. ~_t281 => box 1 ~_t24 [ Axiom 5 ] [ SNF++, 17791, ~_t24 ] % 6.27/6.43 (1,1) [1349,0]. true => ~_t281 | _t24 [ Axiom 5 ] [ Backward Subsumption, 852111 ] % 6.27/6.43 (1,1) [1397,0]. _t23 => box 1 _t24 [ Axiom 5 ] [ SNF++, 17795, _t24 ] % 6.27/6.43 (1,1) [1399,0]. ~_t282 => box 1 ~_t23 [ Axiom 5 ] [ SNF++, 17797, ~_t23 ] % 6.27/6.43 (1,1) [1401,0]. true => ~_t282 | _t23 [ Axiom 5 ] [ Backward Subsumption, 852333 ] % 6.27/6.43 (1,1) [1449,0]. _t22 => box 1 _t23 [ Axiom 5 ] [ SNF++, 17801, _t23 ] % 6.27/6.43 (1,1) [1451,0]. ~_t283 => box 1 ~_t22 [ Axiom 5 ] [ SNF++, 17803, ~_t22 ] % 6.27/6.43 (1,1) [1453,0]. true => ~_t283 | _t22 [ Axiom 5 ] [ Backward Subsumption, 852554 ] % 6.27/6.43 (1,1) [1499,0]. _t21 => box 1 _t22 [ SNF ] [ Backward Subsumption, 17548 ] % 6.27/6.43 (1,1) [1551,0]. true => _t21 | ~_t0 [ SNF ] [ Backward Subsumption, 17475 ] % 6.27/6.43 (289,1) [17085,0]. _t84 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 17479 ] % 6.27/6.43 (1,1) [17086,0]. true => _t84 | ~_t0 [ SNF ] [ Backward Subsumption, 17336 ] % 6.27/6.43 (291,1) [17087,0]. _t51 => ~box 1~ ~p1 [ SNF ] [ Backward Subsumption, 17619 ] % 6.27/6.43 (1,1) [17088,0]. true => _t51 | ~_t0 [ SNF ] [ Backward Subsumption, 17335 ] % 6.27/6.43 (1,1) [17335,0]. true => _t51 [ Unit Resolution, 3, 17088, _t0 ] [ Modal Level Pure Literal Elimination, _t51 ] % 6.27/6.43 (1,1) [17336,0]. true => _t84 [ Unit Resolution, 3, 17086, _t0 ] [ Modal Level Pure Literal Elimination, _t84 ] % 6.27/6.43 (1,1) [17475,0]. true => _t21 [ Unit Resolution, 3, 1551, _t0 ] [ Modal Level Pure Literal Elimination, _t21 ] % 6.27/6.43 (289,1) [17479,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 17336, 17085, _t84 ] [ SNF++, 19405, ~p2 ] % 6.27/6.43 (1,1) [17548,0]. true => box 1 _t22 [ LHS Unit Resolution, 17475, 1499, _t21 ] [ SNF++, 17807, _t22 ] % 6.27/6.43 (291,1) [17619,0]. true => ~box 1~ ~p1 [ LHS Unit Resolution, 17335, 17087, _t51 ] [ SNF++, 19407, ~p1 ] % 6.27/6.43 (1,1) [17753,0]. _t30 => box 1 _t480 [ SNF++, 1037 ] [ Backward Subsumption, 850985 ] % 6.27/6.43 (1,1) [17755,0]. ~_t275 => box 1 _t544 [ SNF++, 1039 ] [ Backward Subsumption, 850982 ] % 6.27/6.43 (1,1) [17759,0]. _t29 => box 1 _t546 [ SNF++, 1084 ] [ Backward Subsumption, 850987 ] % 6.27/6.43 (1,1) [17761,0]. ~_t276 => box 1 _t547 [ SNF++, 1086 ] [ Backward Subsumption, 851210 ] % 6.27/6.43 (1,1) [17765,0]. _t28 => box 1 _t549 [ SNF++, 1137 ] [ Backward Subsumption, 851214 ] % 6.27/6.43 (1,1) [17767,0]. ~_t277 => box 1 _t550 [ SNF++, 1139 ] [ Backward Subsumption, 851436 ] % 6.27/6.43 (1,1) [17771,0]. _t27 => box 1 _t552 [ SNF++, 1189 ] [ Backward Subsumption, 851440 ] % 6.27/6.43 (1,1) [17773,0]. ~_t278 => box 1 _t553 [ SNF++, 1191 ] [ Backward Subsumption, 851661 ] % 6.27/6.43 (1,1) [17777,0]. _t26 => box 1 _t555 [ SNF++, 1241 ] [ Backward Subsumption, 851665 ] % 6.27/6.43 (1,1) [17779,0]. ~_t279 => box 1 _t556 [ SNF++, 1243 ] [ Backward Subsumption, 851885 ] % 6.27/6.43 (1,1) [17783,0]. _t25 => box 1 _t558 [ SNF++, 1293 ] [ Backward Subsumption, 851889 ] % 6.27/6.43 (1,1) [17785,0]. ~_t280 => box 1 _t559 [ SNF++, 1295 ] [ Backward Subsumption, 852108 ] % 6.27/6.43 (1,1) [17789,0]. _t24 => box 1 _t561 [ SNF++, 1345 ] [ Backward Subsumption, 852112 ] % 6.27/6.43 (1,1) [17791,0]. ~_t281 => box 1 _t562 [ SNF++, 1347 ] [ Backward Subsumption, 852330 ] % 6.27/6.43 (1,1) [17795,0]. _t23 => box 1 _t564 [ SNF++, 1397 ] [ Backward Subsumption, 852334 ] % 6.27/6.43 (1,1) [17797,0]. ~_t282 => box 1 _t565 [ SNF++, 1399 ] [ Backward Subsumption, 852551 ] % 6.27/6.43 (1,1) [17801,0]. _t22 => box 1 _t567 [ SNF++, 1449 ] [ Backward Subsumption, 852555 ] % 6.27/6.43 (1,1) [17803,0]. ~_t283 => box 1 _t568 [ SNF++, 1451 ] % 6.27/6.43 (1,1) [17807,0]. true => box 1 _t570 [ SNF++, 17548 ] % 6.27/6.43 (289,1) [19405,0]. true => ~box 1~ _t485 [ SNF++, 17479 ] % 6.27/6.43 (291,1) [19407,0]. true => ~box 1~ _t482 [ SNF++, 17619 ] % 6.27/6.43 (1,1) [118484,0]. true => _t275 | ~_t29 [ GEN3, 17759, 17755, 33658, 19407, _t546, _t544, _t482 ] [ Backward Subsumption, 850981 ] % 6.27/6.43 (1,1) [122850,0]. true => _t276 | ~_t28 [ GEN3, 17765, 17761, 33675, 19407, _t549, _t547, _t482 ] [ Backward Subsumption, 851209 ] % 6.27/6.43 (1,1) [126987,0]. true => _t277 | ~_t27 [ GEN3, 17771, 17767, 33692, 19407, _t552, _t550, _t482 ] [ Backward Subsumption, 851435 ] % 6.27/6.43 (1,1) [131353,0]. true => _t278 | ~_t26 [ GEN3, 17777, 17773, 33709, 19407, _t555, _t553, _t482 ] [ Backward Subsumption, 851660 ] % 6.27/6.43 (1,1) [135719,0]. true => _t279 | ~_t25 [ GEN3, 17783, 17779, 33726, 19407, _t558, _t556, _t482 ] [ Backward Subsumption, 851884 ] % 6.27/6.43 (1,1) [139856,0]. true => _t280 | ~_t24 [ GEN3, 17789, 17785, 33743, 19407, _t561, _t559, _t482 ] [ Backward Subsumption, 852107 ] % 6.27/6.43 (1,1) [144222,0]. true => _t281 | ~_t23 [ GEN3, 17795, 17791, 33760, 19407, _t564, _t562, _t482 ] [ Backward Subsumption, 852329 ] % 6.27/6.43 (1,1) [148588,0]. true => _t282 | ~_t22 [ GEN3, 17801, 17797, 33777, 19407, _t567, _t565, _t482 ] [ Backward Subsumption, 852550 ] % 6.27/6.43 (1,1) [152725,0]. true => _t283 [ GEN3, 17807, 17803, 33794, 19407, _t570, _t568, _t482 ] % 6.27/6.43 (289,1) [849154,0]. true => ~_t30 [ GEN1, 17753, 19405, 37198, _t480, _t485 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 6.27/6.43 (289,1) [850758,0]. true => ~_t275 [ LRES, 849154, 1041, ~_t30 ] [ Modal Level Pure Literal Elimination, ~_t275 ] % 6.27/6.43 (289,1) [850981,0]. true => ~_t29 [ Unit Resolution, 850758, 118484, _t275 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 6.27/6.43 (289,1) [850986,0]. true => ~_t276 [ Unit Resolution, 850981, 1088, _t29 ] [ Modal Level Pure Literal Elimination, ~_t276 ] % 6.27/6.43 (289,1) [851209,0]. true => ~_t28 [ Unit Resolution, 850986, 122850, _t276 ] [ Modal Level Pure Literal Elimination, ~_t28 ] % 6.27/6.43 (289,1) [851213,0]. true => ~_t277 [ Unit Resolution, 851209, 1141, _t28 ] [ Modal Level Pure Literal Elimination, ~_t277 ] % 6.27/6.43 (289,1) [851435,0]. true => ~_t27 [ Unit Resolution, 851213, 126987, _t277 ] [ Modal Level Pure Literal Elimination, ~_t27 ] % 6.27/6.43 (289,1) [851439,0]. true => ~_t278 [ Unit Resolution, 851435, 1193, _t27 ] [ Modal Level Pure Literal Elimination, ~_t278 ] % 6.27/6.43 (289,1) [851660,0]. true => ~_t26 [ Unit Resolution, 851439, 131353, _t278 ] [ Modal Level Pure Literal Elimination, ~_t26 ] % 6.27/6.43 (289,1) [851664,0]. true => ~_t279 [ Unit Resolution, 851660, 1245, _t26 ] [ Modal Level Pure Literal Elimination, ~_t279 ] % 6.27/6.43 (289,1) [851884,0]. true => ~_t25 [ Unit Resolution, 851664, 135719, _t279 ] [ Modal Level Pure Literal Elimination, ~_t25 ] % 6.27/6.43 (289,1) [851888,0]. true => ~_t280 [ Unit Resolution, 851884, 1297, _t25 ] [ Modal Level Pure Literal Elimination, ~_t280 ] % 6.27/6.43 (289,1) [852107,0]. true => ~_t24 [ Unit Resolution, 851888, 139856, _t280 ] [ Modal Level Pure Literal Elimination, ~_t24 ] % 6.27/6.43 (289,1) [852111,0]. true => ~_t281 [ Unit Resolution, 852107, 1349, _t24 ] [ Modal Level Pure Literal Elimination, ~_t281 ] % 6.27/6.43 (289,1) [852329,0]. true => ~_t23 [ Unit Resolution, 852111, 144222, _t281 ] [ Modal Level Pure Literal Elimination, ~_t23 ] % 7.07/7.21 (289,1) [852333,0]. true => ~_t282 [ Unit Resolution, 852329, 1401, _t23 ] [ Modal Level Pure Literal Elimination, ~_t282 ] % 7.07/7.21 (289,1) [852550,0]. true => ~_t22 [ Unit Resolution, 852333, 148588, _t282 ] [ Modal Level Pure Literal Elimination, ~_t22 ] % 7.07/7.21 (289,1) [852554,0]. true => ~_t283 [ Unit Resolution, 852550, 1453, _t22 ] % 7.07/7.21 (289,1) [852768,0]. true => false [ Unit Resolution, 852554, 152725, _t283 ] % 7.07/7.21 (1,1) [17754,1]. true => ~_t480 | p2 [ SNF++, 1037 ] [ Modal Level Pure Literal Elimination, ~_t480 ] % 7.07/7.21 (1,1) [17756,1]. true => ~_t544 | ~_t30 [ SNF++, 1039 ] % 7.07/7.21 (1,1) [17760,1]. true => ~_t546 | _t30 [ SNF++, 1084 ] [ Modal Level Pure Literal Elimination, ~_t546 ] % 7.07/7.21 (1,1) [17762,1]. true => ~_t547 | ~_t29 [ SNF++, 1086 ] % 7.07/7.21 (1,1) [17766,1]. true => ~_t549 | _t29 [ SNF++, 1137 ] [ Modal Level Pure Literal Elimination, ~_t549 ] % 7.07/7.21 (1,1) [17768,1]. true => ~_t550 | ~_t28 [ SNF++, 1139 ] % 7.07/7.21 (1,1) [17772,1]. true => ~_t552 | _t28 [ SNF++, 1189 ] [ Modal Level Pure Literal Elimination, ~_t552 ] % 7.07/7.21 (1,1) [17774,1]. true => ~_t553 | ~_t27 [ SNF++, 1191 ] % 7.07/7.21 (1,1) [17778,1]. true => ~_t555 | _t27 [ SNF++, 1241 ] [ Modal Level Pure Literal Elimination, ~_t555 ] % 7.07/7.21 (1,1) [17780,1]. true => ~_t556 | ~_t26 [ SNF++, 1243 ] % 7.07/7.21 (1,1) [17784,1]. true => ~_t558 | _t26 [ SNF++, 1293 ] [ Modal Level Pure Literal Elimination, ~_t558 ] % 7.07/7.21 (1,1) [17786,1]. true => ~_t559 | ~_t25 [ SNF++, 1295 ] % 7.07/7.21 (1,1) [17790,1]. true => ~_t561 | _t25 [ SNF++, 1345 ] [ Modal Level Pure Literal Elimination, ~_t561 ] % 7.07/7.21 (1,1) [17792,1]. true => ~_t562 | ~_t24 [ SNF++, 1347 ] % 7.07/7.21 (1,1) [17796,1]. true => ~_t564 | _t24 [ SNF++, 1397 ] [ Modal Level Pure Literal Elimination, ~_t564 ] % 7.07/7.21 (1,1) [17798,1]. true => ~_t565 | ~_t23 [ SNF++, 1399 ] % 7.07/7.21 (1,1) [17802,1]. true => ~_t567 | _t23 [ SNF++, 1449 ] [ Modal Level Pure Literal Elimination, ~_t567 ] % 7.07/7.21 (1,1) [17804,1]. true => ~_t568 | ~_t22 [ SNF++, 1451 ] % 7.07/7.21 (1,1) [17808,1]. true => ~_t570 | _t22 [ SNF++, 17548 ] % 7.07/7.21 (289,1) [19406,1]. true => ~_t485 | ~p2 [ SNF++, 17479 ] % 7.07/7.21 (1,1) [33658,1]. true => ~_t546 | ~_t544 [ LRES, 17756, 17760, ~_t30 ] [ Modal Level Pure Literal Elimination, ~_t546 ] % 7.07/7.21 (1,1) [33675,1]. true => ~_t549 | ~_t547 [ LRES, 17762, 17766, ~_t29 ] [ Modal Level Pure Literal Elimination, ~_t549 ] % 7.07/7.21 (1,1) [33692,1]. true => ~_t552 | ~_t550 [ LRES, 17768, 17772, ~_t28 ] [ Modal Level Pure Literal Elimination, ~_t552 ] % 7.07/7.21 (1,1) [33709,1]. true => ~_t555 | ~_t553 [ LRES, 17774, 17778, ~_t27 ] [ Modal Level Pure Literal Elimination, ~_t555 ] % 7.07/7.21 (1,1) [33726,1]. true => ~_t558 | ~_t556 [ LRES, 17780, 17784, ~_t26 ] [ Modal Level Pure Literal Elimination, ~_t558 ] % 7.07/7.21 (1,1) [33743,1]. true => ~_t561 | ~_t559 [ LRES, 17786, 17790, ~_t25 ] [ Modal Level Pure Literal Elimination, ~_t561 ] % 7.07/7.21 (1,1) [33760,1]. true => ~_t564 | ~_t562 [ LRES, 17792, 17796, ~_t24 ] [ Modal Level Pure Literal Elimination, ~_t564 ] % 7.07/7.21 (1,1) [33777,1]. true => ~_t567 | ~_t565 [ LRES, 17798, 17802, ~_t23 ] [ Modal Level Pure Literal Elimination, ~_t567 ] % 7.07/7.21 (1,1) [33794,1]. true => ~_t570 | ~_t568 [ LRES, 17804, 17808, ~_t22 ] % 7.07/7.21 (289,1) [37198,1]. true => ~_t485 | ~_t480 [ LRES, 19406, 17754, ~p2 ] [ Modal Level Pure Literal Elimination, ~_t480 ] % 7.07/7.21 % SZS output end Refutation % 7.07/7.25 % KSP exiting %------------------------------------------------------------------------------