%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP036_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n026.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 103.49s 104.37s % Output : Refutation 108.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.21 % Problem : SYP036_1 : TPTP v9.3.0. Released v9.3.0. % 0.02/0.22 % Command : run_ksp %s % 0.12/0.43 % Computer : n026.cluster.edu % 0.12/0.43 % Model : x86_64 x86_64 % 0.12/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.43 % Memory : 8042.1875MB % 0.12/0.43 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.43 % CPULimit : 300 % 0.12/0.43 % WCLimit : 300 % 0.12/0.43 % DateTime : Mon May 4 16:20:23 EDT 2026 % 0.12/0.44 % CPUTime : % 0.22/0.75 ----KSP format--- % 0.22/0.75 set(box,TRANS). % 0.22/0.75 usable(formulas). % 0.22/0.75 true. % 0.22/0.75 end_of_list. % 0.22/0.75 sos(formulas). % 0.22/0.75 ~ ([] ( 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.22/0.75 end_of_list. % 0.22/0.75 ----------------- % 0.22/0.75 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.NO4I7ywmaf/theBenchmark.ksp % 103.49/104.37 % 103.49/104.37 % SZS status Theorem % 103.49/104.37 % 103.49/104.37 ***************** % 103.49/104.37 FOUND PROOF 1 % 103.49/104.37 ***************** % 103.49/104.37 % SZS output start Refutation % 103.49/104.37 % 103.49/104.37 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 103.49/104.37 (1,1) [42026,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 3038609 ] % 103.49/104.37 (1,1) [46389,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 3038607 ] % 103.49/104.37 (1,1) [2546909,0]. _t40 => box 1 _t41 [ SNF ] [ Backward Subsumption, 3038707 ] % 103.49/104.37 (1,1) [2549820,0]. true => _t40 | ~_t0 [ SNF ] [ Backward Subsumption, 3038509 ] % 103.49/104.37 (1,1) [2903167,0]. _t78 => box 1 _t78 [ Axiom 4 ] [ Backward Subsumption, 3038796 ] % 103.49/104.37 (1,1) [2906077,0]. true => _t78 | ~_t0 [ SNF ] [ Backward Subsumption, 3038474 ] % 103.49/104.37 (1,1) [2974470,0]. _t268 => box 1 _t269 [ SNF ] [ Backward Subsumption, 3038785 ] % 103.49/104.37 (1,1) [2978833,0]. true => _t268 | ~_t0 [ SNF ] [ Backward Subsumption, 3038462 ] % 103.49/104.37 (1,1) [3025423,0]. _t271 => box 1 _t272 [ SNF ] [ Backward Subsumption, 3038774 ] % 103.49/104.37 (1,1) [3029786,0]. true => _t271 | ~_t0 [ SNF ] [ Backward Subsumption, 3038448 ] % 103.49/104.37 (325,1) [3035615,0]. _t69 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 3038768 ] % 103.49/104.37 (1,1) [3035616,0]. true => _t69 | ~_t0 [ SNF ] [ Backward Subsumption, 3038443 ] % 103.49/104.37 (1,1) [3038443,0]. true => _t69 [ Unit Resolution, 3, 3035616, _t0 ] [ Modal Level Pure Literal Elimination, _t69 ] % 103.49/104.37 (1,1) [3038448,0]. true => _t271 [ Unit Resolution, 3, 3029786, _t0 ] [ Modal Level Pure Literal Elimination, _t271 ] % 103.49/104.37 (1,1) [3038462,0]. true => _t268 [ Unit Resolution, 3, 2978833, _t0 ] [ Modal Level Pure Literal Elimination, _t268 ] % 103.49/104.37 (1,1) [3038474,0]. true => _t78 [ Unit Resolution, 3, 2906077, _t0 ] [ Modal Level Pure Literal Elimination, _t78 ] % 103.49/104.37 (1,1) [3038509,0]. true => _t40 [ Unit Resolution, 3, 2549820, _t0 ] [ Modal Level Pure Literal Elimination, _t40 ] % 103.49/104.37 (1,1) [3038607,0]. true => _t1 [ Unit Resolution, 3, 46389, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 103.49/104.37 (1,1) [3038609,0]. true => box 1 _t2 [ LHS Unit Resolution, 3038607, 42026, _t1 ] [ SNF++, 4457560, _t2 ] % 103.49/104.37 (1,1) [3038707,0]. true => box 1 _t41 [ LHS Unit Resolution, 3038509, 2546909, _t40 ] [ SNF++, 4457832, _t41 ] % 103.49/104.37 (325,1) [3038768,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 3038443, 3035615, _t69 ] [ SNF++, 4457984, ~p2 ] % 103.49/104.37 (1,1) [3038774,0]. true => box 1 _t272 [ LHS Unit Resolution, 3038448, 3025423, _t271 ] [ SNF++, 4457972, _t272 ] % 103.49/104.37 (1,1) [3038785,0]. true => box 1 _t269 [ LHS Unit Resolution, 3038462, 2974470, _t268 ] [ SNF++, 4457952, _t269 ] % 103.49/104.37 (1,1) [3038796,0]. true => box 1 _t78 [ LHS Unit Resolution, 3038474, 2903167, _t78 ] [ SNF++, 4457920, _t78 ] % 103.49/104.37 (1,1) [4457560,0]. true => box 1 _t284 [ SNF++, 3038609 ] % 103.49/104.37 (1,1) [4457832,0]. true => box 1 _t313 [ SNF++, 3038707 ] % 103.49/104.37 (1,1) [4457920,0]. true => box 1 _t345 [ SNF++, 3038796 ] % 103.49/104.37 (1,1) [4457952,0]. true => box 1 _t539 [ SNF++, 3038785 ] % 103.49/104.37 (1,1) [4457972,0]. true => box 1 _t541 [ SNF++, 3038774 ] % 103.49/104.37 (325,1) [4457984,0]. true => ~box 1~ _t545 [ SNF++, 3038768 ] % 103.49/104.37 (325,1) [4949466,0]. true => false [ GEN1, 4457972, 4457920, 4457560, 4457832, 4457952, 4457984, 4947999, _t541, _t345, _t284, _t313, _t539, _t545 ] % 103.49/104.37 (1,1) [37666,1]. _t2 => box 1 _t3 [ SNF ] [ SNF++, 4456762, _t3 ] % 103.49/104.37 (1,1) [2544000,1]. _t41 => box 1 _t42 [ SNF ] [ SNF++, 4457344, _t42 ] % 103.49/104.37 (1,1) [2767902,1]. _t42 => box 1 _t42 [ Axiom 4 ] [ SNF++, 4457342, _t42 ] % 103.49/104.37 (1,1) [2903169,1]. _t78 => box 1 _t79 [ Axiom 4 ] [ SNF++, 4457502, _t79 ] % 103.49/104.37 (1,1) [2970110,1]. _t269 => box 1 _t270 [ SNF ] [ SNF++, 4457534, _t270 ] % 103.49/104.37 (315,1) [3025421,1]. _t138 => ~box 1~ ~p1 [ SNF ] [ SNF++, 4457558, ~p1 ] % 103.49/104.37 (1,1) [3025422,1]. true => ~_t272 | _t138 | p2 [ SNF ] % 103.49/104.37 (1,1) [4456762,1]. _t2 => box 1 _t283 [ SNF++, 37666 ] % 103.49/104.37 (1,1) [4457344,1]. _t41 => box 1 _t312 [ SNF++, 2544000 ] % 103.49/104.37 (1,1) [4457502,1]. _t78 => box 1 _t344 [ SNF++, 2903169 ] % 103.49/104.37 (1,1) [4457534,1]. _t269 => box 1 _t538 [ SNF++, 2970110 ] % 103.49/104.37 (315,1) [4457558,1]. _t138 => ~box 1~ _t548 [ SNF++, 3025421 ] % 103.49/104.37 (1,1) [4457561,1]. true => ~_t284 | _t2 [ SNF++, 3038609 ] % 103.49/104.37 (1,1) [4457833,1]. true => ~_t313 | _t41 [ SNF++, 3038707 ] % 103.49/104.37 (1,1) [4457921,1]. true => ~_t345 | _t78 [ SNF++, 3038796 ] % 103.49/104.37 (1,1) [4457953,1]. true => ~_t539 | _t269 [ SNF++, 3038785 ] % 103.49/104.37 (1,1) [4457973,1]. true => ~_t541 | _t272 [ SNF++, 3038774 ] % 103.49/104.37 (325,1) [4457985,1]. true => ~_t545 | ~p2 [ SNF++, 3038768 ] % 103.49/104.37 (325,1) [4479757,1]. true => ~_t545 | ~_t272 | _t138 [ LRES, 4457985, 3025422, ~p2 ] % 103.49/104.37 (315,1) [4909904,1]. true => ~_t269 | ~_t138 | ~_t78 | ~_t41 | ~_t2 [ GEN1, 4457534, 4457344, 4456762, 4457502, 4457558, 4908448, _t538, _t312, _t283, _t344, _t548 ] % 103.49/104.37 (315,1) [4917221,1]. true => ~_t284 | ~_t269 | ~_t138 | ~_t78 | ~_t41 [ LRES, 4909904, 4457561, ~_t2 ] % 103.49/104.37 (315,1) [4917349,1]. true => ~_t313 | ~_t284 | ~_t269 | ~_t138 | ~_t78 [ LRES, 4917221, 4457833, ~_t41 ] % 103.49/104.37 (315,1) [4917393,1]. true => ~_t345 | ~_t313 | ~_t284 | ~_t269 | ~_t138 [ LRES, 4917349, 4457921, ~_t78 ] % 103.49/104.37 (325,1) [4930510,1]. true => ~_t545 | ~_t345 | ~_t313 | ~_t284 | ~_t272 | ~_t269 [ LRES, 4917393, 4479757, ~_t138 ] % 103.49/104.37 (325,1) [4931962,1]. true => ~_t545 | ~_t539 | ~_t345 | ~_t313 | ~_t284 | ~_t272 [ LRES, 4930510, 4457953, ~_t269 ] % 103.49/104.37 (325,1) [4947999,1]. true => ~_t545 | ~_t541 | ~_t539 | ~_t345 | ~_t313 | ~_t284 [ LRES, 4931962, 4457973, ~_t272 ] % 103.49/104.37 (1,1) [33309,2]. _t3 => box 1 _t4 [ SNF ] [ SNF++, 4455928, _t4 ] % 103.49/104.37 (1,1) [2541093,2]. _t42 => box 1 _t43 [ SNF ] [ SNF++, 4456602, _t43 ] % 103.49/104.37 (1,1) [2764996,2]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4456600, _t43 ] % 103.49/104.37 (259,1) [2888614,2]. _t57 => ~box 1~ ~p6 [ SNF ] [ SNF++, 4456754, ~p6 ] % 103.49/104.37 (1,1) [2900260,2]. _t79 => box 1 _t80 [ Axiom 4 ] [ SNF++, 4456732, _t80 ] % 103.49/104.37 (1,1) [2970109,2]. true => ~_t270 | _t57 | p1 [ SNF ] % 103.49/104.37 (1,1) [4455928,2]. _t3 => box 1 _t282 [ SNF++, 33309 ] % 103.49/104.37 (1,1) [4456602,2]. _t42 => box 1 _t311 [ SNF++, 2541093 ] % 103.49/104.37 (1,1) [4456732,2]. _t79 => box 1 _t343 [ SNF++, 2900260 ] % 103.49/104.37 (259,1) [4456754,2]. _t57 => ~box 1~ _t544 [ SNF++, 2888614 ] % 103.49/104.37 (1,1) [4456763,2]. true => ~_t283 | _t3 [ SNF++, 37666 ] % 103.49/104.37 (1,1) [4457343,2]. true => ~_t312 | _t42 [ SNF++, 2767902 ] % 103.49/104.37 (1,1) [4457503,2]. true => ~_t344 | _t79 [ SNF++, 2903169 ] % 103.49/104.37 (1,1) [4457535,2]. true => ~_t538 | _t270 [ SNF++, 2970110 ] % 103.49/104.37 (315,1) [4457559,2]. true => ~_t548 | ~p1 [ SNF++, 3025421 ] % 103.49/104.37 (315,1) [4479753,2]. true => ~_t548 | ~_t270 | _t57 [ LRES, 4457559, 2970109, ~p1 ] % 103.49/104.37 (259,1) [4893874,2]. true => ~_t79 | ~_t57 | ~_t42 | ~_t3 [ GEN1, 4456732, 4455928, 4456602, 4456754, 4879271, _t343, _t282, _t311, _t544 ] % 103.49/104.37 (259,1) [4895333,2]. true => ~_t283 | ~_t79 | ~_t57 | ~_t42 [ LRES, 4893874, 4456763, ~_t3 ] % 103.49/104.37 (259,1) [4898251,2]. true => ~_t312 | ~_t283 | ~_t79 | ~_t57 [ LRES, 4895333, 4457343, ~_t42 ] % 103.49/104.37 (315,1) [4902625,2]. true => ~_t548 | ~_t312 | ~_t283 | ~_t270 | ~_t79 [ LRES, 4898251, 4479753, ~_t57 ] % 103.49/104.37 (315,1) [4904080,2]. true => ~_t548 | ~_t344 | ~_t312 | ~_t283 | ~_t270 [ LRES, 4902625, 4457503, ~_t79 ] % 103.49/104.37 (315,1) [4908448,2]. true => ~_t548 | ~_t538 | ~_t344 | ~_t312 | ~_t283 [ LRES, 4904080, 4457535, ~_t270 ] % 103.49/104.37 (1,1) [28955,3]. _t4 => box 1 _t5 [ SNF ] [ SNF++, 4455052, _t5 ] % 103.49/104.37 (1,1) [2538188,3]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 4455816, _t44 ] % 103.49/104.37 (1,1) [2538189,3]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4455820, _t43 ] % 103.49/104.37 (1,1) [2541096,3]. _t42 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4455818, _t43 ] % 103.49/104.37 (231,1) [2764993,3]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4455916, ~p4 ] % 103.49/104.37 (1,1) [2900259,3]. true => ~_t80 | _t45 | p6 [ Axiom 4 ] % 103.49/104.37 (1,1) [4455052,3]. _t4 => box 1 _t281 [ SNF++, 28955 ] % 103.49/104.37 (1,1) [4455816,3]. _t43 => box 1 _t310 [ SNF++, 2538188 ] % 103.49/104.37 (1,1) [4455820,3]. _t43 => box 1 _t311 [ SNF++, 2538189 ] % 103.49/104.37 (231,1) [4455916,3]. _t45 => ~box 1~ _t543 [ SNF++, 2764993 ] % 103.49/104.37 (1,1) [4455929,3]. true => ~_t282 | _t4 [ SNF++, 33309 ] % 103.49/104.37 (1,1) [4456601,3]. true => ~_t311 | _t43 [ SNF++, 2764996 ] % 103.49/104.37 (1,1) [4456733,3]. true => ~_t343 | _t80 [ SNF++, 2900260 ] % 103.49/104.37 (259,1) [4456755,3]. true => ~_t544 | ~p6 [ SNF++, 2888614 ] % 103.49/104.37 (259,1) [4465236,3]. true => ~_t544 | ~_t80 | _t45 [ LRES, 4456755, 2900259, ~p6 ] % 103.49/104.37 (231,1) [4863252,3]. true => ~_t45 | ~_t43 | ~_t4 [ GEN1, 4455820, 4455052, 4455816, 4455916, 4841448, _t311, _t281, _t310, _t543 ] % 103.49/104.37 (231,1) [4863254,3]. true => ~_t282 | ~_t45 | ~_t43 [ LRES, 4863252, 4455929, ~_t4 ] % 103.49/104.37 (231,1) [4864708,3]. true => ~_t311 | ~_t282 | ~_t45 [ LRES, 4863254, 4456601, ~_t43 ] % 103.49/104.37 (259,1) [4866162,3]. true => ~_t544 | ~_t311 | ~_t282 | ~_t80 [ LRES, 4864708, 4465236, ~_t45 ] % 103.49/104.37 (259,1) [4879271,3]. true => ~_t544 | ~_t343 | ~_t311 | ~_t282 [ LRES, 4866162, 4456733, ~_t80 ] % 103.49/104.37 (1,1) [24604,4]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 4454156, _t6 ] % 103.49/104.37 (193,1) [2538186,4]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4455040, ~p4 ] % 103.49/104.37 (1,1) [2538187,4]. true => _t45 | ~_t44 | p4 [ SNF ] % 103.49/104.37 (1,1) [2538191,4]. _t43 => box 1 _t44 [ Axiom 4 ] [ SNF++, 4454988, _t44 ] % 103.49/104.37 (1,1) [2538192,4]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4454862, _t43 ] % 103.49/104.37 (1,1) [4454156,4]. _t5 => box 1 _t280 [ SNF++, 24604 ] % 103.49/104.37 (1,1) [4454862,4]. _t43 => box 1 _t311 [ SNF++, 2538192 ] % 103.49/104.37 (1,1) [4454988,4]. _t43 => box 1 _t310 [ SNF++, 2538191 ] % 103.49/104.37 (193,1) [4455040,4]. _t45 => ~box 1~ _t543 [ SNF++, 2538186 ] % 103.49/104.37 (1,1) [4455053,4]. true => ~_t281 | _t5 [ SNF++, 28955 ] % 103.49/104.37 (1,1) [4455817,4]. true => ~_t310 | _t44 [ SNF++, 2538188 ] % 103.49/104.37 (1,1) [4455819,4]. true => ~_t311 | _t43 [ SNF++, 2541096 ] % 103.49/104.37 (231,1) [4455917,4]. true => ~_t543 | ~p4 [ SNF++, 2764993 ] % 103.49/104.37 (231,1) [4465232,4]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4455917, 2538187, ~p4 ] % 103.49/104.37 (231,1) [4498627,4]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465232, 4455817, ~_t44 ] % 103.49/104.37 (193,1) [4838544,4]. true => ~_t45 | ~_t43 | ~_t5 [ GEN1, 4454862, 4454156, 4454988, 4455040, 4813844, _t311, _t280, _t310, _t543 ] % 103.49/104.37 (193,1) [4838545,4]. true => ~_t281 | ~_t45 | ~_t43 [ LRES, 4838544, 4455053, ~_t5 ] % 103.49/104.37 (193,1) [4839995,4]. true => ~_t311 | ~_t281 | ~_t45 [ LRES, 4838545, 4455819, ~_t43 ] % 103.49/104.37 (231,1) [4841448,4]. true => ~_t543 | ~_t311 | ~_t310 | ~_t281 [ LRES, 4839995, 4498627, ~_t45 ] % 103.49/104.37 (1,1) [20256,5]. _t6 => box 1 _t7 [ SNF ] [ SNF++, 4453240, _t7 ] % 103.49/104.37 (1,1) [2032543,5]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 4454038, _t44 ] % 103.49/104.37 (1,1) [2032544,5]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4454042, _t43 ] % 103.49/104.37 (1,1) [2035447,5]. _t42 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4454040, _t43 ] % 103.49/104.37 (169,1) [2363797,5]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4454144, ~p4 ] % 103.49/104.37 (1,1) [2538190,5]. true => _t45 | ~_t44 | p4 [ Axiom 4 ] % 103.49/104.37 (1,1) [4453240,5]. _t6 => box 1 _t279 [ SNF++, 20256 ] % 103.49/104.37 (1,1) [4454038,5]. _t43 => box 1 _t310 [ SNF++, 2032543 ] % 103.49/104.37 (1,1) [4454042,5]. _t43 => box 1 _t311 [ SNF++, 2032544 ] % 103.49/104.37 (169,1) [4454144,5]. _t45 => ~box 1~ _t543 [ SNF++, 2363797 ] % 103.49/104.37 (1,1) [4454157,5]. true => ~_t280 | _t6 [ SNF++, 24604 ] % 103.49/104.37 (1,1) [4454863,5]. true => ~_t311 | _t43 [ SNF++, 2538192 ] % 103.49/104.37 (1,1) [4454989,5]. true => ~_t310 | _t44 [ SNF++, 2538191 ] % 103.49/104.37 (193,1) [4455041,5]. true => ~_t543 | ~p4 [ SNF++, 2538186 ] % 103.49/104.37 (193,1) [4465229,5]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4455041, 2538190, ~p4 ] % 103.49/104.37 (193,1) [4498626,5]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465229, 4454989, ~_t44 ] % 103.49/104.37 (169,1) [4810939,5]. true => ~_t45 | ~_t43 | ~_t6 [ GEN1, 4454042, 4453240, 4454038, 4454144, 4783390, _t311, _t279, _t310, _t543 ] % 103.49/104.37 (169,1) [4810941,5]. true => ~_t280 | ~_t45 | ~_t43 [ LRES, 4810939, 4454157, ~_t6 ] % 103.49/104.37 (169,1) [4812391,5]. true => ~_t311 | ~_t280 | ~_t45 [ LRES, 4810941, 4454863, ~_t43 ] % 103.49/104.37 (193,1) [4813844,5]. true => ~_t543 | ~_t311 | ~_t310 | ~_t280 [ LRES, 4812391, 4498626, ~_t45 ] % 103.49/104.37 (1,1) [15911,6]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 4452308, _t8 ] % 103.49/104.37 (131,1) [2032541,6]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4453228, ~p4 ] % 103.49/104.37 (1,1) [2032542,6]. true => _t45 | ~_t44 | p4 [ SNF ] % 103.49/104.37 (1,1) [2032546,6]. _t43 => box 1 _t44 [ Axiom 4 ] [ SNF++, 4453174, _t44 ] % 103.49/104.37 (1,1) [2032547,6]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4453040, _t43 ] % 103.49/104.37 (1,1) [4452308,6]. _t7 => box 1 _t278 [ SNF++, 15911 ] % 103.49/104.37 (1,1) [4453040,6]. _t43 => box 1 _t311 [ SNF++, 2032547 ] % 103.49/104.37 (1,1) [4453174,6]. _t43 => box 1 _t310 [ SNF++, 2032546 ] % 103.49/104.37 (131,1) [4453228,6]. _t45 => ~box 1~ _t543 [ SNF++, 2032541 ] % 103.49/104.37 (1,1) [4453241,6]. true => ~_t279 | _t7 [ SNF++, 20256 ] % 103.49/104.37 (1,1) [4454039,6]. true => ~_t310 | _t44 [ SNF++, 2032543 ] % 103.49/104.37 (1,1) [4454041,6]. true => ~_t311 | _t43 [ SNF++, 2035447 ] % 103.49/104.37 (169,1) [4454145,6]. true => ~_t543 | ~p4 [ SNF++, 2363797 ] % 103.49/104.37 (169,1) [4465226,6]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4454145, 2032542, ~p4 ] % 103.49/104.37 (169,1) [4498625,6]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465226, 4454039, ~_t44 ] % 103.49/104.37 (131,1) [4774721,6]. true => ~_t45 | ~_t43 | ~_t7 [ GEN1, 4453040, 4452308, 4453174, 4453228, 4715475, _t311, _t278, _t310, _t543 ] % 103.49/104.37 (131,1) [4774722,6]. true => ~_t279 | ~_t45 | ~_t43 [ LRES, 4774721, 4453241, ~_t7 ] % 103.49/104.37 (131,1) [4776170,6]. true => ~_t311 | ~_t279 | ~_t45 [ LRES, 4774722, 4454041, ~_t43 ] % 103.49/104.37 (169,1) [4783390,6]. true => ~_t543 | ~_t311 | ~_t310 | ~_t279 [ LRES, 4776170, 4498625, ~_t45 ] % 103.49/104.37 (1,1) [11569,7]. _t8 => box 1 _t9 [ SNF ] [ SNF++, 4451364, _t9 ] % 103.49/104.37 (1,1) [1326884,7]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 4452188, _t44 ] % 103.49/104.37 (1,1) [1326885,7]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4452192, _t43 ] % 103.49/104.37 (1,1) [1329784,7]. _t42 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4452190, _t43 ] % 103.49/104.37 (107,1) [1788576,7]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4452298, ~p4 ] % 103.49/104.37 (1,1) [2032545,7]. true => _t45 | ~_t44 | p4 [ Axiom 4 ] % 103.49/104.37 (1,1) [4451364,7]. _t8 => box 1 _t277 [ SNF++, 11569 ] % 103.49/104.37 (1,1) [4452188,7]. _t43 => box 1 _t310 [ SNF++, 1326884 ] % 103.49/104.37 (1,1) [4452192,7]. _t43 => box 1 _t311 [ SNF++, 1326885 ] % 103.49/104.37 (107,1) [4452298,7]. _t45 => ~box 1~ _t543 [ SNF++, 1788576 ] % 103.49/104.37 (1,1) [4452309,7]. true => ~_t278 | _t8 [ SNF++, 15911 ] % 103.49/104.37 (1,1) [4453041,7]. true => ~_t311 | _t43 [ SNF++, 2032547 ] % 103.49/104.37 (1,1) [4453175,7]. true => ~_t310 | _t44 [ SNF++, 2032546 ] % 103.49/104.37 (131,1) [4453229,7]. true => ~_t543 | ~p4 [ SNF++, 2032541 ] % 103.49/104.37 (131,1) [4465223,7]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4453229, 2032545, ~p4 ] % 103.49/104.37 (131,1) [4504415,7]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465223, 4453175, ~_t44 ] % 103.49/104.37 (107,1) [4705355,7]. true => ~_t45 | ~_t43 | ~_t8 [ GEN1, 4452192, 4451364, 4452188, 4452298, 4643192, _t311, _t277, _t310, _t543 ] % 103.49/104.37 (107,1) [4705357,7]. true => ~_t278 | ~_t45 | ~_t43 [ LRES, 4705355, 4452309, ~_t8 ] % 103.49/104.37 (107,1) [4709694,7]. true => ~_t311 | ~_t278 | ~_t45 [ LRES, 4705357, 4453041, ~_t43 ] % 103.49/104.37 (131,1) [4715475,7]. true => ~_t543 | ~_t311 | ~_t310 | ~_t278 [ LRES, 4709694, 4504415, ~_t45 ] % 103.49/104.37 (1,1) [7230,8]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 4450408, _t10 ] % 103.49/104.37 (67,1) [1326882,8]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4451352, ~p4 ] % 103.49/104.37 (1,1) [1326883,8]. true => _t45 | ~_t44 | p4 [ SNF ] % 103.49/104.37 (1,1) [1326887,8]. _t43 => box 1 _t44 [ Axiom 4 ] [ SNF++, 4451298, _t44 ] % 103.49/104.37 (1,1) [1326888,8]. _t43 => box 1 _t43 [ Axiom 4 ] [ SNF++, 4450516, _t43 ] % 103.49/104.37 (1,1) [4450408,8]. _t9 => box 1 _t276 [ SNF++, 7230 ] % 103.49/104.37 (1,1) [4450516,8]. _t43 => box 1 _t311 [ SNF++, 1326888 ] % 103.49/104.37 (1,1) [4451298,8]. _t43 => box 1 _t310 [ SNF++, 1326887 ] % 103.49/104.37 (67,1) [4451352,8]. _t45 => ~box 1~ _t543 [ SNF++, 1326882 ] % 103.49/104.37 (1,1) [4451365,8]. true => ~_t277 | _t9 [ SNF++, 11569 ] % 103.49/104.37 (1,1) [4452189,8]. true => ~_t310 | _t44 [ SNF++, 1326884 ] % 103.49/104.37 (1,1) [4452191,8]. true => ~_t311 | _t43 [ SNF++, 1329784 ] % 103.49/104.37 (107,1) [4452299,8]. true => ~_t543 | ~p4 [ SNF++, 1788576 ] % 103.49/104.37 (107,1) [4472473,8]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4452299, 1326883, ~p4 ] % 103.49/104.37 (107,1) [4511646,8]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4472473, 4452189, ~_t44 ] % 103.49/104.37 (67,1) [4641734,8]. true => ~_t45 | ~_t43 | ~_t9 [ GEN1, 4450516, 4450408, 4451298, 4451352, 4555042, _t311, _t276, _t310, _t543 ] % 103.49/104.37 (67,1) [4641735,8]. true => ~_t277 | ~_t45 | ~_t43 [ LRES, 4641734, 4451365, ~_t9 ] % 103.49/104.37 (67,1) [4643183,8]. true => ~_t311 | ~_t277 | ~_t45 [ LRES, 4641735, 4452191, ~_t43 ] % 103.49/104.37 (107,1) [4643192,8]. true => ~_t543 | ~_t311 | ~_t310 | ~_t277 [ LRES, 4643183, 4511646, ~_t45 ] % 103.49/104.37 (1,1) [2894,9]. _t10 => box 1 _t11 [ SNF ] [ SNF++, 4449440, _t11 ] % 103.49/104.37 (1,1) [139164,9]. _t43 => box 1 _t44 [ SNF ] [ SNF++, 4449560, _t44 ] % 103.49/104.37 (43,1) [1013437,9]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 4450398, ~p4 ] % 103.49/104.37 (1,1) [1326886,9]. true => _t45 | ~_t44 | p4 [ Axiom 4 ] % 103.49/104.37 (1,1) [4449440,9]. _t10 => box 1 _t275 [ SNF++, 2894 ] % 103.49/104.37 (1,1) [4449560,9]. _t43 => box 1 _t310 [ SNF++, 139164 ] % 103.49/104.37 (43,1) [4450398,9]. _t45 => ~box 1~ _t543 [ SNF++, 1013437 ] % 103.49/104.37 (1,1) [4450409,9]. true => ~_t276 | _t10 [ SNF++, 7230 ] % 103.49/104.37 (1,1) [4450517,9]. true => ~_t311 | _t43 [ SNF++, 1326888 ] % 103.49/104.37 (1,1) [4451299,9]. true => ~_t310 | _t44 [ SNF++, 1326887 ] % 103.49/104.37 (67,1) [4451353,9]. true => ~_t543 | ~p4 [ SNF++, 1326882 ] % 103.49/104.37 (67,1) [4465214,9]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4451353, 1326886, ~p4 ] % 108.99/109.82 (67,1) [4504414,9]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465214, 4451299, ~_t44 ] % 108.99/109.82 (43,1) [4547801,9]. true => ~_t45 | ~_t43 | ~_t10 [ GEN1, 4449560, 4449440, 4450398, 4534790, _t310, _t275, _t543 ] % 108.99/109.82 (43,1) [4550690,9]. true => ~_t276 | ~_t45 | ~_t43 [ LRES, 4547801, 4450409, ~_t10 ] % 108.99/109.82 (43,1) [4552136,9]. true => ~_t311 | ~_t276 | ~_t45 [ LRES, 4550690, 4450517, ~_t43 ] % 108.99/109.82 (67,1) [4555042,9]. true => ~_t543 | ~_t311 | ~_t310 | ~_t276 [ LRES, 4552136, 4504414, ~_t45 ] % 108.99/109.82 (1,1) [4,10]. _t11 => box 1 p4 [ SNF ] [ SNF++, 3038930, p4 ] % 108.99/109.82 (3,1) [139162,10]. _t45 => ~box 1~ ~p4 [ SNF ] [ SNF++, 3039898, ~p4 ] % 108.99/109.82 (1,1) [139163,10]. true => _t45 | ~_t44 | p4 [ SNF ] % 108.99/109.82 (1,1) [3038930,10]. _t11 => box 1 _t274 [ SNF++, 4 ] % 108.99/109.82 (3,1) [3039898,10]. _t45 => ~box 1~ _t543 [ SNF++, 139162 ] % 108.99/109.82 (1,1) [4449441,10]. true => ~_t275 | _t11 [ SNF++, 2894 ] % 108.99/109.82 (1,1) [4449561,10]. true => ~_t310 | _t44 [ SNF++, 139164 ] % 108.99/109.82 (43,1) [4450399,10]. true => ~_t543 | ~p4 [ SNF++, 1013437 ] % 108.99/109.82 (43,1) [4465245,10]. true => ~_t543 | _t45 | ~_t44 [ LRES, 4450399, 139163, ~p4 ] % 108.99/109.82 (3,1) [4497181,10]. true => ~_t45 | ~_t11 [ GEN1, 3038930, 3039898, 4457997, _t274, _t543 ] % 108.99/109.82 (3,1) [4498628,10]. true => ~_t275 | ~_t45 [ LRES, 4497181, 4449441, ~_t11 ] % 108.99/109.82 (43,1) [4518877,10]. true => ~_t543 | ~_t310 | _t45 [ LRES, 4465245, 4449561, ~_t44 ] % 108.99/109.82 (43,1) [4534790,10]. true => ~_t543 | ~_t310 | ~_t275 [ LRES, 4518877, 4498628, _t45 ] % 108.99/109.82 (1,1) [3038931,11]. true => ~_t274 | p4 [ SNF++, 4 ] % 108.99/109.82 (3,1) [3039899,11]. true => ~_t543 | ~p4 [ SNF++, 139162 ] % 108.99/109.82 (3,1) [4457997,11]. true => ~_t543 | ~_t274 [ LRES, 3039899, 3038931, ~p4 ] % 108.99/109.82 % SZS output end Refutation % 0.32/109.99 % KSP exiting %------------------------------------------------------------------------------