%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP033-4 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n024.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:34 EDT 2024
% Result : Unsatisfiable 0.14s 0.52s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : GRP033-4 : TPTP v8.2.0. Released v1.0.0.
% 0.05/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.28 % Computer : n024.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Thu Jun 20 10:37:09 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.14/0.49 start to proof:theBenchmark
% 0.14/0.52 %-------------------------------------------
% 0.14/0.52 % File :CSE---1.7
% 0.14/0.52 % Problem :theBenchmark
% 0.14/0.52 % Transform :cnf
% 0.14/0.52 % Format :tptp:raw
% 0.14/0.52 % Command :java -jar mcs_scs.jar %d %s
% 0.14/0.52
% 0.14/0.52 % Result :Theorem 0.000000s
% 0.14/0.52 % Output :CNFRefutation 0.000000s
% 0.14/0.52 %-------------------------------------------
% 0.14/0.52 %--------------------------------------------------------------------------
% 0.14/0.52 % File : GRP033-4 : TPTP v8.2.0. Released v1.0.0.
% 0.14/0.52 % Domain : Group Theory (Subgroups)
% 0.14/0.52 % Problem : In subgroups, the identity is the group identity
% 0.14/0.52 % Version : [Wos65] axioms.
% 0.14/0.52 % English :
% 0.14/0.52
% 0.14/0.52 % Refs : [Wos65] Wos (1965), Unpublished Note
% 0.14/0.52 % Source : [SPRFN]
% 0.14/0.52 % Names : Problem 13 [Wos65]
% 0.14/0.52
% 0.14/0.52 % Status : Unsatisfiable
% 0.14/0.52 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.0.0
% 0.14/0.52 % Syntax : Number of clauses : 12 ( 6 unt; 0 nHn; 7 RR)
% 0.14/0.52 % Number of literals : 26 ( 1 equ; 15 neg)
% 0.14/0.52 % Maximal clause size : 4 ( 2 avg)
% 0.14/0.52 % Maximal term depth : 2 ( 1 avg)
% 0.14/0.52 % Number of predicates : 3 ( 2 usr; 0 prp; 1-3 aty)
% 0.14/0.52 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 0.14/0.52 % Number of variables : 27 ( 0 sgn)
% 0.14/0.52 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.14/0.52
% 0.14/0.52 % Comments :
% 0.14/0.52 %--------------------------------------------------------------------------
% 0.14/0.52 %----Include group theory axioms
% 0.14/0.52 include('Axioms/GRP003-0.ax').
% 0.14/0.52 %----Include sub-group theory axioms
% 0.14/0.52 include('Axioms/GRP003-2.ax').
% 0.14/0.52 %--------------------------------------------------------------------------
% 0.14/0.52 %----j(A) is an element for which A is identity. In a subgroup this can
% 0.14/0.52 %----be any element.
% 0.14/0.52
% 0.14/0.52 cnf(a_is_in_subgroup,hypothesis,
% 0.14/0.52 subgroup_member(a) ).
% 0.14/0.52
% 0.14/0.52 cnf(subgr2_clause1,hypothesis,
% 0.14/0.52 ( ~ subgroup_member(A)
% 0.14/0.52 | subgroup_member(j(A)) ) ).
% 0.14/0.52
% 0.14/0.52 cnf(prove_subgr2,negated_conjecture,
% 0.14/0.52 ( ~ product(j(A),A,j(A))
% 0.14/0.52 | ~ product(A,j(A),j(A))
% 0.14/0.52 | ~ subgroup_member(A) ) ).
% 0.14/0.52
% 0.14/0.52 %--------------------------------------------------------------------------
% 0.14/0.52 %-------------------------------------------
% 0.14/0.52 % Proof found
% 0.14/0.52 % SZS status Theorem for theBenchmark
% 0.14/0.52 % SZS output start Proof
% 0.14/0.53 %ClaNum:23(EqnAxiom:11)
% 0.14/0.53 %VarNum:59(SingletonVarNum:27)
% 0.14/0.53 %MaxLitNum:4
% 0.14/0.53 %MaxfuncDepth:1
% 0.14/0.53 %SharedTerms:3
% 0.14/0.53 %goalClause: 21
% 0.14/0.53 [12]P1(a1)
% 0.14/0.53 [13]P2(x131,a2,x131)
% 0.14/0.53 [14]P2(a2,x141,x141)
% 0.14/0.53 [15]P2(x151,f3(x151),a2)
% 0.14/0.53 [16]P2(f3(x161),x161,a2)
% 0.14/0.53 [17]P2(x171,x172,f4(x171,x172))
% 0.14/0.53 [18]~P1(x181)+P1(f5(x181))
% 0.14/0.53 [21]~P1(x211)+~P2(x211,f5(x211),f5(x211))+~P2(f5(x211),x211,f5(x211))
% 0.14/0.53 [20]~P2(x203,x204,x201)+E(x201,x202)+~P2(x203,x204,x202)
% 0.14/0.53 [19]P1(x191)+~P1(x192)+~P1(x193)+~P2(x193,f3(x192),x191)
% 0.14/0.53 [22]~P2(x226,x224,x221)+P2(x221,x222,x223)+~P2(x224,x222,x225)+~P2(x226,x225,x223)
% 0.14/0.53 [23]~P2(x231,x236,x234)+P2(x231,x232,x233)+~P2(x234,x235,x233)+~P2(x236,x235,x232)
% 0.14/0.53 %EqnAxiom
% 0.14/0.53 [1]E(x11,x11)
% 0.14/0.53 [2]E(x22,x21)+~E(x21,x22)
% 0.14/0.53 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.14/0.53 [4]~E(x41,x42)+E(f3(x41),f3(x42))
% 0.14/0.53 [5]~E(x51,x52)+E(f5(x51),f5(x52))
% 0.14/0.53 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 0.14/0.53 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 0.14/0.53 [8]~P1(x81)+P1(x82)+~E(x81,x82)
% 0.14/0.53 [9]P2(x92,x93,x94)+~E(x91,x92)+~P2(x91,x93,x94)
% 0.14/0.53 [10]P2(x103,x102,x104)+~E(x101,x102)+~P2(x103,x101,x104)
% 0.14/0.53 [11]P2(x113,x114,x112)+~E(x111,x112)+~P2(x113,x114,x111)
% 0.14/0.53
% 0.14/0.53 %-------------------------------------------
% 0.14/0.53 cnf(25,plain,
% 0.14/0.53 (P2(a2,x251,x251)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(26,plain,
% 0.14/0.53 (P2(x261,a2,x261)),
% 0.14/0.53 inference(rename_variables,[],[13])).
% 0.14/0.53 cnf(28,plain,
% 0.14/0.53 (E(x281,f4(a2,x281))),
% 0.14/0.53 inference(scs_inference,[],[14,25,13,17,21,20])).
% 0.14/0.53 cnf(29,plain,
% 0.14/0.53 (P2(x291,x292,f4(x291,x292))),
% 0.14/0.53 inference(rename_variables,[],[17])).
% 0.14/0.53 cnf(32,plain,
% 0.14/0.53 (P2(a2,x321,x321)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(34,plain,
% 0.14/0.53 (P2(a2,x341,x341)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(35,plain,
% 0.14/0.53 (P2(x351,f3(x351),f4(a2,a2))),
% 0.14/0.53 inference(scs_inference,[],[14,25,32,13,17,15,21,20,9,10,11])).
% 0.14/0.53 cnf(40,plain,
% 0.14/0.53 (P2(a2,x401,x401)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(41,plain,
% 0.14/0.53 (P2(x411,a2,x411)),
% 0.14/0.53 inference(rename_variables,[],[13])).
% 0.14/0.53 cnf(49,plain,
% 0.14/0.53 (~P1(f4(a2,a2))),
% 0.14/0.53 inference(scs_inference,[],[12,14,25,32,34,40,13,26,41,17,29,15,16,21,20,9,10,11,19,22,23,2,8])).
% 0.14/0.53 cnf(52,plain,
% 0.14/0.53 (E(x521,f4(a2,x521))),
% 0.14/0.53 inference(rename_variables,[],[28])).
% 0.14/0.53 cnf(54,plain,
% 0.14/0.53 (P2(x541,f3(x541),f4(a2,a2))),
% 0.14/0.53 inference(rename_variables,[],[35])).
% 0.14/0.53 cnf(55,plain,
% 0.14/0.53 (P2(a2,x551,x551)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(58,plain,
% 0.14/0.53 (E(x581,f4(a2,x581))),
% 0.14/0.53 inference(rename_variables,[],[28])).
% 0.14/0.53 cnf(60,plain,
% 0.14/0.53 (P2(a2,x601,x601)),
% 0.14/0.53 inference(rename_variables,[],[14])).
% 0.14/0.53 cnf(63,plain,
% 0.14/0.53 ($false),
% 0.14/0.53 inference(scs_inference,[],[12,49,14,55,60,35,54,28,52,58,2,8,20,11,10,9,19]),
% 0.14/0.53 ['proof']).
% 0.14/0.53 % SZS output end Proof
% 0.14/0.53 % Total time :0.000000s
%------------------------------------------------------------------------------