%------------------------------------------------------------------------------ % File : KSP---0.1.7 % Problem : SYP033_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_ksp %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:12:54 PM UTC 2026 % Result : Theorem 1.45s 1.66s % Output : Refutation 1.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYP033_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_ksp %s % 0.16/0.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Mon May 4 16:15:27 EDT 2026 % 0.16/0.34 % CPUTime : % 0.36/0.61 ----KSP format--- % 0.36/0.61 set(box,TRANS). % 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 ~ (( [] ( ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 ) -> [] ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) ) -> ( [] ( $false ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 ) -> [] ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) ) -> ( [] ( $false ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 ) -> [] ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( $false ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( $false ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) -> [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) ) -> ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) ) & ( [] ( ( [] ( ( ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) -> [] ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) ) -> ( [] ( [] ( [] ( $false ) | p1 | p2 | p3 | p4 ) | p1 | p2 | p3 | p4 ) | p1 ) ) & ( [] ( ( [] ( ( ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) -> [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) & ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) ) ) ) ) ) -> ( ( [] ( ( [] ( ( p1 -> [] ( p1 ) ) ) -> p1 ) ) -> [] ( p1 ) ) | ( [] ( ( [] ( ( p2 -> [] ( p2 ) ) ) -> p2 ) ) -> [] ( p2 ) ) | ( [] ( ( [] ( ( p3 -> [] ( p3 ) ) ) -> p3 ) ) -> [] ( p3 ) ) ) ). % 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/sandbox2/tmp/tmp.Sm137LVNkE/theBenchmark.ksp % 1.45/1.66 % 1.45/1.66 % SZS status Theorem % 1.45/1.66 % 1.45/1.66 ***************** % 1.45/1.66 FOUND PROOF 1 % 1.45/1.66 ***************** % 1.45/1.66 % SZS output start Refutation % 1.45/1.66 % 1.45/1.66 (1,1) [3,0]. true => _t0 [ SNF ] [ Modal Level Pure Literal Elimination, _t0 ] % 1.45/1.66 (1,1) [1875,0]. _t1 => box 1 _t2 [ SNF ] [ Backward Subsumption, 67925 ] % 1.45/1.66 (1,1) [4060,0]. true => _t1 | ~_t0 [ SNF ] [ Backward Subsumption, 67923 ] % 1.45/1.66 (1,1) [8449,0]. _t18 => box 1 _t18 [ Axiom 4 ] [ Backward Subsumption, 67932 ] % 1.45/1.66 (1,1) [10633,0]. true => _t18 | ~_t0 [ SNF ] [ Backward Subsumption, 67920 ] % 1.45/1.66 (24,1) [10638,0]. _t22 => ~box 1~ ~p2 [ SNF ] [ Backward Subsumption, 67929 ] % 1.45/1.66 (1,1) [10639,0]. true => _t22 | ~_t0 [ SNF ] [ Backward Subsumption, 67917 ] % 1.45/1.66 (1,1) [67917,0]. true => _t22 [ Unit Resolution, 3, 10639, _t0 ] [ Modal Level Pure Literal Elimination, _t22 ] % 1.45/1.66 (1,1) [67920,0]. true => _t18 [ Unit Resolution, 3, 10633, _t0 ] [ Modal Level Pure Literal Elimination, _t18 ] % 1.45/1.66 (1,1) [67923,0]. true => _t1 [ Unit Resolution, 3, 4060, _t0 ] [ Modal Level Pure Literal Elimination, _t1 ] % 1.45/1.66 (1,1) [67925,0]. true => box 1 _t2 [ LHS Unit Resolution, 67923, 1875, _t1 ] [ SNF++, 82258, _t2 ] % 1.45/1.66 (24,1) [67929,0]. true => ~box 1~ ~p2 [ LHS Unit Resolution, 67917, 10638, _t22 ] [ SNF++, 82282, ~p2 ] % 1.45/1.66 (1,1) [67932,0]. true => box 1 _t18 [ LHS Unit Resolution, 67920, 8449, _t18 ] [ SNF++, 82272, _t18 ] % 1.45/1.66 (1,1) [82258,0]. true => box 1 _t116 [ SNF++, 67925 ] % 1.45/1.66 (1,1) [82272,0]. true => box 1 _t121 [ SNF++, 67932 ] % 1.45/1.66 (24,1) [82282,0]. true => ~box 1~ _t130 [ SNF++, 67929 ] % 1.45/1.66 (24,1) [118358,0]. true => false [ GEN1, 82272, 82258, 82282, 114644, _t121, _t116, _t130 ] % 1.45/1.66 (3,1) [1873,1]. _t3 => ~box 1~ _t4 [ SNF ] [ SNF++, 82224, _t4 ] % 1.45/1.66 (1,1) [1874,1]. true => _t3 | ~_t2 | p2 [ SNF ] % 1.45/1.66 (1,1) [8455,1]. _t18 => box 1 _t19 [ Axiom 4 ] [ SNF++, 82242, _t19 ] % 1.45/1.66 (3,1) [82224,1]. _t3 => ~box 1~ _t127 [ SNF++, 1873 ] % 1.45/1.66 (1,1) [82242,1]. _t18 => box 1 _t120 [ SNF++, 8455 ] % 1.45/1.66 (1,1) [82259,1]. true => ~_t116 | _t2 [ SNF++, 67925 ] % 1.45/1.66 (1,1) [82273,1]. true => ~_t121 | _t18 [ SNF++, 67932 ] % 1.45/1.66 (24,1) [82283,1]. true => ~_t130 | ~p2 [ SNF++, 67929 ] % 1.45/1.66 (24,1) [86030,1]. true => ~_t130 | _t3 | ~_t2 [ LRES, 82283, 1874, ~p2 ] % 1.45/1.66 (24,1) [89152,1]. true => ~_t130 | ~_t116 | _t3 [ LRES, 86030, 82259, ~_t2 ] % 1.45/1.66 (3,1) [112783,1]. true => ~_t18 | ~_t3 [ GEN1, 82242, 82224, 111552, _t120, _t127 ] % 1.45/1.66 (24,1) [113096,1]. true => ~_t130 | ~_t116 | ~_t18 [ LRES, 112783, 89152, ~_t3 ] % 1.45/1.66 (24,1) [114644,1]. true => ~_t130 | ~_t121 | ~_t116 [ LRES, 113096, 82273, ~_t18 ] % 1.45/1.66 (3,1) [4,2]. true => ~_t4 | ~p2 [ SNF ] % 1.45/1.66 (1,1) [628,2]. _t5 => box 1 _t6 [ SNF ] [ SNF++, 82176, _t6 ] % 1.45/1.66 (3,1) [1872,2]. true => _t5 | ~_t4 [ SNF ] % 1.45/1.66 (18,1) [8453,2]. _t20 => ~box 1~ _t21 [ Axiom 4 ] [ SNF++, 82220, _t21 ] % 1.45/1.66 (1,1) [8454,2]. true => _t20 | ~_t19 | p2 [ Axiom 4 ] % 1.45/1.66 (1,1) [82176,2]. _t5 => box 1 _t114 [ SNF++, 628 ] % 1.45/1.66 (18,1) [82220,2]. _t20 => ~box 1~ _t131 [ SNF++, 8453 ] % 1.45/1.66 (3,1) [82225,2]. true => ~_t127 | _t4 [ SNF++, 1873 ] % 1.45/1.66 (1,1) [82243,2]. true => ~_t120 | _t19 [ SNF++, 8455 ] % 1.45/1.66 (3,1) [82289,2]. true => _t20 | ~_t19 | ~_t4 [ LRES, 4, 8454, ~p2 ] % 1.45/1.66 (3,1) [84786,2]. true => ~_t127 | _t5 [ LRES, 1872, 82225, ~_t4 ] % 1.45/1.66 (3,1) [89162,2]. true => ~_t127 | _t20 | ~_t19 [ LRES, 82289, 82225, ~_t4 ] % 1.45/1.66 (3,1) [89483,2]. true => ~_t127 | ~_t120 | _t20 [ LRES, 89162, 82243, ~_t19 ] [ Backward Subsumption, 111552 ] % 1.45/1.66 (18,1) [109387,2]. true => ~_t20 | ~_t5 [ GEN1, 82176, 82220, 109076, _t114, _t131 ] % 1.45/1.66 (18,1) [109700,2]. true => ~_t127 | ~_t20 [ LRES, 109387, 84786, ~_t5 ] % 1.45/1.66 (18,1) [111552,2]. true => ~_t127 | ~_t120 [ LRES, 109700, 89483, ~_t20 ] % 1.45/1.66 (1,1) [5,3]. _t7 => box 1 p2 [ SNF ] [ SNF++, 67936, p2 ] % 1.45/1.66 (1,1) [627,3]. true => _t7 | ~_t6 | ~p2 [ SNF ] % 1.45/1.66 (18,1) [8450,3]. true => ~_t21 | p2 [ Axiom 4 ] % 1.45/1.66 (17,1) [8451,3]. _t22 => ~box 1~ ~p2 [ Axiom 4 ] [ SNF++, 67974, ~p2 ] % 1.45/1.66 (18,1) [8452,3]. true => _t22 | ~_t21 [ Axiom 4 ] % 1.45/1.66 (1,1) [67936,3]. _t7 => box 1 _t112 [ SNF++, 5 ] % 1.45/1.66 (17,1) [67974,3]. _t22 => ~box 1~ _t130 [ SNF++, 8451 ] % 1.45/1.66 (1,1) [82177,3]. true => ~_t114 | _t6 [ SNF++, 628 ] % 1.45/1.66 (18,1) [82221,3]. true => ~_t131 | _t21 [ SNF++, 8453 ] % 1.45/1.66 (18,1) [87283,3]. true => ~_t131 | _t22 [ LRES, 8452, 82221, ~_t21 ] % 1.55/1.73 (17,1) [88843,3]. true => ~_t22 | ~_t7 [ GEN1, 67936, 67974, 82298, _t112, _t130 ] % 1.55/1.73 (18,1) [91048,3]. true => ~_t21 | _t7 | ~_t6 [ LRES, 627, 8450, ~p2 ] % 1.55/1.73 (18,1) [96656,3]. true => ~_t114 | ~_t21 | _t7 [ LRES, 91048, 82177, ~_t6 ] % 1.55/1.73 (18,1) [100102,3]. true => ~_t114 | ~_t22 | ~_t21 [ LRES, 96656, 88843, _t7 ] % 1.55/1.73 (18,1) [101339,3]. true => ~_t131 | ~_t114 | ~_t22 [ LRES, 100102, 82221, ~_t21 ] [ Backward Subsumption, 109076 ] % 1.55/1.73 (18,1) [109076,3]. true => ~_t131 | ~_t114 [ LRES, 101339, 87283, ~_t22 ] % 1.55/1.73 (1,1) [67937,4]. true => ~_t112 | p2 [ SNF++, 5 ] % 1.55/1.73 (17,1) [67975,4]. true => ~_t130 | ~p2 [ SNF++, 8451 ] % 1.55/1.73 (17,1) [82298,4]. true => ~_t130 | ~_t112 [ LRES, 67975, 67937, ~p2 ] % 1.55/1.73 % SZS output end Refutation % 1.55/1.73 % KSP exiting %------------------------------------------------------------------------------