%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP123-6.003 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:38:47 EDT 2024 % Result : Unsatisfiable 58.58s 58.64s % Output : CNFRefutation 58.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP123-6.003 : TPTP v8.2.0. Released v1.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Jun 20 08:59:54 EDT 2024 % 0.13/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 58.58/58.62 %------------------------------------------- % 58.58/58.62 % File :CSE---1.7 % 58.58/58.62 % Problem :theBenchmark % 58.58/58.62 % Transform :cnf % 58.58/58.62 % Format :tptp:raw % 58.58/58.62 % Command :java -jar mcs_scs.jar %d %s % 58.58/58.62 % 58.58/58.62 % Result :Theorem 58.000000s % 58.58/58.62 % Output :CNFRefutation 58.000000s % 58.58/58.62 %------------------------------------------- % 58.58/58.64 %-------------------------------------------------------------------------- % 58.58/58.64 % File : GRP123-6.003 : TPTP v8.2.0. Released v1.2.0. % 58.58/58.64 % Domain : Group Theory (Quasigroups) % 58.58/58.64 % Problem : (3,2,1) conjugate orthogonality % 58.58/58.64 % Version : [Sla93] axioms. % 58.58/58.64 % Theorem formulation : Uses a second group. % 58.58/58.64 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*b=a iff ab=c % 58.58/58.64 % Generate the multiplication table for the specified quasi- % 58.58/58.64 % group with 3 elements. % 58.58/58.64 % 58.58/58.64 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 58.58/58.64 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 58.58/58.64 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 58.58/58.64 % Source : [Sla93] % 58.58/58.64 % Names : QG1a [Sla93] % 58.58/58.64 % 58.58/58.64 % Status : Unsatisfiable % 58.58/58.64 % Rating : 0.00 v2.1.0 % 58.58/58.64 % Syntax : Number of clauses : 20 ( 11 unt; 2 nHn; 18 RR) % 58.58/58.64 % Number of literals : 42 ( 0 equ; 24 neg) % 58.58/58.64 % Maximal clause size : 5 ( 2 avg) % 58.58/58.64 % Maximal term depth : 1 ( 1 avg) % 58.58/58.64 % Number of predicates : 4 ( 4 usr; 0 prp; 1-3 aty) % 58.58/58.64 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 58.58/58.64 % Number of variables : 34 ( 0 sgn) % 58.58/58.64 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.58/58.64 % 58.58/58.64 % Comments : [SFS93]'s axiomatization has been modified for this. % 58.58/58.64 % : Substitution axioms are not needed, as any positive equality % 58.58/58.64 % literals should resolve on negative ones directly. % 58.58/58.64 % : tptp2X: -f tptp -s3 GRP123-6.g % 58.58/58.64 %-------------------------------------------------------------------------- % 58.58/58.64 cnf(element_1,axiom, % 58.58/58.64 group_element(e_1) ). % 58.58/58.64 % 58.58/58.64 cnf(element_2,axiom, % 58.58/58.64 group_element(e_2) ). % 58.58/58.64 % 58.58/58.64 cnf(element_3,axiom, % 58.58/58.64 group_element(e_3) ). % 58.58/58.64 % 58.58/58.64 cnf(e_1_is_not_e_2,axiom, % 58.58/58.64 ~ equalish(e_1,e_2) ). % 58.58/58.64 % 58.58/58.64 cnf(e_1_is_not_e_3,axiom, % 58.58/58.64 ~ equalish(e_1,e_3) ). % 58.58/58.64 % 58.58/58.64 cnf(e_2_is_not_e_1,axiom, % 58.58/58.64 ~ equalish(e_2,e_1) ). % 58.58/58.64 % 58.58/58.64 cnf(e_2_is_not_e_3,axiom, % 58.58/58.64 ~ equalish(e_2,e_3) ). % 58.58/58.64 % 58.58/58.64 cnf(e_3_is_not_e_1,axiom, % 58.58/58.64 ~ equalish(e_3,e_1) ). % 58.58/58.64 % 58.58/58.64 cnf(e_3_is_not_e_2,axiom, % 58.58/58.64 ~ equalish(e_3,e_2) ). % 58.58/58.64 % 58.58/58.64 cnf(product1_total_function1,axiom, % 58.58/58.64 ( ~ group_element(X) % 58.58/58.64 | ~ group_element(Y) % 58.58/58.64 | product1(X,Y,e_1) % 58.58/58.64 | product1(X,Y,e_2) % 58.58/58.64 | product1(X,Y,e_3) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product1_total_function2,axiom, % 58.58/58.64 ( ~ product1(X,Y,W) % 58.58/58.64 | ~ product1(X,Y,Z) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product1_right_cancellation,axiom, % 58.58/58.64 ( ~ product1(X,W,Y) % 58.58/58.64 | ~ product1(X,Z,Y) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product1_left_cancellation,axiom, % 58.58/58.64 ( ~ product1(W,Y,X) % 58.58/58.64 | ~ product1(Z,Y,X) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product1_idempotence,axiom, % 58.58/58.64 product1(X,X,X) ). % 58.58/58.64 % 58.58/58.64 cnf(product2_total_function1,axiom, % 58.58/58.64 ( ~ group_element(X) % 58.58/58.64 | ~ group_element(Y) % 58.58/58.64 | product2(X,Y,e_1) % 58.58/58.64 | product2(X,Y,e_2) % 58.58/58.64 | product2(X,Y,e_3) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product2_total_function2,axiom, % 58.58/58.64 ( ~ product2(X,Y,W) % 58.58/58.64 | ~ product2(X,Y,Z) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product2_right_cancellation,axiom, % 58.58/58.64 ( ~ product2(X,W,Y) % 58.58/58.64 | ~ product2(X,Z,Y) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product2_left_cancellation,axiom, % 58.58/58.64 ( ~ product2(W,Y,X) % 58.58/58.64 | ~ product2(Z,Y,X) % 58.58/58.64 | equalish(W,Z) ) ). % 58.58/58.64 % 58.58/58.64 cnf(product2_idempotence,axiom, % 58.58/58.64 product2(X,X,X) ). % 58.58/58.64 % 58.58/58.64 cnf(qg1a,negated_conjecture, % 58.58/58.64 ( ~ product1(X,Y,Z1) % 58.58/58.64 | ~ product1(Z1,Y,Z2) % 58.58/58.64 | product2(Z2,X,Y) ) ). % 58.58/58.64 % 58.58/58.64 %-------------------------------------------------------------------------- % 58.58/58.64 %------------------------------------------- % 58.58/58.64 % Proof found % 58.58/58.64 % SZS status Theorem for theBenchmark % 58.58/58.64 % SZS output start Proof % 58.58/58.66 %ClaNum:20(EqnAxiom:0) % 58.58/58.66 %VarNum:79(SingletonVarNum:34) % 58.62/58.66 %MaxLitNum:5 % 58.62/58.66 %MaxfuncDepth:0 % 58.62/58.66 %SharedTerms:12 % 58.62/58.66 %goalClause: 20 % 58.62/58.66 [1]P1(a1) % 58.62/58.66 [2]P1(a2) % 58.62/58.66 [3]P1(a3) % 58.62/58.66 [6]~P2(a1,a2) % 58.62/58.66 [7]~P2(a1,a3) % 58.62/58.66 [8]~P2(a2,a1) % 58.62/58.66 [9]~P2(a2,a3) % 58.62/58.66 [10]~P2(a3,a1) % 58.62/58.66 [11]~P2(a3,a2) % 58.62/58.66 [4]P3(x41,x41,x41) % 58.62/58.66 [5]P4(x51,x51,x51) % 58.62/58.66 [14]~P3(x143,x144,x141)+P2(x141,x142)+~P3(x143,x144,x142) % 58.62/58.66 [15]~P4(x153,x154,x151)+P2(x151,x152)+~P4(x153,x154,x152) % 58.62/58.66 [16]~P3(x163,x161,x164)+P2(x161,x162)+~P3(x163,x162,x164) % 58.62/58.66 [17]~P4(x173,x171,x174)+P2(x171,x172)+~P4(x173,x172,x174) % 58.62/58.66 [18]~P3(x181,x183,x184)+P2(x181,x182)+~P3(x182,x183,x184) % 58.62/58.66 [19]~P4(x191,x193,x194)+P2(x191,x192)+~P4(x192,x193,x194) % 58.62/58.66 [20]~P3(x202,x203,x204)+P4(x201,x202,x203)+~P3(x204,x203,x201) % 58.62/58.66 [12]~P1(x122)+~P1(x121)+P3(x121,x122,a2)+P3(x121,x122,a3)+P3(x121,x122,a1) % 58.62/58.66 [13]~P1(x132)+~P1(x131)+P4(x131,x132,a2)+P4(x131,x132,a3)+P4(x131,x132,a1) % 58.62/58.66 %EqnAxiom % 58.62/58.66 % 58.62/58.66 %------------------------------------------- % 58.82/58.84 cnf(53,plain, % 58.82/58.84 (P4(a2,a1,a2)+P3(a1,a2,a3)+P3(a1,a2,a1)), % 58.82/58.84 inference(scs_inference,[],[4,2,1,20,12])). % 58.82/58.84 cnf(145,plain, % 58.82/58.84 (~P3(x1451,a2,a1)+~P3(a1,a2,x1451)), % 58.82/58.84 inference(scs_inference,[],[5,6,15,20])). % 58.82/58.84 cnf(176,plain, % 58.82/58.84 (P4(a2,a1,a2)+P3(a1,a2,a3)), % 58.82/58.84 inference(scs_inference,[],[145,53])). % 58.82/58.84 cnf(238,plain, % 58.82/58.85 (~P3(a3,a2,a1)+P4(a2,a1,a2)), % 58.82/58.85 inference(scs_inference,[],[145,176])). % 58.82/58.85 cnf(269,plain, % 58.82/58.85 (P3(a3,a2,a2)+P3(a3,a2,a3)+P4(a2,a1,a2)), % 58.82/58.85 inference(scs_inference,[],[2,3,238,12])). % 58.82/58.85 cnf(161685,plain, % 58.82/58.85 (P3(x1616851,x1616851,x1616851)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161688,plain, % 58.82/58.85 (P3(x1616881,x1616881,x1616881)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161691,plain, % 58.82/58.85 (P4(x1616911,x1616911,x1616911)), % 58.82/58.85 inference(rename_variables,[],[5])). % 58.82/58.85 cnf(161697,plain, % 58.82/58.85 (P4(x1616971,x1616971,x1616971)), % 58.82/58.85 inference(rename_variables,[],[5])). % 58.82/58.85 cnf(161699,plain, % 58.82/58.85 (~P4(a3,a1,a1)), % 58.82/58.85 inference(scs_inference,[],[7,4,161685,161688,5,161691,161697,18,16,17,14,15,19])). % 58.82/58.85 cnf(161702,plain, % 58.82/58.85 (P4(a3,a1,a2)), % 58.82/58.85 inference(scs_inference,[],[1,7,3,4,161685,161688,5,161691,161697,18,16,17,14,15,19,13])). % 58.82/58.85 cnf(161709,plain, % 58.82/58.85 (P3(x1617091,x1617091,x1617091)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161712,plain, % 58.82/58.85 (P3(x1617121,x1617121,x1617121)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161718,plain, % 58.82/58.85 (P3(x1617181,x1617181,x1617181)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161723,plain, % 58.82/58.85 (~P4(a3,a2,a2)), % 58.82/58.85 inference(scs_inference,[],[8,161699,161702,4,161709,161712,161718,5,20,14,15,16,18,17])). % 58.82/58.85 cnf(161730,plain, % 58.82/58.85 (P3(x1617301,x1617301,x1617301)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161733,plain, % 58.82/58.85 (P3(x1617331,x1617331,x1617331)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161736,plain, % 58.82/58.85 (P3(x1617361,x1617361,x1617361)), % 58.82/58.85 inference(rename_variables,[],[4])). % 58.82/58.85 cnf(161742,plain, % 58.82/58.85 (P4(x1617421,x1617421,x1617421)), % 58.82/58.85 inference(rename_variables,[],[5])). % 58.82/58.85 cnf(161747,plain, % 58.82/58.85 (~P4(a2,a1,a2)), % 58.82/58.85 inference(scs_inference,[],[9,11,161723,161702,4,161730,161733,161736,5,161742,20,16,18,14,15,17,19])). % 58.82/58.85 cnf(161749,plain, % 58.82/58.85 (P3(a3,a2,a2)), % 58.82/58.85 inference(scs_inference,[],[9,11,161723,161702,4,161730,161733,161736,5,161742,20,16,18,14,15,17,19,269])). % 58.82/58.85 cnf(161755,plain, % 58.82/58.85 (P3(a1,a2,a3)), % 58.82/58.85 inference(scs_inference,[],[161747,176])). % 58.82/58.85 cnf(161773,plain, % 58.82/58.85 ($false), % 58.82/58.85 inference(scs_inference,[],[161755,161749,161747,20]), % 58.82/58.85 ['proof']). % 58.94/58.97 % SZS output end Proof % 58.94/58.97 % Total time :58.000000s %------------------------------------------------------------------------------