%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP538-1 : TPTP v8.2.0. Released v2.6.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n020.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 06:39:53 EDT 2024 % Result : Unsatisfiable 2.23s 2.30s % Output : CNFRefutation 2.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP538-1 : TPTP v8.2.0. Released v2.6.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.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 : Thu Jun 20 08:53:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 2.23/2.29 %------------------------------------------- % 2.23/2.29 % File :CSE---1.7 % 2.23/2.29 % Problem :theBenchmark % 2.23/2.29 % Transform :cnf % 2.23/2.29 % Format :tptp:raw % 2.23/2.29 % Command :java -jar mcs_scs.jar %d %s % 2.23/2.29 % 2.23/2.29 % Result :Theorem 1.690000s % 2.23/2.29 % Output :CNFRefutation 1.690000s % 2.23/2.29 %------------------------------------------- % 2.23/2.29 %-------------------------------------------------------------------------- % 2.23/2.29 % File : GRP538-1 : TPTP v8.2.0. Released v2.6.0. % 2.23/2.29 % Domain : Group Theory (Abelian) % 2.23/2.29 % Problem : Axiom for Abelian group theory, in division, part 2 % 2.23/2.29 % Version : [McC93] (equality) axioms. % 2.23/2.29 % English : % 2.23/2.29 % 2.23/2.29 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 2.23/2.29 % Source : [TPTP] % 2.23/2.29 % Names : % 2.23/2.29 % 2.23/2.29 % Status : Unsatisfiable % 2.23/2.29 % Rating : 0.00 v7.4.0, 0.09 v7.3.0, 0.00 v6.0.0, 0.05 v5.5.0, 0.00 v2.6.0 % 2.23/2.29 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 2.23/2.29 % Number of literals : 5 ( 5 equ; 1 neg) % 2.23/2.29 % Maximal clause size : 1 ( 1 avg) % 2.23/2.29 % Maximal term depth : 4 ( 2 avg) % 2.23/2.29 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 2.23/2.29 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 2.23/2.29 % Number of variables : 9 ( 0 sgn) % 2.23/2.29 % SPC : CNF_UNS_RFO_PEQ_UEQ % 2.23/2.29 % 2.23/2.29 % Comments : A UEQ part of GRP092-1 % 2.23/2.29 %-------------------------------------------------------------------------- % 2.23/2.29 cnf(single_axiom,axiom, % 2.23/2.29 divide(divide(A,B),divide(divide(A,C),B)) = C ). % 2.23/2.29 % 2.23/2.29 cnf(multiply,axiom, % 2.23/2.29 multiply(A,B) = divide(A,divide(divide(C,C),B)) ). % 2.23/2.29 % 2.23/2.29 cnf(inverse,axiom, % 2.23/2.29 inverse(A) = divide(divide(B,B),A) ). % 2.23/2.29 % 2.23/2.29 cnf(identity,axiom, % 2.23/2.29 identity = divide(A,A) ). % 2.23/2.30 % 2.23/2.30 cnf(prove_these_axioms_2,negated_conjecture, % 2.23/2.30 multiply(multiply(inverse(b2),b2),a2) != a2 ). % 2.23/2.30 % 2.23/2.30 %-------------------------------------------------------------------------- % 2.23/2.30 %------------------------------------------- % 2.23/2.30 % Proof found % 2.23/2.30 % SZS status Theorem for theBenchmark % 2.23/2.30 % SZS output start Proof % 2.23/2.30 %ClaNum:13(EqnAxiom:8) % 2.23/2.30 %VarNum:18(SingletonVarNum:9) % 2.23/2.30 %MaxLitNum:1 % 2.23/2.30 %MaxfuncDepth:3 % 2.23/2.30 %SharedTerms:7 % 2.23/2.30 %goalClause: 13 % 2.23/2.30 %singleGoalClaCount:1 % 2.23/2.30 [13]~E(f6(f6(f5(a2),a2),a3),a3) % 2.23/2.30 [9]E(f1(x91,x91),a4) % 2.23/2.30 [10]E(f1(f1(x101,x101),x102),f5(x102)) % 2.23/2.30 [11]E(f1(x111,f1(f1(x112,x112),x113)),f6(x111,x113)) % 2.23/2.30 [12]E(f1(f1(x121,x122),f1(f1(x121,x123),x122)),x123) % 2.23/2.30 %EqnAxiom % 2.23/2.30 [1]E(x11,x11) % 2.23/2.30 [2]E(x22,x21)+~E(x21,x22) % 2.23/2.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.23/2.30 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 2.23/2.30 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 2.23/2.30 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 2.23/2.30 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 2.23/2.30 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 2.23/2.30 % 2.23/2.30 %------------------------------------------- % 2.23/2.30 cnf(14,plain, % 2.23/2.30 (E(a4,f1(x141,x141))), % 2.23/2.30 inference(scs_inference,[],[9,2])). % 2.23/2.30 cnf(15,plain, % 2.23/2.30 (E(f5(x151),f1(f1(x152,x152),x151))), % 2.23/2.30 inference(scs_inference,[],[10,2])). % 2.23/2.30 cnf(16,plain, % 2.23/2.30 (E(f1(f1(x161,x162),f1(f1(x161,a4),x162)),f1(x163,x163))), % 2.23/2.30 inference(scs_inference,[],[14,10,12,2,3])). % 2.23/2.30 cnf(18,plain, % 2.23/2.30 (E(f1(x181,x181),f1(f1(x182,x183),f1(f1(x182,a4),x183)))), % 2.23/2.30 inference(scs_inference,[],[16,2])). % 2.23/2.30 cnf(19,plain, % 2.23/2.30 (E(f1(f1(x191,x191),x192),f1(f1(x193,x193),x192))), % 2.23/2.30 inference(scs_inference,[],[15,16,10,2,3])). % 2.23/2.30 cnf(21,plain, % 2.23/2.30 (E(f6(x211,x212),f1(x211,f1(f1(x213,x213),x212)))), % 2.23/2.30 inference(scs_inference,[],[11,2])). % 2.23/2.30 cnf(22,plain, % 2.23/2.30 (E(f5(f1(x221,x221)),f1(f1(x222,x223),f1(f1(x222,a4),x223)))), % 2.23/2.30 inference(scs_inference,[],[18,15,11,2,3])). % 2.23/2.30 cnf(25,plain, % 2.23/2.30 (E(f1(f1(x251,x252),f1(f1(x251,a4),x252)),f5(f1(x253,x253)))), % 2.23/2.30 inference(scs_inference,[],[22,2])). % 2.23/2.30 cnf(27,plain, % 2.23/2.30 (E(x271,f1(f1(x272,x273),f1(f1(x272,x271),x273)))), % 2.23/2.30 inference(scs_inference,[],[12,2])). % 2.23/2.30 cnf(28,plain, % 2.23/2.30 (E(f6(f1(a4,x281),x281),f5(f1(x282,x282)))), % 2.23/2.30 inference(scs_inference,[],[21,25,12,2,3])). % 2.23/2.30 cnf(31,plain, % 2.23/2.30 (E(f5(f1(x311,x311)),f6(f1(a4,x312),x312))), % 2.23/2.30 inference(scs_inference,[],[28,2])). % 2.23/2.30 cnf(32,plain, % 2.23/2.30 (E(a4,f5(f1(x321,x321)))), % 2.23/2.30 inference(scs_inference,[],[27,25,28,2,3])). % 2.23/2.30 cnf(35,plain, % 2.23/2.30 (E(f5(f1(x351,x351)),a4)), % 2.23/2.30 inference(scs_inference,[],[32,2])). % 2.23/2.30 cnf(36,plain, % 2.23/2.30 (E(f1(f1(x361,x362),f1(f1(x361,a4),x362)),f6(f1(a4,x363),x363))), % 2.23/2.30 inference(scs_inference,[],[31,25,32,2,3])). % 2.23/2.30 cnf(38,plain, % 2.23/2.30 (E(f6(f1(a4,x381),x381),f1(f1(x382,x383),f1(f1(x382,a4),x383)))), % 2.23/2.30 inference(scs_inference,[],[36,2])). % 2.23/2.30 cnf(39,plain, % 2.23/2.30 (E(f5(f1(x391,x391)),f1(f1(a4,x392),f1(f1(x393,x393),x392)))), % 2.23/2.30 inference(scs_inference,[],[21,31,36,2,3])). % 2.23/2.30 cnf(41,plain, % 2.23/2.30 (E(f1(f1(a4,x411),f1(f1(x412,x412),x411)),f5(f1(x413,x413)))), % 2.23/2.30 inference(scs_inference,[],[39,2])). % 2.23/2.30 cnf(42,plain, % 2.23/2.30 (E(f1(f1(x421,x422),f1(f1(x421,a4),x422)),f1(f1(x423,x423),f1(x424,x424)))), % 2.23/2.30 inference(scs_inference,[],[15,25,39,2,3])). % 2.23/2.30 cnf(44,plain, % 2.23/2.30 (E(f1(f1(x441,x441),f1(x442,x442)),f1(f1(x443,x444),f1(f1(x443,a4),x444)))), % 2.23/2.30 inference(scs_inference,[],[42,2])). % 2.23/2.30 cnf(45,plain, % 2.23/2.30 (E(f1(f1(a4,x451),f1(f1(x452,x452),x451)),a4)), % 2.23/2.30 inference(scs_inference,[],[41,35,42,2,3])). % 2.23/2.30 cnf(47,plain, % 2.23/2.30 (E(a4,f1(f1(a4,x471),f1(f1(x472,x472),x471)))), % 2.23/2.30 inference(scs_inference,[],[45,2])). % 2.23/2.30 cnf(48,plain, % 2.23/2.30 (E(f6(f1(x481,x481),f1(x482,x482)),f1(f1(x483,x484),f1(f1(x483,a4),x484)))), % 2.23/2.30 inference(scs_inference,[],[44,21,45,2,3])). % 2.23/2.30 cnf(51,plain, % 2.23/2.30 (E(f1(f1(x511,x512),f1(f1(x511,a4),x512)),f6(f1(x513,x513),f1(x514,x514)))), % 2.23/2.30 inference(scs_inference,[],[48,2])). % 2.23/2.30 cnf(52,plain, % 2.23/2.30 (E(f1(f1(a4,x521),f1(f1(x522,x522),x521)),f6(f1(a4,x523),x523))), % 2.23/2.30 inference(scs_inference,[],[41,31,48,2,3])). % 2.23/2.30 cnf(54,plain, % 2.23/2.30 (E(f6(f1(a4,x541),x541),f1(f1(a4,x542),f1(f1(x543,x543),x542)))), % 2.23/2.30 inference(scs_inference,[],[52,2])). % 2.23/2.30 cnf(55,plain, % 2.23/2.30 (E(f6(f1(a4,x551),x551),f6(f1(x552,x552),f1(x553,x553)))), % 2.23/2.31 inference(scs_inference,[],[51,38,52,2,3])). % 2.23/2.31 cnf(57,plain, % 2.23/2.31 (E(f6(f1(x571,x571),f1(x572,x572)),f6(f1(a4,x573),x573))), % 2.23/2.31 inference(scs_inference,[],[55,2])). % 2.23/2.31 cnf(58,plain, % 2.23/2.31 (E(f5(f1(x581,x581)),f1(x582,x582))), % 2.23/2.31 inference(scs_inference,[],[35,14,55,2,3])). % 2.23/2.31 cnf(59,plain, % 2.23/2.31 (E(f1(x591,x591),f5(f1(x592,x592)))), % 2.23/2.31 inference(scs_inference,[],[58,2])). % 2.23/2.31 cnf(60,plain, % 2.23/2.31 (E(f6(f1(x601,x601),f1(x602,x602)),f1(f1(a4,x603),f1(f1(x604,x604),x603)))), % 2.23/2.31 inference(scs_inference,[],[57,54,58,2,3])). % 2.23/2.31 cnf(62,plain, % 2.23/2.31 (E(f1(f1(a4,x621),f1(f1(x622,x622),x621)),f6(f1(x623,x623),f1(x624,x624)))), % 2.23/2.31 inference(scs_inference,[],[60,2])). % 2.23/2.31 cnf(68,plain, % 2.23/2.31 (E(f6(f1(x681,x681),f1(x682,x682)),a4)), % 2.23/2.31 inference(scs_inference,[],[62,47,3,2])). % 2.23/2.31 cnf(69,plain, % 2.23/2.31 (E(f6(f1(f1(x691,x691),x692),x692),f5(f1(x693,x693)))), % 2.23/2.31 inference(scs_inference,[],[59,21,3])). % 2.23/2.31 cnf(72,plain, % 2.23/2.31 (E(f5(f1(x721,x721)),f6(f1(f1(x722,x722),x723),x723))), % 2.23/2.31 inference(scs_inference,[],[59,21,3,2])). % 2.23/2.31 cnf(73,plain, % 2.23/2.31 (E(f1(x731,x731),f6(f1(f1(x732,x732),x733),x733))), % 2.23/2.31 inference(scs_inference,[],[72,59,3])). % 2.23/2.31 cnf(75,plain, % 2.23/2.31 (E(f6(f1(f1(x751,x751),x752),x752),f1(x753,x753))), % 2.23/2.31 inference(scs_inference,[],[72,59,3,2])). % 2.23/2.31 cnf(77,plain, % 2.23/2.31 (E(f1(x771,x771),f6(f1(x772,x772),f1(x773,x773)))), % 2.23/2.31 inference(scs_inference,[],[68,14,3,2])). % 2.23/2.31 cnf(80,plain, % 2.23/2.31 (E(f6(f1(x801,x801),f1(x802,x802)),f6(f1(f1(x803,x803),x804),x804))), % 2.23/2.31 inference(scs_inference,[],[75,77,3,2])). % 2.23/2.31 cnf(83,plain, % 2.23/2.31 (E(f1(f1(x831,x831),f1(x832,x832)),f1(f1(a4,x833),f1(f1(x834,x834),x833)))), % 2.23/2.31 inference(scs_inference,[],[41,15,3,2])). % 2.23/2.31 cnf(87,plain, % 2.23/2.31 (E(f6(f1(x871,x871),f1(x872,x872)),f1(f1(x873,x873),f1(x874,x874)))), % 2.23/2.31 inference(scs_inference,[],[83,51,3,2])). % 2.23/2.31 cnf(96,plain, % 2.23/2.31 (E(f5(f1(x961,x961)),f6(f1(x962,x962),f1(x963,x963)))), % 2.23/2.31 inference(scs_inference,[],[80,69,3,2])). % 2.23/2.31 cnf(99,plain, % 2.23/2.31 (E(f1(f1(x991,x991),f1(x992,x992)),f5(f1(x993,x993)))), % 2.23/2.31 inference(scs_inference,[],[96,87,3,2])). % 2.23/2.31 cnf(105,plain, % 2.23/2.31 (E(a4,f1(f1(x1051,x1051),f1(x1052,x1052)))), % 2.23/2.31 inference(scs_inference,[],[99,35,3,2])). % 2.23/2.31 cnf(138,plain, % 2.23/2.31 (E(f1(f1(x1381,x1381),f1(x1382,x1382)),f1(x1383,x1383))), % 2.23/2.31 inference(scs_inference,[],[59,15,3,2])). % 2.23/2.31 cnf(147,plain, % 2.23/2.31 (E(f6(f1(f1(x1471,x1471),x1472),x1472),a4)), % 2.23/2.31 inference(scs_inference,[],[14,73,3,2])). % 2.23/2.31 cnf(257,plain, % 2.23/2.31 (E(f1(f1(x2571,x2571),f1(f1(x2572,a4),x2572)),f1(x2573,x2573))), % 2.23/2.31 inference(scs_inference,[],[19,16,3])). % 2.23/2.31 cnf(261,plain, % 2.23/2.31 (E(f1(f1(x2611,x2611),f1(f1(x2612,a4),x2612)),f6(f1(a4,x2613),x2613))), % 2.23/2.31 inference(scs_inference,[],[19,257,36,2,3])). % 2.23/2.31 cnf(265,plain, % 2.23/2.31 (E(f1(f1(x2651,x2651),f1(f1(x2652,x2652),x2653)),f6(f1(x2654,x2654),x2653))), % 2.23/2.31 inference(scs_inference,[],[19,261,11,2,3])). % 2.23/2.31 cnf(306,plain, % 2.23/2.31 (E(f6(f1(x3061,x3061),x3062),x3062)), % 2.23/2.31 inference(scs_inference,[],[27,265,3,2])). % 2.23/2.31 cnf(309,plain, % 2.23/2.31 (~E(f6(f5(a2),a2),f1(x3091,x3091))), % 2.23/2.31 inference(scs_inference,[],[306,13,3,6])). % 2.23/2.31 cnf(310,plain, % 2.23/2.31 (~E(f6(f5(a2),a2),f1(f1(x3101,x3101),f1(x3102,x3102)))), % 2.23/2.31 inference(scs_inference,[],[138,309,3])). % 2.23/2.31 cnf(321,plain, % 2.23/2.31 (~E(f6(f5(a2),a2),a4)), % 2.23/2.31 inference(scs_inference,[],[105,310,3])). % 2.23/2.31 cnf(339,plain, % 2.23/2.31 ($false), % 2.23/2.31 inference(scs_inference,[],[147,15,321,3,6]), % 2.23/2.31 ['proof']). % 2.23/2.31 % SZS output end Proof % 2.23/2.31 % Total time :1.690000s %------------------------------------------------------------------------------