%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP031-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 : 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:33 EDT 2024
% Result : Unsatisfiable 28.47s 28.53s
% Output : CNFRefutation 28.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP031-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 : 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 13:12:09 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 28.47/28.52 %-------------------------------------------
% 28.47/28.52 % File :CSE---1.7
% 28.47/28.52 % Problem :theBenchmark
% 28.47/28.52 % Transform :cnf
% 28.47/28.52 % Format :tptp:raw
% 28.47/28.52 % Command :java -jar mcs_scs.jar %d %s
% 28.47/28.52
% 28.47/28.52 % Result :Theorem 27.910000s
% 28.47/28.52 % Output :CNFRefutation 27.910000s
% 28.47/28.52 %-------------------------------------------
% 28.47/28.52 %--------------------------------------------------------------------------
% 28.47/28.52 % File : GRP031-2 : TPTP v8.2.0. Released v1.0.0.
% 28.47/28.52 % Domain : Group Theory (Semigroups)
% 28.47/28.52 % Problem : In semigroups, left inverse and id => right inverse exists
% 28.47/28.52 % Version : [MOW76] axioms : Reduced > Incomplete.
% 28.47/28.52 % English : If there are right inverses and right identity, then every
% 28.47/28.52 % element has a left inverse.
% 28.47/28.52
% 28.47/28.52 % Refs : [LS74] Lawrence & Starkey (1974), Experimental tests of resol
% 28.47/28.52 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 28.47/28.52 % Source : [SPRFN]
% 28.47/28.52 % Names : ls23 [LS74]
% 28.47/28.52 % : ls23 [WM76]
% 28.47/28.52
% 28.47/28.52 % Status : Unsatisfiable
% 28.47/28.52 % 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.00 v2.4.0, 0.14 v2.3.0, 0.00 v2.2.1, 0.11 v2.1.0, 0.00 v2.0.0
% 28.47/28.52 % Syntax : Number of clauses : 7 ( 4 unt; 0 nHn; 4 RR)
% 28.47/28.52 % Number of literals : 15 ( 0 equ; 9 neg)
% 28.47/28.52 % Maximal clause size : 4 ( 2 avg)
% 28.47/28.52 % Maximal term depth : 2 ( 1 avg)
% 28.47/28.52 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 28.47/28.52 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 28.47/28.52 % Number of variables : 21 ( 1 sgn)
% 28.47/28.52 % SPC : CNF_UNS_RFO_NEQ_HRN
% 28.47/28.52
% 28.47/28.52 % Comments : This can also be viewed as a group theory problem, showing
% 28.47/28.52 % that the left inverse axiom is dependant on the rest of the
% 28.47/28.52 % axiom set; i.e., if there is a right inverse then there
% 28.47/28.52 % is a left inverse.
% 28.47/28.52 %--------------------------------------------------------------------------
% 28.47/28.52 %----Don't include semi-group axioms because most equality is missing
% 28.47/28.52 %include('Axioms/GRP002-0.ax').
% 28.47/28.52 %--------------------------------------------------------------------------
% 28.47/28.52 %----This axiom is called closure or totality in some axiomatisations
% 28.47/28.53 cnf(total_function1,axiom,
% 28.47/28.53 product(X,Y,multiply(X,Y)) ).
% 28.47/28.53
% 28.47/28.53 %----This axiom is called well_definedness in some axiomatisations
% 28.47/28.53 cnf(total_function2,axiom,
% 28.47/28.53 ( ~ product(X,Y,Z)
% 28.47/28.53 | ~ product(X,Y,W)
% 28.47/28.53 | equalish(Z,W) ) ).
% 28.47/28.53
% 28.47/28.53 cnf(associativity1,axiom,
% 28.47/28.53 ( ~ product(X,Y,U)
% 28.47/28.53 | ~ product(Y,Z,V)
% 28.47/28.53 | ~ product(U,Z,W)
% 28.47/28.53 | product(X,V,W) ) ).
% 28.47/28.53
% 28.47/28.53 cnf(associativity2,axiom,
% 28.47/28.53 ( ~ product(X,Y,U)
% 28.47/28.53 | ~ product(Y,Z,V)
% 28.47/28.53 | ~ product(X,V,W)
% 28.47/28.53 | product(U,Z,W) ) ).
% 28.47/28.53
% 28.47/28.53 cnf(right_inverse,hypothesis,
% 28.47/28.53 product(A,inverse(A),identity) ).
% 28.47/28.53
% 28.47/28.53 cnf(right_identity,hypothesis,
% 28.47/28.53 product(A,identity,A) ).
% 28.47/28.53
% 28.47/28.53 cnf(prove_a_has_a_left_inverse,negated_conjecture,
% 28.47/28.53 ~ product(A,a,identity) ).
% 28.47/28.53
% 28.47/28.53 %--------------------------------------------------------------------------
% 28.47/28.53 %-------------------------------------------
% 28.47/28.53 % Proof found
% 28.47/28.53 % SZS status Theorem for theBenchmark
% 28.47/28.53 % SZS output start Proof
% 28.47/28.53 %ClaNum:7(EqnAxiom:0)
% 28.47/28.53 %VarNum:41(SingletonVarNum:21)
% 28.47/28.53 %MaxLitNum:4
% 28.47/28.53 %MaxfuncDepth:1
% 28.47/28.53 %SharedTerms:2
% 28.47/28.53 %goalClause: 4
% 28.47/28.53 %singleGoalClaCount:1
% 28.47/28.53 [1]P1(x11,a1,x11)
% 28.47/28.53 [4]~P1(x41,a2,a1)
% 28.47/28.53 [2]P1(x21,f3(x21),a1)
% 28.47/28.53 [3]P1(x31,x32,f4(x31,x32))
% 28.47/28.53 [5]~P1(x53,x54,x51)+P2(x51,x52)+~P1(x53,x54,x52)
% 28.47/28.53 [6]~P1(x66,x64,x61)+P1(x61,x62,x63)+~P1(x64,x62,x65)+~P1(x66,x65,x63)
% 28.47/28.53 [7]~P1(x71,x76,x74)+P1(x71,x72,x73)+~P1(x74,x75,x73)+~P1(x76,x75,x72)
% 28.47/28.53 %EqnAxiom
% 28.47/28.53
% 28.47/28.53 %-------------------------------------------
% 28.47/28.53 cnf(10,plain,
% 28.47/28.53 (P1(x101,a1,x101)),
% 28.47/28.53 inference(rename_variables,[],[1])).
% 28.47/28.53 cnf(12,plain,
% 28.47/28.53 (P1(x121,f4(a1,a1),x121)),
% 28.47/28.53 inference(scs_inference,[],[4,1,10,3,2,6,7])).
% 28.47/28.53 cnf(17,plain,
% 28.47/28.53 (P1(x171,f4(a1,a1),x171)),
% 28.47/28.53 inference(rename_variables,[],[12])).
% 28.47/28.53 cnf(20,plain,
% 28.47/28.53 (P1(x201,f4(f4(a1,a1),f4(a1,a1)),x201)),
% 28.47/28.53 inference(scs_inference,[],[4,12,17,3,6,7])).
% 28.47/28.53 cnf(24,plain,
% 28.47/28.53 (P1(x241,f3(x241),a1)),
% 28.47/28.53 inference(rename_variables,[],[2])).
% 28.47/28.54 cnf(25,plain,
% 28.47/28.54 (P1(x251,f4(f4(a1,a1),f4(a1,a1)),x251)),
% 28.47/28.54 inference(rename_variables,[],[20])).
% 28.47/28.54 cnf(27,plain,
% 28.47/28.54 (P1(f4(f4(a1,a1),f4(a1,a1)),a1,a1)),
% 28.47/28.54 inference(scs_inference,[],[4,20,25,2,24,6,7])).
% 28.47/28.54 cnf(31,plain,
% 28.47/28.54 (P1(a1,a1,f4(f4(a1,a1),f4(a1,a1)))),
% 28.47/28.54 inference(scs_inference,[],[27,12,3,6])).
% 28.47/28.54 cnf(43,plain,
% 28.47/28.54 (P1(x431,f3(x431),f4(f4(a1,a1),f4(a1,a1)))),
% 28.47/28.54 inference(scs_inference,[],[2,31,1,7])).
% 28.47/28.54 cnf(77,plain,
% 28.47/28.54 (P1(x771,f4(f4(a1,a1),f4(a1,a1)),x771)),
% 28.47/28.54 inference(rename_variables,[],[20])).
% 28.47/28.54 cnf(78,plain,
% 28.47/28.54 (P1(x781,x782,f4(x781,x782))),
% 28.47/28.54 inference(rename_variables,[],[3])).
% 28.47/28.54 cnf(80,plain,
% 28.47/28.54 (~P1(x801,a2,f4(f4(a1,a1),f4(a1,a1)))),
% 28.47/28.54 inference(scs_inference,[],[3,78,4,20,77,7,6])).
% 28.47/28.54 cnf(85,plain,
% 28.47/28.54 (P1(a1,f4(a1,a1),f4(a1,a1))),
% 28.47/28.54 inference(scs_inference,[],[3,1,7])).
% 28.47/28.54 cnf(103,plain,
% 28.47/28.54 (P1(x1031,f4(a1,a1),f4(x1031,a1))),
% 28.47/28.54 inference(scs_inference,[],[3,85,12,7])).
% 28.47/28.54 cnf(107,plain,
% 28.47/28.54 (P1(x1071,f4(x1072,a1),f4(x1071,x1072))),
% 28.47/28.54 inference(scs_inference,[],[3,103,12,7])).
% 28.47/28.54 cnf(208,plain,
% 28.47/28.54 (~P1(f4(x2081,a2),a1,f4(f4(a1,a1),f4(a1,a1)))),
% 28.47/28.54 inference(scs_inference,[],[80,1,3,7])).
% 28.47/28.54 cnf(647,plain,
% 28.47/28.54 (~P1(f4(x6471,a2),x6472,x6472)),
% 28.47/28.54 inference(scs_inference,[],[208,43,2,7])).
% 28.47/28.54 cnf(1420,plain,
% 28.47/28.54 (~P1(f4(x14201,a2),f4(x14202,f4(a1,a1)),x14202)),
% 28.47/28.54 inference(scs_inference,[],[647,3,12,7])).
% 28.47/28.54 cnf(2272,plain,
% 28.47/28.54 (~P1(a2,f4(x22721,f4(a1,a1)),f4(a1,a1))),
% 28.47/28.54 inference(scs_inference,[],[1420,3,12,6])).
% 28.47/28.54 cnf(3127,plain,
% 28.47/28.54 (~P1(f4(a2,x31271),f4(f4(a1,a1),a1),f4(a1,a1))),
% 28.47/28.54 inference(scs_inference,[],[2272,3,107,7])).
% 28.47/28.54 cnf(3801,plain,
% 28.47/28.54 (~P1(f4(a2,x38011),a1,f4(a1,a1))),
% 28.47/28.54 inference(scs_inference,[],[3127,3,12,7])).
% 28.47/28.54 cnf(4234,plain,
% 28.47/28.54 (P1(x42341,x42342,f4(x42341,x42342))),
% 28.47/28.54 inference(rename_variables,[],[3])).
% 28.47/28.54 cnf(4236,plain,
% 28.47/28.54 (~P1(a1,a1,f4(a2,x42361))),
% 28.47/28.54 inference(scs_inference,[],[3801,3,4234,12,1,7,6])).
% 28.47/28.54 cnf(4526,plain,
% 28.47/28.54 ($false),
% 28.47/28.54 inference(scs_inference,[],[4236,31,3,12,1,2,7,6]),
% 28.47/28.54 ['proof']).
% 28.47/28.54 % SZS output end Proof
% 28.47/28.54 % Total time :27.910000s
%------------------------------------------------------------------------------