%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP123-8.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 : n026.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.60s 58.64s % Output : CNFRefutation 58.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP123-8.003 : TPTP v8.2.0. Released v1.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n026.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 07:01:54 EDT 2024 % 0.13/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 58.55/58.61 %------------------------------------------- % 58.55/58.61 % File :CSE---1.7 % 58.55/58.61 % Problem :theBenchmark % 58.55/58.61 % Transform :cnf % 58.55/58.61 % Format :tptp:raw % 58.55/58.61 % Command :java -jar mcs_scs.jar %d %s % 58.55/58.61 % 58.55/58.61 % Result :Theorem 58.010000s % 58.55/58.61 % Output :CNFRefutation 58.010000s % 58.55/58.61 %------------------------------------------- % 58.60/58.63 %-------------------------------------------------------------------------- % 58.60/58.63 % File : GRP123-8.003 : TPTP v8.2.0. Released v1.2.0. % 58.60/58.63 % Domain : Group Theory (Quasigroups) % 58.60/58.63 % Problem : (3,2,1) conjugate orthogonality % 58.60/58.63 % Version : [Sla93] axioms : Augmented. % 58.60/58.63 % Theorem formulation : Uses a second group. % 58.60/58.63 % English : If ab=xy and a*b = x*y then a=x and b=y, where c*b=a iff ab=c. % 58.60/58.63 % Generate the multiplication table for the specified quasi- % 58.60/58.63 % group with 3 elements. % 58.60/58.63 % 58.60/58.63 % Refs : [FSB93] Fujita et al. (1993), Automatic Generation of Some Res % 58.60/58.63 % : [Sla93] Slaney (1993), Email to G. Sutcliffe % 58.60/58.63 % : [SFS95] Slaney et al. (1995), Automated Reasoning and Exhausti % 58.60/58.63 % Source : [TPTP] % 58.60/58.63 % Names : % 58.60/58.63 % 58.60/58.63 % Status : Unsatisfiable % 58.60/58.63 % Rating : 0.00 v2.1.0 % 58.60/58.63 % Syntax : Number of clauses : 36 ( 21 unt; 3 nHn; 34 RR) % 58.60/58.63 % Number of literals : 79 ( 0 equ; 45 neg) % 58.60/58.63 % Maximal clause size : 6 ( 2 avg) % 58.60/58.63 % Maximal term depth : 1 ( 1 avg) % 58.60/58.63 % Number of predicates : 8 ( 8 usr; 0 prp; 1-3 aty) % 58.60/58.63 % Number of functors : 4 ( 4 usr; 4 con; 0-0 aty) % 58.60/58.63 % Number of variables : 54 ( 0 sgn) % 58.60/58.63 % SPC : CNF_UNS_EPR_NEQ_NHN % 58.60/58.63 % 58.60/58.63 % Comments : [SFS93]'s axiomatization has been modified for this. % 58.60/58.63 % : Substitution axioms are not needed, as any positive equality % 58.60/58.63 % literals should resolve on negative ones directly. % 58.60/58.63 % : Version 8 has complex isomorphism avoidance (mentioned in % 58.60/58.63 % [SFS95] % 58.60/58.63 % : tptp2X: -f tptp -s3 GRP123-8.g % 58.60/58.63 %-------------------------------------------------------------------------- % 58.60/58.63 cnf(e_0_then_e_1,axiom, % 58.60/58.63 next(e_0,e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(e_1_then_e_2,axiom, % 58.60/58.63 next(e_1,e_2) ). % 58.60/58.63 % 58.60/58.63 cnf(e_2_then_e_3,axiom, % 58.60/58.63 next(e_2,e_3) ). % 58.60/58.63 % 58.60/58.63 cnf(e_1_greater_e_0,axiom, % 58.60/58.63 greater(e_1,e_0) ). % 58.60/58.63 % 58.60/58.63 cnf(e_2_greater_e_0,axiom, % 58.60/58.63 greater(e_2,e_0) ). % 58.60/58.63 % 58.60/58.63 cnf(e_3_greater_e_0,axiom, % 58.60/58.63 greater(e_3,e_0) ). % 58.60/58.63 % 58.60/58.63 cnf(e_2_greater_e_1,axiom, % 58.60/58.63 greater(e_2,e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(e_3_greater_e_1,axiom, % 58.60/58.63 greater(e_3,e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(e_3_greater_e_2,axiom, % 58.60/58.63 greater(e_3,e_2) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle1,axiom, % 58.60/58.63 ( ~ cycle(X,Y) % 58.60/58.63 | ~ cycle(X,Z) % 58.60/58.63 | equalish(Y,Z) ) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle2,axiom, % 58.60/58.63 ( ~ group_element(X) % 58.60/58.63 | cycle(X,e_0) % 58.60/58.63 | cycle(X,e_1) % 58.60/58.63 | cycle(X,e_2) ) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle3,axiom, % 58.60/58.63 cycle(e_3,e_0) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle4,axiom, % 58.60/58.63 ( ~ cycle(X,Y) % 58.60/58.63 | ~ cycle(W,Z) % 58.60/58.63 | ~ next(X,W) % 58.60/58.63 | ~ greater(Y,e_0) % 58.60/58.63 | ~ next(Z,Z1) % 58.60/58.63 | equalish(Y,Z1) ) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle5,axiom, % 58.60/58.63 ( ~ cycle(X,Z1) % 58.60/58.63 | ~ cycle(Y,e_0) % 58.60/58.63 | ~ cycle(W,Z2) % 58.60/58.63 | ~ next(Y,W) % 58.60/58.63 | ~ greater(Y,X) % 58.60/58.63 | ~ greater(Z1,Z2) ) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle6,axiom, % 58.60/58.63 ( ~ cycle(X,e_0) % 58.60/58.63 | ~ product(X,e_1,Y) % 58.60/58.63 | ~ greater(Y,X) ) ). % 58.60/58.63 % 58.60/58.63 cnf(cycle7,axiom, % 58.60/58.63 ( ~ cycle(X,Y) % 58.60/58.63 | ~ product(X,e_1,Z) % 58.60/58.63 | ~ greater(Y,e_0) % 58.60/58.63 | ~ next(X,X1) % 58.60/58.63 | equalish(Z,X1) ) ). % 58.60/58.63 % 58.60/58.63 cnf(element_1,axiom, % 58.60/58.63 group_element(e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(element_2,axiom, % 58.60/58.63 group_element(e_2) ). % 58.60/58.63 % 58.60/58.63 cnf(element_3,axiom, % 58.60/58.63 group_element(e_3) ). % 58.60/58.63 % 58.60/58.63 cnf(e_1_is_not_e_2,axiom, % 58.60/58.63 ~ equalish(e_1,e_2) ). % 58.60/58.63 % 58.60/58.63 cnf(e_1_is_not_e_3,axiom, % 58.60/58.63 ~ equalish(e_1,e_3) ). % 58.60/58.63 % 58.60/58.63 cnf(e_2_is_not_e_1,axiom, % 58.60/58.63 ~ equalish(e_2,e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(e_2_is_not_e_3,axiom, % 58.60/58.63 ~ equalish(e_2,e_3) ). % 58.60/58.63 % 58.60/58.63 cnf(e_3_is_not_e_1,axiom, % 58.60/58.63 ~ equalish(e_3,e_1) ). % 58.60/58.63 % 58.60/58.63 cnf(e_3_is_not_e_2,axiom, % 58.60/58.63 ~ equalish(e_3,e_2) ). % 58.60/58.63 % 58.60/58.63 cnf(product1_total_function1,axiom, % 58.60/58.63 ( ~ group_element(X) % 58.60/58.63 | ~ group_element(Y) % 58.60/58.63 | product1(X,Y,e_1) % 58.60/58.63 | product1(X,Y,e_2) % 58.60/58.63 | product1(X,Y,e_3) ) ). % 58.60/58.63 % 58.60/58.63 cnf(product1_total_function2,axiom, % 58.60/58.63 ( ~ product1(X,Y,W) % 58.60/58.63 | ~ product1(X,Y,Z) % 58.60/58.63 | equalish(W,Z) ) ). % 58.60/58.63 % 58.60/58.63 cnf(product1_right_cancellation,axiom, % 58.60/58.63 ( ~ product1(X,W,Y) % 58.60/58.63 | ~ product1(X,Z,Y) % 58.60/58.63 | equalish(W,Z) ) ). % 58.60/58.63 % 58.60/58.64 cnf(product1_left_cancellation,axiom, % 58.60/58.64 ( ~ product1(W,Y,X) % 58.60/58.64 | ~ product1(Z,Y,X) % 58.60/58.64 | equalish(W,Z) ) ). % 58.60/58.64 % 58.60/58.64 cnf(product1_idempotence,axiom, % 58.60/58.64 product1(X,X,X) ). % 58.60/58.64 % 58.60/58.64 cnf(product2_total_function1,axiom, % 58.60/58.64 ( ~ group_element(X) % 58.60/58.64 | ~ group_element(Y) % 58.60/58.64 | product2(X,Y,e_1) % 58.60/58.64 | product2(X,Y,e_2) % 58.60/58.64 | product2(X,Y,e_3) ) ). % 58.60/58.64 % 58.60/58.64 cnf(product2_total_function2,axiom, % 58.60/58.64 ( ~ product2(X,Y,W) % 58.60/58.64 | ~ product2(X,Y,Z) % 58.60/58.64 | equalish(W,Z) ) ). % 58.60/58.64 % 58.60/58.64 cnf(product2_right_cancellation,axiom, % 58.60/58.64 ( ~ product2(X,W,Y) % 58.60/58.64 | ~ product2(X,Z,Y) % 58.60/58.64 | equalish(W,Z) ) ). % 58.60/58.64 % 58.60/58.64 cnf(product2_left_cancellation,axiom, % 58.60/58.64 ( ~ product2(W,Y,X) % 58.60/58.64 | ~ product2(Z,Y,X) % 58.60/58.64 | equalish(W,Z) ) ). % 58.60/58.64 % 58.60/58.64 cnf(product2_idempotence,axiom, % 58.60/58.64 product2(X,X,X) ). % 58.60/58.64 % 58.60/58.64 cnf(qg1a,negated_conjecture, % 58.60/58.64 ( ~ product1(X,Y,Z1) % 58.60/58.64 | ~ product1(Z1,Y,Z2) % 58.60/58.64 | product2(Z2,X,Y) ) ). % 58.60/58.64 % 58.60/58.64 %-------------------------------------------------------------------------- % 58.60/58.64 %------------------------------------------- % 58.60/58.64 % Proof found % 58.60/58.64 % SZS status Theorem for theBenchmark % 58.60/58.64 % SZS output start Proof % 58.60/58.64 %ClaNum:36(EqnAxiom:0) % 58.60/58.64 %VarNum:125(SingletonVarNum:54) % 58.60/58.64 %MaxLitNum:6 % 58.60/58.64 %MaxfuncDepth:0 % 58.60/58.64 %SharedTerms:23 % 58.60/58.64 %goalClause: 36 % 58.60/58.64 [1]P1(a1) % 58.60/58.64 [2]P1(a3) % 58.60/58.64 [3]P1(a4) % 58.60/58.64 [4]P5(a2,a1) % 58.60/58.64 [5]P5(a1,a3) % 58.60/58.64 [6]P5(a3,a4) % 58.60/58.64 [7]P2(a1,a2) % 58.60/58.64 [8]P2(a3,a2) % 58.60/58.64 [9]P2(a3,a1) % 58.60/58.64 [10]P2(a4,a2) % 58.60/58.64 [11]P2(a4,a1) % 58.60/58.64 [12]P2(a4,a3) % 58.60/58.64 [13]P3(a4,a2) % 58.60/58.64 [16]~P4(a1,a3) % 58.60/58.64 [17]~P4(a1,a4) % 58.60/58.64 [18]~P4(a3,a1) % 58.60/58.64 [19]~P4(a3,a4) % 58.60/58.64 [20]~P4(a4,a1) % 58.60/58.64 [21]~P4(a4,a3) % 58.60/58.64 [14]P6(x141,x141,x141) % 58.60/58.64 [15]P8(x151,x151,x151) % 58.60/58.64 [25]~P2(x251,x252)+~P7(x252,a1,x251)+~P3(x252,a2) % 58.60/58.64 [23]~P3(x233,x231)+P4(x231,x232)+~P3(x233,x232) % 58.60/58.64 [30]~P6(x303,x304,x301)+P4(x301,x302)+~P6(x303,x304,x302) % 58.60/58.64 [31]~P8(x313,x314,x311)+P4(x311,x312)+~P8(x313,x314,x312) % 58.60/58.64 [32]~P6(x323,x321,x324)+P4(x321,x322)+~P6(x323,x322,x324) % 58.60/58.64 [33]~P8(x333,x331,x334)+P4(x331,x332)+~P8(x333,x332,x334) % 58.60/58.64 [34]~P6(x341,x343,x344)+P4(x341,x342)+~P6(x342,x343,x344) % 58.60/58.64 [35]~P8(x351,x353,x354)+P4(x351,x352)+~P8(x352,x353,x354) % 58.60/58.64 [36]~P6(x362,x363,x364)+P8(x361,x362,x363)+~P6(x364,x363,x361) % 58.60/58.64 [22]~P1(x221)+P3(x221,a1)+P3(x221,a3)+P3(x221,a2) % 58.60/58.64 [28]~P1(x282)+~P1(x281)+P6(x281,x282,a3)+P6(x281,x282,a4)+P6(x281,x282,a1) % 58.60/58.64 [29]~P1(x292)+~P1(x291)+P8(x291,x292,a3)+P8(x291,x292,a4)+P8(x291,x292,a1) % 58.60/58.64 [27]P4(x271,x272)+~P5(x273,x272)+~P3(x273,x274)+~P7(x273,a1,x271)+~P2(x274,a2) % 58.60/58.64 [24]~P3(x245,x243)+~P3(x244,x241)+P4(x241,x242)+~P5(x243,x242)+~P5(x244,x245)+~P2(x241,a2) % 58.60/58.64 [26]~P3(x262,x265)+~P3(x263,x264)+~P5(x261,x262)+~P2(x261,x263)+~P2(x264,x265)+~P3(x261,a2) % 58.60/58.64 %EqnAxiom % 58.60/58.64 % 58.60/58.64 %------------------------------------------- % 58.77/58.78 cnf(231078,plain, % 58.77/58.78 (~P8(a4,a4,a3)), % 58.77/58.78 inference(scs_inference,[],[19,15,31])). % 58.77/58.78 cnf(231079,plain, % 58.77/58.78 (P8(x2310791,x2310791,x2310791)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231081,plain, % 58.77/58.78 (~P6(a4,a3,a3)), % 58.77/58.78 inference(scs_inference,[],[19,15,14,31,34])). % 58.77/58.78 cnf(231082,plain, % 58.77/58.78 (P6(x2310821,x2310821,x2310821)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231087,plain, % 58.77/58.78 (P8(x2310871,x2310871,x2310871)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231093,plain, % 58.77/58.78 (P6(x2310931,x2310931,x2310931)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231098,plain, % 58.77/58.78 (~P6(x2310981,a3,a4)+~P6(a4,a3,x2310981)), % 58.77/58.78 inference(scs_inference,[],[19,15,231079,231087,13,14,231082,231093,31,34,23,35,33,32,30,36])). % 58.77/58.78 cnf(231104,plain, % 58.77/58.78 (~P8(a1,a3,a1)), % 58.77/58.78 inference(scs_inference,[],[15,16,33])). % 58.77/58.78 cnf(231105,plain, % 58.77/58.78 (P8(x2311051,x2311051,x2311051)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231108,plain, % 58.77/58.78 (P8(x2311081,x2311081,x2311081)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231111,plain, % 58.77/58.78 (P6(x2311111,x2311111,x2311111)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231117,plain, % 58.77/58.78 (P6(x2311171,x2311171,x2311171)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231119,plain, % 58.77/58.78 (~P6(a1,a3,a1)), % 58.77/58.78 inference(scs_inference,[],[15,231105,231108,16,14,231111,231117,33,31,34,35,30,32])). % 58.77/58.78 cnf(231124,plain, % 58.77/58.78 (P6(a4,a3,a1)+P6(a4,a3,a4)), % 58.77/58.78 inference(scs_inference,[],[231081,3,19,15,231105,231108,16,2,14,231111,231117,33,31,34,35,30,32,23,28])). % 58.77/58.78 cnf(231131,plain, % 58.77/58.78 (P8(x2311311,x2311311,x2311311)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231134,plain, % 58.77/58.78 (P8(x2311341,x2311341,x2311341)), % 58.77/58.78 inference(rename_variables,[],[15])). % 58.77/58.78 cnf(231136,plain, % 58.77/58.78 (~P6(a1,a3,a3)), % 58.77/58.78 inference(scs_inference,[],[15,231131,13,18,8,6,4,14,23,24,33,31,34])). % 58.77/58.78 cnf(231137,plain, % 58.77/58.78 (P6(x2311371,x2311371,x2311371)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231140,plain, % 58.77/58.78 (P6(x2311401,x2311401,x2311401)), % 58.77/58.78 inference(rename_variables,[],[14])). % 58.77/58.78 cnf(231150,plain, % 58.77/58.78 (P8(a1,a3,a4)), % 58.77/58.78 inference(scs_inference,[],[1,231104,15,231131,231134,13,18,8,6,4,2,14,231137,231140,23,24,33,31,34,30,32,35,22,29])). % 58.77/58.78 cnf(231165,plain, % 58.77/58.78 ($false), % 58.77/58.78 inference(scs_inference,[],[1,231078,231119,231136,231150,19,16,2,33,35,28,231098,231124,36]), % 58.77/58.78 ['proof']). % 58.88/58.88 % SZS output end Proof % 58.88/58.88 % Total time :58.010000s %------------------------------------------------------------------------------