%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP033-3 : TPTP v8.2.0. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n017.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.23s 0.55s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : GRP033-3 : TPTP v8.2.0. Bugfixed v4.0.0.
% 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n017.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu Jun 20 07:17:38 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.23/0.50 start to proof:theBenchmark
% 0.23/0.54 %-------------------------------------------
% 0.23/0.54 % File :CSE---1.7
% 0.23/0.54 % Problem :theBenchmark
% 0.23/0.54 % Transform :cnf
% 0.23/0.54 % Format :tptp:raw
% 0.23/0.54 % Command :java -jar mcs_scs.jar %d %s
% 0.23/0.54
% 0.23/0.54 % Result :Theorem 0.000000s
% 0.23/0.54 % Output :CNFRefutation 0.000000s
% 0.23/0.54 %-------------------------------------------
% 0.23/0.54 %--------------------------------------------------------------------------
% 0.23/0.54 % File : GRP033-3 : TPTP v8.2.0. Bugfixed v4.0.0.
% 0.23/0.54 % Domain : Group Theory (Subgroups)
% 0.23/0.55 % Problem : In subgroups, the identity is the group identity
% 0.23/0.55 % Version : [Wos65] axioms : Reduced > Incomplete.
% 0.23/0.55 % English :
% 0.23/0.55
% 0.23/0.55 % Refs : [Wos65] Wos (1965), Unpublished Note
% 0.23/0.55 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 0.23/0.55 % Source : [SPRFN]
% 0.23/0.55 % Names : Problem 13 [Wos65]
% 0.23/0.55 % : wos13 [WM76]
% 0.23/0.55
% 0.23/0.55 % Status : Unsatisfiable
% 0.23/0.55 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.00 v5.1.0, 0.06 v5.0.0, 0.00 v4.1.0, 0.07 v4.0.1, 0.00 v4.0.0
% 0.23/0.55 % Syntax : Number of clauses : 22 ( 7 unt; 0 nHn; 14 RR)
% 0.23/0.55 % Number of literals : 50 ( 0 equ; 29 neg)
% 0.23/0.55 % Maximal clause size : 4 ( 2 avg)
% 0.23/0.55 % Maximal term depth : 2 ( 1 avg)
% 0.23/0.55 % Number of predicates : 3 ( 3 usr; 0 prp; 1-3 aty)
% 0.23/0.55 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 0.23/0.55 % Number of variables : 55 ( 0 sgn)
% 0.23/0.55 % SPC : CNF_UNS_RFO_NEQ_HRN
% 0.23/0.55
% 0.23/0.55 % Comments : Omits j substitutivity.
% 0.23/0.55 % Bugfixes : v4.0.0 - Removed duplicate clause closure_of_product_and_inverse
% 0.23/0.55 %--------------------------------------------------------------------------
% 0.23/0.55 %----Include group theory axioms
% 0.23/0.55 %include('Axioms/GRP003-0.ax').
% 0.23/0.55 %----Include sub-group theory axioms
% 0.23/0.55 %include('Axioms/GRP003-2.ax').
% 0.23/0.55 %--------------------------------------------------------------------------
% 0.23/0.55 cnf(reflexivity,axiom,
% 0.23/0.55 equalish(X,X) ).
% 0.23/0.55
% 0.23/0.55 cnf(symmetry,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | equalish(Y,X) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(transitivity,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | ~ equalish(Y,Z)
% 0.23/0.55 | equalish(X,Z) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(inverse_substitution,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | equalish(inverse(X),inverse(Y)) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(multiply_substitution1,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | equalish(multiply(X,W),multiply(Y,W)) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(multiply_substitution2,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | equalish(multiply(W,X),multiply(W,Y)) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(product_substitution1,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | ~ product(X,W,Z)
% 0.23/0.55 | product(Y,W,Z) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(product_substitution2,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | ~ product(W,X,Z)
% 0.23/0.55 | product(W,Y,Z) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(product_substitution3,axiom,
% 0.23/0.55 ( ~ equalish(X,Y)
% 0.23/0.55 | ~ product(W,Z,X)
% 0.23/0.55 | product(W,Z,Y) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(subgroup_member_substitution,axiom,
% 0.23/0.55 ( ~ equalish(A,B)
% 0.23/0.55 | ~ subgroup_member(A)
% 0.23/0.55 | subgroup_member(B) ) ).
% 0.23/0.55
% 0.23/0.55 %----j(A) is an element for which A is identity. In a subgroup this can
% 0.23/0.55 %----be any element.
% 0.23/0.55
% 0.23/0.55 %----This subsitution axiom really should be in, but Wos omits it
% 0.23/0.55 % input_clause(j_substitutivity1,axiom,
% 0.23/0.55 % [--equalish(A,B),
% 0.23/0.55 % ++equalish(j(A),j(B))]).
% 0.23/0.55
% 0.23/0.55 cnf(left_identity,axiom,
% 0.23/0.55 product(identity,X,X) ).
% 0.23/0.55
% 0.23/0.55 cnf(right_identity,axiom,
% 0.23/0.55 product(X,identity,X) ).
% 0.23/0.55
% 0.23/0.55 cnf(left_inverse,axiom,
% 0.23/0.55 product(inverse(X),X,identity) ).
% 0.23/0.55
% 0.23/0.55 cnf(right_inverse,axiom,
% 0.23/0.55 product(X,inverse(X),identity) ).
% 0.23/0.55
% 0.23/0.55 %----This axiom is called closure or totality in some axiomatisations
% 0.23/0.55 cnf(total_function1,axiom,
% 0.23/0.55 product(X,Y,multiply(X,Y)) ).
% 0.23/0.55
% 0.23/0.55 %----This axiom is called well_definedness in some axiomatisations
% 0.23/0.55 cnf(total_function2,axiom,
% 0.23/0.55 ( ~ product(X,Y,Z)
% 0.23/0.55 | ~ product(X,Y,W)
% 0.23/0.55 | equalish(Z,W) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(associativity1,axiom,
% 0.23/0.55 ( ~ product(X,Y,U)
% 0.23/0.55 | ~ product(Y,Z,V)
% 0.23/0.55 | ~ product(U,Z,W)
% 0.23/0.55 | product(X,V,W) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(associativity2,axiom,
% 0.23/0.55 ( ~ product(X,Y,U)
% 0.23/0.55 | ~ product(Y,Z,V)
% 0.23/0.55 | ~ product(X,V,W)
% 0.23/0.55 | product(U,Z,W) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(closure_of_product_and_inverse,axiom,
% 0.23/0.55 ( ~ subgroup_member(A)
% 0.23/0.55 | ~ subgroup_member(B)
% 0.23/0.55 | ~ product(A,inverse(B),C)
% 0.23/0.55 | subgroup_member(C) ) ).
% 0.23/0.55
% 0.23/0.55 %----j(A) is an element for which A is identity. In a subgroup this can
% 0.23/0.55 %----be any element.
% 0.23/0.55
% 0.23/0.55 %----This subsitution axiom really should be in, but Wos omits it
% 0.23/0.55 % input_clause(j_substitutivity1,axiom,
% 0.23/0.55 % [--equalish(A,B),
% 0.23/0.55 % ++equalish(j(A),j(B))]).
% 0.23/0.55
% 0.23/0.55 cnf(a_is_in_subgroup,hypothesis,
% 0.23/0.55 subgroup_member(a) ).
% 0.23/0.55
% 0.23/0.55 cnf(subgr2_clause1,hypothesis,
% 0.23/0.55 ( ~ subgroup_member(A)
% 0.23/0.55 | subgroup_member(j(A)) ) ).
% 0.23/0.55
% 0.23/0.55 cnf(prove_subgr2,negated_conjecture,
% 0.23/0.55 ( ~ product(j(A),A,j(A))
% 0.23/0.55 | ~ product(A,j(A),j(A))
% 0.23/0.55 | ~ subgroup_member(A) ) ).
% 0.23/0.55
% 0.23/0.55 %--------------------------------------------------------------------------
% 0.23/0.55 %-------------------------------------------
% 0.23/0.55 % Proof found
% 0.23/0.55 % SZS status Theorem for theBenchmark
% 0.23/0.55 % SZS output start Proof
% 0.23/0.55 %ClaNum:22(EqnAxiom:0)
% 0.23/0.55 %VarNum:115(SingletonVarNum:55)
% 0.23/0.55 %MaxLitNum:4
% 0.23/0.55 %MaxfuncDepth:1
% 0.23/0.55 %SharedTerms:3
% 0.23/0.55 %goalClause: 20
% 0.23/0.55 [1]P1(a1)
% 0.23/0.55 [2]P2(x21,x21)
% 0.23/0.55 [3]P3(x31,a2,x31)
% 0.23/0.55 [4]P3(a2,x41,x41)
% 0.23/0.55 [5]P3(x51,f3(x51),a2)
% 0.23/0.55 [6]P3(f3(x61),x61,a2)
% 0.23/0.55 [7]P3(x71,x72,f4(x71,x72))
% 0.23/0.55 [8]~P1(x81)+P1(f5(x81))
% 0.23/0.55 [10]~P2(x102,x101)+P2(x101,x102)
% 0.23/0.55 [11]~P2(x111,x112)+P2(f3(x111),f3(x112))
% 0.23/0.55 [13]~P2(x132,x133)+P2(f4(x131,x132),f4(x131,x133))
% 0.23/0.55 [14]~P2(x141,x143)+P2(f4(x141,x142),f4(x143,x142))
% 0.23/0.55 [20]~P1(x201)+~P3(x201,f5(x201),f5(x201))+~P3(f5(x201),x201,f5(x201))
% 0.23/0.55 [9]~P2(x92,x91)+P1(x91)+~P1(x92)
% 0.23/0.55 [12]~P2(x121,x123)+P2(x121,x122)+~P2(x123,x122)
% 0.23/0.55 [16]~P3(x161,x162,x164)+P3(x161,x162,x163)+~P2(x164,x163)
% 0.23/0.55 [17]~P3(x171,x174,x173)+P3(x171,x172,x173)+~P2(x174,x172)
% 0.23/0.55 [18]~P3(x184,x182,x183)+P3(x181,x182,x183)+~P2(x184,x181)
% 0.23/0.55 [19]~P3(x193,x194,x191)+P2(x191,x192)+~P3(x193,x194,x192)
% 0.23/0.55 [15]P1(x151)+~P1(x152)+~P1(x153)+~P3(x153,f3(x152),x151)
% 0.23/0.55 [21]~P3(x216,x214,x211)+P3(x211,x212,x213)+~P3(x214,x212,x215)+~P3(x216,x215,x213)
% 0.23/0.55 [22]~P3(x221,x226,x224)+P3(x221,x222,x223)+~P3(x224,x225,x223)+~P3(x226,x225,x222)
% 0.23/0.55 %EqnAxiom
% 0.23/0.55
% 0.23/0.55 %-------------------------------------------
% 0.23/0.55 cnf(23,plain,
% 0.23/0.55 (~P1(a2)),
% 0.23/0.55 inference(scs_inference,[],[4,3,20])).
% 0.23/0.55 cnf(24,plain,
% 0.23/0.55 (P3(a2,x241,x241)),
% 0.23/0.55 inference(rename_variables,[],[4])).
% 0.23/0.55 cnf(29,plain,
% 0.23/0.55 (P2(x291,f4(a2,x291))),
% 0.23/0.55 inference(scs_inference,[],[1,4,24,3,7,20,9,19])).
% 0.23/0.55 cnf(30,plain,
% 0.23/0.55 (P3(x301,x302,f4(x301,x302))),
% 0.23/0.55 inference(rename_variables,[],[7])).
% 0.23/0.55 cnf(33,plain,
% 0.23/0.55 (P3(x331,x332,f4(x331,x332))),
% 0.23/0.55 inference(rename_variables,[],[7])).
% 0.23/0.55 cnf(38,plain,
% 0.23/0.55 (P3(a2,x381,x381)),
% 0.23/0.55 inference(rename_variables,[],[4])).
% 0.23/0.55 cnf(42,plain,
% 0.23/0.55 (P3(f4(a2,a2),x421,x421)),
% 0.23/0.55 inference(scs_inference,[],[1,4,24,38,3,7,30,33,20,9,19,15,22,10,18])).
% 0.23/0.55 cnf(48,plain,
% 0.23/0.55 (P3(x481,f3(x481),a2)),
% 0.23/0.55 inference(rename_variables,[],[5])).
% 0.23/0.55 cnf(49,plain,
% 0.23/0.55 (P3(a2,x491,x491)),
% 0.23/0.55 inference(rename_variables,[],[4])).
% 0.23/0.55 cnf(52,plain,
% 0.23/0.55 (P3(x521,f3(x521),a2)),
% 0.23/0.55 inference(rename_variables,[],[5])).
% 0.23/0.55 cnf(53,plain,
% 0.23/0.55 (P3(a2,x531,x531)),
% 0.23/0.55 inference(rename_variables,[],[4])).
% 0.23/0.55 cnf(54,plain,
% 0.23/0.55 (P3(f4(a2,a2),x541,x541)),
% 0.23/0.55 inference(rename_variables,[],[42])).
% 0.23/0.55 cnf(57,plain,
% 0.23/0.55 (P3(x571,f3(x571),a2)),
% 0.23/0.55 inference(rename_variables,[],[5])).
% 0.23/0.55 cnf(61,plain,
% 0.23/0.55 ($false),
% 0.23/0.55 inference(scs_inference,[],[1,23,4,49,53,42,54,29,5,48,52,57,17,19,21,22,15]),
% 0.23/0.55 ['proof']).
% 0.23/0.55 % SZS output end Proof
% 0.23/0.55 % Total time :0.000000s
%------------------------------------------------------------------------------