%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP466-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 : 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 : Mon Jun 24 06:39:44 EDT 2024 % Result : Unsatisfiable 241.71s 241.82s % Output : CNFRefutation 241.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP466-1 : TPTP v8.2.0. Released v2.6.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n017.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 : Thu Jun 20 12:39:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 241.64/241.75 %------------------------------------------- % 241.64/241.75 % File :CSE---1.7 % 241.64/241.75 % Problem :theBenchmark % 241.64/241.75 % Transform :cnf % 241.64/241.75 % Format :tptp:raw % 241.64/241.75 % Command :java -jar mcs_scs.jar %d %s % 241.64/241.75 % 241.64/241.75 % Result :Theorem 241.020000s % 241.64/241.75 % Output :CNFRefutation 241.020000s % 241.64/241.75 %------------------------------------------- % 241.71/241.82 %-------------------------------------------------------------------------- % 241.71/241.82 % File : GRP466-1 : TPTP v8.2.0. Released v2.6.0. % 241.71/241.82 % Domain : Group Theory % 241.71/241.82 % Problem : Axiom for group theory, in division and inverse, part 1 % 241.71/241.82 % Version : [McC93] (equality) axioms. % 241.71/241.82 % English : % 241.71/241.82 % 241.71/241.82 % Refs : [McC93] McCune (1993), Single Axioms for Groups and Abelian Gr % 241.71/241.82 % Source : [TPTP] % 241.71/241.82 % Names : % 241.71/241.82 % 241.71/241.82 % Status : Unsatisfiable % 241.71/241.82 % Rating : 0.18 v8.2.0, 0.17 v8.1.0, 0.20 v7.5.0, 0.17 v7.3.0, 0.16 v7.1.0, 0.06 v7.0.0, 0.05 v6.4.0, 0.11 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 % 241.71/241.82 % Syntax : Number of clauses : 3 ( 3 unt; 0 nHn; 1 RR) % 241.71/241.82 % Number of literals : 3 ( 3 equ; 1 neg) % 241.71/241.82 % Maximal clause size : 1 ( 1 avg) % 241.71/241.82 % Maximal term depth : 6 ( 2 avg) % 241.71/241.82 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 241.71/241.82 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 241.71/241.82 % Number of variables : 6 ( 0 sgn) % 241.71/241.82 % SPC : CNF_UNS_RFO_PEQ_UEQ % 241.71/241.82 % 241.71/241.82 % Comments : A UEQ part of GRP070-1 % 241.71/241.82 %-------------------------------------------------------------------------- % 241.71/241.82 cnf(single_axiom,axiom, % 241.71/241.82 divide(divide(A,A),divide(B,divide(divide(C,divide(D,B)),inverse(D)))) = C ). % 241.71/241.82 % 241.71/241.82 cnf(multiply,axiom, % 241.71/241.82 multiply(A,B) = divide(A,inverse(B)) ). % 241.71/241.82 % 241.71/241.82 cnf(prove_these_axioms_1,negated_conjecture, % 241.71/241.82 multiply(inverse(a1),a1) != multiply(inverse(b1),b1) ). % 241.71/241.82 % 241.71/241.82 %-------------------------------------------------------------------------- % 241.71/241.82 %------------------------------------------- % 241.71/241.82 % Proof found % 241.71/241.82 % SZS status Theorem for theBenchmark % 241.71/241.82 % SZS output start Proof % 241.79/241.90 %ClaNum:8(EqnAxiom:6) % 241.79/241.90 %VarNum:8(SingletonVarNum:4) % 241.79/241.90 %MaxLitNum:1 % 241.79/241.90 %MaxfuncDepth:4 % 241.79/241.90 %SharedTerms:7 % 241.79/241.90 %goalClause: 8 % 241.79/241.90 %singleGoalClaCount:1 % 241.79/241.90 [8]~E(f1(f4(a2),f4(a2)),f1(f4(a3),f4(a3))) % 241.79/241.90 [7]E(f1(f1(x71,x71),f1(x72,f1(f1(x73,f1(x74,x72)),f4(x74)))),x73) % 241.79/241.90 %EqnAxiom % 241.79/241.90 [1]E(x11,x11) % 241.79/241.90 [2]E(x22,x21)+~E(x21,x22) % 241.79/241.90 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 241.79/241.90 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 241.79/241.90 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 241.79/241.90 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 241.79/241.90 % 241.79/241.90 %------------------------------------------- % 241.85/241.96 cnf(9,plain, % 241.85/241.96 (E(x91,f1(f1(x92,x92),f1(x93,f1(f1(x91,f1(x94,x93)),f4(x94)))))), % 241.85/241.96 inference(scs_inference,[],[7,2])). % 241.85/241.96 cnf(10,plain, % 241.85/241.96 (~E(f1(f4(a2),f4(a2)),f1(f1(x101,x101),f1(x102,f1(f1(f1(f4(a3),f4(a3)),f1(x103,x102)),f4(x103)))))), % 241.85/241.96 inference(scs_inference,[],[8,7,3])). % 241.85/241.96 cnf(21,plain, % 241.85/241.96 (E(f1(x211,x212),f1(f1(f1(x213,x213),f1(x214,f1(f1(x211,f1(x215,x214)),f4(x215)))),x212))), % 241.85/241.96 inference(scs_inference,[],[9,6,5,4])). % 241.85/241.96 cnf(35,plain, % 241.85/241.96 (E(f1(f1(x351,x351),f1(x352,f1(f1(x353,f1(x354,x352)),f4(x354)))),f1(f1(x355,x355),f1(x356,f1(f1(x353,f1(x357,x356)),f4(x357)))))), % 241.85/241.96 inference(scs_inference,[],[7,9,3])). % 241.85/241.96 cnf(44,plain, % 241.85/241.96 (~E(f1(f1(x441,x441),f1(x442,f1(f1(f1(f4(a2),f4(a2)),f1(x443,x442)),f4(x443)))),f1(f1(x444,x444),f1(x445,f1(f1(f1(f4(a3),f4(a3)),f1(x446,x445)),f4(x446)))))), % 241.85/241.96 inference(scs_inference,[],[9,21,10,5,6,4,2,3])). % 241.85/241.96 cnf(754,plain, % 241.85/241.96 (~E(f1(x7541,f1(f1(f1(f4(a2),f4(a2)),f1(x7542,x7541)),f4(x7542))),f1(x7543,f1(f1(f1(f4(a3),f4(a3)),f1(x7544,x7543)),f4(x7544))))), % 241.85/241.96 inference(scs_inference,[],[44,5])). % 241.85/241.96 cnf(763,plain, % 241.85/241.96 ($false), % 241.85/241.96 inference(scs_inference,[],[35,754,5,2,4]), % 241.85/241.96 ['proof']). % 241.85/241.96 % SZS output end Proof % 241.85/241.96 % Total time :241.020000s %------------------------------------------------------------------------------