%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP046-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 : n023.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:37 EDT 2024
% Result : Unsatisfiable 6.14s 6.22s
% Output : CNFRefutation 6.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GRP046-2 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n023.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Thu Jun 20 13:05:09 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.44/0.60 start to proof:theBenchmark
% 6.14/6.21 %-------------------------------------------
% 6.14/6.21 % File :CSE---1.7
% 6.14/6.21 % Problem :theBenchmark
% 6.14/6.21 % Transform :cnf
% 6.14/6.21 % Format :tptp:raw
% 6.14/6.21 % Command :java -jar mcs_scs.jar %d %s
% 6.14/6.21
% 6.14/6.21 % Result :Theorem 5.560000s
% 6.14/6.21 % Output :CNFRefutation 5.560000s
% 6.14/6.21 %-------------------------------------------
% 6.14/6.22 %--------------------------------------------------------------------------
% 6.14/6.22 % File : GRP046-2 : TPTP v8.2.0. Released v1.0.0.
% 6.14/6.22 % Domain : Group Theory
% 6.14/6.22 % Problem : Multiply substitution 1 is dependent
% 6.14/6.22 % Version : [Ver92] axioms.
% 6.14/6.22 % English :
% 6.14/6.22
% 6.14/6.22 % Refs : [Ver92] Veroff (1992), Email to G. Sutcliffe
% 6.14/6.22 % Source : [Ver92]
% 6.14/6.22 % Names : - [Ver92]
% 6.14/6.22
% 6.14/6.22 % Status : Unsatisfiable
% 6.14/6.22 % 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.08 v5.1.0, 0.06 v5.0.0, 0.00 v2.1.0, 0.00 v2.0.0
% 6.14/6.22 % Syntax : Number of clauses : 9 ( 5 unt; 0 nHn; 6 RR)
% 6.14/6.22 % Number of literals : 19 ( 0 equ; 11 neg)
% 6.14/6.22 % Maximal clause size : 4 ( 2 avg)
% 6.14/6.22 % Maximal term depth : 2 ( 1 avg)
% 6.14/6.22 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 6.14/6.22 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 6.14/6.22 % Number of variables : 24 ( 0 sgn)
% 6.14/6.22 % SPC : CNF_UNS_RFO_NEQ_HRN
% 6.14/6.22
% 6.14/6.22 % Comments :
% 6.14/6.22 %--------------------------------------------------------------------------
% 6.14/6.22 %----Include Veroff's minimal axiom set
% 6.14/6.22 include('Axioms/GRP005-0.ax').
% 6.14/6.22 %--------------------------------------------------------------------------
% 6.14/6.22 cnf(a_equals_b,hypothesis,
% 6.14/6.22 equalish(a,b) ).
% 6.14/6.22
% 6.14/6.22 cnf(prove_multiply_substitution1,negated_conjecture,
% 6.14/6.22 ~ equalish(multiply(a,c),multiply(b,c)) ).
% 6.14/6.22
% 6.14/6.22 %--------------------------------------------------------------------------
% 6.14/6.22 %-------------------------------------------
% 6.14/6.22 % Proof found
% 6.14/6.22 % SZS status Theorem for theBenchmark
% 6.14/6.22 % SZS output start Proof
% 6.14/6.22 %ClaNum:9(EqnAxiom:0)
% 6.14/6.22 %VarNum:48(SingletonVarNum:24)
% 6.14/6.22 %MaxLitNum:4
% 6.14/6.22 %MaxfuncDepth:1
% 6.14/6.22 %SharedTerms:8
% 6.14/6.22 %goalClause: 5
% 6.14/6.22 %singleGoalClaCount:1
% 6.14/6.22 [1]P1(a1,a2)
% 6.14/6.22 [5]~P1(f6(a1,a4),f6(a2,a4))
% 6.14/6.22 [2]P2(a3,x21,x21)
% 6.14/6.22 [3]P2(f5(x31),x31,a3)
% 6.14/6.22 [4]P2(x41,x42,f6(x41,x42))
% 6.14/6.22 [6]~P2(x61,x62,x64)+P2(x61,x62,x63)+~P1(x64,x63)
% 6.14/6.22 [7]~P2(x73,x74,x71)+P1(x71,x72)+~P2(x73,x74,x72)
% 6.14/6.22 [8]~P2(x86,x84,x81)+P2(x81,x82,x83)+~P2(x84,x82,x85)+~P2(x86,x85,x83)
% 6.14/6.22 [9]~P2(x91,x96,x94)+P2(x91,x92,x93)+~P2(x94,x95,x93)+~P2(x96,x95,x92)
% 6.14/6.22 %EqnAxiom
% 6.14/6.22
% 6.14/6.22 %-------------------------------------------
% 6.14/6.23 cnf(12,plain,
% 6.14/6.23 (P2(a3,a1,a2)),
% 6.14/6.23 inference(scs_inference,[],[2,1,7,6])).
% 6.14/6.23 cnf(24,plain,
% 6.14/6.23 (P1(x241,f6(a3,x241))),
% 6.14/6.23 inference(scs_inference,[],[2,4,7])).
% 6.14/6.23 cnf(46,plain,
% 6.14/6.23 (P2(f5(x461),x461,f6(a3,a3))),
% 6.14/6.23 inference(scs_inference,[],[3,24,6])).
% 6.14/6.23 cnf(49,plain,
% 6.14/6.23 (P1(a3,f6(f5(x491),x491))),
% 6.14/6.23 inference(scs_inference,[],[3,24,4,6,7])).
% 6.14/6.23 cnf(50,plain,
% 6.14/6.23 (P2(x501,x502,f6(x501,x502))),
% 6.14/6.23 inference(rename_variables,[],[4])).
% 6.14/6.23 cnf(53,plain,
% 6.14/6.23 (P2(f5(x531),x531,a3)),
% 6.14/6.23 inference(rename_variables,[],[3])).
% 6.14/6.23 cnf(55,plain,
% 6.14/6.23 (P2(a3,x551,f6(f5(a3),x551))),
% 6.14/6.23 inference(scs_inference,[],[3,53,24,2,4,50,6,7,9,8])).
% 6.14/6.23 cnf(62,plain,
% 6.14/6.23 (P1(x621,f6(f5(a3),x621))),
% 6.14/6.23 inference(scs_inference,[],[3,49,2,55,6,7])).
% 6.14/6.23 cnf(70,plain,
% 6.14/6.23 (P2(f5(x701),f6(x701,x702),x702)),
% 6.14/6.23 inference(scs_inference,[],[3,2,4,9])).
% 6.14/6.23 cnf(71,plain,
% 6.14/6.23 (P2(x711,x712,f6(x711,x712))),
% 6.14/6.23 inference(rename_variables,[],[4])).
% 6.14/6.23 cnf(73,plain,
% 6.14/6.23 (P1(f6(f5(x731),f6(x731,x732)),x732)),
% 6.14/6.23 inference(scs_inference,[],[3,2,4,71,9,7])).
% 6.14/6.23 cnf(78,plain,
% 6.14/6.23 (P2(a3,x781,x781)),
% 6.14/6.23 inference(rename_variables,[],[2])).
% 6.14/6.23 cnf(80,plain,
% 6.14/6.23 (P2(a3,f6(a3,x801),x801)),
% 6.14/6.23 inference(scs_inference,[],[3,73,2,78,70,6,8])).
% 6.14/6.23 cnf(158,plain,
% 6.14/6.23 (P2(f5(a3),f6(f5(a3),x1581),x1581)),
% 6.14/6.23 inference(scs_inference,[],[3,2,55,9])).
% 6.14/6.23 cnf(163,plain,
% 6.14/6.23 (P2(a3,f6(f5(a3),x1631),x1631)),
% 6.14/6.23 inference(scs_inference,[],[3,2,158,8])).
% 6.14/6.23 cnf(180,plain,
% 6.14/6.23 (P2(x1801,x1802,f6(f5(a3),f6(x1801,x1802)))),
% 6.14/6.23 inference(scs_inference,[],[4,62,6])).
% 6.14/6.23 cnf(198,plain,
% 6.14/6.23 (P2(x1981,x1982,f6(a3,f6(x1981,x1982)))),
% 6.14/6.23 inference(scs_inference,[],[4,24,6])).
% 6.14/6.23 cnf(583,plain,
% 6.14/6.23 (P2(a2,x5831,f6(a1,x5831))),
% 6.14/6.23 inference(scs_inference,[],[12,180,163,8])).
% 6.14/6.23 cnf(595,plain,
% 6.14/6.23 (P2(a2,x5951,f6(a1,x5951))),
% 6.14/6.23 inference(rename_variables,[],[583])).
% 6.14/6.23 cnf(596,plain,
% 6.14/6.23 (P2(x5961,x5962,f6(a3,f6(x5961,x5962)))),
% 6.14/6.23 inference(rename_variables,[],[198])).
% 6.14/6.23 cnf(602,plain,
% 6.14/6.23 (P2(a3,f6(a3,f6(a2,x6021)),f6(a1,x6021))),
% 6.14/6.23 inference(scs_inference,[],[12,2,198,596,583,595,7,8,6])).
% 6.14/6.23 cnf(1449,plain,
% 6.14/6.23 (P2(f5(x14491),x14491,f6(a3,a3))),
% 6.14/6.23 inference(rename_variables,[],[46])).
% 6.14/6.23 cnf(1455,plain,
% 6.14/6.23 ($false),
% 6.14/6.23 inference(scs_inference,[],[46,1449,5,2,602,4,80,9,8,7]),
% 6.14/6.23 ['proof']).
% 6.14/6.23 % SZS output end Proof
% 6.14/6.23 % Total time :5.560000s
%------------------------------------------------------------------------------