%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP123-7.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 : n032.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.38s 58.51s % Output : CNFRefutation 58.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : GRP123-7.003 : TPTP v8.2.0. Released v1.2.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.28 % Computer : n032.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 300 % 0.10/0.28 % DateTime : Thu Jun 20 08:33:54 EDT 2024 % 0.10/0.28 % CPUTime : % 0.14/0.45 start to proof:theBenchmark % 58.38/58.49 %------------------------------------------- % 58.38/58.49 % File :CSE---1.7 % 58.38/58.49 % Problem :theBenchmark % 58.38/58.49 % Transform :cnf % 58.38/58.49 % Format :tptp:raw % 58.38/58.49 % Command :java -jar mcs_scs.jar %d %s % 58.38/58.49 % 58.38/58.49 % Result :Theorem 58.000000s % 58.38/58.49 % Output :CNFRefutation 58.000000s % 58.38/58.49 %------------------------------------------- % 58.38/58.51 %-------------------------------------------------------------------------- % 58.38/58.51 % File : GRP123-7.003 : TPTP v8.2.0. Released v1.2.0. % 58.38/58.51 % Domain : Group Theory (Quasigroups) % 58.38/58.51 % Problem : (3,2,1) conjugate orthogonality % 58.38/58.51 % Version : [Sla93] axioms : Augmented. % 58.38/58.51 % Theorem formulation : Uses a second group. % 58.38/58.51 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*b=a iff ab=c. % 58.38/58.51 % Generate the multiplication table for the specified quasi- % 58.38/58.51 % group with 3 elements. % 58.38/58.51 % 58.38/58.51 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 58.38/58.51 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 58.38/58.51 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 58.38/58.51 % Source : [TPTP] % 58.38/58.51 % Names : % 58.38/58.51 % 58.38/58.51 % Status : Unsatisfiable % 58.38/58.51 % Rating : 0.00 v2.1.0 % 58.38/58.51 % Syntax : Number of clauses : 26 ( 16 unt; 2 nHn; 24 RR) % 58.38/58.51 % Number of literals : 50 ( 0 equ; 27 neg) % 58.38/58.51 % Maximal clause size : 5 ( 1 avg) % 58.38/58.51 % Maximal term depth : 1 ( 1 avg) % 58.38/58.51 % Number of predicates : 7 ( 7 usr; 0 prp; 1-3 aty) % 58.38/58.51 % Number of functors : 3 ( 3 usr; 3 con; 0-0 aty) % 58.38/58.51 % Number of variables : 37 ( 0 sgn) % 58.38/58.51 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.38/58.51 % 58.38/58.51 % Comments : [SFS93]'s axiomatization has been modified for this. % 58.38/58.51 % : Substitution axioms are not needed, as any positive equality % 58.38/58.51 % literals should resolve on negative ones directly. % 58.38/58.51 % : Version 7 has simple isomorphism avoidance (as mentioned in % 58.38/58.51 % [FSB93]) % 58.38/58.51 % : tptp2X: -f tptp -s3 GRP123-7.g % 58.38/58.51 %-------------------------------------------------------------------------- % 58.38/58.51 cnf(e_1_then_e_2,axiom, % 58.38/58.51 next(e_1,e_2) ). % 58.38/58.51 % 58.38/58.51 cnf(e_2_then_e_3,axiom, % 58.38/58.51 next(e_2,e_3) ). % 58.38/58.51 % 58.38/58.51 cnf(e_2_greater_e_1,axiom, % 58.38/58.51 greater(e_2,e_1) ). % 58.38/58.51 % 58.38/58.51 cnf(e_3_greater_e_1,axiom, % 58.38/58.51 greater(e_3,e_1) ). % 58.38/58.51 % 58.38/58.51 cnf(e_3_greater_e_2,axiom, % 58.38/58.51 greater(e_3,e_2) ). % 58.38/58.51 % 58.38/58.51 cnf(no_redundancy,axiom, % 58.38/58.51 ( ~ product(X,e_1,Y) % 58.38/58.51 | ~ next(X,X1) % 58.38/58.51 | ~ greater(Y,X1) ) ). % 58.38/58.51 % 58.38/58.51 cnf(element_1,axiom, % 58.38/58.51 group_element(e_1) ). % 58.38/58.51 % 58.38/58.51 cnf(element_2,axiom, % 58.38/58.51 group_element(e_2) ). % 58.38/58.51 % 58.38/58.51 cnf(element_3,axiom, % 58.38/58.51 group_element(e_3) ). % 58.38/58.51 % 58.38/58.51 cnf(e_1_is_not_e_2,axiom, % 58.38/58.51 ~ equalish(e_1,e_2) ). % 58.38/58.51 % 58.38/58.51 cnf(e_1_is_not_e_3,axiom, % 58.38/58.51 ~ equalish(e_1,e_3) ). % 58.38/58.51 % 58.38/58.51 cnf(e_2_is_not_e_1,axiom, % 58.38/58.51 ~ equalish(e_2,e_1) ). % 58.38/58.51 % 58.38/58.51 cnf(e_2_is_not_e_3,axiom, % 58.38/58.51 ~ equalish(e_2,e_3) ). % 58.38/58.51 % 58.38/58.51 cnf(e_3_is_not_e_1,axiom, % 58.38/58.51 ~ equalish(e_3,e_1) ). % 58.38/58.51 % 58.38/58.51 cnf(e_3_is_not_e_2,axiom, % 58.38/58.51 ~ equalish(e_3,e_2) ). % 58.38/58.51 % 58.38/58.51 cnf(product1_total_function1,axiom, % 58.38/58.51 ( ~ group_element(X) % 58.38/58.51 | ~ group_element(Y) % 58.38/58.51 | product1(X,Y,e_1) % 58.38/58.51 | product1(X,Y,e_2) % 58.38/58.51 | product1(X,Y,e_3) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product1_total_function2,axiom, % 58.38/58.51 ( ~ product1(X,Y,W) % 58.38/58.51 | ~ product1(X,Y,Z) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product1_right_cancellation,axiom, % 58.38/58.51 ( ~ product1(X,W,Y) % 58.38/58.51 | ~ product1(X,Z,Y) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product1_left_cancellation,axiom, % 58.38/58.51 ( ~ product1(W,Y,X) % 58.38/58.51 | ~ product1(Z,Y,X) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product1_idempotence,axiom, % 58.38/58.51 product1(X,X,X) ). % 58.38/58.51 % 58.38/58.51 cnf(product2_total_function1,axiom, % 58.38/58.51 ( ~ group_element(X) % 58.38/58.51 | ~ group_element(Y) % 58.38/58.51 | product2(X,Y,e_1) % 58.38/58.51 | product2(X,Y,e_2) % 58.38/58.51 | product2(X,Y,e_3) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product2_total_function2,axiom, % 58.38/58.51 ( ~ product2(X,Y,W) % 58.38/58.51 | ~ product2(X,Y,Z) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product2_right_cancellation,axiom, % 58.38/58.51 ( ~ product2(X,W,Y) % 58.38/58.51 | ~ product2(X,Z,Y) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product2_left_cancellation,axiom, % 58.38/58.51 ( ~ product2(W,Y,X) % 58.38/58.51 | ~ product2(Z,Y,X) % 58.38/58.51 | equalish(W,Z) ) ). % 58.38/58.51 % 58.38/58.51 cnf(product2_idempotence,axiom, % 58.38/58.51 product2(X,X,X) ). % 58.38/58.51 % 58.38/58.51 cnf(qg1a,negated_conjecture, % 58.38/58.51 ( ~ product1(X,Y,Z1) % 58.38/58.51 | ~ product1(Z1,Y,Z2) % 58.38/58.51 | product2(Z2,X,Y) ) ). % 58.38/58.51 % 58.38/58.51 %-------------------------------------------------------------------------- % 58.38/58.51 %------------------------------------------- % 58.38/58.51 % Proof found % 58.38/58.51 % SZS status Theorem for theBenchmark % 58.38/58.51 % SZS output start Proof % 58.46/58.52 %ClaNum:26(EqnAxiom:0) % 58.46/58.52 %VarNum:85(SingletonVarNum:37) % 58.46/58.52 %MaxLitNum:5 % 58.46/58.52 %MaxfuncDepth:0 % 58.46/58.52 %SharedTerms:17 % 58.46/58.52 %goalClause: 26 % 58.46/58.52 [1]P1(a1) % 58.46/58.52 [2]P1(a2) % 58.46/58.52 [3]P1(a3) % 58.46/58.52 [4]P4(a1,a2) % 58.46/58.52 [5]P4(a2,a3) % 58.46/58.52 [6]P2(a2,a1) % 58.46/58.52 [7]P2(a3,a1) % 58.46/58.52 [8]P2(a3,a2) % 58.46/58.52 [11]~P3(a1,a2) % 58.46/58.52 [12]~P3(a1,a3) % 58.46/58.52 [13]~P3(a2,a1) % 58.46/58.52 [14]~P3(a2,a3) % 58.46/58.52 [15]~P3(a3,a1) % 58.46/58.52 [16]~P3(a3,a2) % 58.46/58.52 [9]P5(x91,x91,x91) % 58.46/58.52 [10]P7(x101,x101,x101) % 58.46/58.52 [17]~P4(x171,x172)+~P2(x173,x172)+~P6(x171,a1,x173) % 58.46/58.52 [20]~P5(x203,x204,x201)+P3(x201,x202)+~P5(x203,x204,x202) % 58.46/58.52 [21]~P7(x213,x214,x211)+P3(x211,x212)+~P7(x213,x214,x212) % 58.46/58.52 [22]~P5(x223,x221,x224)+P3(x221,x222)+~P5(x223,x222,x224) % 58.46/58.52 [23]~P7(x233,x231,x234)+P3(x231,x232)+~P7(x233,x232,x234) % 58.46/58.52 [24]~P5(x241,x243,x244)+P3(x241,x242)+~P5(x242,x243,x244) % 58.46/58.52 [25]~P7(x251,x253,x254)+P3(x251,x252)+~P7(x252,x253,x254) % 58.46/58.52 [26]~P5(x262,x263,x264)+P7(x261,x262,x263)+~P5(x264,x263,x261) % 58.46/58.52 [18]~P1(x182)+~P1(x181)+P5(x181,x182,a2)+P5(x181,x182,a3)+P5(x181,x182,a1) % 58.46/58.52 [19]~P1(x192)+~P1(x191)+P7(x191,x192,a2)+P7(x191,x192,a3)+P7(x191,x192,a1) % 58.46/58.52 %EqnAxiom % 58.46/58.52 % 58.46/58.52 %------------------------------------------- % 58.53/58.61 cnf(59,plain, % 58.53/58.61 (P7(a2,a1,a2)+P5(a1,a2,a3)+P5(a1,a2,a1)), % 58.53/58.61 inference(scs_inference,[],[9,2,1,26,18])). % 58.53/58.61 cnf(151,plain, % 58.53/58.61 (~P5(x1511,a2,a1)+~P5(a1,a2,x1511)), % 58.53/58.61 inference(scs_inference,[],[10,11,21,26])). % 58.53/58.61 cnf(182,plain, % 58.53/58.61 (P7(a2,a1,a2)+P5(a1,a2,a3)), % 58.53/58.61 inference(scs_inference,[],[151,59])). % 58.53/58.61 cnf(244,plain, % 58.53/58.61 (~P5(a3,a2,a1)+P7(a2,a1,a2)), % 58.53/58.61 inference(scs_inference,[],[151,182])). % 58.53/58.61 cnf(275,plain, % 58.53/58.61 (P5(a3,a2,a2)+P5(a3,a2,a3)+P7(a2,a1,a2)), % 58.53/58.61 inference(scs_inference,[],[2,3,244,18])). % 58.53/58.61 cnf(492,plain, % 58.53/58.62 (P5(a3,a2,a2)+P5(a3,a2,a3)+~P5(a1,a2,a3)), % 58.53/58.62 inference(scs_inference,[],[2,3,151,18])). % 58.53/58.62 cnf(523,plain, % 58.53/58.62 (P7(a2,a3,a2)+P5(a3,a2,a3)+~P5(a1,a2,a3)), % 58.53/58.62 inference(scs_inference,[],[9,492,26])). % 58.53/58.62 cnf(151248,plain, % 58.53/58.62 (P7(x1512481,x1512481,x1512481)), % 58.53/58.62 inference(rename_variables,[],[10])). % 58.53/58.62 cnf(151251,plain, % 58.53/58.62 (P5(x1512511,x1512511,x1512511)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151254,plain, % 58.53/58.62 (P5(x1512541,x1512541,x1512541)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151260,plain, % 58.53/58.62 (P7(x1512601,x1512601,x1512601)), % 58.53/58.62 inference(rename_variables,[],[10])). % 58.53/58.62 cnf(151265,plain, % 58.53/58.62 (P7(a3,a1,a2)), % 58.53/58.62 inference(scs_inference,[],[1,12,3,10,151248,151260,9,151251,151254,21,24,20,22,23,25,19])). % 58.53/58.62 cnf(151272,plain, % 58.53/58.62 (P5(x1512721,x1512721,x1512721)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151275,plain, % 58.53/58.62 (P5(x1512751,x1512751,x1512751)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151281,plain, % 58.53/58.62 (P7(x1512811,x1512811,x1512811)), % 58.53/58.62 inference(rename_variables,[],[10])). % 58.53/58.62 cnf(151283,plain, % 58.53/58.62 (~P7(a1,a2,a2)), % 58.53/58.62 inference(scs_inference,[],[13,10,151281,9,151272,151275,20,24,22,21,25])). % 58.53/58.62 cnf(151286,plain, % 58.53/58.62 (~P7(a3,a2,a2)), % 58.53/58.62 inference(scs_inference,[],[13,151265,10,151281,9,151272,151275,20,24,22,21,25,23])). % 58.53/58.62 cnf(151290,plain, % 58.53/58.62 (P5(x1512901,x1512901,x1512901)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151293,plain, % 58.53/58.62 (P5(x1512931,x1512931,x1512931)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151299,plain, % 58.53/58.62 (P7(x1512991,x1512991,x1512991)), % 58.53/58.62 inference(rename_variables,[],[10])). % 58.53/58.62 cnf(151306,plain, % 58.53/58.62 (P5(a3,a2,a2)), % 58.53/58.62 inference(scs_inference,[],[14,16,151265,10,151299,9,151290,151293,22,24,20,21,23,25,275])). % 58.53/58.62 cnf(151308,plain, % 58.53/58.62 (P7(a3,a2,a1)), % 58.53/58.62 inference(scs_inference,[],[14,16,151286,151265,3,2,10,151299,9,151290,151293,22,24,20,21,23,25,275,523,19])). % 58.53/58.62 cnf(151314,plain, % 58.53/58.62 (P5(x1513141,x1513141,x1513141)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151317,plain, % 58.53/58.62 (P5(x1513171,x1513171,x1513171)), % 58.53/58.62 inference(rename_variables,[],[9])). % 58.53/58.62 cnf(151324,plain, % 58.53/58.62 (P7(a1,a2,a3)), % 58.53/58.62 inference(scs_inference,[],[1,15,151283,151308,2,9,151314,151317,20,24,22,25,19])). % 58.53/58.62 cnf(151332,plain, % 58.53/58.62 ($false), % 58.53/58.62 inference(scs_inference,[],[151306,151324,11,14,9,22,23,24]), % 58.53/58.62 ['proof']). % 58.65/58.70 % SZS output end Proof % 58.65/58.70 % Total time :58.000000s %------------------------------------------------------------------------------