%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP108_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n007.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:13:00 PM UTC 2026 % Result : Theorem 1.25s 1.42s % Output : Refutation 1.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SYP108_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.08 % Command : run_ksp %s % 0.09/0.27 % Computer : n007.cluster.edu % 0.09/0.27 % Model : x86_64 x86_64 % 0.09/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.27 % Memory : 8042.1875MB % 0.09/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.27 % CPULimit : 300 % 0.09/0.27 % WCLimit : 300 % 0.09/0.27 % DateTime : Mon May 4 17:43:38 EDT 2026 % 0.09/0.27 % CPUTime : % 0.20/0.43 ----KSP format--- % 0.20/0.43 set(box,REF). % 0.20/0.43 usable(formulas). % 0.20/0.43 true. % 0.20/0.43 end_of_list. % 0.20/0.43 sos(formulas). % 0.20/0.43 ~ ([] ( 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.20/0.43 end_of_list. % 0.20/0.43 ----------------- % 0.20/0.43 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.XYr8xhQ8qq/theBenchmark.ksp % 1.25/1.42 % 1.25/1.42 % SZS status Theorem % 1.25/1.42 % 1.25/1.42 ***************** % 1.25/1.42 FOUND PROOF 1 % 1.25/1.42 ***************** % 1.25/1.42 % SZS output start Refutation % 1.25/1.42 % 1.25/1.42 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 1.25/1.42 (1,1) [381,0]. true => _t24 | ~_t23 [ Axiom T ] [ Backward Subsumption, 3262 ] % 1.25/1.42 (1,1) [383,0]. true => _t25 | ~_t24 [ Axiom T ] [ Backward Subsumption, 3588 ] % 1.25/1.42 (1,1) [385,0]. true => _t26 | ~_t25 [ Axiom T ] [ Backward Subsumption, 3620 ] % 1.25/1.42 (1,1) [387,0]. true => _t27 | ~_t26 [ Axiom T ] [ Backward Subsumption, 3622 ] % 1.25/1.42 (1,1) [389,0]. true => _t28 | ~_t27 [ Axiom T ] [ Backward Subsumption, 3637 ] % 1.25/1.42 (1,1) [391,0]. true => _t29 | ~_t28 [ Axiom T ] [ Backward Subsumption, 3644 ] % 1.25/1.42 (1,1) [393,0]. true => _t30 | ~_t29 [ Axiom T ] [ Backward Subsumption, 3653 ] % 1.25/1.42 (1,1) [395,0]. true => _t31 | ~_t30 [ Axiom T ] [ Backward Subsumption, 3661 ] % 1.25/1.42 (1,1) [397,0]. true => _t32 | ~_t31 [ Axiom T ] [ Backward Subsumption, 3663 ] % 1.25/1.42 (1,1) [399,0]. true => _t33 | ~_t32 [ Axiom T ] [ Backward Subsumption, 3670 ] % 1.25/1.42 (1,1) [400,0]. _t33 => box 1 p2 [ Axiom T ] [ Backward Subsumption, 3673 ] % 1.25/1.42 (1,1) [402,0]. true => _t23 | ~_t0 [ SNF ] [ Backward Subsumption, 3257 ] % 1.25/1.42 (7,1) [799,0]. _t69 => ~box 1~ ~p2 [ Axiom T ] [ Backward Subsumption, 3411 ] % 1.25/1.42 (1,1) [3083,0]. true => _t69 | ~_t0 [ SNF ] [ Backward Subsumption, 3101 ] % 1.25/1.42 (1,1) [3101,0]. true => _t69 [ Unit Resolution, 3, 3083, _t0 ] [ Modal Level Pure Literal Elimination, _t69 ] % 1.25/1.42 (1,1) [3257,0]. true => _t23 [ Unit Resolution, 3, 402, _t0 ] [ Modal Level Pure Literal Elimination, _t23 ] % 1.25/1.42 (1,1) [3262,0]. true => _t24 [ Unit Resolution, 3257, 381, _t23 ] [ Modal Level Pure Literal Elimination, _t24 ] % 1.25/1.42 (7,1) [3411,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 3101, 799, _t69 ] [ SNF++, 6384, ~p2 ] % 1.25/1.42 (1,1) [3588,0]. true => _t25 [ Unit Resolution, 3262, 383, _t24 ] [ Modal Level Pure Literal Elimination, _t25 ] % 1.25/1.42 (1,1) [3620,0]. true => _t26 [ Unit Resolution, 3588, 385, _t25 ] [ Modal Level Pure Literal Elimination, _t26 ] % 1.25/1.42 (1,1) [3622,0]. true => _t27 [ Unit Resolution, 3620, 387, _t26 ] [ Modal Level Pure Literal Elimination, _t27 ] % 1.25/1.42 (1,1) [3637,0]. true => _t28 [ Unit Resolution, 3622, 389, _t27 ] [ Modal Level Pure Literal Elimination, _t28 ] % 1.25/1.42 (1,1) [3644,0]. true => _t29 [ Unit Resolution, 3637, 391, _t28 ] [ Modal Level Pure Literal Elimination, _t29 ] % 1.25/1.42 (1,1) [3653,0]. true => _t30 [ Unit Resolution, 3644, 393, _t29 ] [ Modal Level Pure Literal Elimination, _t30 ] % 1.25/1.42 (1,1) [3661,0]. true => _t31 [ Unit Resolution, 3653, 395, _t30 ] [ Modal Level Pure Literal Elimination, _t31 ] % 1.25/1.42 (1,1) [3663,0]. true => _t32 [ Unit Resolution, 3661, 397, _t31 ] [ Modal Level Pure Literal Elimination, _t32 ] % 1.25/1.42 (1,1) [3670,0]. true => _t33 [ Unit Resolution, 3663, 399, _t32 ] [ Modal Level Pure Literal Elimination, _t33 ] % 1.25/1.42 (1,1) [3673,0]. true => box 1 p2 [ LHS Unit Resolution, 3670, 400, _t33 ] [ SNF++, 5980, p2 ] % 1.25/1.42 (1,1) [5980,0]. true => box 1 _t276 [ SNF++, 3673 ] % 1.25/1.42 (7,1) [6384,0]. true => ~box 1~ _t279 [ SNF++, 3411 ] % 1.25/1.42 (7,1) [21879,0]. true => false [ GEN1, 5980, 6384, 8323, _t276, _t279 ] % 1.25/1.42 (1,1) [5981,1]. true => ~_t276 | p2 [ SNF++, 3673 ] % 1.25/1.42 (7,1) [6385,1]. true => ~_t279 | ~p2 [ SNF++, 3411 ] % 1.25/1.42 (7,1) [8323,1]. true => ~_t279 | ~_t276 [ LRES, 6385, 5981, ~p2 ] % 1.25/1.42 % SZS output end Refutation % 1.25/1.42 % KSP exiting %------------------------------------------------------------------------------