%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP493-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 : n022.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:47 EDT 2024 % Result : Unsatisfiable 58.67s 58.70s % Output : CNFRefutation 58.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP493-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.32 % Computer : n022.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Thu Jun 20 13:23:09 EDT 2024 % 0.12/0.32 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 58.66/58.67 %------------------------------------------- % 58.66/58.67 % File :CSE---1.7 % 58.66/58.67 % Problem :theBenchmark % 58.66/58.68 % Transform :cnf % 58.66/58.68 % Format :tptp:raw % 58.66/58.68 % Command :java -jar mcs_scs.jar %d %s % 58.66/58.68 % 58.66/58.68 % Result :Theorem 58.070000s % 58.66/58.68 % Output :CNFRefutation 58.070000s % 58.66/58.68 %------------------------------------------- % 58.67/58.70 %-------------------------------------------------------------------------- % 58.67/58.70 % File : GRP493-1 : TPTP v8.2.0. Released v2.6.0. % 58.67/58.70 % Domain : Group Theory % 58.67/58.70 % Problem : Axiom for group theory, in double division and identity, part 1 % 58.67/58.70 % Version : [McC93] (equality) axioms. % 58.67/58.70 % English : % 58.67/58.70 % 58.67/58.70 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 58.67/58.70 % Source : [TPTP] % 58.67/58.70 % Names : % 58.67/58.70 % 58.67/58.70 % Status : Unsatisfiable % 58.67/58.70 % Rating : 0.00 v7.4.0, 0.04 v7.3.0, 0.00 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.00 v2.6.0 % 58.67/58.70 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR) % 58.67/58.70 % Number of literals : 5 ( 5 equ; 1 neg) % 58.67/58.70 % Maximal clause size : 1 ( 1 avg) % 58.67/58.70 % Maximal term depth : 5 ( 2 avg) % 58.67/58.70 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 58.67/58.70 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 58.67/58.70 % Number of variables : 7 ( 0 sgn) % 58.67/58.70 % SPC : CNF_UNS_RFO_PEQ_UEQ % 58.67/58.70 % 58.67/58.70 % Comments : A UEQ part of GRP079-1 % 58.67/58.70 %-------------------------------------------------------------------------- % 58.67/58.70 cnf(single_axiom,axiom, % 58.67/58.70 double_divide(double_divide(identity,A),double_divide(double_divide(double_divide(B,C),double_divide(identity,identity)),double_divide(A,C))) = B ). % 58.67/58.70 % 58.67/58.70 cnf(multiply,axiom, % 58.67/58.70 multiply(A,B) = double_divide(double_divide(B,A),identity) ). % 58.67/58.70 % 58.67/58.70 cnf(inverse,axiom, % 58.67/58.70 inverse(A) = double_divide(A,identity) ). % 58.67/58.70 % 58.67/58.70 cnf(identity,axiom, % 58.67/58.70 identity = double_divide(A,inverse(A)) ). % 58.67/58.70 % 58.67/58.70 cnf(prove_these_axioms_1,negated_conjecture, % 58.67/58.70 multiply(inverse(a1),a1) != identity ). % 58.67/58.70 % 58.67/58.70 %-------------------------------------------------------------------------- % 58.67/58.70 %------------------------------------------- % 58.67/58.70 % Proof found % 58.67/58.70 % SZS status Theorem for theBenchmark % 58.67/58.70 % SZS output start Proof % 58.71/58.72 %ClaNum:8(EqnAxiom:5) % 58.71/58.72 %VarNum:8(SingletonVarNum:4) % 58.71/58.72 %MaxLitNum:1 % 58.71/58.72 %MaxfuncDepth:3 % 58.71/58.72 %SharedTerms:7 % 58.71/58.72 %goalClause: 8 % 58.71/58.72 %singleGoalClaCount:1 % 58.71/58.72 [8]~E(f2(f2(a3,f2(a3,a1)),a1),a1) % 58.71/58.72 [6]E(f2(x61,f2(x61,a1)),a1) % 58.71/58.72 [7]E(f2(f2(a1,x71),f2(f2(f2(x72,x73),f2(a1,a1)),f2(x71,x73))),x72) % 58.71/58.72 %EqnAxiom % 58.71/58.72 [1]E(x11,x11) % 58.71/58.72 [2]E(x22,x21)+~E(x21,x22) % 58.71/58.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.71/58.72 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 58.71/58.72 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 58.71/58.72 % 58.71/58.72 %------------------------------------------- % 58.72/58.74 cnf(9,plain, % 58.72/58.74 (E(a1,f2(x91,f2(x91,a1)))), % 58.72/58.74 inference(scs_inference,[],[6,2])). % 58.72/58.74 cnf(10,plain, % 58.72/58.74 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x101,f2(x101,a1)))), % 58.72/58.74 inference(scs_inference,[],[8,6,2,3])). % 58.72/58.74 cnf(11,plain, % 58.72/58.74 (E(x111,f2(f2(a1,x112),f2(f2(f2(x111,x113),f2(a1,a1)),f2(x112,x113))))), % 58.72/58.74 inference(scs_inference,[],[7,2])). % 58.72/58.74 cnf(14,plain, % 58.72/58.74 (E(f2(f2(a1,x141),f2(f2(f2(a1,x142),f2(a1,a1)),f2(x141,x142))),f2(x143,f2(x143,a1)))), % 58.72/58.74 inference(scs_inference,[],[6,11,3,2])). % 58.72/58.74 cnf(15,plain, % 58.72/58.74 (~E(a1,f2(f2(a3,f2(a3,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[10,5])). % 58.72/58.74 cnf(16,plain, % 58.72/58.74 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(x161,f2(x161,a1)))), % 58.72/58.74 inference(rename_variables,[],[10])). % 58.72/58.74 cnf(17,plain, % 58.72/58.74 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(a1,x171),f2(f2(f2(a1,x172),f2(a1,a1)),f2(x171,x172))))), % 58.72/58.74 inference(scs_inference,[],[14,10,16,5,3])). % 58.72/58.74 cnf(19,plain, % 58.72/58.74 (E(f2(f2(x191,f2(x191,a1)),x192),f2(a1,x192))), % 58.72/58.74 inference(scs_inference,[],[6,4])). % 58.72/58.74 cnf(20,plain, % 58.72/58.74 (E(f2(x201,f2(x202,f2(x202,a1))),f2(x201,a1))), % 58.72/58.74 inference(scs_inference,[],[6,4,5])). % 58.72/58.74 cnf(22,plain, % 58.72/58.74 (~E(f2(x221,f2(x221,a1)),f2(f2(a3,f2(a3,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[6,9,15,17,4,5,2,3])). % 58.72/58.74 cnf(23,plain, % 58.72/58.74 (E(f2(f2(f2(x231,f2(x231,a1)),x232),x233),f2(f2(a1,x232),x233))), % 58.72/58.74 inference(scs_inference,[],[19,4])). % 58.72/58.74 cnf(27,plain, % 58.72/58.74 (~E(f2(f2(a3,f2(a3,a1)),a1),f2(f2(x271,f2(x271,a1)),f2(a1,a1)))), % 58.72/58.74 inference(scs_inference,[],[19,22,4,5,3,2])). % 58.72/58.74 cnf(29,plain, % 58.72/58.74 (E(f2(x291,f2(x292,f2(x293,f2(x293,a1)))),f2(x291,f2(x292,a1)))), % 58.72/58.74 inference(scs_inference,[],[20,4,5])). % 58.72/58.74 cnf(30,plain, % 58.72/58.74 (~E(f2(a1,a1),f2(f2(x301,f2(x301,a1)),f2(a1,a1)))), % 58.72/58.74 inference(scs_inference,[],[20,27,19,4,5,3])). % 58.72/58.74 cnf(32,plain, % 58.72/58.74 (~E(f2(f2(x321,f2(x321,a1)),f2(a1,a1)),f2(a1,a1))), % 58.72/58.74 inference(scs_inference,[],[20,27,19,4,5,3,2])). % 58.72/58.74 cnf(33,plain, % 58.72/58.74 (E(f2(a1,x331),f2(f2(x332,f2(x332,a1)),x331))), % 58.72/58.74 inference(scs_inference,[],[9,4])). % 58.72/58.74 cnf(34,plain, % 58.72/58.74 (E(f2(x341,a1),f2(x341,f2(x342,f2(x342,a1))))), % 58.72/58.74 inference(scs_inference,[],[9,4,5])). % 58.72/58.74 cnf(39,plain, % 58.72/58.74 (E(f2(f2(a1,x391),x392),f2(f2(f2(x393,f2(x393,a1)),x391),x392))), % 58.72/58.74 inference(scs_inference,[],[33,4])). % 58.72/58.74 cnf(40,plain, % 58.72/58.74 (E(f2(x401,f2(a1,x402)),f2(x401,f2(f2(x403,f2(x403,a1)),x402)))), % 58.72/58.74 inference(scs_inference,[],[33,4,5])). % 58.72/58.74 cnf(41,plain, % 58.72/58.74 (~E(f2(f2(x411,f2(x411,a1)),a1),f2(f2(x412,f2(x412,a1)),f2(a1,a1)))), % 58.72/58.74 inference(scs_inference,[],[30,33,4,5,3])). % 58.72/58.74 cnf(43,plain, % 58.72/58.74 (~E(f2(f2(x431,f2(x431,a1)),f2(a1,a1)),f2(f2(x432,f2(x432,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[30,33,4,5,3,2])). % 58.72/58.74 cnf(46,plain, % 58.72/58.74 (~E(f2(f2(x461,f2(x461,a1)),f2(x462,f2(x462,a1))),f2(f2(x463,f2(x463,a1)),f2(a1,a1)))), % 58.72/58.74 inference(scs_inference,[],[34,41,4,5,3])). % 58.72/58.74 cnf(51,plain, % 58.72/58.74 (~E(f2(f2(f2(x511,f2(x511,a1)),f2(a1,a1)),f2(a1,a1)),f2(f2(x512,f2(x512,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[43,39,7,4,5,3])). % 58.72/58.74 cnf(55,plain, % 58.72/58.74 (~E(f2(f2(x551,f2(x551,a1)),f2(f2(x552,f2(x552,a1)),a1)),f2(a1,a1))), % 58.72/58.74 inference(scs_inference,[],[51,40,32,2,3])). % 58.72/58.74 cnf(58,plain, % 58.72/58.74 (~E(a1,f2(a1,a1))), % 58.72/58.74 inference(scs_inference,[],[6,55,2,3])). % 58.72/58.74 cnf(61,plain, % 58.72/58.74 (~E(f2(a1,a1),a1)), % 58.72/58.74 inference(scs_inference,[],[58,2])). % 58.72/58.74 cnf(62,plain, % 58.72/58.74 (~E(f2(f2(a1,x621),f2(f2(f2(a1,x622),f2(a1,a1)),f2(x621,x622))),f2(a1,a1))), % 58.72/58.74 inference(scs_inference,[],[58,11,2,3])). % 58.72/58.74 cnf(64,plain, % 58.72/58.74 (~E(f2(a1,a1),f2(f2(a1,x641),f2(f2(f2(a1,x642),f2(a1,a1)),f2(x641,x642))))), % 58.72/58.74 inference(scs_inference,[],[62,2])). % 58.72/58.74 cnf(65,plain, % 58.72/58.74 (~E(f2(f2(a1,x651),f2(f2(f2(a1,f2(x651,a1)),f2(a1,a1)),a1)),f2(a1,a1))), % 58.72/58.74 inference(scs_inference,[],[62,29,2,3])). % 58.72/58.74 cnf(69,plain, % 58.72/58.74 (~E(f2(f2(a1,x691),f2(f2(f2(f2(a1,a1),x692),f2(a1,a1)),f2(x691,x692))),a1)), % 58.72/58.74 inference(scs_inference,[],[61,65,11,2,3])). % 58.72/58.74 cnf(71,plain, % 58.72/58.74 (~E(a1,f2(f2(a1,x711),f2(f2(f2(f2(a1,a1),x712),f2(a1,a1)),f2(x711,x712))))), % 58.72/58.74 inference(scs_inference,[],[69,2])). % 58.72/58.74 cnf(72,plain, % 58.72/58.74 (~E(f2(f2(a1,x721),f2(f2(f2(f2(a1,a1),f2(x721,a1)),f2(a1,a1)),a1)),a1)), % 58.72/58.74 inference(scs_inference,[],[69,29,2,3])). % 58.72/58.74 cnf(75,plain, % 58.72/58.74 (~E(a1,f2(f2(a1,x751),f2(f2(f2(f2(a1,a1),f2(x751,a1)),f2(a1,a1)),a1)))), % 58.72/58.74 inference(scs_inference,[],[72,2])). % 58.72/58.74 cnf(76,plain, % 58.72/58.74 (~E(f2(f2(x761,f2(x761,a1)),a1),f2(f2(a1,x762),f2(f2(f2(a1,x763),f2(a1,a1)),f2(x762,x763))))), % 58.72/58.74 inference(scs_inference,[],[64,72,33,2,3])). % 58.72/58.74 cnf(78,plain, % 58.72/58.74 (~E(f2(f2(a1,x781),f2(f2(f2(a1,x782),f2(a1,a1)),f2(x781,x782))),f2(f2(x783,f2(x783,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[76,2])). % 58.72/58.74 cnf(79,plain, % 58.72/58.74 (~E(f2(f2(f2(x791,f2(x791,a1)),f2(a1,a1)),f2(x792,f2(x792,a1))),f2(f2(x793,f2(x793,a1)),f2(a1,a1)))), % 58.72/58.74 inference(scs_inference,[],[46,76,39,2,3])). % 58.72/58.74 cnf(83,plain, % 58.72/58.74 (~E(f2(x831,f2(x831,a1)),f2(f2(a1,x832),f2(f2(f2(f2(a1,a1),x833),f2(a1,a1)),f2(x832,x833))))), % 58.72/58.74 inference(scs_inference,[],[71,79,9,2,3])). % 58.72/58.74 cnf(84,plain, % 58.72/58.74 (~E(f2(f2(a1,x841),f2(f2(f2(f2(a1,a1),x842),f2(a1,a1)),f2(x841,x842))),f2(x843,f2(x843,a1)))), % 58.72/58.74 inference(scs_inference,[],[83,2])). % 58.72/58.74 cnf(85,plain, % 58.72/58.74 (~E(a1,f2(f2(x851,f2(x851,a1)),a1))), % 58.72/58.74 inference(scs_inference,[],[7,83,78,2,3])). % 58.72/58.74 cnf(88,plain, % 58.72/58.74 (~E(f2(a1,a1),f2(x881,f2(x881,a1)))), % 58.72/58.74 inference(scs_inference,[],[7,85,84,2,3])). % 58.72/58.74 cnf(92,plain, % 58.72/58.74 ($false), % 58.72/58.74 inference(scs_inference,[],[9,88,75,23,2,3]), % 58.72/58.74 ['proof']). % 58.72/58.74 % SZS output end Proof % 58.72/58.74 % Total time :58.070000s %------------------------------------------------------------------------------