%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP004-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n001.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:25 EDT 2024
% Result : Unsatisfiable 7.32s 7.45s
% Output : CNFRefutation 7.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP004-2 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n001.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 07:18:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 7.32/7.45 %-------------------------------------------
% 7.32/7.45 % File :CSE---1.7
% 7.32/7.45 % Problem :theBenchmark
% 7.32/7.45 % Transform :cnf
% 7.32/7.45 % Format :tptp:raw
% 7.32/7.45 % Command :java -jar mcs_scs.jar %d %s
% 7.32/7.45
% 7.32/7.45 % Result :Theorem 6.850000s
% 7.32/7.45 % Output :CNFRefutation 6.850000s
% 7.32/7.45 %-------------------------------------------
% 7.32/7.45 %--------------------------------------------------------------------------
% 7.32/7.45 % File : GRP004-2 : TPTP v8.2.0. Released v1.0.0.
% 7.32/7.45 % Domain : Group Theory
% 7.32/7.45 % Problem : Left inverse and identity => Right inverse exists
% 7.32/7.45 % Version : [Ver92] axioms.
% 7.32/7.45 % English : In a group with left inverses and left identity every element
% 7.32/7.45 % has a right inverse.
% 7.32/7.45
% 7.32/7.45 % Refs : [Ver92] Veroff (1992), Email to G. Sutcliffe
% 7.32/7.45 % Source : [TPTP]
% 7.32/7.45 % Names :
% 7.32/7.45
% 7.32/7.45 % Status : Unsatisfiable
% 7.32/7.45 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.00 v2.1.0, 0.00 v2.0.0
% 7.32/7.45 % Syntax : Number of clauses : 8 ( 4 unt; 0 nHn; 5 RR)
% 7.32/7.45 % Number of literals : 18 ( 0 equ; 11 neg)
% 7.32/7.45 % Maximal clause size : 4 ( 2 avg)
% 7.32/7.45 % Maximal term depth : 2 ( 1 avg)
% 7.32/7.45 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 7.32/7.45 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 7.32/7.45 % Number of variables : 24 ( 0 sgn)
% 7.32/7.45 % SPC : CNF_UNS_RFO_NEQ_HRN
% 7.32/7.45
% 7.32/7.45 % Comments :
% 7.32/7.45 %--------------------------------------------------------------------------
% 7.32/7.45 %----Include Veroff's minimal axiom set
% 7.32/7.45 include('Axioms/GRP005-0.ax').
% 7.32/7.45 %--------------------------------------------------------------------------
% 7.32/7.45 cnf(prove_right_inverse,negated_conjecture,
% 7.32/7.45 ~ product(a,inverse(a),identity) ).
% 7.32/7.45
% 7.32/7.45 %--------------------------------------------------------------------------
% 7.32/7.45 %-------------------------------------------
% 7.32/7.45 % Proof found
% 7.32/7.45 % SZS status Theorem for theBenchmark
% 7.32/7.45 % SZS output start Proof
% 7.32/7.46 %ClaNum:8(EqnAxiom:0)
% 7.32/7.46 %VarNum:48(SingletonVarNum:24)
% 7.32/7.46 %MaxLitNum:4
% 7.32/7.46 %MaxfuncDepth:1
% 7.32/7.46 %SharedTerms:4
% 7.32/7.46 %goalClause: 4
% 7.32/7.46 %singleGoalClaCount:1
% 7.32/7.46 [4]~P1(a2,f3(a2),a1)
% 7.32/7.46 [1]P1(a1,x11,x11)
% 7.32/7.46 [2]P1(f3(x21),x21,a1)
% 7.32/7.46 [3]P1(x31,x32,f4(x31,x32))
% 7.32/7.46 [5]~P1(x51,x52,x54)+P1(x51,x52,x53)+~P2(x54,x53)
% 7.32/7.46 [6]~P1(x63,x64,x61)+P2(x61,x62)+~P1(x63,x64,x62)
% 7.32/7.46 [7]~P1(x76,x74,x71)+P1(x71,x72,x73)+~P1(x74,x72,x75)+~P1(x76,x75,x73)
% 7.32/7.46 [8]~P1(x81,x86,x84)+P1(x81,x82,x83)+~P1(x84,x85,x83)+~P1(x86,x85,x82)
% 7.32/7.46 %EqnAxiom
% 7.32/7.46
% 7.32/7.46 %-------------------------------------------
% 7.32/7.46 cnf(11,plain,
% 7.32/7.46 (P1(f4(f3(x111),a1),x111,a1)),
% 7.32/7.46 inference(scs_inference,[],[1,3,2,6,7])).
% 7.32/7.46 cnf(13,plain,
% 7.32/7.46 (P1(x131,x132,f4(x131,x132))),
% 7.32/7.46 inference(rename_variables,[],[3])).
% 7.32/7.46 cnf(15,plain,
% 7.32/7.46 (P1(a1,f4(a1,a1),a1)),
% 7.32/7.46 inference(scs_inference,[],[1,3,13,2,6,7,8])).
% 7.32/7.46 cnf(20,plain,
% 7.32/7.46 (P2(a1,f4(a1,f4(a1,a1)))),
% 7.32/7.46 inference(scs_inference,[],[15,3,6])).
% 7.32/7.46 cnf(21,plain,
% 7.32/7.46 (P1(x211,x212,f4(x211,x212))),
% 7.32/7.46 inference(rename_variables,[],[3])).
% 7.32/7.46 cnf(25,plain,
% 7.32/7.46 (P1(x251,x252,f4(x251,x252))),
% 7.32/7.46 inference(rename_variables,[],[3])).
% 7.32/7.46 cnf(27,plain,
% 7.32/7.46 (P1(a1,f4(f4(a1,a1),f4(a1,a1)),a1)),
% 7.32/7.46 inference(scs_inference,[],[15,3,21,25,2,6,7,8])).
% 7.32/7.46 cnf(30,plain,
% 7.32/7.46 (P2(f4(f3(x301),x301),a1)),
% 7.32/7.46 inference(scs_inference,[],[3,2,6])).
% 7.32/7.46 cnf(36,plain,
% 7.32/7.46 (P2(a1,f4(f4(a1,a1),f4(a1,a1)))),
% 7.32/7.46 inference(scs_inference,[],[27,1,6])).
% 7.32/7.46 cnf(45,plain,
% 7.32/7.46 (P1(a1,x451,x451)),
% 7.32/7.46 inference(rename_variables,[],[1])).
% 7.32/7.46 cnf(47,plain,
% 7.32/7.46 (P1(a1,x471,f4(f4(a1,a1),x471))),
% 7.32/7.46 inference(scs_inference,[],[15,36,3,1,45,5,6,7])).
% 7.32/7.46 cnf(79,plain,
% 7.32/7.46 (P1(a1,x791,x791)),
% 7.32/7.46 inference(rename_variables,[],[1])).
% 7.32/7.46 cnf(81,plain,
% 7.32/7.46 (P2(x811,f4(a1,x811))),
% 7.32/7.46 inference(scs_inference,[],[1,79,3,30,5,6])).
% 7.32/7.46 cnf(91,plain,
% 7.32/7.46 (P1(a1,x911,x911)),
% 7.32/7.46 inference(rename_variables,[],[1])).
% 7.32/7.46 cnf(93,plain,
% 7.32/7.46 (P2(x931,f4(f4(a1,a1),x931))),
% 7.32/7.46 inference(scs_inference,[],[1,91,47,20,5,6])).
% 7.32/7.46 cnf(102,plain,
% 7.32/7.46 (P1(a1,a1,f4(f4(a1,a1),f4(a1,a1)))),
% 7.32/7.46 inference(scs_inference,[],[1,36,5])).
% 7.32/7.46 cnf(110,plain,
% 7.32/7.46 (P2(a1,f4(f3(x1101),x1101))),
% 7.32/7.46 inference(scs_inference,[],[2,3,93,5,6])).
% 7.32/7.46 cnf(111,plain,
% 7.32/7.46 (P1(x1111,x1112,f4(x1111,x1112))),
% 7.32/7.46 inference(rename_variables,[],[3])).
% 7.32/7.47 cnf(113,plain,
% 7.32/7.47 (P1(f3(x1131),f4(x1131,a1),f4(f4(a1,a1),f4(a1,a1)))),
% 7.32/7.47 inference(scs_inference,[],[2,102,3,111,93,5,6,8])).
% 7.32/7.47 cnf(125,plain,
% 7.32/7.47 (P1(f3(x1251),x1251,f4(f3(x1252),x1252))),
% 7.32/7.47 inference(scs_inference,[],[2,110,5])).
% 7.32/7.47 cnf(138,plain,
% 7.32/7.47 (P1(f3(x1381),x1381,f4(a1,f4(a1,a1)))),
% 7.32/7.47 inference(scs_inference,[],[2,20,5])).
% 7.32/7.47 cnf(150,plain,
% 7.32/7.47 (P1(f3(x1501),x1501,f4(f4(a1,a1),f4(a1,a1)))),
% 7.32/7.47 inference(scs_inference,[],[2,36,5])).
% 7.32/7.47 cnf(186,plain,
% 7.32/7.47 (P1(x1861,x1862,f4(x1861,x1862))),
% 7.32/7.47 inference(rename_variables,[],[3])).
% 7.32/7.47 cnf(188,plain,
% 7.32/7.47 (P1(x1881,x1882,f4(f4(a1,a1),f4(x1881,x1882)))),
% 7.32/7.47 inference(scs_inference,[],[3,186,47,93,6,5])).
% 7.32/7.47 cnf(199,plain,
% 7.32/7.47 (P2(f4(a1,x1991),x1991)),
% 7.32/7.47 inference(scs_inference,[],[3,1,81,5,6])).
% 7.32/7.47 cnf(216,plain,
% 7.32/7.47 (P2(f4(f4(a1,a1),f4(a1,x2161)),x2161)),
% 7.32/7.47 inference(scs_inference,[],[188,1,6])).
% 7.32/7.47 cnf(217,plain,
% 7.32/7.47 (P1(a1,x2171,x2171)),
% 7.32/7.47 inference(rename_variables,[],[1])).
% 7.32/7.47 cnf(218,plain,
% 7.32/7.47 (P1(x2181,x2182,f4(f4(a1,a1),f4(x2181,x2182)))),
% 7.32/7.47 inference(rename_variables,[],[188])).
% 7.32/7.47 cnf(220,plain,
% 7.32/7.47 (~P1(f4(f4(a1,a1),f4(a2,a1)),f3(a2),a1)),
% 7.42/7.47 inference(scs_inference,[],[4,188,218,1,217,6,8])).
% 7.42/7.47 cnf(233,plain,
% 7.42/7.47 (P1(f4(f3(x2331),a1),x2331,f4(a1,a1))),
% 7.42/7.47 inference(scs_inference,[],[11,81,5])).
% 7.42/7.47 cnf(305,plain,
% 7.42/7.47 (P1(a1,f4(a1,x3051),x3051)),
% 7.42/7.47 inference(scs_inference,[],[47,3,216,6,5])).
% 7.42/7.47 cnf(306,plain,
% 7.42/7.47 (P1(a1,x3061,f4(f4(a1,a1),x3061))),
% 7.42/7.47 inference(rename_variables,[],[47])).
% 7.42/7.47 cnf(308,plain,
% 7.42/7.47 (~P1(f4(a2,a1),f3(a2),f4(a1,a1))),
% 7.42/7.47 inference(scs_inference,[],[47,306,3,220,216,6,5,7])).
% 7.42/7.47 cnf(332,plain,
% 7.42/7.47 (~P1(f4(a1,a2),f3(a2),a1)),
% 7.42/7.47 inference(scs_inference,[],[4,305,1,47,6,7])).
% 7.42/7.47 cnf(394,plain,
% 7.42/7.47 (P1(f3(x3941),f4(x3941,a1),a1)),
% 7.42/7.47 inference(scs_inference,[],[113,216,5])).
% 7.42/7.47 cnf(555,plain,
% 7.42/7.47 (~P1(f4(a2,a1),f3(a2),f4(a1,f4(a1,a1)))),
% 7.42/7.47 inference(scs_inference,[],[308,199,5])).
% 7.42/7.47 cnf(589,plain,
% 7.42/7.47 (~P1(f4(a1,a2),f3(a2),f4(f4(a1,a1),f4(a1,a1)))),
% 7.42/7.47 inference(scs_inference,[],[332,216,5])).
% 7.42/7.47 cnf(708,plain,
% 7.42/7.47 (~P1(f3(f3(a2)),a1,f4(a1,a2))),
% 7.42/7.47 inference(scs_inference,[],[1,589,150,7])).
% 7.42/7.47 cnf(715,plain,
% 7.42/7.47 (P1(f3(x7151),x7151,f4(a1,f4(a1,a1)))),
% 7.42/7.47 inference(rename_variables,[],[138])).
% 7.42/7.47 cnf(717,plain,
% 7.42/7.47 (~P1(f3(f3(a2)),a1,f4(a2,a1))),
% 7.42/7.47 inference(scs_inference,[],[1,555,138,715,394,708,8,7])).
% 7.42/7.47 cnf(721,plain,
% 7.42/7.47 (~P1(f4(f3(x7211),x7211),f4(a2,a1),f4(a2,a1))),
% 7.42/7.47 inference(scs_inference,[],[125,394,717,8])).
% 7.42/7.47 cnf(797,plain,
% 7.42/7.47 (P1(f3(a1),f4(f4(a1,a1),f4(a1,x7971)),x7971)),
% 7.42/7.47 inference(scs_inference,[],[2,305,47,8])).
% 7.42/7.47 cnf(932,plain,
% 7.42/7.47 (~P1(f4(f3(x9321),x9321),f4(a2,a1),f4(a2,a1))),
% 7.42/7.47 inference(rename_variables,[],[721])).
% 7.42/7.47 cnf(935,plain,
% 7.42/7.47 ($false),
% 7.42/7.47 inference(scs_inference,[],[721,932,125,233,188,1,797,8,7]),
% 7.42/7.47 ['proof']).
% 7.42/7.47 % SZS output end Proof
% 7.42/7.47 % Total time :6.850000s
%------------------------------------------------------------------------------