%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : GRP012+5 : TPTP v8.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:28 EDT 2024 % Result : Theorem 1.50s 1.60s % Output : CNFRefutation 1.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP012+5 : TPTP v8.2.0. Released v3.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.32 % Computer : n022.cluster.edu % 0.13/0.32 % Model : x86_64 x86_64 % 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.32 % Memory : 8042.1875MB % 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.32 % CPULimit : 300 % 0.13/0.32 % WCLimit : 300 % 0.13/0.32 % DateTime : Thu Jun 20 13:30:08 EDT 2024 % 0.13/0.32 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 1.50/1.59 %------------------------------------------- % 1.50/1.59 % File :CSE---1.7 % 1.50/1.59 % Problem :theBenchmark % 1.50/1.59 % Transform :cnf % 1.50/1.59 % Format :tptp:raw % 1.50/1.59 % Command :java -jar mcs_scs.jar %d %s % 1.50/1.59 % 1.50/1.59 % Result :Theorem 1.010000s % 1.50/1.59 % Output :CNFRefutation 1.010000s % 1.50/1.59 %------------------------------------------- % 1.50/1.60 %------------------------------------------------------------------------------ % 1.50/1.60 % File : GRP012+5 : TPTP v8.2.0. Released v3.1.0. % 1.50/1.60 % Domain : Group Theory % 1.50/1.60 % Problem : Inverse of products = Product of inverses % 1.50/1.60 % Version : Especial. % 1.50/1.60 % English : The inverse of products equals the product of the inverse, % 1.50/1.60 % in opposite order % 1.50/1.60 % 1.50/1.60 % Refs : [Shu04] Shults (2004), Email to G. Sutcliffe % 1.50/1.60 % Source : [Shu04] % 1.50/1.60 % Names : % 1.50/1.60 % 1.50/1.60 % Status : Theorem % 1.50/1.60 % Rating : 0.12 v8.2.0, 0.20 v8.1.0, 0.21 v7.5.0, 0.33 v7.4.0, 0.12 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.24 v6.0.0, 0.25 v5.5.0, 0.29 v5.4.0, 0.22 v5.3.0, 0.35 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0, 0.20 v3.7.0, 0.29 v3.5.0, 0.25 v3.4.0, 0.00 v3.1.0 % 1.50/1.60 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 1.50/1.60 % Number of atoms : 16 ( 0 equ) % 1.50/1.60 % Maximal formula atoms : 16 ( 16 avg) % 1.50/1.60 % Number of connectives : 15 ( 0 ~; 0 |; 11 &) % 1.50/1.60 % ( 0 <=>; 4 =>; 0 <=; 0 <~>) % 1.50/1.60 % Maximal formula depth : 15 ( 15 avg) % 1.50/1.60 % Maximal term depth : 2 ( 1 avg) % 1.50/1.60 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 1.50/1.60 % Number of functors : 1 ( 1 usr; 0 con; 1-1 aty) % 1.50/1.60 % Number of variables : 24 ( 23 !; 1 ?) % 1.50/1.60 % SPC : FOF_THM_RFO_NEQ % 1.50/1.60 % 1.50/1.60 % Comments : % 1.50/1.60 %------------------------------------------------------------------------------ % 1.50/1.60 fof(prove_distribution,conjecture, % 1.50/1.60 ! [E] : % 1.50/1.60 ( ( ! [X,Y] : % 1.50/1.60 ? [Z] : product(X,Y,Z) % 1.50/1.60 & ! [X,Y,Z,U,V,W] : % 1.50/1.60 ( ( product(X,Y,U) % 1.50/1.60 & product(Y,Z,V) % 1.50/1.60 & product(U,Z,W) ) % 1.50/1.60 => product(X,V,W) ) % 1.50/1.60 & ! [X,Y,Z,U,V,W] : % 1.50/1.60 ( ( product(X,Y,U) % 1.50/1.60 & product(Y,Z,V) % 1.50/1.60 & product(X,V,W) ) % 1.50/1.60 => product(U,Z,W) ) % 1.50/1.60 & ! [X] : product(X,E,X) % 1.50/1.60 & ! [X] : product(E,X,X) % 1.50/1.60 & ! [X] : product(X,inverse(X),E) % 1.50/1.60 & ! [X] : product(inverse(X),X,E) ) % 1.50/1.60 => ! [U,V,W,X] : % 1.50/1.60 ( ( product(inverse(U),inverse(V),W) % 1.50/1.60 & product(V,U,X) ) % 1.50/1.60 => product(inverse(W),inverse(X),E) ) ) ). % 1.50/1.60 % 1.50/1.60 %------------------------------------------------------------------------------ % 1.50/1.60 %------------------------------------------- % 1.50/1.60 % Proof found % 1.50/1.60 % SZS status Theorem for theBenchmark % 1.50/1.60 % SZS output start Proof % 1.50/1.60 %ClaNum:10(EqnAxiom:0) % 1.50/1.60 %VarNum:36(SingletonVarNum:18) % 1.50/1.60 %MaxLitNum:4 % 1.50/1.60 %MaxfuncDepth:1 % 1.50/1.60 %SharedTerms:12 % 1.50/1.60 %goalClause: 1 2 3 4 5 6 7 8 9 10 % 1.50/1.60 %singleGoalClaCount:8 % 1.50/1.60 [1]P1(a1,a2,a5) % 1.50/1.60 [6]P1(f7(a2),f7(a1),a6) % 1.50/1.60 [8]~P1(f7(a6),f7(a5),a3) % 1.50/1.60 [2]P1(x21,a3,x21) % 1.50/1.60 [3]P1(a3,x31,x31) % 1.50/1.60 [4]P1(x41,f7(x41),a3) % 1.50/1.60 [5]P1(f7(x51),x51,a3) % 1.50/1.60 [7]P1(x71,x72,f4(x71,x72)) % 1.50/1.60 [9]~P1(x96,x94,x91)+P1(x91,x92,x93)+~P1(x94,x92,x95)+~P1(x96,x95,x93) % 1.50/1.60 [10]~P1(x101,x106,x104)+P1(x101,x102,x103)+~P1(x104,x105,x103)+~P1(x106,x105,x102) % 1.50/1.60 %EqnAxiom % 1.50/1.60 % 1.50/1.60 %------------------------------------------- % 1.50/1.60 cnf(38,plain, % 1.50/1.60 (P1(a5,x381,a3)+~P1(a2,x381,f7(a1))), % 1.50/1.60 inference(scs_inference,[],[1,5,3,4,10,9])). % 1.50/1.60 cnf(163,plain, % 1.50/1.60 (~P1(f4(f7(a6),f7(a5)),a3,a3)), % 1.50/1.60 inference(scs_inference,[],[8,2,7,10])). % 1.50/1.60 cnf(171,plain, % 1.50/1.60 (~P1(a3,f4(f7(a6),f7(a5)),a3)), % 1.50/1.60 inference(scs_inference,[],[163,4,5,10])). % 1.50/1.60 cnf(205,plain, % 1.50/1.60 (P1(a2,a6,f7(a1))), % 1.50/1.60 inference(scs_inference,[],[4,171,6,3,9,10])). % 1.50/1.60 cnf(304,plain, % 1.50/1.60 (P1(a5,a3,f7(a6))), % 1.50/1.60 inference(scs_inference,[],[205,4,3,38,10])). % 1.50/1.60 cnf(743,plain, % 1.50/1.60 ($false), % 1.50/1.60 inference(scs_inference,[],[8,304,4,3,9]), % 1.50/1.61 ['proof']). % 1.50/1.61 % SZS output end Proof % 1.50/1.61 % Total time :1.010000s %------------------------------------------------------------------------------