%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP072_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n016.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 0.38s 0.72s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP072_1 : TPTP v9.3.0. Released v9.3.0. % 0.10/0.13 % Command : run_ksp %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Mon May 4 17:12:36 EDT 2026 % 0.13/0.34 % CPUTime : % 0.30/0.57 ----KSP format--- % 0.30/0.57 set(box,SYM). % 0.30/0.57 usable(formulas). % 0.30/0.57 true. % 0.30/0.57 end_of_list. % 0.30/0.57 sos(formulas). % 0.30/0.57 ~ ([] ( 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 | $false | <> ( <> ( <> ( <> ( ~ ( 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 ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( 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 ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p2 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p2 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p2 ) ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p4 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p4 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p4 ) ) ) ) ) ) ) ) ) ) ) | $false | $false | $false | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) & [] ( p6 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) & [] ( p6 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) & [] ( p6 ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p2 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p4 ) ) ) ) ) ) ) ) ) ) ) ) | <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( <> ( ~ ( p6 ) ) ) ) ) ) ) ) ) ) ) ) ). % 0.30/0.57 end_of_list. % 0.30/0.57 ----------------- % 0.30/0.57 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.dVHqrn9Ych/theBenchmark.ksp % 0.38/0.72 % 0.38/0.72 % SZS status Theorem % 0.38/0.72 % 0.38/0.72 ***************** % 0.38/0.72 FOUND PROOF 1 % 0.38/0.72 ***************** % 0.38/0.72 % SZS output start Refutation % 0.38/0.72 % 0.38/0.72 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 0.38/0.72 (1,1) [252,0]. _t295 => box 1 ~_t32 [ Axiom SYM ] [ SNF++, 6812, ~_t32 ] % 0.38/0.72 (1,1) [253,0]. _t33 => box 1 p2 [ SNF ] [ SNF++, 6814, p2 ] % 0.38/0.72 (1,1) [254,0]. true => _t295 | _t33 [ Axiom SYM ] [ Modal Level Pure Literal Elimination, _t295 ] % 0.38/0.72 (1,1) [266,0]. _t297 => box 1 ~_t30 [ Axiom SYM ] [ SNF++, 6816, ~_t30 ] % 0.38/0.72 (1,1) [267,0]. _t31 => box 1 _t32 [ SNF ] [ SNF++, 6818, _t32 ] % 0.38/0.72 (1,1) [268,0]. true => _t297 | _t31 [ Axiom SYM ] [ Backward Subsumption, 8973 ] % 0.38/0.72 (1,1) [277,0]. _t299 => box 1 ~_t28 [ Axiom SYM ] [ SNF++, 6820, ~_t28 ] % 0.38/0.72 (1,1) [278,0]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 6822, _t30 ] % 0.38/0.72 (1,1) [279,0]. true => _t299 | _t29 [ Axiom SYM ] [ Backward Subsumption, 8978 ] % 0.38/0.72 (1,1) [285,0]. _t301 => box 1 ~_t26 [ Axiom SYM ] [ SNF++, 6824, ~_t26 ] % 0.38/0.72 (1,1) [286,0]. _t27 => box 1 _t28 [ SNF ] [ SNF++, 6826, _t28 ] % 0.38/0.72 (1,1) [287,0]. true => _t301 | _t27 [ Axiom SYM ] [ Backward Subsumption, 8983 ] % 0.38/0.72 (1,1) [290,0]. _t303 => box 1 ~_t24 [ Axiom SYM ] [ SNF++, 6828, ~_t24 ] % 0.38/0.72 (1,1) [291,0]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 6830, _t26 ] % 0.38/0.72 (1,1) [292,0]. true => _t303 | _t25 [ Axiom SYM ] [ Backward Subsumption, 8988 ] % 0.38/0.72 (1,1) [293,0]. _t23 => box 1 _t24 [ SNF ] [ Backward Subsumption, 3380 ] % 0.38/0.72 (1,1) [294,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 3376 ] % 0.38/0.72 (7,1) [531,0]. _t69 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 3515 ] % 0.38/0.72 (19,1) [1071,0]. _t138 => ~box 1~ ~p1 [ SNF ] [ Backward Subsumption, 3403 ] % 0.38/0.72 (1,1) [3161,0]. true => _t69 | ~_t0 [ SNF ] [ Backward Subsumption, 3220 ] % 0.38/0.72 (1,1) [3162,0]. true => _t138 | ~_t0 [ SNF ] [ Backward Subsumption, 3219 ] % 0.38/0.72 (1,1) [3219,0]. true => _t138 [ Unit Resolution, 3, 3162, _t0 ] [ Modal Level Pure Literal Elimination, _t138 ] % 0.38/0.72 (1,1) [3220,0]. true => _t69 [ Unit Resolution, 3, 3161, _t0 ] [ Modal Level Pure Literal Elimination, _t69 ] % 0.38/0.72 (1,1) [3376,0]. true => _t23 [ Unit Resolution, 3, 294, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 0.38/0.72 (1,1) [3380,0]. true => box 1 _t24 [ LHS Unit Resolution, 3376, 293, _t23 ] [ SNF++, 6832, _t24 ] % 0.38/0.72 (19,1) [3403,0]. true => ~box 1~ ~p1 [ LHS Unit Resolution, 3219, 1071, _t138 ] [ SNF++, 7214, ~p1 ] % 0.38/0.72 (7,1) [3515,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 3220, 531, _t69 ] [ SNF++, 7208, ~p2 ] % 0.38/0.72 (1,1) [6812,0]. _t295 => box 1 _t527 [ SNF++, 252 ] [ Backward Subsumption, 8971 ] % 0.38/0.72 (1,1) [6814,0]. _t33 => box 1 _t491 [ SNF++, 253 ] [ Backward Subsumption, 8972 ] % 0.38/0.72 (1,1) [6816,0]. _t297 => box 1 _t618 [ SNF++, 266 ] [ Backward Subsumption, 8976 ] % 0.38/0.72 (1,1) [6818,0]. _t31 => box 1 _t528 [ SNF++, 267 ] [ Backward Subsumption, 8977 ] % 0.38/0.72 (1,1) [6820,0]. _t299 => box 1 _t710 [ SNF++, 277 ] [ Backward Subsumption, 8981 ] % 0.38/0.72 (1,1) [6822,0]. _t29 => box 1 _t619 [ SNF++, 278 ] [ Backward Subsumption, 8982 ] % 0.38/0.72 (1,1) [6824,0]. _t301 => box 1 _t803 [ SNF++, 285 ] [ Backward Subsumption, 8986 ] % 0.38/0.72 (1,1) [6826,0]. _t27 => box 1 _t711 [ SNF++, 286 ] [ Backward Subsumption, 8987 ] % 0.38/0.72 (1,1) [6828,0]. _t303 => box 1 _t902 [ SNF++, 290 ] % 0.38/0.72 (1,1) [6830,0]. _t25 => box 1 _t804 [ SNF++, 291 ] % 0.38/0.72 (1,1) [6832,0]. true => box 1 _t903 [ SNF++, 3380 ] % 0.38/0.72 (7,1) [7208,0]. true => ~box 1~ _t494 [ SNF++, 3515 ] % 0.38/0.72 (19,1) [7214,0]. true => ~box 1~ _t520 [ SNF++, 3403 ] % 0.38/0.72 (1,1) [8145,0]. true => ~_t295 | ~_t31 [ GEN3, 6818, 6812, 7367, 7214, _t528, _t527, _t520 ] [ Backward Subsumption, 8970 ] % 0.38/0.72 (1,1) [8152,0]. true => _t297 | ~_t295 [ LRES, 8145, 268, ~_t31 ] [ Backward Subsumption, 8969 ] % 0.38/0.72 (1,1) [8176,0]. true => ~_t297 | ~_t29 [ GEN3, 6822, 6816, 7385, 7214, _t619, _t618, _t520 ] [ Backward Subsumption, 8975 ] % 0.38/0.72 (1,1) [8182,0]. true => _t299 | ~_t297 [ LRES, 8176, 279, ~_t29 ] [ Backward Subsumption, 8974 ] % 0.38/0.72 (1,1) [8212,0]. true => ~_t299 | ~_t27 [ GEN3, 6826, 6820, 7406, 7214, _t711, _t710, _t520 ] [ Backward Subsumption, 8980 ] % 0.38/0.72 (1,1) [8219,0]. true => _t301 | ~_t299 [ LRES, 8212, 287, ~_t27 ] [ Backward Subsumption, 8979 ] % 0.38/0.72 (1,1) [8252,0]. true => ~_t301 | ~_t25 [ GEN3, 6830, 6824, 7424, 7214, _t804, _t803, _t520 ] [ Backward Subsumption, 8985 ] % 0.38/0.73 (1,1) [8259,0]. true => _t303 | ~_t301 [ LRES, 8252, 292, ~_t25 ] [ Backward Subsumption, 8984 ] % 0.38/0.73 (1,1) [8273,0]. true => ~_t303 [ GEN3, 6832, 6828, 7444, 7214, _t903, _t902, _t520 ] % 0.38/0.73 (7,1) [8966,0]. true => ~_t33 [ GEN1, 6814, 7208, 7726, _t491, _t494 ] [ Modal Level Pure Literal Elimination, ~_t33 ] % 0.38/0.73 (7,1) [8968,0]. true => _t295 [ LRES, 8966, 254, ~_t33 ] [ Modal Level Pure Literal Elimination, _t295 ] % 0.38/0.73 (7,1) [8969,0]. true => _t297 [ Unit Resolution, 8968, 8152, _t295 ] [ Modal Level Pure Literal Elimination, _t297 ] % 0.38/0.73 (7,1) [8974,0]. true => _t299 [ Unit Resolution, 8969, 8182, _t297 ] [ Modal Level Pure Literal Elimination, _t299 ] % 0.38/0.73 (7,1) [8979,0]. true => _t301 [ Unit Resolution, 8974, 8219, _t299 ] [ Modal Level Pure Literal Elimination, _t301 ] % 0.38/0.73 (7,1) [8984,0]. true => _t303 [ Unit Resolution, 8979, 8259, _t301 ] % 0.38/0.73 (7,1) [8989,0]. true => false [ Unit Resolution, 8984, 8273, _t303 ] % 0.38/0.73 (1,1) [6813,1]. true => ~_t527 | ~_t32 [ SNF++, 252 ] % 0.38/0.73 (1,1) [6815,1]. true => ~_t491 | p2 [ SNF++, 253 ] [ Modal Level Pure Literal Elimination, ~_t491 ] % 0.38/0.73 (1,1) [6817,1]. true => ~_t618 | ~_t30 [ SNF++, 266 ] % 0.38/0.73 (1,1) [6819,1]. true => ~_t528 | _t32 [ SNF++, 267 ] [ Modal Level Pure Literal Elimination, ~_t528 ] % 0.38/0.73 (1,1) [6821,1]. true => ~_t710 | ~_t28 [ SNF++, 277 ] % 0.38/0.73 (1,1) [6823,1]. true => ~_t619 | _t30 [ SNF++, 278 ] [ Modal Level Pure Literal Elimination, ~_t619 ] % 0.38/0.73 (1,1) [6825,1]. true => ~_t803 | ~_t26 [ SNF++, 285 ] % 0.38/0.73 (1,1) [6827,1]. true => ~_t711 | _t28 [ SNF++, 286 ] [ Modal Level Pure Literal Elimination, ~_t711 ] % 0.38/0.73 (1,1) [6829,1]. true => ~_t902 | ~_t24 [ SNF++, 290 ] % 0.38/0.73 (1,1) [6831,1]. true => ~_t804 | _t26 [ SNF++, 291 ] % 0.38/0.73 (1,1) [6833,1]. true => ~_t903 | _t24 [ SNF++, 3380 ] % 0.38/0.73 (7,1) [7209,1]. true => ~_t494 | ~p2 [ SNF++, 3515 ] % 0.38/0.73 (1,1) [7367,1]. true => ~_t528 | ~_t527 [ LRES, 6813, 6819, ~_t32 ] [ Modal Level Pure Literal Elimination, ~_t528 ] % 0.38/0.73 (1,1) [7385,1]. true => ~_t619 | ~_t618 [ LRES, 6817, 6823, ~_t30 ] [ Modal Level Pure Literal Elimination, ~_t619 ] % 0.38/0.73 (1,1) [7406,1]. true => ~_t711 | ~_t710 [ LRES, 6821, 6827, ~_t28 ] [ Modal Level Pure Literal Elimination, ~_t711 ] % 0.38/0.73 (1,1) [7424,1]. true => ~_t804 | ~_t803 [ LRES, 6825, 6831, ~_t26 ] % 0.38/0.73 (1,1) [7444,1]. true => ~_t903 | ~_t902 [ LRES, 6829, 6833, ~_t24 ] % 0.38/0.73 (7,1) [7726,1]. true => ~_t494 | ~_t491 [ LRES, 7209, 6815, ~p2 ] [ Modal Level Pure Literal Elimination, ~_t491 ] % 0.38/0.73 % SZS output end Refutation % 0.38/0.73 % KSP exiting %------------------------------------------------------------------------------