%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP010-1 : 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 : n028.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:26 EDT 2024
% Result : Unsatisfiable 0.56s 0.63s
% Output : CNFRefutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP010-1 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.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 12:51:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.55 start to proof:theBenchmark
% 0.56/0.63 %-------------------------------------------
% 0.56/0.63 % File :CSE---1.7
% 0.56/0.63 % Problem :theBenchmark
% 0.56/0.63 % Transform :cnf
% 0.56/0.63 % Format :tptp:raw
% 0.56/0.63 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.63
% 0.56/0.63 % Result :Theorem 0.040000s
% 0.56/0.63 % Output :CNFRefutation 0.040000s
% 0.56/0.63 %-------------------------------------------
% 0.56/0.63 %--------------------------------------------------------------------------
% 0.56/0.63 % File : GRP010-1 : TPTP v8.2.0. Released v1.0.0.
% 0.56/0.63 % Domain : Group Theory
% 0.56/0.63 % Problem : Inverse is a symmetric relationship
% 0.56/0.63 % Version : [MOW76] axioms.
% 0.56/0.63 % English : If a is an inverse of b then b is an inverse of a.
% 0.56/0.63
% 0.56/0.63 % Refs : [Wos65] Wos (1965), Unpublished Note
% 0.56/0.63 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 0.56/0.63 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 0.56/0.63 % Source : [SPRFN]
% 0.56/0.63 % Names : Problem 7 [Wos65]
% 0.56/0.63 % : wos7 [WM76]
% 0.56/0.63
% 0.56/0.63 % Status : Unsatisfiable
% 0.56/0.63 % Rating : 0.00 v5.3.0, 0.08 v5.2.0, 0.00 v2.0.0
% 0.56/0.63 % Syntax : Number of clauses : 10 ( 7 unt; 0 nHn; 5 RR)
% 0.56/0.63 % Number of literals : 18 ( 1 equ; 9 neg)
% 0.56/0.63 % Maximal clause size : 4 ( 1 avg)
% 0.56/0.63 % Maximal term depth : 2 ( 1 avg)
% 0.56/0.63 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 0.56/0.63 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 0.56/0.63 % Number of variables : 22 ( 0 sgn)
% 0.56/0.63 % SPC : CNF_UNS_RFO_SEQ_HRN
% 0.56/0.63
% 0.56/0.63 % Comments :
% 0.56/0.63 %--------------------------------------------------------------------------
% 0.56/0.63 %----Include group theory axioms
% 0.56/0.63 include('Axioms/GRP003-0.ax').
% 0.56/0.63 %--------------------------------------------------------------------------
% 0.56/0.63 cnf(a_multiply_b_is_identity,hypothesis,
% 0.56/0.63 product(a,b,identity) ).
% 0.56/0.63
% 0.56/0.63 cnf(prove_b_multiply_a_is_identity,negated_conjecture,
% 0.56/0.63 ~ product(b,a,identity) ).
% 0.56/0.63
% 0.56/0.63 %--------------------------------------------------------------------------
% 0.56/0.63 %-------------------------------------------
% 0.56/0.63 % Proof found
% 0.56/0.63 % SZS status Theorem for theBenchmark
% 0.56/0.63 % SZS output start Proof
% 0.56/0.63 %ClaNum:19(EqnAxiom:9)
% 0.56/0.63 %VarNum:44(SingletonVarNum:22)
% 0.56/0.63 %MaxLitNum:4
% 0.56/0.63 %MaxfuncDepth:1
% 0.56/0.63 %SharedTerms:5
% 0.56/0.63 %goalClause: 16
% 0.56/0.63 %singleGoalClaCount:1
% 0.56/0.63 [10]P1(a1,a2,a3)
% 0.56/0.63 [16]~P1(a2,a1,a3)
% 0.56/0.63 [11]P1(x111,a3,x111)
% 0.56/0.63 [12]P1(a3,x121,x121)
% 0.56/0.63 [13]P1(x131,f4(x131),a3)
% 0.56/0.63 [14]P1(f4(x141),x141,a3)
% 0.56/0.63 [15]P1(x151,x152,f5(x151,x152))
% 0.56/0.63 [17]~P1(x173,x174,x171)+E(x171,x172)+~P1(x173,x174,x172)
% 0.56/0.63 [18]~P1(x186,x184,x181)+P1(x181,x182,x183)+~P1(x184,x182,x185)+~P1(x186,x185,x183)
% 0.56/0.63 [19]~P1(x191,x196,x194)+P1(x191,x192,x193)+~P1(x194,x195,x193)+~P1(x196,x195,x192)
% 0.56/0.63 %EqnAxiom
% 0.56/0.63 [1]E(x11,x11)
% 0.56/0.63 [2]E(x22,x21)+~E(x21,x22)
% 0.56/0.63 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/0.63 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 0.56/0.63 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 0.56/0.63 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 0.56/0.63 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 0.56/0.63 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 0.56/0.63 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 0.56/0.63
% 0.56/0.63 %-------------------------------------------
% 0.61/0.64 cnf(20,plain,
% 0.61/0.64 (~E(f4(a1),a2)),
% 0.61/0.64 inference(scs_inference,[],[16,14,7])).
% 0.61/0.64 cnf(22,plain,
% 0.61/0.64 (E(x221,f5(x221,a3))),
% 0.61/0.64 inference(scs_inference,[],[16,11,15,14,7,17])).
% 0.61/0.64 cnf(23,plain,
% 0.61/0.64 (P1(x231,x232,f5(x231,x232))),
% 0.61/0.64 inference(rename_variables,[],[15])).
% 0.61/0.64 cnf(26,plain,
% 0.61/0.64 (P1(x261,a3,x261)),
% 0.61/0.64 inference(rename_variables,[],[11])).
% 0.61/0.64 cnf(28,plain,
% 0.61/0.64 (P1(x281,x282,f5(x281,x282))),
% 0.61/0.64 inference(rename_variables,[],[15])).
% 0.61/0.64 cnf(29,plain,
% 0.61/0.64 (~P1(a3,a1,f4(a2))),
% 0.61/0.64 inference(scs_inference,[],[16,11,26,15,23,13,14,7,17,8,9,18])).
% 0.61/0.64 cnf(31,plain,
% 0.61/0.64 (P1(x311,a3,x311)),
% 0.61/0.64 inference(rename_variables,[],[11])).
% 0.61/0.64 cnf(33,plain,
% 0.61/0.64 (P1(x331,f5(a3,a3),x331)),
% 0.61/0.64 inference(scs_inference,[],[16,11,26,31,15,23,28,13,14,7,17,8,9,18,19])).
% 0.61/0.64 cnf(37,plain,
% 0.61/0.64 (~E(f5(a2,a1),f5(a3,a3))),
% 0.61/0.64 inference(scs_inference,[],[16,11,26,31,15,23,28,13,14,7,17,8,9,18,19,2,3])).
% 0.61/0.64 cnf(38,plain,
% 0.61/0.64 (E(f5(x381,a3),x381)),
% 0.61/0.64 inference(scs_inference,[],[22,2])).
% 0.61/0.64 cnf(39,plain,
% 0.61/0.64 (E(x391,f5(x391,f5(a3,a3)))),
% 0.61/0.64 inference(scs_inference,[],[33,22,15,2,17])).
% 0.61/0.64 cnf(40,plain,
% 0.61/0.64 (P1(x401,x402,f5(x401,x402))),
% 0.61/0.64 inference(rename_variables,[],[15])).
% 0.61/0.64 cnf(42,plain,
% 0.61/0.64 (P1(x421,f5(a3,a3),f5(x421,a3))),
% 0.61/0.64 inference(scs_inference,[],[33,22,15,2,17,9])).
% 0.61/0.64 cnf(43,plain,
% 0.61/0.64 (P1(x431,f5(a3,a3),x431)),
% 0.61/0.64 inference(rename_variables,[],[33])).
% 0.61/0.64 cnf(44,plain,
% 0.61/0.64 (P1(f5(x441,a3),f5(a3,a3),x441)),
% 0.61/0.64 inference(scs_inference,[],[33,43,22,15,2,17,9,7])).
% 0.61/0.64 cnf(45,plain,
% 0.61/0.64 (P1(x451,f5(a3,a3),x451)),
% 0.61/0.64 inference(rename_variables,[],[33])).
% 0.61/0.64 cnf(48,plain,
% 0.61/0.64 (P1(a3,x481,x481)),
% 0.61/0.64 inference(rename_variables,[],[12])).
% 0.61/0.64 cnf(51,plain,
% 0.61/0.64 (P1(x511,f5(a3,a3),x511)),
% 0.61/0.64 inference(rename_variables,[],[33])).
% 0.61/0.64 cnf(53,plain,
% 0.61/0.64 (P1(x531,f5(f5(a3,a3),f5(a3,a3)),x531)),
% 0.61/0.64 inference(scs_inference,[],[33,43,45,51,20,29,22,12,48,15,40,2,17,9,7,3,8,18,19])).
% 0.61/0.64 cnf(56,plain,
% 0.61/0.64 (E(f5(x561,f5(a3,a3)),x561)),
% 0.61/0.64 inference(scs_inference,[],[39,2])).
% 0.61/0.64 cnf(57,plain,
% 0.61/0.64 (E(x571,f5(f5(x571,a3),a3))),
% 0.61/0.64 inference(scs_inference,[],[44,39,42,2,17])).
% 0.61/0.64 cnf(60,plain,
% 0.61/0.64 (P1(f5(f5(x601,a3),f5(a3,a3)),f5(a3,a3),x601)),
% 0.61/0.64 inference(scs_inference,[],[44,39,42,2,17,7])).
% 0.61/0.64 cnf(61,plain,
% 0.61/0.64 (E(x611,f5(x611,f5(a3,a3)))),
% 0.62/0.64 inference(rename_variables,[],[39])).
% 0.62/0.64 cnf(62,plain,
% 0.62/0.64 (E(f5(x621,a3),f5(x621,f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[44,39,61,42,38,2,17,7,3])).
% 0.62/0.64 cnf(63,plain,
% 0.62/0.64 (E(x631,f5(x631,f5(a3,a3)))),
% 0.62/0.64 inference(rename_variables,[],[39])).
% 0.62/0.64 cnf(64,plain,
% 0.62/0.64 (P1(f5(x641,a3),f5(a3,a3),f5(x641,f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[44,39,61,63,42,38,2,17,7,3,9])).
% 0.62/0.64 cnf(65,plain,
% 0.62/0.64 (P1(f5(x651,a3),f5(a3,a3),x651)),
% 0.62/0.64 inference(rename_variables,[],[44])).
% 0.62/0.64 cnf(66,plain,
% 0.62/0.64 (P1(f5(x661,a3),f5(f5(a3,a3),f5(a3,a3)),x661)),
% 0.62/0.64 inference(scs_inference,[],[44,65,39,61,63,42,38,2,17,7,3,9,8])).
% 0.62/0.64 cnf(72,plain,
% 0.62/0.64 (P1(f5(a3,a3),a3,a3)),
% 0.62/0.64 inference(scs_inference,[],[53,44,65,33,29,39,61,63,42,38,12,2,17,7,3,9,8,18,19])).
% 0.62/0.64 cnf(77,plain,
% 0.62/0.64 (E(f5(x771,f5(a3,a3)),f5(x771,a3))),
% 0.62/0.64 inference(scs_inference,[],[62,2])).
% 0.62/0.64 cnf(78,plain,
% 0.62/0.64 (E(x781,f5(f5(x781,a3),f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[60,33,62,2,17])).
% 0.62/0.64 cnf(79,plain,
% 0.62/0.64 (P1(x791,f5(a3,a3),x791)),
% 0.62/0.64 inference(rename_variables,[],[33])).
% 0.62/0.64 cnf(82,plain,
% 0.62/0.64 (E(f5(x821,f5(a3,a3)),x821)),
% 0.62/0.64 inference(rename_variables,[],[56])).
% 0.62/0.64 cnf(87,plain,
% 0.62/0.64 (P1(f5(a3,a3),f5(f5(a3,a3),a3),a3)),
% 0.62/0.64 inference(scs_inference,[],[60,72,20,33,79,56,82,62,57,2,17,3,9,7,8])).
% 0.62/0.64 cnf(89,plain,
% 0.62/0.64 (P1(x891,f5(a3,a3),f5(f5(x891,a3),f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[60,72,53,20,33,79,56,82,62,57,15,2,17,3,9,7,8,18])).
% 0.62/0.64 cnf(97,plain,
% 0.62/0.64 (E(f5(f5(x971,a3),f5(a3,a3)),x971)),
% 0.62/0.64 inference(scs_inference,[],[78,2])).
% 0.62/0.64 cnf(99,plain,
% 0.62/0.64 (E(x991,f5(f5(x991,a3),f5(a3,a3)))),
% 0.62/0.64 inference(rename_variables,[],[78])).
% 0.62/0.64 cnf(101,plain,
% 0.62/0.64 (E(x1011,f5(f5(x1011,a3),f5(a3,a3)))),
% 0.62/0.64 inference(rename_variables,[],[78])).
% 0.62/0.64 cnf(104,plain,
% 0.62/0.64 (P1(a1,f5(f5(a2,a3),f5(a3,a3)),a3)),
% 0.62/0.64 inference(scs_inference,[],[72,78,99,101,37,77,10,2,9,7,3,8])).
% 0.62/0.64 cnf(106,plain,
% 0.62/0.64 (P1(f5(f5(x1061,a3),f5(a3,a3)),a3,x1061)),
% 0.62/0.64 inference(scs_inference,[],[89,72,78,99,101,37,77,10,11,2,9,7,3,8,18])).
% 0.62/0.64 cnf(109,plain,
% 0.62/0.64 (P1(x1091,a3,f5(f5(x1091,a3),f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[89,53,72,78,99,101,37,66,77,10,11,2,9,7,3,8,18,19])).
% 0.62/0.64 cnf(113,plain,
% 0.62/0.64 (E(f5(f5(x1131,a3),a3),x1131)),
% 0.62/0.64 inference(scs_inference,[],[57,2])).
% 0.62/0.64 cnf(116,plain,
% 0.62/0.64 (~E(f4(a1),f5(f5(a2,a3),f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[20,97,64,57,2,9,3])).
% 0.62/0.64 cnf(119,plain,
% 0.62/0.64 (E(f5(x1191,a3),x1191)),
% 0.62/0.64 inference(rename_variables,[],[38])).
% 0.62/0.64 cnf(120,plain,
% 0.62/0.64 (P1(f5(x1201,a3),a3,x1201)),
% 0.62/0.64 inference(scs_inference,[],[20,44,97,64,87,38,119,57,2,9,3,7,8])).
% 0.62/0.64 cnf(122,plain,
% 0.62/0.64 (P1(f5(f5(x1221,a3),f5(a3,a3)),f4(x1221),a3)),
% 0.62/0.64 inference(scs_inference,[],[109,20,44,97,64,87,38,119,57,13,12,2,9,3,7,8,18])).
% 0.62/0.64 cnf(124,plain,
% 0.62/0.64 (P1(a3,x1241,x1241)),
% 0.62/0.64 inference(rename_variables,[],[12])).
% 0.62/0.64 cnf(126,plain,
% 0.62/0.64 (P1(f4(a1),a3,f5(f5(a2,a3),f5(a3,a3)))),
% 0.62/0.64 inference(scs_inference,[],[109,20,44,97,64,87,104,38,119,57,13,14,12,124,2,9,3,7,8,18,19])).
% 0.62/0.64 cnf(134,plain,
% 0.62/0.64 (E(f5(x1341,f5(a3,a3)),x1341)),
% 0.62/0.64 inference(rename_variables,[],[56])).
% 0.62/0.64 cnf(142,plain,
% 0.62/0.64 (P1(f5(f5(x1421,a3),f5(a3,a3)),a3,x1421)),
% 0.62/0.64 inference(rename_variables,[],[106])).
% 0.62/0.64 cnf(149,plain,
% 0.62/0.64 ($false),
% 0.62/0.64 inference(scs_inference,[],[126,122,106,142,109,20,29,113,116,120,56,134,39,11,17,9,7,8,3,18,19,2]),
% 0.62/0.64 ['proof']).
% 0.62/0.64 % SZS output end Proof
% 0.62/0.64 % Total time :0.040000s
%------------------------------------------------------------------------------