%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP131-2.002 : TPTP v8.2.0. Released v1.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.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:57 EDT 2024 % Result : Unsatisfiable 61.10s 61.47s % Output : CNFRefutation 61.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : GRP131-2.002 : TPTP v8.2.0. Released v1.2.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 08:17:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 61.10/61.45 %------------------------------------------- % 61.10/61.45 % File :CSE---1.7 % 61.10/61.45 % Problem :theBenchmark % 61.10/61.45 % Transform :cnf % 61.10/61.45 % Format :tptp:raw % 61.10/61.45 % Command :java -jar mcs_scs.jar %d %s % 61.10/61.45 % 61.10/61.45 % Result :Theorem 60.610000s % 61.10/61.45 % Output :CNFRefutation 60.610000s % 61.10/61.45 %------------------------------------------- % 61.10/61.46 %-------------------------------------------------------------------------- % 61.10/61.46 % File : GRP131-2.002 : TPTP v8.2.0. Released v1.2.0. % 61.10/61.46 % Domain : Group Theory (Quasigroups) % 61.10/61.46 % Problem : (3,2,1) conjugate orthogonality, no idempotence % 61.10/61.46 % Version : [Sla93] axioms : Augmented. % 61.10/61.46 % English : Generate the multiplication table for the specified quasi- % 61.10/61.46 % group with 2 elements. % 61.10/61.46 % 61.10/61.46 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 61.10/61.46 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 61.10/61.46 % : [Zha94] Zhang (1994), Email to G. Sutcliffe % 61.10/61.46 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 61.10/61.46 % Source : [TPTP] % 61.10/61.46 % Names : % 61.10/61.46 % 61.10/61.46 % Status : Unsatisfiable % 61.10/61.46 % Rating : 0.00 v2.1.0 % 61.10/61.46 % Syntax : Number of clauses : 13 ( 6 unt; 1 nHn; 13 RR) % 61.10/61.46 % Number of literals : 32 ( 0 equ; 21 neg) % 61.10/61.46 % Maximal clause size : 5 ( 2 avg) % 61.10/61.46 % Maximal term depth : 1 ( 1 avg) % 61.10/61.46 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty) % 61.10/61.46 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 61.10/61.46 % Number of variables : 29 ( 0 sgn) % 61.10/61.46 % SPC : CNF_UNS_EPR_NEQ_NHN % 61.10/61.47 % 61.10/61.47 % Comments : Slaney's [1993] axiomatization has been modified for this. % 61.10/61.47 % : Substitution axioms are not needed, as any positive equality % 61.10/61.47 % literals should resolve on negative ones directly. % 61.10/61.47 % : Zhang [Zha94] has pointed out that either one of qg1_1 % 61.10/61.47 % or qg1_2 may be used, as each implies the other in this % 61.10/61.47 % scenario, with the help of cancellation. The dependence % 61.10/61.47 % cannot be proved, so both have been left in here. % 61.10/61.47 % : This version adds a simple isomorphism avoidance clause, % 61.10/61.47 % mentioned in [FSB93]. % 61.10/61.47 % : tptp2X: -f tptp -s2 GRP131-2.g % 61.10/61.47 %-------------------------------------------------------------------------- % 61.10/61.47 cnf(e_1_then_e_2,axiom, % 61.10/61.47 next(e_1,e_2) ). % 61.10/61.47 % 61.10/61.47 cnf(e_2_greater_e_1,axiom, % 61.10/61.47 greater(e_2,e_1) ). % 61.10/61.47 % 61.10/61.47 cnf(no_redundancy,axiom, % 61.10/61.47 ( ~ product(X,e_1,Y) % 61.10/61.47 | ~ next(X,X1) % 61.10/61.47 | ~ greater(Y,X1) ) ). % 61.10/61.47 % 61.10/61.47 cnf(element_1,axiom, % 61.10/61.47 group_element(e_1) ). % 61.10/61.47 % 61.10/61.47 cnf(element_2,axiom, % 61.10/61.47 group_element(e_2) ). % 61.10/61.47 % 61.10/61.47 cnf(e_1_is_not_e_2,axiom, % 61.10/61.47 ~ equalish(e_1,e_2) ). % 61.10/61.47 % 61.10/61.47 cnf(e_2_is_not_e_1,axiom, % 61.10/61.47 ~ equalish(e_2,e_1) ). % 61.10/61.47 % 61.10/61.47 cnf(product_total_function1,axiom, % 61.10/61.47 ( ~ group_element(X) % 61.10/61.47 | ~ group_element(Y) % 61.10/61.47 | product(X,Y,e_1) % 61.10/61.47 | product(X,Y,e_2) ) ). % 61.10/61.47 % 61.10/61.47 cnf(product_total_function2,axiom, % 61.10/61.47 ( ~ product(X,Y,W) % 61.10/61.47 | ~ product(X,Y,Z) % 61.10/61.47 | equalish(W,Z) ) ). % 61.10/61.47 % 61.10/61.47 cnf(product_right_cancellation,axiom, % 61.10/61.47 ( ~ product(X,W,Y) % 61.10/61.47 | ~ product(X,Z,Y) % 61.10/61.47 | equalish(W,Z) ) ). % 61.10/61.47 % 61.10/61.47 cnf(product_left_cancellation,axiom, % 61.10/61.47 ( ~ product(W,Y,X) % 61.10/61.47 | ~ product(Z,Y,X) % 61.10/61.47 | equalish(W,Z) ) ). % 61.10/61.47 % 61.10/61.47 cnf(qg1_1,negated_conjecture, % 61.10/61.47 ( ~ product(X1,Y1,Z1) % 61.10/61.47 | ~ product(X2,Y2,Z1) % 61.10/61.47 | ~ product(Z2,Y1,X1) % 61.10/61.47 | ~ product(Z2,Y2,X2) % 61.10/61.47 | equalish(X1,X2) ) ). % 61.10/61.47 % 61.10/61.47 cnf(qg1_2,negated_conjecture, % 61.10/61.47 ( ~ product(X1,Y1,Z1) % 61.10/61.47 | ~ product(X2,Y2,Z1) % 61.10/61.47 | ~ product(Z2,Y1,X1) % 61.10/61.47 | ~ product(Z2,Y2,X2) % 61.10/61.47 | equalish(Y1,Y2) ) ). % 61.10/61.47 % 61.10/61.47 %-------------------------------------------------------------------------- % 61.10/61.47 %------------------------------------------- % 61.10/61.47 % Proof found % 61.10/61.47 % SZS status Theorem for theBenchmark % 61.10/61.47 % SZS output start Proof % 61.10/61.47 %ClaNum:13(EqnAxiom:0) % 61.10/61.47 %VarNum:64(SingletonVarNum:29) % 61.10/61.47 %MaxLitNum:5 % 61.10/61.47 %MaxfuncDepth:0 % 61.10/61.47 %SharedTerms:8 % 61.10/61.47 %goalClause: 12 13 % 61.10/61.47 [1]P1(a1) % 61.10/61.47 [2]P1(a2) % 61.10/61.47 [3]P4(a1,a2) % 61.10/61.47 [4]P2(a2,a1) % 61.10/61.47 [5]~P3(a1,a2) % 61.10/61.47 [6]~P3(a2,a1) % 61.10/61.47 [8]~P4(x81,x82)+~P2(x83,x82)+~P5(x81,a1,x83) % 61.10/61.47 [9]~P5(x93,x94,x91)+P3(x91,x92)+~P5(x93,x94,x92) % 61.10/61.47 [10]~P5(x103,x101,x104)+P3(x101,x102)+~P5(x103,x102,x104) % 61.10/61.47 [11]~P5(x111,x113,x114)+P3(x111,x112)+~P5(x112,x113,x114) % 61.10/61.47 [7]~P1(x72)+~P1(x71)+P5(x71,x72,a2)+P5(x71,x72,a1) % 61.10/61.47 [12]~P5(x125,x121,x126)+P3(x121,x122)+~P5(x123,x122,x124)+~P5(x123,x121,x125)+~P5(x124,x122,x126) % 61.10/61.47 [13]~P5(x131,x135,x136)+P3(x131,x132)+~P5(x133,x134,x132)+~P5(x133,x135,x131)+~P5(x132,x134,x136) % 61.10/61.47 %EqnAxiom % 61.10/61.47 % 61.10/61.47 %------------------------------------------- % 61.24/61.52 cnf(16,plain, % 61.24/61.52 (~P5(a1,a1,a2)+P5(a1,a2,a1)), % 61.24/61.52 inference(scs_inference,[],[5,2,1,10,7])). % 61.24/61.52 cnf(75656,plain, % 61.24/61.52 (P5(a1,a1,a1)+P5(a1,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[1,4,8,7])). % 61.24/61.52 cnf(75661,plain, % 61.24/61.52 (~P5(x756611,x756612,a1)+~P5(x756611,x756612,a2)), % 61.24/61.52 inference(scs_inference,[],[6,3,8,9])). % 61.24/61.52 cnf(75666,plain, % 61.24/61.52 (~P5(x756661,a1,x756662)+~P5(x756661,a2,x756662)), % 61.24/61.52 inference(scs_inference,[],[4,6,8,10])). % 61.24/61.52 cnf(75671,plain, % 61.24/61.52 (~P5(a2,x756711,x756712)+~P5(a1,x756711,x756712)), % 61.24/61.52 inference(scs_inference,[],[5,3,8,11])). % 61.24/61.52 cnf(75673,plain, % 61.24/61.52 (P5(a1,a2,a2)+~P5(a1,a1,a1)), % 61.24/61.52 inference(scs_inference,[],[2,1,75666,7])). % 61.24/61.52 cnf(75676,plain, % 61.24/61.52 (P5(a2,a2,a1)+P5(a2,a2,a2)), % 61.24/61.52 inference(scs_inference,[],[2,4,8,7])). % 61.24/61.52 cnf(75678,plain, % 61.24/61.52 (~P5(a1,a1,a1)+~P5(a2,a2,a2)), % 61.24/61.52 inference(scs_inference,[],[75671,75673])). % 61.24/61.52 cnf(75681,plain, % 61.24/61.52 (~P5(a1,a1,a1)+P5(a2,a2,a1)), % 61.24/61.52 inference(scs_inference,[],[75676,75678])). % 61.24/61.52 cnf(75684,plain, % 61.24/61.52 (~P5(x756841,a1,x756842)+~P5(x756843,a2,x756844)+~P5(x756844,a2,x756842)+~P5(x756843,a1,x756841)), % 61.24/61.52 inference(scs_inference,[],[6,4,12])). % 61.24/61.52 cnf(75685,plain, % 61.24/61.52 (P5(a1,a1,a2)+P5(a2,a2,a1)), % 61.24/61.52 inference(scs_inference,[],[75681,75656])). % 61.24/61.52 cnf(75692,plain, % 61.24/61.52 (~P5(a2,x756921,x756922)+~P5(x756923,x756924,a1)+~P5(a1,x756924,x756922)+~P5(x756923,x756921,a2)), % 61.24/61.52 inference(scs_inference,[],[5,3,13])). % 61.24/61.52 cnf(81505,plain, % 61.24/61.52 (~P5(a1,a1,a2)+~P5(a1,a1,x815051)+~P5(x815051,a1,a1)), % 61.24/61.52 inference(scs_inference,[],[16,75684])). % 61.24/61.52 cnf(81511,plain, % 61.24/61.52 (P5(a1,a1,a1)+~P5(a2,a1,a1)), % 61.24/61.52 inference(scs_inference,[],[81505,75656])). % 61.24/61.52 cnf(81514,plain, % 61.24/61.52 (~P5(a2,a1,a1)+~P5(a1,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[81511,75661])). % 61.24/61.52 cnf(81520,plain, % 61.24/61.52 (~P5(a1,a1,a2)+P5(a2,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[1,2,81514,7])). % 61.24/61.52 cnf(81521,plain, % 61.24/61.52 (P5(a2,a2,a1)+P5(a2,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[81520,75685])). % 61.24/61.52 cnf(81524,plain, % 61.24/61.52 (~P5(a2,a1,a1)+P5(a2,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[81521,75666])). % 61.24/61.52 cnf(81530,plain, % 61.24/61.52 (P5(a2,a1,a2)), % 61.24/61.52 inference(scs_inference,[],[2,1,81524,7])). % 61.24/61.52 cnf(81548,plain, % 61.24/61.52 ($false), % 61.24/61.52 inference(scs_inference,[],[6,81530,4,75666,9,11,8,12,75656,75673,75681,75671,10,75692]), % 61.24/61.52 ['proof']). % 61.24/61.57 % SZS output end Proof % 61.24/61.57 % Total time :60.610000s %------------------------------------------------------------------------------