%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP682-10 : TPTP v8.2.0. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n001.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:40:27 EDT 2024 % Result : Unsatisfiable 121.72s 125.38s % Output : CNFRefutation 121.72s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP682-10 : TPTP v8.2.0. Released v8.1.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n001.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 08:47:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.55 start to proof:theBenchmark % 121.65/125.35 %------------------------------------------- % 121.65/125.35 % File :CSE---1.7 % 121.65/125.35 % Problem :theBenchmark % 121.65/125.35 % Transform :cnf % 121.65/125.35 % Format :tptp:raw % 121.65/125.35 % Command :java -jar mcs_scs.jar %d %s % 121.65/125.35 % 121.65/125.35 % Result :Theorem 121.130000s % 121.65/125.35 % Output :CNFRefutation 121.130000s % 121.65/125.35 %------------------------------------------- % 121.72/125.38 %------------------------------------------------------------------------------ % 121.72/125.38 % File : GRP682-10 : TPTP v8.2.0. Released v8.1.0. % 121.72/125.38 % Domain : Group Theory (Quasigroups) % 121.72/125.38 % Problem : Axioms of rectangular loops - a % 121.72/125.38 % Version : Especial. % 121.72/125.38 % English : % 121.72/125.38 % 121.72/125.38 % Refs : [KP05] Kinyon & Phillips (2005), Rectangular Quasigroups and % 121.72/125.38 % : [PS08] Phillips & Stanovsky (2008), Automated Theorem Proving % 121.72/125.38 % : [Sma21] Smallbone (2021), Email to Geoff Sutcliffe % 121.72/125.38 % Source : [Sma21] % 121.72/125.38 % Names : % 121.72/125.38 % 121.72/125.38 % Status : Unsatisfiable % 121.72/125.38 % Rating : 0.14 v8.2.0, 0.21 v8.1.0 % 121.72/125.38 % Syntax : Number of clauses : 8 ( 8 unt; 0 nHn; 1 RR) % 121.72/125.38 % Number of literals : 8 ( 8 equ; 1 neg) % 121.72/125.38 % Maximal clause size : 1 ( 1 avg) % 121.72/125.38 % Maximal term depth : 4 ( 2 avg) % 121.72/125.38 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 121.72/125.38 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty) % 121.72/125.38 % Number of variables : 16 ( 0 sgn) % 121.72/125.38 % SPC : CNF_UNS_RFO_PEQ_UEQ % 121.72/125.38 % 121.72/125.38 % Comments : UEQ version, converted from GRP682+1.p % 121.72/125.38 %------------------------------------------------------------------------------ % 121.72/125.38 cnf(f01,axiom, % 121.72/125.38 ld(A,mult(A,A)) = A ). % 121.72/125.38 % 121.72/125.38 cnf(f02,axiom, % 121.72/125.38 rd(mult(A,A),A) = A ). % 121.72/125.38 % 121.72/125.38 cnf(f03,axiom, % 121.72/125.38 mult(A,ld(A,B)) = ld(A,mult(A,B)) ). % 121.72/125.38 % 121.72/125.38 cnf(f04,axiom, % 121.72/125.38 mult(rd(A,B),B) = rd(mult(A,B),B) ). % 121.72/125.38 % 121.72/125.38 cnf(f05,axiom, % 121.72/125.38 ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D) ). % 121.72/125.38 % 121.72/125.38 cnf(f06,axiom, % 121.72/125.38 rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)) ). % 121.72/125.38 % 121.72/125.38 cnf(f07,axiom, % 121.72/125.38 ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B) ). % 121.72/125.38 % 121.72/125.38 cnf(goal,negated_conjecture, % 121.72/125.38 ld(ld(x0,x1),mult(ld(x0,x1),x2)) != ld(x0,mult(x0,x2)) ). % 121.72/125.38 % 121.72/125.38 %------------------------------------------------------------------------------ % 121.72/125.38 %------------------------------------------- % 121.72/125.38 % Proof found % 121.72/125.38 % SZS status Theorem for theBenchmark % 121.72/125.38 % SZS output start Proof % 121.72/125.41 %ClaNum:17(EqnAxiom:9) % 121.72/125.41 %VarNum:48(SingletonVarNum:16) % 121.72/125.41 %MaxLitNum:1 % 121.72/125.41 %MaxfuncDepth:3 % 121.72/125.41 %SharedTerms:9 % 121.72/125.41 %goalClause: 17 % 121.72/125.41 %singleGoalClaCount:1 % 121.72/125.41 [17]~E(f2(f2(a4,a5),f1(f2(a4,a5),a6)),f2(a4,f1(a4,a6))) % 121.72/125.41 [10]E(f2(x101,f1(x101,x101)),x101) % 121.72/125.41 [11]E(f3(f1(x111,x111),x111),x111) % 121.72/125.41 [12]E(f1(x121,f2(x121,x122)),f2(x121,f1(x121,x122))) % 121.72/125.41 [13]E(f3(f1(x131,x132),x132),f1(f3(x131,x132),x132)) % 121.72/125.41 [14]E(f3(f1(f3(x141,x141),x142),x142),f2(x141,f1(x141,f2(x142,x142)))) % 121.72/125.41 [15]E(f2(f2(x151,x152),f1(f2(x151,x152),f1(x153,x154))),f1(f2(x151,f1(x151,x153)),x154)) % 121.72/125.41 [16]E(f3(f1(f1(x161,x162),f3(x163,x164)),f3(x163,x164)),f1(x161,f3(f1(x162,x164),x164))) % 121.72/125.41 %EqnAxiom % 121.72/125.41 [1]E(x11,x11) % 121.72/125.41 [2]E(x22,x21)+~E(x21,x22) % 121.72/125.41 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 121.72/125.41 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 121.72/125.41 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 121.72/125.41 [6]~E(x61,x62)+E(f2(x61,x63),f2(x62,x63)) % 121.72/125.41 [7]~E(x71,x72)+E(f2(x73,x71),f2(x73,x72)) % 121.72/125.41 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 121.72/125.41 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 121.72/125.41 % 121.72/125.41 %------------------------------------------- % 121.72/125.44 cnf(18,plain, % 121.72/125.44 (E(x181,f2(x181,f1(x181,x181)))), % 121.72/125.44 inference(scs_inference,[],[10,2])). % 121.72/125.44 cnf(19,plain, % 121.72/125.44 (~E(f2(f2(a4,a5),f1(f2(a4,a5),a6)),f1(a4,f2(a4,a6)))), % 121.72/125.44 inference(scs_inference,[],[17,10,12,2,3])). % 121.72/125.44 cnf(21,plain, % 121.72/125.44 (E(x211,f3(f1(x211,x211),x211))), % 121.72/125.44 inference(scs_inference,[],[11,2])). % 121.72/125.44 cnf(22,plain, % 121.72/125.44 (E(f3(f1(x221,x221),x221),f2(x221,f1(x221,x221)))), % 121.72/125.44 inference(scs_inference,[],[18,11,2,3])). % 121.72/125.44 cnf(24,plain, % 121.72/125.44 (E(f2(x241,f1(x241,x241)),f3(f1(x241,x241),x241))), % 121.72/125.44 inference(scs_inference,[],[22,2])). % 121.72/125.44 cnf(25,plain, % 121.72/125.44 (E(x251,f3(f1(f2(x251,f1(x251,x251)),f2(x251,f1(x251,x251))),f2(x251,f1(x251,x251))))), % 121.72/125.44 inference(scs_inference,[],[21,18,22,2,3])). % 121.72/125.44 cnf(28,plain, % 121.72/125.44 (E(f2(x281,f1(x281,x281)),f1(f3(x281,x281),x281))), % 121.72/125.44 inference(scs_inference,[],[24,25,13,2,3])). % 121.72/125.44 cnf(34,plain, % 121.72/125.44 (E(f1(f2(x341,f1(x341,x342)),x343),f2(f2(x341,x344),f1(f2(x341,x344),f1(x342,x343))))), % 121.72/125.44 inference(scs_inference,[],[15,2])). % 121.72/125.44 cnf(35,plain, % 121.72/125.44 (E(f1(x351,f3(f1(x352,x353),x353)),f3(f1(f1(x351,x352),f3(x354,x353)),f3(x354,x353)))), % 121.72/125.44 inference(scs_inference,[],[16,2])). % 121.72/125.44 cnf(56,plain, % 121.72/125.44 (E(f3(f1(x561,x561),x561),f1(x561,f2(x561,x561)))), % 121.72/125.44 inference(scs_inference,[],[12,24,3,2])). % 121.72/125.44 cnf(64,plain, % 121.72/125.44 (E(f2(f2(x641,x642),f1(f2(x641,x642),f1(x643,x644))),f2(f2(x641,x645),f1(f2(x641,x645),f1(x643,x644))))), % 121.72/125.44 inference(scs_inference,[],[15,34,3])). % 121.72/125.44 cnf(84,plain, % 121.72/125.44 (E(x841,f1(f3(x841,x841),x841))), % 121.72/125.44 inference(scs_inference,[],[18,28,3])). % 121.72/125.44 cnf(90,plain, % 121.72/125.44 (E(x901,f1(x901,f2(x901,x901)))), % 121.72/125.44 inference(scs_inference,[],[21,56,3])). % 121.72/125.44 cnf(240,plain, % 121.72/125.44 (E(f3(x2401,f3(f1(x2402,x2402),x2402)),f3(x2401,x2402))), % 121.72/125.44 inference(scs_inference,[],[11,5,6,9])). % 121.72/125.44 cnf(262,plain, % 121.72/125.44 (E(f3(f1(x2621,x2621),f3(f1(x2621,x2621),x2621)),x2621)), % 121.72/125.44 inference(scs_inference,[],[11,240,5,6,9,7,8,4,3])). % 121.72/125.44 cnf(282,plain, % 121.72/125.44 (E(f3(x2821,f3(f1(x2822,x2822),f3(f1(x2822,x2822),x2822))),f3(x2821,x2822))), % 121.72/125.44 inference(scs_inference,[],[262,9])). % 121.72/125.44 cnf(284,plain, % 121.72/125.44 (E(f2(f3(f1(x2841,x2841),f3(f1(x2841,x2841),x2841)),x2842),f2(x2841,x2842))), % 121.72/125.44 inference(scs_inference,[],[262,9,5,6])). % 121.72/125.44 cnf(303,plain, % 121.72/125.44 (E(f3(x3031,f3(x3032,f3(f1(x3033,x3033),f3(f1(x3033,x3033),x3033)))),f3(x3031,f3(x3032,x3033)))), % 121.72/125.44 inference(scs_inference,[],[282,9])). % 121.72/125.44 cnf(317,plain, % 121.72/125.44 (E(f2(f2(f3(f1(x3171,x3171),f3(f1(x3171,x3171),x3171)),x3172),x3173),f2(f2(x3171,x3172),x3173))), % 121.72/125.44 inference(scs_inference,[],[284,6])). % 121.72/125.44 cnf(318,plain, % 121.72/125.44 (E(f1(x3181,f2(f3(f1(x3182,x3182),f3(f1(x3182,x3182),x3182)),x3183)),f1(x3181,f2(x3182,x3183)))), % 121.72/125.44 inference(scs_inference,[],[284,6,5])). % 121.72/125.44 cnf(697,plain, % 121.72/125.44 (E(f2(x6971,x6972),f2(x6971,f1(x6972,f2(x6972,x6972))))), % 121.72/125.44 inference(scs_inference,[],[90,6,9,7])). % 121.72/125.44 cnf(698,plain, % 121.72/125.44 (E(f1(x6981,x6982),f1(x6981,f1(x6982,f2(x6982,x6982))))), % 121.72/125.44 inference(scs_inference,[],[90,6,9,7,5])). % 121.72/125.44 cnf(719,plain, % 121.72/125.44 (E(f2(x7191,x7192),f2(f2(x7191,f1(x7191,x7191)),x7192))), % 121.72/125.44 inference(scs_inference,[],[18,6])). % 121.72/125.44 cnf(723,plain, % 121.72/125.44 (E(f1(x7231,x7232),f1(f2(x7231,f1(x7231,x7231)),x7232))), % 121.72/125.44 inference(scs_inference,[],[18,6,9,7,5,4])). % 121.72/125.44 cnf(780,plain, % 121.72/125.44 (E(f2(x7801,f1(x7802,x7803)),f2(x7801,f1(x7802,f1(x7803,f2(x7803,x7803)))))), % 121.72/125.44 inference(scs_inference,[],[698,6,7])). % 121.72/125.44 cnf(875,plain, % 121.72/125.44 (~E(f2(f2(a4,a5),f1(f2(a4,a5),f1(a6,f2(a6,a6)))),f1(a4,f2(a4,a6)))), % 121.72/125.44 inference(scs_inference,[],[19,780,35,9,7,8,4,5,6,3])). % 121.72/125.44 cnf(895,plain, % 121.72/125.44 (~E(f1(a4,f2(a4,a6)),f2(f2(a4,x8951),f1(f2(a4,x8951),f1(a6,f2(a6,a6)))))), % 121.72/125.44 inference(scs_inference,[],[64,875,84,6,9,8,7,5,4,3,2])). % 121.72/125.44 cnf(1203,plain, % 121.72/125.44 (~E(f1(a4,f2(a4,a6)),f1(f2(a4,x12031),f2(f2(a4,x12031),f1(a6,f2(a6,a6)))))), % 121.72/125.44 inference(scs_inference,[],[12,895,303,2,3])). % 121.72/125.44 cnf(1225,plain, % 121.72/125.44 (~E(f2(a4,a6),f2(f2(a4,f1(a4,a4)),f1(a6,f2(a6,a6))))), % 121.72/125.44 inference(scs_inference,[],[723,1203,317,2,3,5])). % 121.72/125.44 cnf(1227,plain, % 121.72/125.44 ($false), % 121.72/125.44 inference(scs_inference,[],[719,697,1225,318,2,3]), % 121.72/125.44 ['proof']). % 121.72/125.44 % SZS output end Proof % 121.72/125.44 % Total time :121.130000s %------------------------------------------------------------------------------