%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP054_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n019.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:55 PM UTC 2026 % Result : Theorem 8.54s 8.71s % Output : Refutation 9.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYP054_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_ksp %s % 0.15/0.34 % Computer : n019.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Mon May 4 16:41:14 EDT 2026 % 0.15/0.34 % CPUTime : % 0.36/0.61 ----KSP format--- % 0.36/0.61 set(box,FIVE). % 0.36/0.61 usable(formulas). % 0.36/0.61 true. % 0.36/0.61 end_of_list. % 0.36/0.61 sos(formulas). % 0.36/0.61 ~ ([] ( 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.36/0.61 end_of_list. % 0.36/0.61 ----------------- % 0.36/0.61 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.AXNIBYQ0Wv/theBenchmark.ksp % 8.54/8.71 % 8.54/8.71 % SZS status Theorem % 8.54/8.71 % 8.54/8.71 ***************** % 8.54/8.71 FOUND PROOF 1 % 8.54/8.71 ***************** % 8.54/8.71 % SZS output start Refutation % 8.54/8.71 % 8.54/8.71 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 8.54/8.71 (1,1) [1145,0]. _t33 => box 1 p2 [ Axiom 5 ] [ SNF++, 19715, p2 ] % 8.54/8.71 (1,1) [1147,0]. ~_t296 => box 1 ~_t33 [ Axiom 5 ] [ SNF++, 19717, ~_t33 ] % 8.54/8.71 (1,1) [1149,0]. true => ~_t296 | _t33 [ Axiom 5 ] [ Modal Level Pure Literal Elimination, ~_t296 ] % 8.54/8.71 (1,1) [1192,0]. _t32 => box 1 _t33 [ Axiom 5 ] [ SNF++, 19721, _t33 ] % 8.54/8.71 (1,1) [1194,0]. ~_t297 => box 1 ~_t32 [ Axiom 5 ] [ SNF++, 19723, ~_t32 ] % 8.54/8.71 (1,1) [1196,0]. true => ~_t297 | _t32 [ Axiom 5 ] [ Backward Subsumption, 1004371 ] % 8.54/8.71 (1,1) [1246,0]. _t31 => box 1 _t32 [ Axiom 5 ] [ SNF++, 19727, _t32 ] % 8.54/8.71 (1,1) [1248,0]. ~_t298 => box 1 ~_t31 [ Axiom 5 ] [ SNF++, 19729, ~_t31 ] % 8.54/8.71 (1,1) [1250,0]. true => ~_t298 | _t31 [ Axiom 5 ] [ Backward Subsumption, 1004617 ] % 8.54/8.71 (1,1) [1299,0]. _t30 => box 1 _t31 [ Axiom 5 ] [ SNF++, 19733, _t31 ] % 8.54/8.71 (1,1) [1301,0]. ~_t299 => box 1 ~_t30 [ Axiom 5 ] [ SNF++, 19735, ~_t30 ] % 8.54/8.71 (1,1) [1303,0]. true => ~_t299 | _t30 [ Axiom 5 ] [ Backward Subsumption, 1004862 ] % 8.54/8.71 (1,1) [1351,0]. _t29 => box 1 _t30 [ Axiom 5 ] [ SNF++, 19739, _t30 ] % 8.54/8.71 (1,1) [1353,0]. ~_t300 => box 1 ~_t29 [ Axiom 5 ] [ SNF++, 19741, ~_t29 ] % 8.54/8.71 (1,1) [1355,0]. true => ~_t300 | _t29 [ Axiom 5 ] [ Backward Subsumption, 1005106 ] % 8.54/8.71 (1,1) [1403,0]. _t28 => box 1 _t29 [ Axiom 5 ] [ SNF++, 19745, _t29 ] % 8.54/8.71 (1,1) [1405,0]. ~_t301 => box 1 ~_t28 [ Axiom 5 ] [ SNF++, 19747, ~_t28 ] % 8.54/8.71 (1,1) [1407,0]. true => ~_t301 | _t28 [ Axiom 5 ] [ Backward Subsumption, 1005349 ] % 8.54/8.71 (1,1) [1455,0]. _t27 => box 1 _t28 [ Axiom 5 ] [ SNF++, 19751, _t28 ] % 8.54/8.71 (1,1) [1457,0]. ~_t302 => box 1 ~_t27 [ Axiom 5 ] [ SNF++, 19753, ~_t27 ] % 8.54/8.71 (1,1) [1459,0]. true => ~_t302 | _t27 [ Axiom 5 ] [ Backward Subsumption, 1005591 ] % 8.54/8.71 (1,1) [1507,0]. _t26 => box 1 _t27 [ Axiom 5 ] [ SNF++, 19757, _t27 ] % 8.54/8.71 (1,1) [1509,0]. ~_t303 => box 1 ~_t26 [ Axiom 5 ] [ SNF++, 19759, ~_t26 ] % 8.54/8.71 (1,1) [1511,0]. true => ~_t303 | _t26 [ Axiom 5 ] [ Backward Subsumption, 1005832 ] % 8.54/8.71 (1,1) [1559,0]. _t25 => box 1 _t26 [ Axiom 5 ] [ SNF++, 19763, _t26 ] % 8.54/8.71 (1,1) [1561,0]. ~_t304 => box 1 ~_t25 [ Axiom 5 ] [ SNF++, 19765, ~_t25 ] % 8.54/8.71 (1,1) [1563,0]. true => ~_t304 | _t25 [ Axiom 5 ] [ Backward Subsumption, 1006072 ] % 8.54/8.71 (1,1) [1611,0]. _t24 => box 1 _t25 [ Axiom 5 ] [ SNF++, 19769, _t25 ] % 8.54/8.71 (1,1) [1613,0]. ~_t305 => box 1 ~_t24 [ Axiom 5 ] [ SNF++, 19771, ~_t24 ] % 8.54/8.71 (1,1) [1615,0]. true => ~_t305 | _t24 [ Axiom 5 ] [ Backward Subsumption, 1006311 ] % 8.54/8.71 (1,1) [1661,0]. _t23 => box 1 _t24 [ SNF ] [ Backward Subsumption, 19504 ] % 8.54/8.71 (1,1) [1713,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 19420 ] % 8.54/8.71 (325,1) [18957,0]. _t69 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 19424 ] % 8.54/8.71 (1,1) [18958,0]. true => _t69 | ~_t0 [ SNF ] [ Backward Subsumption, 19264 ] % 8.54/8.71 (327,1) [18959,0]. _t138 => ~box 1~ ~p1 [ SNF ] [ Backward Subsumption, 19581 ] % 8.54/8.71 (1,1) [18960,0]. true => _t138 | ~_t0 [ SNF ] [ Backward Subsumption, 19263 ] % 8.54/8.71 (1,1) [19263,0]. true => _t138 [ Unit Resolution, 3, 18960, _t0 ] [ Modal Level Pure Literal Elimination, _t138 ] % 8.54/8.71 (1,1) [19264,0]. true => _t69 [ Unit Resolution, 3, 18958, _t0 ] [ Modal Level Pure Literal Elimination, _t69 ] % 8.54/8.71 (1,1) [19420,0]. true => _t23 [ Unit Resolution, 3, 1713, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 8.54/8.71 (325,1) [19424,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 19264, 18957, _t69 ] [ SNF++, 21507, ~p2 ] % 8.54/8.71 (1,1) [19504,0]. true => box 1 _t24 [ LHS Unit Resolution, 19420, 1661, _t23 ] [ SNF++, 19775, _t24 ] % 8.54/8.71 (327,1) [19581,0]. true => ~box 1~ ~p1 [ LHS Unit Resolution, 19263, 18959, _t138 ] [ SNF++, 21509, ~p1 ] % 8.54/8.71 (1,1) [19715,0]. _t33 => box 1 _t582 [ SNF++, 1145 ] [ Backward Subsumption, 1004370 ] % 8.54/8.71 (1,1) [19717,0]. ~_t296 => box 1 _t583 [ SNF++, 1147 ] [ Backward Subsumption, 1004367 ] % 8.54/8.71 (1,1) [19721,0]. _t32 => box 1 _t585 [ SNF++, 1192 ] [ Backward Subsumption, 1004372 ] % 8.54/8.71 (1,1) [19723,0]. ~_t297 => box 1 _t586 [ SNF++, 1194 ] [ Backward Subsumption, 1004614 ] % 8.54/8.71 (1,1) [19727,0]. _t31 => box 1 _t588 [ SNF++, 1246 ] [ Backward Subsumption, 1004618 ] % 8.54/8.71 (1,1) [19729,0]. ~_t298 => box 1 _t589 [ SNF++, 1248 ] [ Backward Subsumption, 1004859 ] % 8.54/8.71 (1,1) [19733,0]. _t30 => box 1 _t591 [ SNF++, 1299 ] [ Backward Subsumption, 1004863 ] % 8.54/8.71 (1,1) [19735,0]. ~_t299 => box 1 _t592 [ SNF++, 1301 ] [ Backward Subsumption, 1005103 ] % 8.54/8.71 (1,1) [19739,0]. _t29 => box 1 _t594 [ SNF++, 1351 ] [ Backward Subsumption, 1005107 ] % 8.54/8.71 (1,1) [19741,0]. ~_t300 => box 1 _t595 [ SNF++, 1353 ] [ Backward Subsumption, 1005346 ] % 8.54/8.71 (1,1) [19745,0]. _t28 => box 1 _t597 [ SNF++, 1403 ] [ Backward Subsumption, 1005350 ] % 8.54/8.71 (1,1) [19747,0]. ~_t301 => box 1 _t598 [ SNF++, 1405 ] [ Backward Subsumption, 1005588 ] % 8.54/8.71 (1,1) [19751,0]. _t27 => box 1 _t600 [ SNF++, 1455 ] [ Backward Subsumption, 1005592 ] % 8.54/8.71 (1,1) [19753,0]. ~_t302 => box 1 _t601 [ SNF++, 1457 ] [ Backward Subsumption, 1005829 ] % 8.54/8.71 (1,1) [19757,0]. _t26 => box 1 _t603 [ SNF++, 1507 ] [ Backward Subsumption, 1005833 ] % 8.54/8.71 (1,1) [19759,0]. ~_t303 => box 1 _t604 [ SNF++, 1509 ] [ Backward Subsumption, 1006069 ] % 8.54/8.71 (1,1) [19763,0]. _t25 => box 1 _t606 [ SNF++, 1559 ] [ Backward Subsumption, 1006073 ] % 8.54/8.71 (1,1) [19765,0]. ~_t304 => box 1 _t607 [ SNF++, 1561 ] [ Backward Subsumption, 1006308 ] % 8.54/8.71 (1,1) [19769,0]. _t24 => box 1 _t609 [ SNF++, 1611 ] [ Backward Subsumption, 1006312 ] % 8.54/8.71 (1,1) [19771,0]. ~_t305 => box 1 _t610 [ SNF++, 1613 ] % 8.54/8.71 (1,1) [19775,0]. true => box 1 _t612 [ SNF++, 19504 ] % 8.54/8.71 (325,1) [21507,0]. true => ~box 1~ _t1263 [ SNF++, 19424 ] % 8.54/8.71 (327,1) [21509,0]. true => ~box 1~ _t1264 [ SNF++, 19581 ] % 8.54/8.71 (1,1) [140450,0]. true => _t296 | ~_t32 [ GEN3, 19721, 19717, 36956, 21509, _t585, _t583, _t1264 ] [ Backward Subsumption, 1004366 ] % 8.54/8.71 (1,1) [145177,0]. true => _t297 | ~_t31 [ GEN3, 19727, 19723, 36973, 21509, _t588, _t586, _t1264 ] [ Backward Subsumption, 1004613 ] % 8.54/8.71 (1,1) [149656,0]. true => _t298 | ~_t30 [ GEN3, 19733, 19729, 36990, 21509, _t591, _t589, _t1264 ] [ Backward Subsumption, 1004858 ] % 8.54/8.71 (1,1) [154383,0]. true => _t299 | ~_t29 [ GEN3, 19739, 19735, 37007, 21509, _t594, _t592, _t1264 ] [ Backward Subsumption, 1005102 ] % 8.54/8.71 (1,1) [159110,0]. true => _t300 | ~_t28 [ GEN3, 19745, 19741, 37024, 21509, _t597, _t595, _t1264 ] [ Backward Subsumption, 1005345 ] % 8.54/8.71 (1,1) [163589,0]. true => _t301 | ~_t27 [ GEN3, 19751, 19747, 37041, 21509, _t600, _t598, _t1264 ] [ Backward Subsumption, 1005587 ] % 8.54/8.71 (1,1) [168316,0]. true => _t302 | ~_t26 [ GEN3, 19757, 19753, 37058, 21509, _t603, _t601, _t1264 ] [ Backward Subsumption, 1005828 ] % 8.54/8.71 (1,1) [173043,0]. true => _t303 | ~_t25 [ GEN3, 19763, 19759, 37075, 21509, _t606, _t604, _t1264 ] [ Backward Subsumption, 1006068 ] % 8.54/8.71 (1,1) [177522,0]. true => _t304 | ~_t24 [ GEN3, 19769, 19765, 37092, 21509, _t609, _t607, _t1264 ] [ Backward Subsumption, 1006307 ] % 8.54/8.71 (1,1) [182249,0]. true => _t305 [ GEN3, 19775, 19771, 37109, 21509, _t612, _t610, _t1264 ] % 8.54/8.71 (325,1) [1002387,0]. true => ~_t33 [ GEN1, 19715, 21507, 40779, _t582, _t1263 ] [ Modal Level Pure Literal Elimination, ~_t33 ] % 8.54/8.71 (325,1) [1004124,0]. true => ~_t296 [ LRES, 1002387, 1149, ~_t33 ] [ Modal Level Pure Literal Elimination, ~_t296 ] % 8.54/8.71 (325,1) [1004366,0]. true => ~_t32 [ Unit Resolution, 1004124, 140450, _t296 ] [ Modal Level Pure Literal Elimination, ~_t32 ] % 8.54/8.71 (325,1) [1004371,0]. true => ~_t297 [ Unit Resolution, 1004366, 1196, _t32 ] [ Modal Level Pure Literal Elimination, ~_t297 ] % 8.54/8.71 (325,1) [1004613,0]. true => ~_t31 [ Unit Resolution, 1004371, 145177, _t297 ] [ Modal Level Pure Literal Elimination, ~_t31 ] % 8.54/8.71 (325,1) [1004617,0]. true => ~_t298 [ Unit Resolution, 1004613, 1250, _t31 ] [ Modal Level Pure Literal Elimination, ~_t298 ] % 8.54/8.71 (325,1) [1004858,0]. true => ~_t30 [ Unit Resolution, 1004617, 149656, _t298 ] [ Modal Level Pure Literal Elimination, ~_t30 ] % 8.54/8.71 (325,1) [1004862,0]. true => ~_t299 [ Unit Resolution, 1004858, 1303, _t30 ] [ Modal Level Pure Literal Elimination, ~_t299 ] % 8.54/8.71 (325,1) [1005102,0]. true => ~_t29 [ Unit Resolution, 1004862, 154383, _t299 ] [ Modal Level Pure Literal Elimination, ~_t29 ] % 8.54/8.71 (325,1) [1005106,0]. true => ~_t300 [ Unit Resolution, 1005102, 1355, _t29 ] [ Modal Level Pure Literal Elimination, ~_t300 ] % 8.54/8.71 (325,1) [1005345,0]. true => ~_t28 [ Unit Resolution, 1005106, 159110, _t300 ] [ Modal Level Pure Literal Elimination, ~_t28 ] % 8.54/8.71 (325,1) [1005349,0]. true => ~_t301 [ Unit Resolution, 1005345, 1407, _t28 ] [ Modal Level Pure Literal Elimination, ~_t301 ] % 8.54/8.71 (325,1) [1005587,0]. true => ~_t27 [ Unit Resolution, 1005349, 163589, _t301 ] [ Modal Level Pure Literal Elimination, ~_t27 ] % 8.54/8.71 (325,1) [1005591,0]. true => ~_t302 [ Unit Resolution, 1005587, 1459, _t27 ] [ Modal Level Pure Literal Elimination, ~_t302 ] % 8.54/8.71 (325,1) [1005828,0]. true => ~_t26 [ Unit Resolution, 1005591, 168316, _t302 ] [ Modal Level Pure Literal Elimination, ~_t26 ] % 8.54/8.71 (325,1) [1005832,0]. true => ~_t303 [ Unit Resolution, 1005828, 1511, _t26 ] [ Modal Level Pure Literal Elimination, ~_t303 ] % 8.54/8.71 (325,1) [1006068,0]. true => ~_t25 [ Unit Resolution, 1005832, 173043, _t303 ] [ Modal Level Pure Literal Elimination, ~_t25 ] % 8.54/8.71 (325,1) [1006072,0]. true => ~_t304 [ Unit Resolution, 1006068, 1563, _t25 ] [ Modal Level Pure Literal Elimination, ~_t304 ] % 8.54/8.71 (325,1) [1006307,0]. true => ~_t24 [ Unit Resolution, 1006072, 177522, _t304 ] [ Modal Level Pure Literal Elimination, ~_t24 ] % 8.54/8.71 (325,1) [1006311,0]. true => ~_t305 [ Unit Resolution, 1006307, 1615, _t24 ] % 8.54/8.71 (325,1) [1006543,0]. true => false [ Unit Resolution, 1006311, 182249, _t305 ] % 8.54/8.71 (1,1) [19716,1]. true => ~_t582 | p2 [ SNF++, 1145 ] [ Modal Level Pure Literal Elimination, ~_t582 ] % 8.54/8.71 (1,1) [19718,1]. true => ~_t583 | ~_t33 [ SNF++, 1147 ] % 8.54/8.71 (1,1) [19722,1]. true => ~_t585 | _t33 [ SNF++, 1192 ] [ Modal Level Pure Literal Elimination, ~_t585 ] % 8.54/8.71 (1,1) [19724,1]. true => ~_t586 | ~_t32 [ SNF++, 1194 ] % 8.54/8.71 (1,1) [19728,1]. true => ~_t588 | _t32 [ SNF++, 1246 ] [ Modal Level Pure Literal Elimination, ~_t588 ] % 8.54/8.71 (1,1) [19730,1]. true => ~_t589 | ~_t31 [ SNF++, 1248 ] % 8.54/8.71 (1,1) [19734,1]. true => ~_t591 | _t31 [ SNF++, 1299 ] [ Modal Level Pure Literal Elimination, ~_t591 ] % 8.54/8.71 (1,1) [19736,1]. true => ~_t592 | ~_t30 [ SNF++, 1301 ] % 8.54/8.71 (1,1) [19740,1]. true => ~_t594 | _t30 [ SNF++, 1351 ] [ Modal Level Pure Literal Elimination, ~_t594 ] % 8.54/8.71 (1,1) [19742,1]. true => ~_t595 | ~_t29 [ SNF++, 1353 ] % 8.54/8.71 (1,1) [19746,1]. true => ~_t597 | _t29 [ SNF++, 1403 ] [ Modal Level Pure Literal Elimination, ~_t597 ] % 8.54/8.71 (1,1) [19748,1]. true => ~_t598 | ~_t28 [ SNF++, 1405 ] % 8.54/8.71 (1,1) [19752,1]. true => ~_t600 | _t28 [ SNF++, 1455 ] [ Modal Level Pure Literal Elimination, ~_t600 ] % 8.54/8.71 (1,1) [19754,1]. true => ~_t601 | ~_t27 [ SNF++, 1457 ] % 8.54/8.71 (1,1) [19758,1]. true => ~_t603 | _t27 [ SNF++, 1507 ] [ Modal Level Pure Literal Elimination, ~_t603 ] % 8.54/8.71 (1,1) [19760,1]. true => ~_t604 | ~_t26 [ SNF++, 1509 ] % 8.54/8.71 (1,1) [19764,1]. true => ~_t606 | _t26 [ SNF++, 1559 ] [ Modal Level Pure Literal Elimination, ~_t606 ] % 8.54/8.71 (1,1) [19766,1]. true => ~_t607 | ~_t25 [ SNF++, 1561 ] % 8.54/8.71 (1,1) [19770,1]. true => ~_t609 | _t25 [ SNF++, 1611 ] [ Modal Level Pure Literal Elimination, ~_t609 ] % 8.54/8.71 (1,1) [19772,1]. true => ~_t610 | ~_t24 [ SNF++, 1613 ] % 8.54/8.71 (1,1) [19776,1]. true => ~_t612 | _t24 [ SNF++, 19504 ] % 8.54/8.71 (325,1) [21508,1]. true => ~_t1263 | ~p2 [ SNF++, 19424 ] % 8.54/8.71 (1,1) [36956,1]. true => ~_t585 | ~_t583 [ LRES, 19718, 19722, ~_t33 ] [ Modal Level Pure Literal Elimination, ~_t585 ] % 8.54/8.71 (1,1) [36973,1]. true => ~_t588 | ~_t586 [ LRES, 19724, 19728, ~_t32 ] [ Modal Level Pure Literal Elimination, ~_t588 ] % 8.54/8.71 (1,1) [36990,1]. true => ~_t591 | ~_t589 [ LRES, 19730, 19734, ~_t31 ] [ Modal Level Pure Literal Elimination, ~_t591 ] % 8.54/8.71 (1,1) [37007,1]. true => ~_t594 | ~_t592 [ LRES, 19736, 19740, ~_t30 ] [ Modal Level Pure Literal Elimination, ~_t594 ] % 8.54/8.71 (1,1) [37024,1]. true => ~_t597 | ~_t595 [ LRES, 19742, 19746, ~_t29 ] [ Modal Level Pure Literal Elimination, ~_t597 ] % 8.54/8.71 (1,1) [37041,1]. true => ~_t600 | ~_t598 [ LRES, 19748, 19752, ~_t28 ] [ Modal Level Pure Literal Elimination, ~_t600 ] % 8.54/8.71 (1,1) [37058,1]. true => ~_t603 | ~_t601 [ LRES, 19754, 19758, ~_t27 ] [ Modal Level Pure Literal Elimination, ~_t603 ] % 8.54/8.71 (1,1) [37075,1]. true => ~_t606 | ~_t604 [ LRES, 19760, 19764, ~_t26 ] [ Modal Level Pure Literal Elimination, ~_t606 ] % 8.54/8.71 (1,1) [37092,1]. true => ~_t609 | ~_t607 [ LRES, 19766, 19770, ~_t25 ] [ Modal Level Pure Literal Elimination, ~_t609 ] % 9.44/9.61 (1,1) [37109,1]. true => ~_t612 | ~_t610 [ LRES, 19772, 19776, ~_t24 ] % 9.44/9.61 (325,1) [40779,1]. true => ~_t1263 | ~_t582 [ LRES, 21508, 19716, ~p2 ] [ Modal Level Pure Literal Elimination, ~_t582 ] % 9.44/9.61 % SZS output end Refutation % 9.44/9.65 % KSP exiting %------------------------------------------------------------------------------