%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYO922_1.014 : TPTP v9.0.0. Released v9.0.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n018.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 : Wed Apr 9 10:47:48 PM UTC 2025 % Result : Theorem 220.17s 220.63s % Output : Refutation 226.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO922_1.014 : TPTP v9.0.0. Released v9.0.0. % 0.03/0.12 % Command : run_ksp %s % 0.12/0.33 % Computer : n018.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Apr 9 10:26:47 EDT 2025 % 0.12/0.33 % CPUTime : % 0.42/0.59 ----KSP format--- % 0.42/0.59 set(box,SER,TRANS). % 0.42/0.59 usable(formulas). % 0.42/0.59 true. % 0.42/0.59 end_of_list. % 0.42/0.59 sos(formulas). % 0.42/0.59 ~ (~ ( ( [] ( x0 ) & [] ( ~ ( x0 ) ) ) | ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & <> ( [] ( <> ( ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & <> ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) & <> ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) | [] ( [] ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) & [] ( ( <> ( [] ( ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) ) | <> ( ( p0 | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( [] ( z3 ) & <> ( <> ( [] ( <> ( ~ ( z3 ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( <> ( ( p0 | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( [] ( z3 ) & <> ( <> ( [] ( <> ( ~ ( z3 ) ) ) ) ) ) ) ) ) ) | <> ( [] ( ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) ) ) & ( <> ( [] ( ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( ( p0 | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( [] ( z3 ) & <> ( <> ( [] ( <> ( ~ ( z3 ) ) ) ) ) ) ) ) ) ) ) & [] ( [] ( <> ( [] ( ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) ) ) | ~ ( p0 ) | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) | [] ( ( p0 | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( [] ( z3 ) & <> ( <> ( [] ( <> ( ~ ( z3 ) ) ) ) ) ) ) ) ) & [] ( <> ( ( p0 | ( [] ( z0 ) & <> ( <> ( [] ( <> ( ~ ( z0 ) ) ) ) ) ) ) & <> ( ~ ( p3 ) | ( [] ( z3 ) & <> ( <> ( [] ( <> ( ~ ( z3 ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) ) & [] ( <> ( [] ( ~ ( p1 ) | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) | [] ( [] ( <> ( p1 | ( [] ( z1 ) & <> ( <> ( [] ( <> ( ~ ( z1 ) ) ) ) ) ) ) ) ) ) & [] ( ~ ( p4 ) | ( [] ( z4 ) & <> ( <> ( [] ( <> ( ~ ( z4 ) ) ) ) ) ) ) ) ) ). % 0.42/0.59 end_of_list. % 0.42/0.59 ----------------- % 0.42/0.59 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.HGZP1hFpvR/theBenchmark.ksp % 220.17/220.63 % 220.17/220.63 % SZS status Theorem % 220.17/220.63 % 220.17/220.63 ***************** % 220.17/220.63 FOUND PROOF 1 % 220.17/220.63 ***************** % 220.17/220.63 % SZS output start Refutation % 220.17/220.63 % 220.17/220.63 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 220.17/220.63 (1,1) [5,0]. true => ~_t1 [ Axiom SER ] [ Modal Level Pure Literal Elimination, ~_t1 ] % 220.17/220.63 (1,1) [372781,0]. _t3 => box 1 _t4 [ SNF ] [ Backward Subsumption, 475968 ] % 220.17/220.63 (1,1) [377478,0]. true => _t3 | ~_t2 [ SNF ] [ Backward Subsumption, 475964 ] % 220.17/220.63 (3086,1) [431498,0]. _t81 => ~box 1~ _t82 [ SNF ] [ Backward Subsumption, 475974 ] % 220.17/220.63 (1,1) [431499,0]. true => _t81 | ~_t2 [ SNF ] [ Backward Subsumption, 475959 ] % 220.17/220.63 (1,1) [431500,0]. true => _t2 | _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 453567 ] % 220.17/220.63 (1,1) [453567,0]. true => _t2 | ~_t0 [ Unit Resolution, 5, 431500, _t1 ] [ Backward Subsumption, 453568 ] % 220.17/220.63 (1,1) [453568,0]. true => _t2 [ Unit Resolution, 3, 453567, _t0 ] [ Modal Level Pure Literal Elimination, _t2 ] % 220.17/220.63 (1,1) [475959,0]. true => _t81 [ Unit Resolution, 453568, 431499, _t2 ] [ Modal Level Pure Literal Elimination, _t81 ] % 220.17/220.63 (1,1) [475964,0]. true => _t3 [ Unit Resolution, 453568, 377478, _t2 ] [ Modal Level Pure Literal Elimination, _t3 ] % 220.17/220.63 (1,1) [475968,0]. true => box 1 _t4 [ LHS Unit Resolution, 475964, 372781, _t3 ] [ SNF++, 475983, _t4 ] % 220.17/220.63 (3086,1) [475974,0]. true => ~box 1~ _t82 [ LHS Unit Resolution, 475959, 431498, _t81 ] [ SNF++, 476017, _t82 ] % 220.17/220.63 (1,1) [475983,0]. true => box 1 _t85106 [ SNF++, 475968 ] % 220.17/220.63 (3086,1) [476017,0]. true => ~box 1~ _t85115 [ SNF++, 475974 ] % 220.17/220.63 (3086,1) [6350994,0]. true => false [ GEN1, 475983, 476017, 6350716, _t85106, _t85115 ] % 220.17/220.63 (1,1) [349342,1]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 476019, _t6 ] % 220.17/220.63 (1,1) [354030,1]. true => _t5 | ~_t4 [ SNF ] % 220.17/220.63 (3078,1) [431496,1]. _t83 => ~box 1~ _t84 [ SNF ] [ SNF++, 476093, _t84 ] % 220.17/220.63 (3086,1) [431497,1]. true => _t83 | ~_t82 [ SNF ] % 220.17/220.63 (1,1) [475984,1]. true => ~_t85106 | _t4 [ SNF++, 475968 ] % 220.17/220.63 (3086,1) [476018,1]. true => ~_t85115 | _t82 [ SNF++, 475974 ] % 220.17/220.63 (1,1) [476019,1]. _t5 => box 1 _t85116 [ SNF++, 349342 ] % 220.17/220.63 (3078,1) [476093,1]. _t83 => ~box 1~ _t85126 [ SNF++, 431496 ] % 220.17/220.63 (1,1) [634567,1]. true => ~_t85106 | _t5 [ LRES, 354030, 475984, ~_t4 ] % 220.17/220.63 (3086,1) [634599,1]. true => ~_t85115 | _t83 [ LRES, 431497, 476018, ~_t82 ] % 220.17/220.63 (3078,1) [6350005,1]. true => ~_t83 | ~_t5 [ GEN1, 476019, 476093, 6349393, _t85116, _t85126 ] % 220.17/220.63 (3078,1) [6350446,1]. true => ~_t85106 | ~_t83 [ LRES, 6350005, 634567, ~_t5 ] % 220.17/220.63 (3086,1) [6350716,1]. true => ~_t85115 | ~_t85106 [ LRES, 6350446, 634599, ~_t83 ] % 220.17/220.63 (1,1) [325948,2]. _t7 => box 1 _t8 [ SNF ] [ SNF++, 476095, _t8 ] % 220.17/220.63 (1,1) [330627,2]. true => _t7 | ~_t6 [ SNF ] % 220.17/220.63 (3077,1) [431494,2]. _t85 => ~box 1~ _t86 [ SNF ] [ SNF++, 476207, _t86 ] % 220.17/220.63 (3078,1) [431495,2]. true => _t85 | ~_t84 [ SNF ] % 220.17/220.63 (1,1) [476020,2]. true => ~_t85116 | _t6 [ SNF++, 349342 ] % 220.17/220.63 (3078,1) [476094,2]. true => ~_t85126 | _t84 [ SNF++, 431496 ] % 220.17/220.63 (1,1) [476095,2]. _t7 => box 1 _t85127 [ SNF++, 325948 ] % 220.17/220.63 (3077,1) [476207,2]. _t85 => ~box 1~ _t85132 [ SNF++, 431494 ] % 220.17/220.63 (1,1) [634568,2]. true => ~_t85116 | _t7 [ LRES, 330627, 476020, ~_t6 ] % 220.17/220.63 (3078,1) [637180,2]. true => ~_t85126 | _t85 [ LRES, 431495, 476094, ~_t84 ] % 220.17/220.63 (3077,1) [6348673,2]. true => ~_t85 | ~_t7 [ GEN1, 476095, 476207, 6348397, _t85127, _t85132 ] % 220.17/220.63 (3077,1) [6349036,2]. true => ~_t85116 | ~_t85 [ LRES, 6348673, 634568, ~_t7 ] % 220.17/220.63 (3078,1) [6349393,2]. true => ~_t85126 | ~_t85116 [ LRES, 6349036, 637180, ~_t85 ] % 220.17/220.63 (1,1) [302599,3]. _t9 => box 1 _t10 [ SNF ] [ SNF++, 476209, _t10 ] % 220.17/220.63 (1,1) [307269,3]. true => _t9 | ~_t8 [ SNF ] % 220.17/220.63 (3076,1) [431492,3]. _t87 => ~box 1~ _t88 [ SNF ] [ SNF++, 476331, _t88 ] % 220.17/220.63 (3077,1) [431493,3]. true => _t87 | ~_t86 [ SNF ] % 220.17/220.63 (1,1) [476096,3]. true => ~_t85127 | _t8 [ SNF++, 325948 ] % 220.17/220.63 (3077,1) [476208,3]. true => ~_t85132 | _t86 [ SNF++, 431494 ] % 220.17/220.63 (1,1) [476209,3]. _t9 => box 1 _t85133 [ SNF++, 302599 ] % 220.17/220.63 (3076,1) [476331,3]. _t87 => ~box 1~ _t85136 [ SNF++, 431492 ] % 220.17/220.63 (1,1) [634569,3]. true => ~_t85127 | _t9 [ LRES, 307269, 476096, ~_t8 ] % 220.17/220.63 (3077,1) [637726,3]. true => ~_t85132 | _t87 [ LRES, 431493, 476208, ~_t86 ] % 220.17/220.63 (3076,1) [6348118,3]. true => ~_t87 | ~_t9 [ GEN1, 476209, 476331, 6347845, _t85133, _t85136 ] % 220.17/220.63 (3076,1) [6348120,3]. true => ~_t85127 | ~_t87 [ LRES, 6348118, 634569, ~_t9 ] % 220.17/220.63 (3077,1) [6348397,3]. true => ~_t85132 | ~_t85127 [ LRES, 6348120, 637726, ~_t87 ] % 220.17/220.63 (1,1) [279295,4]. _t11 => box 1 _t12 [ SNF ] [ SNF++, 476333, _t12 ] % 220.17/220.63 (1,1) [283956,4]. true => _t11 | ~_t10 [ SNF ] % 220.17/220.63 (3075,1) [431490,4]. _t89 => ~box 1~ _t90 [ SNF ] [ SNF++, 476471, _t90 ] % 220.17/220.63 (3076,1) [431491,4]. true => _t89 | ~_t88 [ SNF ] % 220.17/220.63 (1,1) [476210,4]. true => ~_t85133 | _t10 [ SNF++, 302599 ] % 220.17/220.63 (3076,1) [476332,4]. true => ~_t85136 | _t88 [ SNF++, 431492 ] % 220.17/220.63 (1,1) [476333,4]. _t11 => box 1 _t85137 [ SNF++, 279295 ] % 220.17/220.63 (3075,1) [476471,4]. _t89 => ~box 1~ _t85140 [ SNF++, 431490 ] % 220.17/220.63 (1,1) [634570,4]. true => ~_t85133 | _t11 [ LRES, 283956, 476210, ~_t10 ] % 220.17/220.63 (3076,1) [639284,4]. true => ~_t85136 | _t89 [ LRES, 431491, 476332, ~_t88 ] % 220.17/220.63 (3075,1) [6347220,4]. true => ~_t89 | ~_t11 [ GEN1, 476333, 476471, 6346867, _t85137, _t85140 ] % 220.17/220.63 (3075,1) [6347576,4]. true => ~_t85133 | ~_t89 [ LRES, 6347220, 634570, ~_t11 ] % 220.17/220.63 (3076,1) [6347845,4]. true => ~_t85136 | ~_t85133 [ LRES, 6347576, 639284, ~_t89 ] % 220.17/220.63 (1,1) [256036,5]. _t13 => box 1 _t14 [ SNF ] [ SNF++, 476473, _t14 ] % 220.17/220.63 (1,1) [260688,5]. true => _t13 | ~_t12 [ SNF ] % 220.17/220.63 (3074,1) [431488,5]. _t91 => ~box 1~ _t92 [ SNF ] [ SNF++, 476625, _t92 ] % 220.17/220.63 (3075,1) [431489,5]. true => _t91 | ~_t90 [ SNF ] % 220.17/220.63 (1,1) [476334,5]. true => ~_t85137 | _t12 [ SNF++, 279295 ] % 220.17/220.63 (3075,1) [476472,5]. true => ~_t85140 | _t90 [ SNF++, 431490 ] % 220.17/220.63 (1,1) [476473,5]. _t13 => box 1 _t85141 [ SNF++, 256036 ] % 220.17/220.63 (3074,1) [476625,5]. _t91 => ~box 1~ _t85145 [ SNF++, 431488 ] % 220.17/220.63 (1,1) [634571,5]. true => ~_t85137 | _t13 [ LRES, 260688, 476334, ~_t12 ] % 220.17/220.63 (3075,1) [640840,5]. true => ~_t85140 | _t91 [ LRES, 431489, 476472, ~_t90 ] % 220.17/220.63 (3074,1) [6346573,5]. true => ~_t91 | ~_t13 [ GEN1, 476473, 476625, 6346126, _t85141, _t85145 ] % 220.17/220.63 (3074,1) [6346771,5]. true => ~_t85137 | ~_t91 [ LRES, 6346573, 634571, ~_t13 ] % 220.17/220.63 (3075,1) [6346867,5]. true => ~_t85140 | ~_t85137 [ LRES, 6346771, 640840, ~_t91 ] % 220.17/220.63 (1,1) [232822,6]. _t15 => box 1 _t16 [ SNF ] [ SNF++, 476627, _t16 ] % 220.17/220.63 (1,1) [237465,6]. true => _t15 | ~_t14 [ SNF ] % 220.17/220.63 (3073,1) [431486,6]. _t93 => ~box 1~ _t94 [ SNF ] [ SNF++, 476787, _t94 ] % 220.17/220.63 (3074,1) [431487,6]. true => _t93 | ~_t92 [ SNF ] % 220.17/220.63 (1,1) [476474,6]. true => ~_t85141 | _t14 [ SNF++, 256036 ] % 220.17/220.63 (3074,1) [476626,6]. true => ~_t85145 | _t92 [ SNF++, 431488 ] % 220.17/220.63 (1,1) [476627,6]. _t15 => box 1 _t85146 [ SNF++, 232822 ] % 220.17/220.63 (3073,1) [476787,6]. _t93 => ~box 1~ _t85148 [ SNF++, 431486 ] % 220.17/220.63 (1,1) [634572,6]. true => ~_t85141 | _t15 [ LRES, 237465, 476474, ~_t14 ] % 220.17/220.63 (3074,1) [642394,6]. true => ~_t85145 | _t93 [ LRES, 431487, 476626, ~_t92 ] % 220.17/220.63 (3073,1) [6345463,6]. true => ~_t93 | ~_t15 [ GEN1, 476627, 476787, 6345271, _t85146, _t85148 ] % 220.17/220.63 (3073,1) [6345736,6]. true => ~_t85141 | ~_t93 [ LRES, 6345463, 634572, ~_t15 ] % 220.17/220.63 (3074,1) [6346126,6]. true => ~_t85145 | ~_t85141 [ LRES, 6345736, 642394, ~_t93 ] % 220.17/220.63 (1,1) [209653,7]. _t17 => box 1 _t18 [ SNF ] [ SNF++, 476789, _t18 ] % 220.17/220.63 (1,1) [214287,7]. true => _t17 | ~_t16 [ SNF ] % 220.17/220.63 (3072,1) [431484,7]. _t95 => ~box 1~ _t96 [ SNF ] [ SNF++, 476957, _t96 ] % 220.17/220.63 (3073,1) [431485,7]. true => _t95 | ~_t94 [ SNF ] % 220.17/220.63 (1,1) [476628,7]. true => ~_t85146 | _t16 [ SNF++, 232822 ] % 220.17/220.63 (3073,1) [476788,7]. true => ~_t85148 | _t94 [ SNF++, 431486 ] % 220.17/220.63 (1,1) [476789,7]. _t17 => box 1 _t85149 [ SNF++, 209653 ] % 220.17/220.63 (3072,1) [476957,7]. _t95 => ~box 1~ _t85151 [ SNF++, 431484 ] % 220.17/220.63 (1,1) [634573,7]. true => ~_t85146 | _t17 [ LRES, 214287, 476628, ~_t16 ] % 220.17/220.63 (3073,1) [643948,7]. true => ~_t85148 | _t95 [ LRES, 431485, 476788, ~_t94 ] % 220.17/220.63 (3072,1) [6344548,7]. true => ~_t95 | ~_t17 [ GEN1, 476789, 476957, 6344100, _t85149, _t85151 ] % 220.17/220.63 (3072,1) [6344992,7]. true => ~_t85146 | ~_t95 [ LRES, 6344548, 634573, ~_t17 ] % 220.17/220.63 (3073,1) [6345271,7]. true => ~_t85148 | ~_t85146 [ LRES, 6344992, 643948, ~_t95 ] % 220.17/220.63 (1,1) [186529,8]. _t19 => box 1 _t20 [ SNF ] [ SNF++, 476959, _t20 ] % 220.17/220.63 (1,1) [191154,8]. true => _t19 | ~_t18 [ SNF ] % 220.17/220.63 (3071,1) [431482,8]. _t97 => ~box 1~ _t98 [ SNF ] [ SNF++, 477135, _t98 ] % 220.17/220.63 (3072,1) [431483,8]. true => _t97 | ~_t96 [ SNF ] % 220.17/220.63 (1,1) [476790,8]. true => ~_t85149 | _t18 [ SNF++, 209653 ] % 220.17/220.63 (3072,1) [476958,8]. true => ~_t85151 | _t96 [ SNF++, 431484 ] % 220.17/220.63 (1,1) [476959,8]. _t19 => box 1 _t85152 [ SNF++, 186529 ] % 220.17/220.63 (3071,1) [477135,8]. _t97 => ~box 1~ _t85154 [ SNF++, 431482 ] % 220.17/220.63 (1,1) [634574,8]. true => ~_t85149 | _t19 [ LRES, 191154, 476790, ~_t18 ] % 220.17/220.63 (3072,1) [645497,8]. true => ~_t85151 | _t97 [ LRES, 431483, 476958, ~_t96 ] % 220.17/220.63 (3071,1) [6343745,8]. true => ~_t97 | ~_t19 [ GEN1, 476959, 477135, 6343645, _t85152, _t85154 ] % 220.17/220.63 (3071,1) [6343746,8]. true => ~_t85149 | ~_t97 [ LRES, 6343745, 634574, ~_t19 ] % 220.17/220.63 (3072,1) [6344100,8]. true => ~_t85151 | ~_t85149 [ LRES, 6343746, 645497, ~_t97 ] % 220.17/220.63 (1,1) [163450,9]. _t21 => box 1 _t22 [ SNF ] [ SNF++, 477137, _t22 ] % 220.17/220.63 (1,1) [168066,9]. true => _t21 | ~_t20 [ SNF ] % 220.17/220.63 (3070,1) [431480,9]. _t99 => ~box 1~ _t100 [ SNF ] [ SNF++, 477321, _t100 ] % 220.17/220.63 (3071,1) [431481,9]. true => _t99 | ~_t98 [ SNF ] % 220.17/220.63 (1,1) [476960,9]. true => ~_t85152 | _t20 [ SNF++, 186529 ] % 220.17/220.63 (3071,1) [477136,9]. true => ~_t85154 | _t98 [ SNF++, 431482 ] % 220.17/220.63 (1,1) [477137,9]. _t21 => box 1 _t85155 [ SNF++, 163450 ] % 220.17/220.63 (3070,1) [477321,9]. _t99 => ~box 1~ _t85157 [ SNF++, 431480 ] % 220.17/220.63 (1,1) [634575,9]. true => ~_t85152 | _t21 [ LRES, 168066, 476960, ~_t20 ] % 220.17/220.63 (3071,1) [647045,9]. true => ~_t85154 | _t99 [ LRES, 431481, 477136, ~_t98 ] % 220.17/220.63 (3070,1) [6343011,9]. true => ~_t99 | ~_t21 [ GEN1, 477137, 477321, 6342823, _t85155, _t85157 ] % 220.17/220.63 (3070,1) [6343284,9]. true => ~_t85152 | ~_t99 [ LRES, 6343011, 634575, ~_t21 ] % 220.17/220.63 (3071,1) [6343645,9]. true => ~_t85154 | ~_t85152 [ LRES, 6343284, 647045, ~_t99 ] % 220.17/220.63 (1,1) [140416,10]. _t23 => box 1 _t24 [ SNF ] [ SNF++, 477323, _t24 ] % 220.17/220.63 (1,1) [145023,10]. true => _t23 | ~_t22 [ SNF ] % 220.17/220.63 (3069,1) [431478,10]. _t101 => ~box 1~ _t102 [ SNF ] [ SNF++, 477515, _t102 ] % 220.17/220.63 (3070,1) [431479,10]. true => _t101 | ~_t100 [ SNF ] % 220.17/220.63 (1,1) [477138,10]. true => ~_t85155 | _t22 [ SNF++, 163450 ] % 220.17/220.63 (3070,1) [477322,10]. true => ~_t85157 | _t100 [ SNF++, 431480 ] % 220.17/220.63 (1,1) [477323,10]. _t23 => box 1 _t85158 [ SNF++, 140416 ] % 220.17/220.63 (3069,1) [477515,10]. _t101 => ~box 1~ _t85160 [ SNF++, 431478 ] % 220.17/220.63 (1,1) [634576,10]. true => ~_t85155 | _t23 [ LRES, 145023, 477138, ~_t22 ] % 220.17/220.63 (3070,1) [648588,10]. true => ~_t85157 | _t101 [ LRES, 431479, 477322, ~_t100 ] % 220.17/220.63 (3069,1) [6342548,10]. true => ~_t101 | ~_t23 [ GEN1, 477323, 477515, 6342448, _t85158, _t85160 ] % 220.17/220.63 (3069,1) [6342550,10]. true => ~_t85155 | ~_t101 [ LRES, 6342548, 634576, ~_t23 ] % 220.17/220.63 (3070,1) [6342823,10]. true => ~_t85157 | ~_t85155 [ LRES, 6342550, 648588, ~_t101 ] % 220.17/220.63 (1,1) [117427,11]. _t25 => box 1 _t26 [ SNF ] [ SNF++, 477517, _t26 ] % 220.17/220.63 (1,1) [122025,11]. true => _t25 | ~_t24 [ SNF ] % 220.17/220.63 (3068,1) [431476,11]. _t103 => ~box 1~ _t104 [ SNF ] [ SNF++, 477717, _t104 ] % 220.17/220.63 (3069,1) [431477,11]. true => _t103 | ~_t102 [ SNF ] % 220.17/220.63 (1,1) [477324,11]. true => ~_t85158 | _t24 [ SNF++, 140416 ] % 220.17/220.63 (3069,1) [477516,11]. true => ~_t85160 | _t102 [ SNF++, 431478 ] % 220.17/220.63 (1,1) [477517,11]. _t25 => box 1 _t85161 [ SNF++, 117427 ] % 220.17/220.63 (3068,1) [477717,11]. _t103 => ~box 1~ _t85163 [ SNF++, 431476 ] % 220.17/220.63 (1,1) [634577,11]. true => ~_t85158 | _t25 [ LRES, 122025, 477324, ~_t24 ] % 220.17/220.63 (3069,1) [650130,11]. true => ~_t85160 | _t103 [ LRES, 431477, 477516, ~_t102 ] % 220.17/220.63 (3068,1) [6342163,11]. true => ~_t103 | ~_t25 [ GEN1, 477517, 477717, 6341976, _t85161, _t85163 ] % 220.17/220.63 (3068,1) [6342346,11]. true => ~_t85158 | ~_t103 [ LRES, 6342163, 634577, ~_t25 ] % 220.17/220.63 (3069,1) [6342448,11]. true => ~_t85160 | ~_t85158 [ LRES, 6342346, 650130, ~_t103 ] % 220.17/220.63 (1,1) [92447,12]. _t27 => box 1 _t28 [ SNF ] [ SNF++, 477719, _t28 ] % 220.17/220.63 (1,1) [92449,12]. _t27 => box 1 _t27 [ Axiom 4 ] [ SNF++, 477721, _t27 ] % 220.17/220.63 (1,1) [99072,12]. true => _t27 | ~_t26 [ SNF ] % 220.17/220.63 (3067,1) [431474,12]. _t105 => ~box 1~ _t106 [ SNF ] [ SNF++, 477927, _t106 ] % 220.17/220.63 (3068,1) [431475,12]. true => _t105 | ~_t104 [ SNF ] % 220.17/220.63 (1,1) [477518,12]. true => ~_t85161 | _t26 [ SNF++, 117427 ] % 220.17/220.63 (3068,1) [477718,12]. true => ~_t85163 | _t104 [ SNF++, 431476 ] % 220.17/220.63 (1,1) [477719,12]. _t27 => box 1 _t85164 [ SNF++, 92447 ] % 220.17/220.63 (1,1) [477721,12]. _t27 => box 1 _t85165 [ SNF++, 92449 ] % 220.17/220.63 (3067,1) [477927,12]. _t105 => ~box 1~ _t85166 [ SNF++, 431474 ] % 220.17/220.63 (1,1) [634578,12]. true => ~_t85161 | _t27 [ LRES, 99072, 477518, ~_t26 ] % 220.17/220.63 (3068,1) [651667,12]. true => ~_t85163 | _t105 [ LRES, 431475, 477718, ~_t104 ] % 220.17/220.63 (3067,1) [6341527,12]. true => ~_t105 | ~_t27 [ GEN1, 477721, 477719, 477927, 6341028, _t85165, _t85164, _t85166 ] % 220.17/220.63 (3067,1) [6341528,12]. true => ~_t85161 | ~_t105 [ LRES, 6341527, 634578, ~_t27 ] % 220.17/220.63 (3068,1) [6341976,12]. true => ~_t85163 | ~_t85161 [ LRES, 6341528, 651667, ~_t105 ] % 220.17/220.63 (1,1) [44224,13]. _t29 => box 1 _t30 [ SNF ] [ SNF++, 477929, _t30 ] % 220.17/220.63 (1,1) [52868,13]. true => _t29 | ~_t28 [ SNF ] % 220.17/220.63 (1,1) [92460,13]. _t27 => box 1 _t28 [ Axiom 4 ] [ SNF++, 477941, _t28 ] % 220.17/220.63 (3057,1) [431467,13]. _t107 => ~box 1~ _t108 [ SNF ] [ SNF++, 478143, _t108 ] % 220.17/220.63 (3067,1) [431468,13]. true => _t107 | ~_t106 [ SNF ] % 220.17/220.63 (1,1) [477720,13]. true => ~_t85164 | _t28 [ SNF++, 92447 ] % 220.17/220.63 (1,1) [477722,13]. true => ~_t85165 | _t27 [ SNF++, 92449 ] % 220.17/220.63 (3067,1) [477928,13]. true => ~_t85166 | _t106 [ SNF++, 431474 ] % 220.17/220.63 (1,1) [477929,13]. _t29 => box 1 _t85167 [ SNF++, 44224 ] % 220.17/220.63 (1,1) [477941,13]. _t27 => box 1 _t85164 [ SNF++, 92460 ] % 220.17/220.63 (3057,1) [478143,13]. _t107 => ~box 1~ _t85169 [ SNF++, 431467 ] % 220.17/220.63 (1,1) [634579,13]. true => ~_t85164 | _t29 [ LRES, 52868, 477720, ~_t28 ] % 220.17/220.63 (3067,1) [653202,13]. true => ~_t85166 | _t107 [ LRES, 431468, 477928, ~_t106 ] % 220.17/220.63 (3057,1) [6339300,13]. true => ~_t107 | ~_t29 | ~_t27 [ GEN1, 477929, 477941, 478143, 6339191, _t85167, _t85164, _t85169 ] % 220.17/220.63 (3057,1) [6339582,13]. true => ~_t85165 | ~_t107 | ~_t29 [ LRES, 6339300, 477722, ~_t27 ] % 220.17/220.63 (3057,1) [6339857,13]. true => ~_t85165 | ~_t85164 | ~_t107 [ LRES, 6339582, 634579, ~_t29 ] % 220.17/220.63 (3067,1) [6341028,13]. true => ~_t85166 | ~_t85165 | ~_t85164 [ LRES, 6339857, 653202, ~_t107 ] % 220.17/220.63 (1,1) [33541,14]. _t48 => box 1 _t49 [ SNF ] [ SNF++, 478157, _t49 ] % 220.17/220.63 (1,1) [38112,14]. true => _t48 | ~_t30 [ SNF ] % 220.17/220.63 (81,1) [40146,14]. _t45 => ~box 1~ _t46 [ SNF ] [ SNF++, 478281, _t46 ] % 220.17/220.63 (101,1) [40151,14]. _t32 => ~box 1~ _t33 [ SNF ] [ SNF++, 478283, _t33 ] % 220.17/220.63 (1,1) [40152,14]. true => ~_t52 | _t45 | _t32 [ SNF ] % 220.17/220.63 (1,1) [40153,14]. true => _t52 | ~_t30 [ SNF ] % 220.17/220.63 (1,1) [44241,14]. _t29 => box 1 _t30 [ Axiom 4 ] [ SNF++, 478163, _t30 ] % 220.17/220.63 (1,1) [92453,14]. true => _t29 | ~_t28 [ Axiom 4 ] % 220.17/220.63 (1,1) [428924,14]. _t108 => box 1 _t109 [ SNF ] [ SNF++, 478263, _t109 ] % 220.17/220.63 (1,1) [477930,14]. true => ~_t85167 | _t30 [ SNF++, 44224 ] % 220.17/220.63 (1,1) [477942,14]. true => ~_t85164 | _t28 [ SNF++, 92460 ] % 220.17/220.63 (3057,1) [478144,14]. true => ~_t85169 | _t108 [ SNF++, 431467 ] % 220.17/220.63 (1,1) [478157,14]. _t48 => box 1 _t85174 [ SNF++, 33541 ] % 220.17/220.63 (1,1) [478163,14]. _t29 => box 1 _t85167 [ SNF++, 44241 ] % 220.17/220.63 (1,1) [478263,14]. _t108 => box 1 _t85177 [ SNF++, 428924 ] % 220.17/220.63 (81,1) [478281,14]. _t45 => ~box 1~ _t85178 [ SNF++, 40146 ] % 220.17/220.63 (101,1) [478283,14]. _t32 => ~box 1~ _t85179 [ SNF++, 40151 ] % 220.17/220.63 (1,1) [634058,14]. true => ~_t85167 | _t52 [ LRES, 40153, 477930, ~_t30 ] % 220.17/220.63 (1,1) [634580,14]. true => ~_t85167 | _t48 [ LRES, 38112, 477930, ~_t30 ] % 220.17/220.63 (1,1) [636151,14]. true => ~_t85164 | _t29 [ LRES, 92453, 477942, ~_t28 ] % 220.17/220.63 (81,1) [963319,14]. true => ~_t45 | ~_t29 [ GEN1, 478163, 478281, 917785, _t85167, _t85178 ] % 220.17/220.63 (81,1) [964408,14]. true => ~_t85164 | ~_t45 [ LRES, 963319, 636151, ~_t29 ] % 220.17/220.63 (101,1) [6337146,14]. true => ~_t108 | ~_t48 | ~_t32 | ~_t29 [ GEN1, 478263, 478163, 478157, 478283, 6336294, _t85177, _t85167, _t85174, _t85179 ] % 220.17/220.63 (101,1) [6337527,14]. true => ~_t85164 | ~_t108 | ~_t48 | ~_t32 [ LRES, 6337146, 636151, ~_t29 ] % 220.17/220.63 (101,1) [6338063,14]. true => ~_t85164 | ~_t108 | ~_t52 | ~_t48 | _t45 [ LRES, 6337527, 40152, ~_t32 ] [ Backward Subsumption, 6338359 ] % 220.17/220.63 (101,1) [6338359,14]. true => ~_t85164 | ~_t108 | ~_t52 | ~_t48 [ LRES, 6338063, 964408, _t45 ] % 220.17/220.63 (101,1) [6338551,14]. true => ~_t85167 | ~_t85164 | ~_t108 | ~_t52 [ LRES, 6338359, 634580, ~_t48 ] [ Backward Subsumption, 6338913 ] % 220.17/220.63 (101,1) [6338913,14]. true => ~_t85167 | ~_t85164 | ~_t108 [ LRES, 6338551, 634058, ~_t52 ] % 220.17/220.63 (3057,1) [6339191,14]. true => ~_t85169 | ~_t85167 | ~_t85164 [ LRES, 6338913, 478144, ~_t108 ] % 220.17/220.63 (1,1) [6674,15]. _t31 => box 1 _t32 [ Axiom 4 ] [ SNF++, 478405, _t32 ] % 220.17/220.63 (1,1) [6676,15]. _t31 => box 1 _t31 [ Axiom 4 ] [ SNF++, 478409, _t31 ] % 220.17/220.63 (1,1) [25417,15]. _t50 => box 1 _t50 [ Axiom 4 ] [ SNF++, 478417, _t50 ] % 220.17/220.63 (1,1) [25418,15]. _t50 => ~box 1~ _t50 [ Axiom SER ] [ SNF++, 478561, _t50 ] % 220.17/220.63 (1,1) [27447,15]. _t51 => box 1 _t33 [ SNF ] [ SNF++, 478419, _t33 ] % 220.17/220.63 (1,1) [29481,15]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 478423, _t37 ] % 220.17/220.63 (1,1) [31511,15]. true => _t37 | ~_t36 [ SNF ] % 220.17/220.63 (73,1) [33538,15]. _t38 => ~box 1~ _t39 [ SNF ] [ SNF++, 478567, _t39 ] % 220.17/220.63 (1,1) [33539,15]. true => _t38 | ~_t36 [ SNF ] % 220.17/220.63 (1,1) [33540,15]. true => _t51 | _t50 | ~_t49 | _t36 | ~p0 [ SNF ] % 220.17/220.63 (1,1) [38114,15]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 478429, _t47 ] % 220.17/220.63 (1,1) [38115,15]. _t46 => ~box 1~ _t47 [ Axiom SER ] [ SNF++, 478575, _t47 ] % 220.17/220.63 (1,1) [38116,15]. _t46 => box 1 _t46 [ Axiom 4 ] [ SNF++, 478431, _t46 ] % 220.17/220.63 (101,1) [40149,15]. true => _t36 | ~_t35 | p0 [ SNF ] % 220.17/220.63 (101,1) [40150,15]. true => _t35 | ~_t33 [ SNF ] % 220.17/220.63 (1,1) [42190,15]. _t54 => box 1 _t31 [ Axiom 4 ] [ SNF++, 478407, _t31 ] % 220.17/220.63 (1,1) [44228,15]. true => _t31 | ~_t30 [ Axiom 4 ] % 220.17/220.63 (3056,1) [428923,15]. _t109 => ~box 1~ _t47 [ SNF ] [ SNF++, 478573, _t47 ] % 220.17/220.63 (1,1) [478158,15]. true => ~_t85174 | _t49 [ SNF++, 33541 ] % 220.17/220.63 (1,1) [478164,15]. true => ~_t85167 | _t30 [ SNF++, 44241 ] % 220.17/220.63 (1,1) [478264,15]. true => ~_t85177 | _t109 [ SNF++, 428924 ] % 220.17/220.63 (81,1) [478282,15]. true => ~_t85178 | _t46 [ SNF++, 40146 ] % 220.17/220.63 (101,1) [478284,15]. true => ~_t85179 | _t33 [ SNF++, 40151 ] % 220.17/220.63 (1,1) [478405,15]. _t31 => box 1 _t85170 [ SNF++, 6674 ] % 220.17/220.63 (1,1) [478409,15]. _t31 => box 1 _t85171 [ SNF++, 6676 ] % 220.17/220.63 (1,1) [478417,15]. _t50 => box 1 _t85181 [ SNF++, 25417 ] % 220.17/220.63 (1,1) [478419,15]. _t51 => box 1 _t85179 [ SNF++, 27447 ] % 220.17/220.63 (1,1) [478423,15]. _t37 => box 1 _t85183 [ SNF++, 29481 ] % 220.17/220.63 (1,1) [478431,15]. _t46 => box 1 _t85178 [ SNF++, 38116 ] % 220.17/220.63 (1,1) [478561,15]. _t50 => ~box 1~ _t85181 [ SNF++, 25418 ] % 220.17/220.63 (73,1) [478567,15]. _t38 => ~box 1~ _t85185 [ SNF++, 33538 ] % 220.17/220.63 (3056,1) [478573,15]. _t109 => ~box 1~ _t85184 [ SNF++, 428923 ] % 220.17/220.63 (1,1) [478575,15]. _t46 => ~box 1~ _t85184 [ SNF++, 38115 ] % 220.17/220.63 (101,1) [634581,15]. true => ~_t85179 | _t35 [ LRES, 40150, 478284, ~_t33 ] % 220.17/220.63 (1,1) [636672,15]. true => ~_t85167 | _t31 [ LRES, 44228, 478164, ~_t30 ] % 220.17/220.63 (73,1) [752093,15]. true => ~_t38 | ~_t37 [ GEN1, 478423, 478567, 751411, _t85183, _t85185 ] % 220.17/220.63 (101,1) [855471,15]. true => _t51 | _t50 | ~_t49 | _t36 | ~_t35 [ LRES, 33540, 40149, ~p0 ] % 220.17/220.63 (101,1) [855735,15]. true => ~_t85179 | _t51 | _t50 | ~_t49 | _t36 [ LRES, 855471, 634581, ~_t35 ] [ Backward Subsumption, 856611 ] % 220.17/220.63 (101,1) [856091,15]. true => ~_t85179 | _t51 | _t50 | ~_t49 | _t37 [ LRES, 855735, 31511, _t36 ] [ Backward Subsumption, 856611 ] % 220.17/220.63 (101,1) [856092,15]. true => ~_t85179 | _t51 | _t50 | ~_t49 | _t38 [ LRES, 855735, 33539, _t36 ] [ Backward Subsumption, 856611 ] % 220.17/220.63 (101,1) [856154,15]. true => ~_t85179 | _t51 | _t50 | ~_t49 | ~_t38 [ LRES, 856091, 752093, _t37 ] [ Backward Subsumption, 856611 ] % 220.17/220.63 (101,1) [856611,15]. true => ~_t85179 | _t51 | _t50 | ~_t49 [ LRES, 856154, 856092, ~_t38 ] % 220.17/220.63 (3056,1) [856694,15]. true => ~_t109 | ~_t51 [ GEN1, 478419, 478573, 856378, _t85179, _t85184 ] % 220.17/220.63 (1,1) [870462,15]. true => ~_t46 | ~_t31 [ GEN3, 478431, 478405, 867283, 478575, _t85178, _t85170, _t85184 ] % 220.17/220.63 (1,1) [916769,15]. true => ~_t85167 | ~_t46 [ LRES, 870462, 636672, ~_t31 ] % 220.17/220.63 (81,1) [917785,15]. true => ~_t85178 | ~_t85167 [ LRES, 916769, 478282, ~_t46 ] % 220.17/220.63 (1,1) [1331939,15]. true => ~_t50 | ~_t31 [ GEN3, 478417, 478409, 1286274, 478561, _t85181, _t85171, _t85181 ] % 220.17/220.63 (1,1) [1419568,15]. true => ~_t85167 | ~_t50 [ LRES, 1331939, 636672, ~_t31 ] % 220.17/220.63 (101,1) [6315162,15]. true => ~_t85179 | ~_t85174 | _t51 | _t50 [ LRES, 856611, 478158, ~_t49 ] % 220.17/220.63 (101,1) [6315283,15]. true => ~_t85179 | ~_t85174 | ~_t85167 | _t51 [ LRES, 6315162, 1419568, _t50 ] % 220.17/220.63 (3056,1) [6315470,15]. true => ~_t85179 | ~_t85174 | ~_t85167 | ~_t109 [ LRES, 6315283, 856694, _t51 ] % 220.17/220.63 (3056,1) [6336294,15]. true => ~_t85179 | ~_t85177 | ~_t85174 | ~_t85167 [ LRES, 6315470, 478264, ~_t109 ] % 220.17/220.63 (1,1) [2100,16]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 478695, _t37 ] % 220.17/220.63 (21,1) [4126,16]. true => _t37 | ~_t36 [ SNF ] % 220.17/220.63 (20,1) [6652,16]. _t38 => ~box 1~ _t39 [ SNF ] [ SNF++, 478831, _t39 ] % 220.17/220.63 (21,1) [6653,16]. true => _t38 | ~_t36 [ SNF ] % 220.17/220.63 (21,1) [6654,16]. true => _t36 | ~_t35 | p0 [ SNF ] % 220.17/220.63 (21,1) [6655,16]. true => _t35 | ~_t33 [ SNF ] % 220.17/220.63 (21,1) [6673,16]. _t32 => ~box 1~ _t33 [ Axiom 4 ] [ SNF++, 478835, _t33 ] % 220.17/220.63 (1,1) [6693,16]. _t31 => box 1 _t31 [ Axiom 4 ] [ SNF++, 478701, _t31 ] % 220.17/220.63 (1,1) [17298,16]. _t46 => box 1 _t47 [ SNF ] [ SNF++, 478703, _t47 ] % 220.17/220.63 (1,1) [25419,16]. _t50 => box 1 _t45 [ Axiom 4 ] [ SNF++, 478711, _t45 ] % 220.17/220.63 (1,1) [25422,16]. _t50 => ~box 1~ _t50 [ Axiom SER ] [ SNF++, 478859, _t50 ] % 220.17/220.63 (1,1) [27451,16]. _t51 => box 1 _t33 [ Axiom 4 ] [ SNF++, 478715, _t33 ] % 220.17/220.63 (72,1) [33537,16]. _t39 => ~box 1~ _t40 [ SNF ] [ SNF++, 478863, _t40 ] % 220.17/220.63 (1,1) [38113,16]. true => ~_t47 | _t36 | ~p0 [ SNF ] % 220.17/220.63 (1,1) [42194,16]. _t54 => box 1 _t31 [ Axiom 4 ] [ SNF++, 478699, _t31 ] % 220.17/220.63 (1,1) [478406,16]. true => ~_t85170 | _t32 [ SNF++, 6674 ] % 220.17/220.63 (1,1) [478408,16]. true => ~_t85171 | _t31 [ SNF++, 42190 ] % 220.17/220.63 (1,1) [478418,16]. true => ~_t85181 | _t50 [ SNF++, 25417 ] % 220.17/220.63 (1,1) [478420,16]. true => ~_t85179 | _t33 [ SNF++, 27447 ] % 220.17/220.63 (1,1) [478424,16]. true => ~_t85183 | _t37 [ SNF++, 29481 ] % 220.17/220.63 (1,1) [478430,16]. true => ~_t85184 | _t47 [ SNF++, 38114 ] % 220.17/220.63 (1,1) [478432,16]. true => ~_t85178 | _t46 [ SNF++, 38116 ] % 220.17/220.63 (73,1) [478568,16]. true => ~_t85185 | _t39 [ SNF++, 33538 ] % 220.17/220.63 (1,1) [478695,16]. _t37 => box 1 _t85183 [ SNF++, 2100 ] % 220.17/220.63 (1,1) [478701,16]. _t31 => box 1 _t85171 [ SNF++, 6693 ] % 220.17/220.63 (1,1) [478703,16]. _t46 => box 1 _t85184 [ SNF++, 17298 ] % 220.17/220.63 (1,1) [478711,16]. _t50 => box 1 _t85180 [ SNF++, 25419 ] % 220.17/220.63 (20,1) [478831,16]. _t38 => ~box 1~ _t85185 [ SNF++, 6652 ] % 220.17/220.63 (21,1) [478835,16]. _t32 => ~box 1~ _t85179 [ SNF++, 6673 ] % 220.17/220.63 (1,1) [478859,16]. _t50 => ~box 1~ _t85181 [ SNF++, 25422 ] % 220.17/220.63 (72,1) [478863,16]. _t39 => ~box 1~ _t85186 [ SNF++, 33537 ] % 220.17/220.63 (21,1) [633537,16]. true => ~_t85179 | _t35 [ LRES, 6655, 478420, ~_t33 ] % 220.17/220.63 (21,1) [707576,16]. true => ~_t47 | _t36 | ~_t35 [ LRES, 38113, 6654, ~p0 ] % 220.17/220.63 (72,1) [707577,16]. true => ~_t39 | ~_t37 [ GEN1, 478695, 478863, 663985, _t85183, _t85186 ] % 220.17/220.63 (72,1) [750849,16]. true => ~_t85183 | ~_t39 [ LRES, 707577, 478424, ~_t37 ] % 220.17/220.63 (73,1) [751411,16]. true => ~_t85185 | ~_t85183 [ LRES, 750849, 478568, ~_t39 ] % 220.17/220.63 (20,1) [842792,16]. true => ~_t38 | ~_t37 [ GEN1, 478695, 478831, 798101, _t85183, _t85185 ] % 220.17/220.63 (21,1) [854431,16]. true => ~_t85179 | ~_t47 | _t36 [ LRES, 707576, 633537, ~_t35 ] [ Backward Subsumption, 856155 ] % 220.17/220.63 (21,1) [854982,16]. true => ~_t85179 | ~_t47 | _t37 [ LRES, 854431, 4126, _t36 ] [ Backward Subsumption, 856155 ] % 220.17/220.63 (21,1) [854983,16]. true => ~_t85179 | ~_t47 | _t38 [ LRES, 854431, 6653, _t36 ] [ Backward Subsumption, 856155 ] % 220.17/220.63 (21,1) [855255,16]. true => ~_t85179 | ~_t47 | ~_t38 [ LRES, 854982, 842792, _t37 ] [ Backward Subsumption, 856155 ] % 220.17/220.63 (21,1) [856155,16]. true => ~_t85179 | ~_t47 [ LRES, 855255, 854983, ~_t38 ] % 220.17/220.63 (21,1) [856378,16]. true => ~_t85184 | ~_t85179 [ LRES, 856155, 478430, ~_t47 ] % 220.17/220.63 (21,1) [863571,16]. true => ~_t46 | ~_t32 [ GEN1, 478703, 478835, 862475, _t85184, _t85179 ] % 220.17/220.63 (21,1) [866687,16]. true => ~_t85170 | ~_t46 [ LRES, 863571, 478406, ~_t32 ] % 220.17/220.63 (21,1) [867283,16]. true => ~_t85178 | ~_t85170 [ LRES, 866687, 478432, ~_t46 ] % 220.17/220.63 (1,1) [1014068,16]. true => ~_t50 | ~_t31 [ GEN3, 478711, 478701, 963321, 478859, _t85180, _t85171, _t85181 ] % 220.17/220.63 (1,1) [1104481,16]. true => ~_t85171 | ~_t50 [ LRES, 1014068, 478408, ~_t31 ] % 220.17/220.63 (1,1) [1286274,16]. true => ~_t85181 | ~_t85171 [ LRES, 1104481, 478418, ~_t50 ] % 220.17/220.63 (1,1) [2103,17]. _t37 => ~box 1~ z0 [ Axiom SER ] [ Backward Subsumption, 431510 ] % 220.17/220.63 (1,1) [2104,17]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 478987, _t37 ] % 220.17/220.63 (19,1) [6651,17]. _t39 => ~box 1~ _t40 [ SNF ] [ SNF++, 479129, _t40 ] % 220.17/220.63 (21,1) [6665,17]. true => _t37 | ~_t36 [ Axiom 4 ] % 220.17/220.63 (20,1) [6669,17]. _t38 => ~box 1~ _t39 [ Axiom 4 ] [ SNF++, 479131, _t39 ] % 220.17/220.63 (21,1) [6670,17]. true => _t38 | ~_t36 [ Axiom 4 ] % 220.17/220.63 (21,1) [6671,17]. true => _t36 | ~_t35 | p0 [ Axiom 4 ] % 220.17/220.63 (21,1) [6672,17]. true => _t35 | ~_t33 [ Axiom 4 ] % 220.17/220.63 (1,1) [6708,17]. _t31 => box 1 _t32 [ Axiom 4 ] [ SNF++, 478989, _t32 ] % 220.17/220.63 (1,1) [17297,17]. true => ~_t47 | _t36 | ~p0 [ SNF ] % 220.17/220.63 (1,1) [17305,17]. _t46 => box 1 _t46 [ Axiom 4 ] [ SNF++, 478997, _t46 ] % 220.17/220.63 (51,1) [19853,17]. _t45 => ~box 1~ _t46 [ Axiom 4 ] [ SNF++, 479149, _t46 ] % 220.17/220.63 (1,1) [31513,17]. _t40 => box 1 _t41 [ SNF ] [ SNF++, 479011, _t41 ] % 220.17/220.63 (1,1) [31515,17]. _t40 => box 1 _t40 [ Axiom 4 ] [ SNF++, 479013, _t40 ] % 220.17/220.63 (1,1) [431510,17]. _t37 => ~box 1~ true [ Modal Level Pure Literal Elimination, 2103, z0 ] % 220.17/220.63 (1,1) [478696,17]. true => ~_t85183 | _t37 [ SNF++, 2100 ] % 220.17/220.63 (1,1) [478700,17]. true => ~_t85171 | _t31 [ SNF++, 42194 ] % 220.17/220.63 (1,1) [478704,17]. true => ~_t85184 | _t47 [ SNF++, 17298 ] % 220.17/220.63 (1,1) [478712,17]. true => ~_t85180 | _t45 [ SNF++, 25419 ] % 220.17/220.63 (1,1) [478716,17]. true => ~_t85179 | _t33 [ SNF++, 27451 ] % 220.17/220.63 (20,1) [478832,17]. true => ~_t85185 | _t39 [ SNF++, 6652 ] % 220.17/220.63 (72,1) [478864,17]. true => ~_t85186 | _t40 [ SNF++, 33537 ] % 220.17/220.63 (1,1) [478987,17]. _t37 => box 1 _t85183 [ SNF++, 2104 ] % 220.17/220.63 (1,1) [478989,17]. _t31 => box 1 _t85170 [ SNF++, 6708 ] % 220.17/220.63 (1,1) [479011,17]. _t40 => box 1 _t85187 [ SNF++, 31513 ] % 220.17/220.63 (19,1) [479129,17]. _t39 => ~box 1~ _t85186 [ SNF++, 6651 ] % 220.17/220.63 (20,1) [479131,17]. _t38 => ~box 1~ _t85185 [ SNF++, 6669 ] % 220.17/220.63 (51,1) [479149,17]. _t45 => ~box 1~ _t85178 [ SNF++, 19853 ] % 220.17/220.63 (21,1) [633538,17]. true => ~_t85179 | _t35 [ LRES, 6672, 478716, ~_t33 ] % 220.17/220.63 (21,1) [662079,17]. true => ~_t47 | _t36 | ~_t35 [ LRES, 17297, 6671, ~p0 ] % 220.17/220.63 (1,1) [662593,17]. true => ~_t40 | ~_t37 [ GEN3, 479011, 478987, 661564, 431510, _t85187, _t85183, true ] % 220.17/220.63 (1,1) [663465,17]. true => ~_t85183 | ~_t40 [ LRES, 662593, 478696, ~_t37 ] % 220.17/220.63 (72,1) [663985,17]. true => ~_t85186 | ~_t85183 [ LRES, 663465, 478864, ~_t40 ] % 220.17/220.63 (19,1) [752263,17]. true => ~_t39 | ~_t37 [ GEN1, 478987, 479129, 750851, _t85183, _t85186 ] % 220.17/220.63 (19,1) [752863,17]. true => ~_t85183 | ~_t39 [ LRES, 752263, 478696, ~_t37 ] % 220.17/220.63 (20,1) [798101,17]. true => ~_t85185 | ~_t85183 [ LRES, 752863, 478832, ~_t39 ] % 220.17/220.63 (20,1) [798662,17]. true => ~_t38 | ~_t37 [ GEN1, 478987, 479131, 798102, _t85183, _t85185 ] % 220.17/220.63 (21,1) [845910,17]. true => ~_t85179 | ~_t47 | _t36 [ LRES, 662079, 633538, ~_t35 ] [ Backward Subsumption, 862467 ] % 220.17/220.63 (21,1) [861134,17]. true => ~_t85179 | ~_t47 | _t37 [ LRES, 845910, 6665, _t36 ] [ Backward Subsumption, 862467 ] % 220.17/220.63 (21,1) [861135,17]. true => ~_t85179 | ~_t47 | _t38 [ LRES, 845910, 6670, _t36 ] [ Backward Subsumption, 862467 ] % 220.17/220.63 (21,1) [861254,17]. true => ~_t85179 | ~_t47 | ~_t38 [ LRES, 861134, 798662, _t37 ] [ Backward Subsumption, 862467 ] % 220.17/220.63 (21,1) [862467,17]. true => ~_t85179 | ~_t47 [ LRES, 861254, 861135, ~_t38 ] % 220.17/220.63 (21,1) [862475,17]. true => ~_t85184 | ~_t85179 [ LRES, 862467, 478704, ~_t47 ] % 220.17/220.63 (51,1) [918631,17]. true => ~_t45 | ~_t31 [ GEN1, 478989, 479149, 916772, _t85170, _t85178 ] % 220.17/220.63 (51,1) [961968,17]. true => ~_t85171 | ~_t45 [ LRES, 918631, 478700, ~_t31 ] % 220.17/220.63 (51,1) [963321,17]. true => ~_t85180 | ~_t85171 [ LRES, 961968, 478712, ~_t45 ] % 220.17/220.63 (1,1) [2106,18]. _t37 => box 1 z0 [ Axiom 4 ] [ SNF++, 479287, z0 ] % 220.17/220.63 (1,1) [2108,18]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 479289, _t37 ] % 220.17/220.63 (1,1) [4128,18]. _t40 => box 1 _t41 [ SNF ] [ SNF++, 479291, _t41 ] % 220.17/220.63 (1,1) [4130,18]. _t40 => box 1 _t40 [ Axiom 4 ] [ SNF++, 479293, _t40 ] % 220.17/220.63 (1,1) [4131,18]. _t40 => ~box 1~ _t40 [ Axiom SER ] [ SNF++, 479435, _t40 ] % 220.17/220.63 (19,1) [6668,18]. _t39 => ~box 1~ _t40 [ Axiom 4 ] [ SNF++, 479433, _t40 ] % 220.17/220.63 (21,1) [6707,18]. _t32 => ~box 1~ _t33 [ Axiom 4 ] [ SNF++, 479441, _t33 ] % 220.17/220.63 (1,1) [17308,18]. _t46 => box 1 _t47 [ Axiom 4 ] [ SNF++, 479301, _t47 ] % 220.17/220.63 (1,1) [27459,18]. _t51 => box 1 _t33 [ Axiom 4 ] [ SNF++, 479313, _t33 ] % 220.17/220.63 (71,1) [31512,18]. _t41 => ~box 1~ ~z0 [ SNF ] [ SNF++, 479469, ~z0 ] % 220.17/220.63 (1,1) [478988,18]. true => ~_t85183 | _t37 [ SNF++, 2104 ] % 220.17/220.63 (1,1) [478990,18]. true => ~_t85170 | _t32 [ SNF++, 6708 ] % 220.17/220.63 (1,1) [478998,18]. true => ~_t85178 | _t46 [ SNF++, 17305 ] % 220.17/220.63 (1,1) [479012,18]. true => ~_t85187 | _t41 [ SNF++, 31513 ] % 220.17/220.63 (1,1) [479014,18]. true => ~_t85186 | _t40 [ SNF++, 31515 ] % 220.17/220.63 (20,1) [479132,18]. true => ~_t85185 | _t39 [ SNF++, 6669 ] % 220.17/220.63 (1,1) [479287,18]. _t37 => box 1 _t85188 [ SNF++, 2106 ] % 220.17/220.63 (1,1) [479289,18]. _t37 => box 1 _t85183 [ SNF++, 2108 ] % 220.17/220.63 (1,1) [479291,18]. _t40 => box 1 _t85187 [ SNF++, 4128 ] % 220.17/220.63 (1,1) [479301,18]. _t46 => box 1 _t85184 [ SNF++, 17308 ] % 220.17/220.63 (19,1) [479433,18]. _t39 => ~box 1~ _t85186 [ SNF++, 6668 ] % 220.17/220.63 (1,1) [479435,18]. _t40 => ~box 1~ _t85186 [ SNF++, 4131 ] % 220.17/220.63 (21,1) [479441,18]. _t32 => ~box 1~ _t85179 [ SNF++, 6707 ] % 220.17/220.63 (71,1) [479469,18]. _t41 => ~box 1~ _t85189 [ SNF++, 31512 ] % 220.17/220.63 (71,1) [660079,18]. true => ~_t41 | ~_t37 [ GEN1, 479287, 479469, 657384, _t85188, _t85189 ] % 220.17/220.63 (71,1) [660651,18]. true => ~_t85183 | ~_t41 [ LRES, 660079, 478988, ~_t37 ] % 220.17/220.63 (71,1) [661564,18]. true => ~_t85187 | ~_t85183 [ LRES, 660651, 479012, ~_t41 ] % 220.17/220.63 (1,1) [664151,18]. true => ~_t40 | ~_t37 [ GEN3, 479291, 479289, 662678, 479435, _t85187, _t85183, _t85186 ] % 220.17/220.63 (1,1) [707578,18]. true => ~_t85183 | ~_t40 [ LRES, 664151, 478988, ~_t37 ] % 220.17/220.63 (1,1) [750851,18]. true => ~_t85186 | ~_t85183 [ LRES, 707578, 479014, ~_t40 ] % 220.17/220.63 (19,1) [753632,18]. true => ~_t39 | ~_t37 [ GEN1, 479289, 479433, 752264, _t85183, _t85186 ] % 220.17/220.63 (19,1) [797059,18]. true => ~_t85183 | ~_t39 [ LRES, 753632, 478988, ~_t37 ] % 220.17/220.63 (20,1) [798102,18]. true => ~_t85185 | ~_t85183 [ LRES, 797059, 479132, ~_t39 ] % 220.17/220.63 (21,1) [871246,18]. true => ~_t46 | ~_t32 [ GEN1, 479301, 479441, 870570, _t85184, _t85179 ] % 220.17/220.63 (21,1) [915765,18]. true => ~_t85170 | ~_t46 [ LRES, 871246, 478990, ~_t32 ] % 220.17/220.63 (21,1) [916772,18]. true => ~_t85178 | ~_t85170 [ LRES, 915765, 478998, ~_t46 ] % 220.17/220.63 (1,1) [2110,19]. _t37 => box 1 z0 [ Axiom 4 ] [ SNF++, 479593, z0 ] % 220.17/220.63 (1,1) [2112,19]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 479595, _t37 ] % 220.17/220.63 (18,1) [4127,19]. _t41 => ~box 1~ ~z0 [ SNF ] [ SNF++, 479737, ~z0 ] % 220.17/220.63 (1,1) [4133,19]. _t40 => box 1 _t41 [ Axiom 4 ] [ SNF++, 479597, _t41 ] % 220.17/220.63 (1,1) [4136,19]. _t40 => ~box 1~ _t40 [ Axiom SER ] [ SNF++, 479743, _t40 ] % 220.17/220.63 (21,1) [6699,19]. true => _t37 | ~_t36 [ Axiom 4 ] % 220.17/220.63 (20,1) [6703,19]. _t38 => ~box 1~ _t39 [ Axiom 4 ] [ SNF++, 479745, _t39 ] % 220.17/220.63 (21,1) [6704,19]. true => _t38 | ~_t36 [ Axiom 4 ] % 220.17/220.63 (21,1) [6705,19]. true => _t36 | ~_t35 | p0 [ Axiom 4 ] % 220.17/220.63 (21,1) [6706,19]. true => _t35 | ~_t33 [ Axiom 4 ] % 220.17/220.63 (1,1) [17307,19]. true => ~_t47 | _t36 | ~p0 [ Axiom 4 ] % 220.17/220.63 (1,1) [479288,19]. true => ~_t85188 | z0 [ SNF++, 2106 ] % 220.17/220.63 (1,1) [479290,19]. true => ~_t85183 | _t37 [ SNF++, 2108 ] % 220.17/220.63 (1,1) [479292,19]. true => ~_t85187 | _t41 [ SNF++, 4128 ] % 220.17/220.63 (1,1) [479294,19]. true => ~_t85186 | _t40 [ SNF++, 4130 ] % 220.17/220.63 (1,1) [479302,19]. true => ~_t85184 | _t47 [ SNF++, 17308 ] % 220.17/220.63 (1,1) [479314,19]. true => ~_t85179 | _t33 [ SNF++, 27459 ] % 220.17/220.63 (71,1) [479470,19]. true => ~_t85189 | ~z0 [ SNF++, 31512 ] % 220.17/220.63 (1,1) [479593,19]. _t37 => box 1 _t85188 [ SNF++, 2110 ] % 220.17/220.63 (1,1) [479595,19]. _t37 => box 1 _t85183 [ SNF++, 2112 ] % 220.17/220.63 (1,1) [479597,19]. _t40 => box 1 _t85187 [ SNF++, 4133 ] % 220.17/220.63 (18,1) [479737,19]. _t41 => ~box 1~ _t85189 [ SNF++, 4127 ] % 220.17/220.63 (1,1) [479743,19]. _t40 => ~box 1~ _t85186 [ SNF++, 4136 ] % 220.17/220.63 (20,1) [479745,19]. _t38 => ~box 1~ _t85185 [ SNF++, 6703 ] % 220.17/220.63 (21,1) [633540,19]. true => ~_t85179 | _t35 [ LRES, 6706, 479314, ~_t33 ] % 220.17/220.63 (71,1) [657384,19]. true => ~_t85189 | ~_t85188 [ LRES, 479470, 479288, ~z0 ] % 220.17/220.63 (18,1) [660080,19]. true => ~_t41 | ~_t37 [ GEN1, 479593, 479737, 657385, _t85188, _t85189 ] % 220.17/220.63 (18,1) [661565,19]. true => ~_t85183 | ~_t41 [ LRES, 660080, 479290, ~_t37 ] % 220.17/220.63 (18,1) [662678,19]. true => ~_t85187 | ~_t85183 [ LRES, 661565, 479292, ~_t41 ] % 220.17/220.63 (1,1) [664236,19]. true => ~_t40 | ~_t37 [ GEN3, 479597, 479595, 662679, 479743, _t85187, _t85183, _t85186 ] % 220.17/220.63 (1,1) [750852,19]. true => ~_t85183 | ~_t40 [ LRES, 664236, 479290, ~_t37 ] % 220.17/220.63 (1,1) [752264,19]. true => ~_t85186 | ~_t85183 [ LRES, 750852, 479294, ~_t40 ] % 220.17/220.63 (20,1) [842795,19]. true => ~_t38 | ~_t37 [ GEN1, 479595, 479745, 798104, _t85183, _t85185 ] % 220.17/220.63 (21,1) [845912,19]. true => ~_t47 | _t36 | ~_t35 [ LRES, 17307, 6705, ~p0 ] % 220.17/220.63 (21,1) [861258,19]. true => ~_t85179 | ~_t47 | _t36 [ LRES, 845912, 633540, ~_t35 ] [ Backward Subsumption, 869895 ] % 220.17/220.63 (21,1) [862480,19]. true => ~_t85179 | ~_t47 | _t37 [ LRES, 861258, 6699, _t36 ] [ Backward Subsumption, 869895 ] % 226.46/226.90 (21,1) [862481,19]. true => ~_t85179 | ~_t47 | _t38 [ LRES, 861258, 6704, _t36 ] [ Backward Subsumption, 869895 ] % 226.46/226.90 (21,1) [864676,19]. true => ~_t85179 | ~_t47 | ~_t38 [ LRES, 862480, 842795, _t37 ] [ Backward Subsumption, 869895 ] % 226.46/226.90 (21,1) [869895,19]. true => ~_t85179 | ~_t47 [ LRES, 864676, 862481, ~_t38 ] % 226.46/226.90 (21,1) [870570,19]. true => ~_t85184 | ~_t85179 [ LRES, 869895, 479302, ~_t47 ] % 226.46/226.90 (1,1) [2114,20]. _t37 => box 1 z0 [ Axiom 4 ] [ SNF++, 479899, z0 ] % 226.46/226.90 (1,1) [2116,20]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 479901, _t37 ] % 226.46/226.90 (18,1) [4132,20]. _t41 => ~box 1~ ~z0 [ Axiom 4 ] [ SNF++, 480043, ~z0 ] % 226.46/226.90 (1,1) [4140,20]. _t40 => box 1 _t40 [ Axiom 4 ] [ SNF++, 479905, _t40 ] % 226.46/226.90 (19,1) [6702,20]. _t39 => ~box 1~ _t40 [ Axiom 4 ] [ SNF++, 480047, _t40 ] % 226.46/226.90 (1,1) [479594,20]. true => ~_t85188 | z0 [ SNF++, 2110 ] % 226.46/226.90 (1,1) [479596,20]. true => ~_t85183 | _t37 [ SNF++, 2112 ] % 226.46/226.90 (1,1) [479598,20]. true => ~_t85187 | _t41 [ SNF++, 4133 ] % 226.46/226.90 (18,1) [479738,20]. true => ~_t85189 | ~z0 [ SNF++, 4127 ] % 226.46/226.90 (20,1) [479746,20]. true => ~_t85185 | _t39 [ SNF++, 6703 ] % 226.46/226.90 (1,1) [479899,20]. _t37 => box 1 _t85188 [ SNF++, 2114 ] % 226.46/226.90 (1,1) [479901,20]. _t37 => box 1 _t85183 [ SNF++, 2116 ] % 226.46/226.90 (18,1) [480043,20]. _t41 => ~box 1~ _t85189 [ SNF++, 4132 ] % 226.46/226.90 (19,1) [480047,20]. _t39 => ~box 1~ _t85186 [ SNF++, 6702 ] % 226.46/226.90 (18,1) [657385,20]. true => ~_t85189 | ~_t85188 [ LRES, 479738, 479594, ~z0 ] % 226.46/226.90 (18,1) [660081,20]. true => ~_t41 | ~_t37 [ GEN1, 479899, 480043, 657386, _t85188, _t85189 ] % 226.46/226.90 (18,1) [661566,20]. true => ~_t85183 | ~_t41 [ LRES, 660081, 479596, ~_t37 ] % 226.46/226.90 (18,1) [662679,20]. true => ~_t85187 | ~_t85183 [ LRES, 661566, 479598, ~_t41 ] % 226.46/226.90 (19,1) [753806,20]. true => ~_t39 | ~_t37 [ GEN1, 479901, 480047, 752266, _t85183, _t85186 ] % 226.46/226.90 (19,1) [797061,20]. true => ~_t85183 | ~_t39 [ LRES, 753806, 479596, ~_t37 ] % 226.46/226.90 (20,1) [798104,20]. true => ~_t85185 | ~_t85183 [ LRES, 797061, 479746, ~_t39 ] % 226.46/226.90 (1,1) [2120,21]. _t37 => box 1 _t37 [ Axiom 4 ] [ SNF++, 480207, _t37 ] % 226.46/226.90 (1,1) [4143,21]. _t40 => box 1 _t41 [ Axiom 4 ] [ SNF++, 480209, _t41 ] % 226.46/226.90 (1,1) [4146,21]. _t40 => ~box 1~ _t40 [ Axiom SER ] [ SNF++, 480355, _t40 ] % 226.46/226.90 (1,1) [479900,21]. true => ~_t85188 | z0 [ SNF++, 2114 ] % 226.46/226.90 (1,1) [479902,21]. true => ~_t85183 | _t37 [ SNF++, 2116 ] % 226.46/226.90 (1,1) [479906,21]. true => ~_t85186 | _t40 [ SNF++, 4140 ] % 226.46/226.90 (18,1) [480044,21]. true => ~_t85189 | ~z0 [ SNF++, 4132 ] % 226.46/226.90 (1,1) [480207,21]. _t37 => box 1 _t85183 [ SNF++, 2120 ] % 226.46/226.90 (1,1) [480209,21]. _t40 => box 1 _t85187 [ SNF++, 4143 ] % 226.46/226.90 (1,1) [480355,21]. _t40 => ~box 1~ _t85186 [ SNF++, 4146 ] % 226.46/226.90 (18,1) [657386,21]. true => ~_t85189 | ~_t85188 [ LRES, 480044, 479900, ~z0 ] % 226.46/226.90 (1,1) [664408,21]. true => ~_t40 | ~_t37 [ GEN3, 480209, 480207, 662681, 480355, _t85187, _t85183, _t85186 ] % 226.46/226.90 (1,1) [750854,21]. true => ~_t85183 | ~_t40 [ LRES, 664408, 479902, ~_t37 ] % 226.46/226.90 (1,1) [752266,21]. true => ~_t85186 | ~_t85183 [ LRES, 750854, 479906, ~_t40 ] % 226.46/226.90 (1,1) [2122,22]. _t37 => box 1 z0 [ Axiom 4 ] [ SNF++, 480511, z0 ] % 226.46/226.90 (18,1) [4142,22]. _t41 => ~box 1~ ~z0 [ Axiom 4 ] [ SNF++, 480655, ~z0 ] % 226.46/226.90 (1,1) [480208,22]. true => ~_t85183 | _t37 [ SNF++, 2120 ] % 226.46/226.90 (1,1) [480210,22]. true => ~_t85187 | _t41 [ SNF++, 4143 ] % 226.46/226.90 (1,1) [480511,22]. _t37 => box 1 _t85188 [ SNF++, 2122 ] % 226.46/226.90 (18,1) [480655,22]. _t41 => ~box 1~ _t85189 [ SNF++, 4142 ] % 226.46/226.90 (18,1) [660083,22]. true => ~_t41 | ~_t37 [ GEN1, 480511, 480655, 657388, _t85188, _t85189 ] % 226.46/226.90 (18,1) [661568,22]. true => ~_t85183 | ~_t41 [ LRES, 660083, 480208, ~_t37 ] % 226.46/226.90 (18,1) [662681,22]. true => ~_t85187 | ~_t85183 [ LRES, 661568, 480210, ~_t41 ] % 226.46/226.90 (1,1) [480512,23]. true => ~_t85188 | z0 [ SNF++, 2122 ] % 226.46/226.90 (18,1) [480656,23]. true => ~_t85189 | ~z0 [ SNF++, 4142 ] % 226.46/226.90 (18,1) [657388,23]. true => ~_t85189 | ~_t85188 [ LRES, 480656, 480512, ~z0 ] % 226.46/226.90 % SZS output end Refutation % 226.63/227.11 % KSP exiting %------------------------------------------------------------------------------