%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN072-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n027.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 : Mon Jun 24 19:04:28 EDT 2024 % Result : Unsatisfiable 0.73s 0.79s % Output : CNFRefutation 0.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN072-1 : TPTP v8.2.0. Released v1.0.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 22:55:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.57 start to proof:theBenchmark % 0.73/0.79 %------------------------------------------- % 0.73/0.79 % File :CSE---1.7 % 0.73/0.79 % Problem :theBenchmark % 0.73/0.79 % Transform :cnf % 0.73/0.79 % Format :tptp:raw % 0.73/0.79 % Command :java -jar mcs_scs.jar %d %s % 0.73/0.79 % 0.73/0.79 % Result :Theorem 0.190000s % 0.73/0.79 % Output :CNFRefutation 0.190000s % 0.73/0.79 %------------------------------------------- % 0.73/0.79 %-------------------------------------------------------------------------- % 0.73/0.79 % File : SYN072-1 : TPTP v8.2.0. Released v1.0.0. % 0.73/0.79 % Domain : Syntactic % 0.73/0.79 % Problem : Pelletier Problem 49 % 0.73/0.79 % Version : Especial. % 0.73/0.79 % English : % 0.73/0.79 % 0.73/0.79 % Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 0.73/0.79 % Source : [Pel86] % 0.73/0.79 % Names : Pelletier 49 [Pel86] % 0.73/0.79 % 0.73/0.79 % Status : Unsatisfiable % 0.73/0.79 % Rating : 0.00 v6.1.0, 0.12 v6.0.0, 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v2.6.0, 0.11 v2.5.0, 0.00 v2.4.0, 0.00 v2.2.0, 0.33 v2.1.0, 0.00 v2.0.0 % 0.73/0.79 % Syntax : Number of clauses : 5 ( 4 unt; 1 nHn; 4 RR) % 0.73/0.79 % Number of literals : 6 ( 3 equ; 2 neg) % 0.73/0.79 % Maximal clause size : 2 ( 1 avg) % 0.73/0.79 % Maximal term depth : 1 ( 1 avg) % 0.73/0.79 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.73/0.79 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 0.73/0.79 % Number of variables : 1 ( 0 sgn) % 0.73/0.79 % SPC : CNF_UNS_EPR_SEQ_NHN % 0.73/0.79 % 0.73/0.79 % Comments : % 0.73/0.79 %-------------------------------------------------------------------------- % 0.73/0.79 cnf(clause_1,axiom, % 0.73/0.79 ( X = c % 0.73/0.79 | X = d ) ). % 0.73/0.79 % 0.73/0.79 cnf(clause_2,axiom, % 0.73/0.79 big_p(a) ). % 0.73/0.79 % 0.73/0.79 cnf(clause_3,axiom, % 0.73/0.79 big_p(b) ). % 0.73/0.79 % 0.73/0.79 cnf(clause_4,axiom, % 0.73/0.79 a != b ). % 0.73/0.79 % 0.73/0.79 cnf(prove_this,negated_conjecture, % 0.73/0.79 ~ big_p(e) ). % 0.73/0.79 % 0.73/0.79 %-------------------------------------------------------------------------- % 0.73/0.79 %------------------------------------------- % 0.73/0.79 % Proof found % 0.73/0.79 % SZS status Theorem for theBenchmark % 0.73/0.79 % SZS output start Proof % 0.73/0.79 %ClaNum:9(EqnAxiom:4) % 0.73/0.79 %VarNum:2(SingletonVarNum:1) % 0.73/0.79 %MaxLitNum:2 % 0.73/0.79 %MaxfuncDepth:0 % 0.73/0.79 %SharedTerms:9 % 0.73/0.79 %goalClause: 8 % 0.73/0.79 %singleGoalClaCount:1 % 0.73/0.79 [5]P1(a1) % 0.73/0.79 [6]P1(a2) % 0.73/0.79 [7]~E(a1,a2) % 0.73/0.79 [8]~P1(a3) % 0.73/0.79 [9]E(x91,a5)+E(x91,a4) % 0.73/0.79 %EqnAxiom % 0.73/0.79 [1]E(x11,x11) % 0.73/0.80 [2]E(x22,x21)+~E(x21,x22) % 0.73/0.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.73/0.80 [4]~P1(x41)+P1(x42)+~E(x41,x42) % 0.73/0.80 % 0.73/0.80 %------------------------------------------- % 0.73/0.80 cnf(10,plain, % 0.73/0.80 (E(a5,x101)+E(x101,a4)), % 0.73/0.80 inference(scs_inference,[],[2,9])). % 0.73/0.80 cnf(11,plain, % 0.73/0.80 (E(a4,x111)+E(a5,x111)), % 0.73/0.80 inference(scs_inference,[],[10,2])). % 0.73/0.80 cnf(12,plain, % 0.73/0.80 (E(x121,a5)+E(a4,x121)), % 0.73/0.80 inference(scs_inference,[],[11,2])). % 0.73/0.80 cnf(13,plain, % 0.73/0.80 (~E(a1,a4)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[7,12,3])). % 0.73/0.80 cnf(14,plain, % 0.73/0.80 (E(a1,a5)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[13,9])). % 0.73/0.80 cnf(18,plain, % 0.73/0.80 (~E(a3,a1)), % 0.73/0.80 inference(scs_inference,[],[5,8,4,2])). % 0.73/0.80 cnf(19,plain, % 0.73/0.80 (~E(x191,a3)+~E(x191,a1)), % 0.73/0.80 inference(scs_inference,[],[18,2,3])). % 0.73/0.80 cnf(20,plain, % 0.73/0.80 (E(a1,a4)+~E(a5,a3)), % 0.73/0.80 inference(scs_inference,[],[19,10])). % 0.73/0.80 cnf(21,plain, % 0.73/0.80 (~E(a5,a3)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[20,13])). % 0.73/0.80 cnf(22,plain, % 0.73/0.80 (E(a4,a3)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[21,11])). % 0.73/0.80 cnf(27,plain, % 0.73/0.80 (E(a5,a2)+E(a1,a5)), % 0.73/0.80 inference(scs_inference,[],[2,14])). % 0.73/0.80 cnf(28,plain, % 0.73/0.80 (E(a5,a1)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[27,2])). % 0.73/0.80 cnf(29,plain, % 0.73/0.80 (~E(a5,a3)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[28,19])). % 0.73/0.80 cnf(30,plain, % 0.73/0.80 (E(a3,a4)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[29,10])). % 0.73/0.80 cnf(31,plain, % 0.73/0.80 (E(a4,a3)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[30,2])). % 0.73/0.80 cnf(32,plain, % 0.73/0.80 (~E(a4,a1)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[31,19])). % 0.73/0.80 cnf(33,plain, % 0.73/0.80 (~E(a1,a4)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[32,2])). % 0.73/0.80 cnf(34,plain, % 0.73/0.80 (~E(x341,a4)+~E(a1,x341)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[33,3])). % 0.73/0.80 cnf(35,plain, % 0.73/0.80 (~E(a5,a4)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[34,27])). % 0.73/0.80 cnf(36,plain, % 0.73/0.80 (~E(a4,a5)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[35,2])). % 0.73/0.80 cnf(37,plain, % 0.73/0.80 (~E(x371,a5)+~E(a4,x371)+E(a5,a2)), % 0.73/0.80 inference(scs_inference,[],[36,3])). % 0.73/0.80 cnf(38,plain, % 0.73/0.80 (~E(a3,a5)+E(a5,a2)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[37,22])). % 0.73/0.80 cnf(39,plain, % 0.73/0.80 (~E(a1,a5)+~E(a3,a5)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[7,38,3])). % 0.73/0.80 cnf(40,plain, % 0.73/0.80 (E(a1,a4)+~E(a3,a5)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[39,9])). % 0.73/0.80 cnf(41,plain, % 0.73/0.80 (~E(a4,a2)+~E(a3,a5)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[7,40,3])). % 0.73/0.80 cnf(42,plain, % 0.73/0.80 (E(a2,a5)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[41,12])). % 0.73/0.80 cnf(43,plain, % 0.73/0.80 (E(a5,a2)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[42,2])). % 0.73/0.80 cnf(44,plain, % 0.73/0.80 (~E(a1,a5)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[7,43,3])). % 0.73/0.80 cnf(45,plain, % 0.73/0.80 (E(a1,a4)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[44,9])). % 0.73/0.80 cnf(46,plain, % 0.73/0.80 (E(a4,a1)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[45,2])). % 0.73/0.80 cnf(47,plain, % 0.73/0.80 (~E(a4,a3)+~E(a3,a5)), % 0.73/0.80 inference(scs_inference,[],[46,19])). % 0.73/0.80 cnf(51,plain, % 0.73/0.80 (E(a4,a1)+~E(a5,a3)), % 0.73/0.80 inference(scs_inference,[],[2,20])). % 0.73/0.80 cnf(52,plain, % 0.73/0.80 (E(a4,a1)+E(a3,a4)), % 0.73/0.80 inference(scs_inference,[],[51,10])). % 0.73/0.80 cnf(55,plain, % 0.73/0.80 (~E(a3,a2)), % 0.73/0.80 inference(scs_inference,[],[6,8,2,4])). % 0.73/0.80 cnf(56,plain, % 0.73/0.80 (E(a3,a4)+E(a2,a5)), % 0.73/0.80 inference(scs_inference,[],[2,22])). % 0.73/0.80 cnf(57,plain, % 0.73/0.80 (E(a5,a2)+E(a2,a5)+~E(a1,a3)), % 0.73/0.80 inference(scs_inference,[],[56,34])). % 0.73/0.80 cnf(58,plain, % 0.73/0.80 (E(a2,a5)+~E(a1,a3)), % 0.73/0.80 inference(scs_inference,[],[57,2])). % 0.73/0.80 cnf(59,plain, % 0.73/0.80 (P1(a5)+~E(a1,a3)), % 0.73/0.80 inference(scs_inference,[],[6,58,4])). % 0.73/0.80 cnf(60,plain, % 0.73/0.80 (~E(x601,a3)+~E(a1,x601)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[59,3])). % 0.73/0.80 cnf(61,plain, % 0.73/0.80 (~E(a4,a3)+E(a1,a5)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[60,9])). % 0.73/0.80 cnf(62,plain, % 0.73/0.80 (~E(a5,a2)+~E(a4,a3)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[7,61,3])). % 0.73/0.80 cnf(63,plain, % 0.73/0.80 (E(a5,a3)+~E(a5,a2)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[62,11])). % 0.73/0.80 cnf(69,plain, % 0.73/0.80 (E(a2,a5)+~E(a5,a4)), % 0.73/0.80 inference(scs_inference,[],[2,35])). % 0.73/0.80 cnf(70,plain, % 0.73/0.80 (P1(a5)+~E(a5,a4)), % 0.73/0.80 inference(scs_inference,[],[6,69,4])). % 0.73/0.80 cnf(74,plain, % 0.73/0.80 (~E(x741,a4)+~E(a5,x741)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[70,3])). % 0.73/0.80 cnf(75,plain, % 0.73/0.80 (~E(a3,a4)+~E(a5,a2)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[74,63])). % 0.73/0.80 cnf(76,plain, % 0.73/0.80 (E(a3,a5)+~E(a5,a2)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[75,9])). % 0.73/0.80 cnf(84,plain, % 0.73/0.80 (~E(a4,x841)+~E(a5,x841)+P1(a5)), % 0.73/0.80 inference(scs_inference,[],[2,74])). % 0.73/0.81 cnf(85,plain, % 0.73/0.81 (~E(a5,a3)+~E(a5,x851)+~E(a4,x851)), % 0.73/0.81 inference(scs_inference,[],[8,84,4])). % 0.73/0.81 cnf(87,plain, % 0.73/0.81 (E(a2,a5)+~E(a4,a5)), % 0.73/0.81 inference(scs_inference,[],[2,36])). % 0.73/0.81 cnf(88,plain, % 0.73/0.81 (~E(x881,a5)+~E(a4,x881)+E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[87,3])). % 0.73/0.81 cnf(89,plain, % 0.73/0.81 (~E(x891,a4)+E(a2,a5)+~E(x891,a5)), % 0.73/0.81 inference(scs_inference,[],[88,2])). % 0.73/0.81 cnf(90,plain, % 0.73/0.81 (E(a5,a2)+~E(x901,a5)+~E(x901,a4)), % 0.73/0.81 inference(scs_inference,[],[89,2])). % 0.73/0.81 cnf(91,plain, % 0.73/0.81 (~E(a3,a5)+~E(x911,a4)+~E(x911,a5)), % 0.73/0.81 inference(scs_inference,[],[55,90,3])). % 0.73/0.81 cnf(93,plain, % 0.73/0.81 (~E(a5,a3)+~E(a3,a4)), % 0.73/0.81 inference(scs_inference,[],[2,91])). % 0.73/0.81 cnf(94,plain, % 0.73/0.81 (~E(x941,a3)+~E(a5,x941)+~E(a3,a4)), % 0.73/0.81 inference(scs_inference,[],[93,3])). % 0.73/0.81 cnf(95,plain, % 0.73/0.81 (~E(a5,x951)+~E(x951,a3)+E(a3,a5)), % 0.73/0.81 inference(scs_inference,[],[94,9])). % 0.73/0.81 cnf(96,plain, % 0.73/0.81 (~E(a5,a2)+~E(x961,a3)+~E(a5,x961)), % 0.73/0.81 inference(scs_inference,[],[55,95,3])). % 0.73/0.81 cnf(97,plain, % 0.73/0.81 (E(a2,a4)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[96,10])). % 0.73/0.81 cnf(98,plain, % 0.73/0.81 (E(a4,a2)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[97,2])). % 0.73/0.81 cnf(99,plain, % 0.73/0.81 (~E(a3,a4)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[55,98,3])). % 0.73/0.81 cnf(106,plain, % 0.73/0.81 (E(a1,a4)+E(a3,a4)), % 0.73/0.81 inference(scs_inference,[],[2,52])). % 0.73/0.81 cnf(107,plain, % 0.73/0.81 (E(a1,a4)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[106,99])). % 0.73/0.81 cnf(108,plain, % 0.73/0.81 (E(a4,a1)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[107,2])). % 0.73/0.81 cnf(109,plain, % 0.73/0.81 (~E(a4,a3)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[108,19])). % 0.73/0.81 cnf(110,plain, % 0.73/0.81 (E(a5,a3)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[109,11])). % 0.73/0.81 cnf(115,plain, % 0.73/0.81 (~E(a2,a5)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[2,96])). % 0.73/0.81 cnf(116,plain, % 0.73/0.81 (~E(x1161,a3)+~E(a2,x1161)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[115,3])). % 0.73/0.81 cnf(117,plain, % 0.73/0.81 (~E(a5,a3)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[116,21])). % 0.73/0.81 cnf(118,plain, % 0.73/0.81 (E(a3,a4)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[117,10])). % 0.73/0.81 cnf(119,plain, % 0.73/0.81 (E(a4,a3)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[118,2])). % 0.73/0.81 cnf(120,plain, % 0.73/0.81 (~E(a4,a1)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[119,19])). % 0.73/0.81 cnf(121,plain, % 0.73/0.81 (E(a5,a1)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[120,11])). % 0.73/0.81 cnf(122,plain, % 0.73/0.81 (E(a1,a5)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[121,2])). % 0.73/0.81 cnf(123,plain, % 0.73/0.81 (~E(a3,a5)+~E(a2,a5)), % 0.73/0.81 inference(scs_inference,[],[122,44])). % 0.73/0.81 cnf(124,plain, % 0.73/0.81 (~E(a5,a2)+~E(a2,a5)+P1(a5)), % 0.73/0.81 inference(scs_inference,[],[123,76])). % 0.73/0.81 cnf(125,plain, % 0.73/0.81 (~E(a1,a4)+~E(a2,a5)+P1(a5)), % 0.73/0.81 inference(scs_inference,[],[124,33])). % 0.73/0.81 cnf(126,plain, % 0.73/0.81 (~E(a1,a4)+P1(a5)), % 0.73/0.81 inference(scs_inference,[],[125,13])). % 0.73/0.81 cnf(135,plain, % 0.73/0.81 (~E(a5,a3)+~E(a1,a4)), % 0.73/0.81 inference(scs_inference,[],[8,126,4])). % 0.73/0.81 cnf(136,plain, % 0.73/0.81 (~E(a1,a4)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[135,110])). % 0.73/0.81 cnf(137,plain, % 0.73/0.81 (~E(a5,a3)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[136,20])). % 0.73/0.81 cnf(138,plain, % 0.73/0.81 (~E(a2,a3)+E(a4,a3)), % 0.73/0.81 inference(scs_inference,[],[137,11])). % 0.73/0.81 cnf(139,plain, % 0.73/0.81 (~E(a3,a5)+~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[138,47])). % 0.73/0.81 cnf(140,plain, % 0.73/0.81 (~E(a2,a3)+E(a3,a4)), % 0.73/0.81 inference(scs_inference,[],[139,9])). % 0.73/0.81 cnf(141,plain, % 0.73/0.81 (~E(a2,a3)), % 0.73/0.81 inference(scs_inference,[],[140,99])). % 0.73/0.81 cnf(142,plain, % 0.73/0.81 (E(a5,a1)+P1(a5)), % 0.73/0.81 inference(scs_inference,[],[126,10])). % 0.73/0.81 cnf(143,plain, % 0.73/0.81 (~E(a5,a3)+E(a5,a1)), % 0.73/0.81 inference(scs_inference,[],[8,142,4])). % 0.73/0.81 cnf(144,plain, % 0.73/0.81 (E(a5,a1)+E(a4,a3)), % 0.73/0.81 inference(scs_inference,[],[143,11])). % 0.73/0.81 cnf(145,plain, % 0.73/0.81 (E(a4,a3)+~E(a5,a3)), % 0.73/0.81 inference(scs_inference,[],[144,19])). % 0.73/0.81 cnf(146,plain, % 0.73/0.81 (~E(a3,a5)+E(a4,a3)), % 0.73/0.81 inference(scs_inference,[],[145,2])). % 0.73/0.81 cnf(147,plain, % 0.73/0.81 (~E(a3,a5)), % 0.73/0.81 inference(scs_inference,[],[146,47])). % 0.73/0.81 cnf(157,plain, % 0.73/0.81 (E(a4,a3)), % 0.73/0.81 inference(scs_inference,[],[147,2,9])). % 0.73/0.81 cnf(165,plain, % 0.73/0.81 (E(a5,a2)), % 0.73/0.81 inference(scs_inference,[],[8,157,141,2,4,85,3,9,10])). % 0.73/0.81 cnf(169,plain, % 0.73/0.81 (E(a1,a5)), % 0.73/0.81 inference(scs_inference,[],[8,157,141,2,4,85,3,9,10,120,121,122])). % 0.73/0.81 cnf(176,plain, % 0.73/0.81 ($false), % 0.73/0.81 inference(scs_inference,[],[7,165,169,3]), % 0.73/0.81 ['proof']). % 0.73/0.81 % SZS output end Proof % 0.73/0.81 % Total time :0.190000s %------------------------------------------------------------------------------