%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP029-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 : n019.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 0.53s 0.75s
% Output : CNFRefutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP029-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.13/0.33 % Computer : n019.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 11:17:54 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 0.53/0.74 %-------------------------------------------
% 0.53/0.74 % File :CSE---1.7
% 0.53/0.74 % Problem :theBenchmark
% 0.53/0.74 % Transform :cnf
% 0.53/0.74 % Format :tptp:raw
% 0.53/0.74 % Command :java -jar mcs_scs.jar %d %s
% 0.53/0.74
% 0.53/0.74 % Result :Theorem 0.130000s
% 0.53/0.74 % Output :CNFRefutation 0.130000s
% 0.53/0.74 %-------------------------------------------
% 0.53/0.74 %--------------------------------------------------------------------------
% 0.53/0.74 % File : GRP029-2 : TPTP v8.2.0. Released v1.0.0.
% 0.53/0.74 % Domain : Group Theory (Semigroups)
% 0.53/0.74 % Problem : In semigroups, left id and inverse => right id exists
% 0.53/0.74 % Version : [MOW76] axioms : Incomplete.
% 0.53/0.74 % English : If there are a left identity and left inverse, then there
% 0.53/0.74 % is a right identity element.
% 0.53/0.74
% 0.53/0.74 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 0.53/0.74 % Source : [SPRFN]
% 0.53/0.74 % Names : G5 [MOW76]
% 0.53/0.74
% 0.53/0.74 % Status : Unsatisfiable
% 0.53/0.74 % 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.2.1, 0.11 v2.1.0, 0.14 v2.0.0
% 0.53/0.74 % Syntax : Number of clauses : 16 ( 5 unt; 0 nHn; 10 RR)
% 0.53/0.74 % Number of literals : 36 ( 0 equ; 21 neg)
% 0.53/0.74 % Maximal clause size : 4 ( 2 avg)
% 0.53/0.74 % Maximal term depth : 2 ( 1 avg)
% 0.53/0.74 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 0.53/0.74 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% 0.53/0.74 % Number of variables : 47 ( 0 sgn)
% 0.53/0.74 % SPC : CNF_UNS_RFO_NEQ_HRN
% 0.53/0.74
% 0.53/0.74 % Comments : This may also be viewed as a group theory problem, to prove
% 0.53/0.74 % that the right identity axiom is dependant on the rest of the
% 0.53/0.74 % axiom set; i.e., each element has a right identity. Note that
% 0.53/0.74 % this is a corollary to proving that the right identity axiom
% 0.53/0.74 % is dependant on the rest of the axiom set, but also that the
% 0.53/0.74 % proof is different due to the introduction of a skolem
% 0.53/0.74 % function for the right identity of each element of the group.
% 0.53/0.74 % : The not_right_identity substitution axioms are missing.
% 0.53/0.74 %--------------------------------------------------------------------------
% 0.53/0.74 %----Include semi-group axioms
% 0.53/0.74 %include('Axioms/GRP002-0.ax').
% 0.53/0.74 %--------------------------------------------------------------------------
% 0.53/0.74 cnf(reflexivity,axiom,
% 0.53/0.74 equalish(X,X) ).
% 0.53/0.74
% 0.53/0.74 cnf(symmetry,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | equalish(Y,X) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(transitivity,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | ~ equalish(Y,Z)
% 0.53/0.74 | equalish(X,Z) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(multiply_substitution1,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(multiply_substitution2,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | equalish(multiply(W,X),multiply(W,Y)) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(product_substitution1,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | ~ product(X,W,Z)
% 0.53/0.74 | product(Y,W,Z) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(product_substitution2,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | ~ product(W,X,Z)
% 0.53/0.74 | product(W,Y,Z) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(product_substitution3,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.74 | ~ product(W,Z,X)
% 0.53/0.74 | product(W,Z,Y) ) ).
% 0.53/0.74
% 0.53/0.74 cnf(inverse_substitution,axiom,
% 0.53/0.74 ( ~ equalish(X,Y)
% 0.53/0.75 | equalish(inverse(X),inverse(Y)) ) ).
% 0.53/0.75
% 0.53/0.75 %----This axiom is called closure or totality in some axiomatisations
% 0.53/0.75 cnf(total_function1,axiom,
% 0.53/0.75 product(X,Y,multiply(X,Y)) ).
% 0.53/0.75
% 0.53/0.75 %----This axiom is called well_definedness in some axiomatisations
% 0.53/0.75 cnf(total_function2,axiom,
% 0.53/0.75 ( ~ product(X,Y,Z)
% 0.53/0.75 | ~ product(X,Y,W)
% 0.53/0.75 | equalish(Z,W) ) ).
% 0.53/0.75
% 0.53/0.75 cnf(associativity1,axiom,
% 0.53/0.75 ( ~ product(X,Y,U)
% 0.53/0.75 | ~ product(Y,Z,V)
% 0.53/0.75 | ~ product(U,Z,W)
% 0.53/0.75 | product(X,V,W) ) ).
% 0.53/0.75
% 0.53/0.75 cnf(associativity2,axiom,
% 0.53/0.75 ( ~ product(X,Y,U)
% 0.53/0.75 | ~ product(Y,Z,V)
% 0.53/0.75 | ~ product(X,V,W)
% 0.53/0.75 | product(U,Z,W) ) ).
% 0.53/0.75
% 0.53/0.75 cnf(left_identity,axiom,
% 0.53/0.75 product(identity,A,A) ).
% 0.53/0.75
% 0.53/0.75 cnf(left_inverse,axiom,
% 0.53/0.75 product(inverse(A),A,identity) ).
% 0.53/0.75
% 0.53/0.75 cnf(prove_there_is_a_right_identity,negated_conjecture,
% 0.53/0.75 ~ product(not_right_identity(A),A,not_right_identity(A)) ).
% 0.53/0.75
% 0.53/0.75 %--------------------------------------------------------------------------
% 0.53/0.75 %-------------------------------------------
% 0.53/0.75 % Proof found
% 0.53/0.75 % SZS status Theorem for theBenchmark
% 0.53/0.75 % SZS output start Proof
% 0.53/0.75 %ClaNum:16(EqnAxiom:0)
% 0.53/0.75 %VarNum:95(SingletonVarNum:47)
% 0.53/0.75 %MaxLitNum:4
% 0.53/0.75 %MaxfuncDepth:1
% 0.53/0.75 %SharedTerms:1
% 0.53/0.75 %goalClause: 5
% 0.53/0.75 %singleGoalClaCount:1
% 0.53/0.75 [1]P1(x11,x11)
% 0.53/0.75 [2]P2(a1,x21,x21)
% 0.53/0.75 [3]P2(f2(x31),x31,a1)
% 0.53/0.75 [5]~P2(f4(x51),x51,f4(x51))
% 0.53/0.75 [4]P2(x41,x42,f3(x41,x42))
% 0.53/0.75 [6]~P1(x62,x61)+P1(x61,x62)
% 0.53/0.75 [7]~P1(x71,x72)+P1(f2(x71),f2(x72))
% 0.53/0.75 [9]~P1(x92,x93)+P1(f3(x91,x92),f3(x91,x93))
% 0.53/0.75 [10]~P1(x101,x103)+P1(f3(x101,x102),f3(x103,x102))
% 0.53/0.75 [8]~P1(x81,x83)+P1(x81,x82)+~P1(x83,x82)
% 0.53/0.75 [11]~P2(x111,x112,x114)+P2(x111,x112,x113)+~P1(x114,x113)
% 0.53/0.75 [12]~P2(x121,x124,x123)+P2(x121,x122,x123)+~P1(x124,x122)
% 0.53/0.75 [13]~P2(x134,x132,x133)+P2(x131,x132,x133)+~P1(x134,x131)
% 0.53/0.75 [14]~P2(x143,x144,x141)+P1(x141,x142)+~P2(x143,x144,x142)
% 0.53/0.75 [15]~P2(x156,x154,x151)+P2(x151,x152,x153)+~P2(x154,x152,x155)+~P2(x156,x155,x153)
% 0.53/0.75 [16]~P2(x161,x166,x164)+P2(x161,x162,x163)+~P2(x164,x165,x163)+~P2(x166,x165,x162)
% 0.53/0.75 %EqnAxiom
% 0.53/0.75
% 0.53/0.75 %-------------------------------------------
% 0.53/0.75 cnf(17,plain,
% 0.53/0.75 (P1(x171,f3(a1,x171))),
% 0.53/0.75 inference(scs_inference,[],[2,4,14])).
% 0.53/0.75 cnf(18,plain,
% 0.53/0.75 (P2(x181,x182,f3(x181,x182))),
% 0.53/0.75 inference(rename_variables,[],[4])).
% 0.53/0.75 cnf(22,plain,
% 0.53/0.75 (P2(x221,x222,f3(x221,x222))),
% 0.53/0.75 inference(rename_variables,[],[4])).
% 0.53/0.75 cnf(24,plain,
% 0.53/0.75 (P2(a1,f3(a1,a1),a1)),
% 0.53/0.75 inference(scs_inference,[],[2,4,18,22,3,14,15,16])).
% 0.53/0.75 cnf(27,plain,
% 0.53/0.75 (P2(a1,x271,x271)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(29,plain,
% 0.53/0.75 (P2(f3(a1,a1),x291,x291)),
% 0.53/0.75 inference(scs_inference,[],[2,27,4,18,22,3,14,15,16,13])).
% 0.53/0.75 cnf(31,plain,
% 0.53/0.75 (P2(f3(a1,a1),x311,f3(a1,x311))),
% 0.53/0.75 inference(scs_inference,[],[29,17,11])).
% 0.53/0.75 cnf(32,plain,
% 0.53/0.75 (P1(x321,f3(a1,x321))),
% 0.53/0.75 inference(rename_variables,[],[17])).
% 0.53/0.75 cnf(34,plain,
% 0.53/0.75 (P2(f3(a1,a1),f3(a1,x341),x341)),
% 0.53/0.75 inference(scs_inference,[],[29,17,32,11,12])).
% 0.53/0.75 cnf(35,plain,
% 0.53/0.75 (P1(x351,f3(a1,x351))),
% 0.53/0.75 inference(rename_variables,[],[17])).
% 0.53/0.75 cnf(37,plain,
% 0.53/0.75 (P1(x371,f3(f3(a1,a1),x371))),
% 0.53/0.75 inference(scs_inference,[],[29,17,32,4,11,12,14])).
% 0.53/0.75 cnf(40,plain,
% 0.53/0.75 (P2(f3(a1,f3(a1,a1)),x401,x401)),
% 0.53/0.75 inference(scs_inference,[],[29,17,32,35,4,11,12,14,13])).
% 0.53/0.75 cnf(53,plain,
% 0.53/0.75 (P1(x531,f3(f3(a1,a1),x531))),
% 0.53/0.75 inference(rename_variables,[],[37])).
% 0.53/0.75 cnf(55,plain,
% 0.53/0.75 (P2(f3(a1,a1),x551,f3(f3(a1,a1),f3(a1,x551)))),
% 0.53/0.75 inference(scs_inference,[],[31,37,53,12,11])).
% 0.53/0.75 cnf(56,plain,
% 0.53/0.75 (P1(x561,f3(f3(a1,a1),x561))),
% 0.53/0.75 inference(rename_variables,[],[37])).
% 0.53/0.75 cnf(58,plain,
% 0.53/0.75 (P1(f3(a1,f3(a1,x581)),x581)),
% 0.53/0.75 inference(scs_inference,[],[31,37,53,34,12,11,14])).
% 0.53/0.75 cnf(59,plain,
% 0.53/0.75 (P2(f3(a1,a1),x591,f3(a1,x591))),
% 0.53/0.75 inference(rename_variables,[],[31])).
% 0.53/0.75 cnf(61,plain,
% 0.53/0.75 (P2(f3(f3(a1,a1),f3(a1,a1)),x611,f3(a1,x611))),
% 0.53/0.75 inference(scs_inference,[],[31,59,37,53,56,34,12,11,14,13])).
% 0.53/0.75 cnf(64,plain,
% 0.53/0.75 (P1(f3(f3(a1,a1),f3(a1,x641)),f3(a1,x641))),
% 0.53/0.75 inference(scs_inference,[],[55,31,14])).
% 0.53/0.75 cnf(68,plain,
% 0.53/0.75 (P2(f3(a1,a1),x681,f3(f3(a1,a1),f3(a1,x681)))),
% 0.53/0.75 inference(rename_variables,[],[55])).
% 0.53/0.75 cnf(71,plain,
% 0.53/0.75 (P2(a1,x711,f3(f3(a1,a1),f3(a1,x711)))),
% 0.53/0.75 inference(scs_inference,[],[55,68,31,24,61,2,14,16,15])).
% 0.53/0.75 cnf(74,plain,
% 0.53/0.75 (P1(f3(f2(x741),x741),a1)),
% 0.53/0.75 inference(scs_inference,[],[4,3,14])).
% 0.53/0.75 cnf(82,plain,
% 0.53/0.75 (P1(f3(f3(a1,a1),f3(a1,x821)),x821)),
% 0.53/0.75 inference(scs_inference,[],[71,2,14])).
% 0.53/0.75 cnf(86,plain,
% 0.53/0.75 (P2(a1,x861,x861)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(89,plain,
% 0.53/0.75 (P2(a1,x891,x891)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(94,plain,
% 0.53/0.75 (P1(x941,f3(f3(a1,a1),f3(a1,x941)))),
% 0.53/0.75 inference(scs_inference,[],[2,86,89,82,64,37,71,12,11,13,14])).
% 0.53/0.75 cnf(99,plain,
% 0.53/0.75 (P2(a1,x991,x991)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(102,plain,
% 0.53/0.75 (P2(f3(f3(a1,a1),f3(a1,a1)),f3(a1,x1021),x1021)),
% 0.53/0.75 inference(scs_inference,[],[2,86,89,99,55,82,64,37,34,71,4,3,12,11,13,14,16,15])).
% 0.53/0.75 cnf(106,plain,
% 0.53/0.75 (P2(a1,f3(a1,f3(a1,x1061)),x1061)),
% 0.53/0.75 inference(scs_inference,[],[2,58,11])).
% 0.53/0.75 cnf(107,plain,
% 0.53/0.75 (P2(a1,x1071,x1071)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(110,plain,
% 0.53/0.75 (P2(a1,x1101,x1101)),
% 0.53/0.75 inference(rename_variables,[],[2])).
% 0.53/0.75 cnf(112,plain,
% 0.53/0.75 (P2(f3(f3(a1,a1),f3(a1,a1)),x1121,x1121)),
% 0.53/0.75 inference(scs_inference,[],[2,107,110,94,58,11,12,13])).
% 0.53/0.75 cnf(115,plain,
% 0.53/0.75 (P1(x1151,f3(a1,f3(a1,x1151)))),
% 0.53/0.75 inference(scs_inference,[],[2,107,110,94,102,58,61,11,12,13,14])).
% 0.53/0.75 cnf(131,plain,
% 0.53/0.75 (P1(f3(a1,x1311),x1311)),
% 0.53/0.75 inference(scs_inference,[],[2,112,74,17,102,12,11,14])).
% 0.53/0.75 cnf(158,plain,
% 0.53/0.75 (P2(f2(x1581),x1581,a1)),
% 0.53/0.75 inference(rename_variables,[],[3])).
% 0.53/0.75 cnf(160,plain,
% 0.53/0.75 (P2(f2(x1601),x1601,f3(a1,f3(a1,a1)))),
% 0.53/0.75 inference(scs_inference,[],[3,158,131,115,17,13,12,11])).
% 0.53/0.75 cnf(163,plain,
% 0.53/0.75 (P1(a1,f3(f2(x1631),x1631))),
% 0.53/0.75 inference(scs_inference,[],[3,158,131,115,17,4,13,12,11,14])).
% 0.53/0.75 cnf(176,plain,
% 0.53/0.75 (P2(f2(x1761),x1761,a1)),
% 0.53/0.75 inference(rename_variables,[],[3])).
% 0.53/0.75 cnf(184,plain,
% 0.53/0.75 ($false),
% 0.53/0.75 inference(scs_inference,[],[3,176,5,160,106,40,163,12,11,16,15]),
% 0.53/0.75 ['proof']).
% 0.53/0.75 % SZS output end Proof
% 0.53/0.75 % Total time :0.130000s
%------------------------------------------------------------------------------