%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP047-2 : 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 : n025.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 59.78s 59.86s
% Output : CNFRefutation 59.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP047-2 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 20 08:20:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.57/0.61 start to proof:theBenchmark
% 59.78/59.85 %-------------------------------------------
% 59.78/59.85 % File :CSE---1.7
% 59.78/59.86 % Problem :theBenchmark
% 59.78/59.86 % Transform :cnf
% 59.78/59.86 % Format :tptp:raw
% 59.78/59.86 % Command :java -jar mcs_scs.jar %d %s
% 59.78/59.86
% 59.78/59.86 % Result :Theorem 59.190000s
% 59.78/59.86 % Output :CNFRefutation 59.190000s
% 59.78/59.86 %-------------------------------------------
% 59.78/59.86 %--------------------------------------------------------------------------
% 59.78/59.86 % File : GRP047-2 : TPTP v8.2.0. Released v1.0.0.
% 59.78/59.86 % Domain : Group Theory
% 59.78/59.86 % Problem : Multiply substitution 2 is dependent
% 59.78/59.86 % Version : [Ver92] axioms.
% 59.78/59.86 % English :
% 59.78/59.86
% 59.78/59.86 % Refs : [Ver92] Veroff (1992), Email to G. Sutcliffe
% 59.78/59.86 % Source : [Ver92]
% 59.78/59.86 % Names : - [Ver92]
% 59.78/59.86
% 59.78/59.86 % Status : Unsatisfiable
% 59.78/59.86 % 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.4.0, 0.14 v2.3.0, 0.00 v2.1.0, 0.00 v2.0.0
% 59.78/59.86 % Syntax : Number of clauses : 9 ( 5 unt; 0 nHn; 6 RR)
% 59.78/59.86 % Number of literals : 19 ( 0 equ; 11 neg)
% 59.78/59.86 % Maximal clause size : 4 ( 2 avg)
% 59.78/59.86 % Maximal term depth : 2 ( 1 avg)
% 59.78/59.86 % Number of predicates : 2 ( 2 usr; 0 prp; 2-3 aty)
% 59.78/59.86 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 59.78/59.86 % Number of variables : 24 ( 0 sgn)
% 59.78/59.86 % SPC : CNF_UNS_RFO_NEQ_HRN
% 59.78/59.86
% 59.78/59.86 % Comments :
% 59.78/59.86 %--------------------------------------------------------------------------
% 59.78/59.86 %----Include Veroff's minimal axiom set
% 59.78/59.86 include('Axioms/GRP005-0.ax').
% 59.78/59.86 %--------------------------------------------------------------------------
% 59.78/59.86 cnf(a_equals_b,hypothesis,
% 59.78/59.86 equalish(a,b) ).
% 59.78/59.86
% 59.78/59.86 cnf(prove_multiply_substitution2,negated_conjecture,
% 59.78/59.86 ~ equalish(multiply(c,a),multiply(c,b)) ).
% 59.78/59.86
% 59.78/59.86 %--------------------------------------------------------------------------
% 59.78/59.86 %-------------------------------------------
% 59.78/59.86 % Proof found
% 59.78/59.86 % SZS status Theorem for theBenchmark
% 59.78/59.86 % SZS output start Proof
% 59.78/59.87 %ClaNum:9(EqnAxiom:0)
% 59.78/59.87 %VarNum:48(SingletonVarNum:24)
% 59.78/59.87 %MaxLitNum:4
% 59.78/59.87 %MaxfuncDepth:1
% 59.78/59.87 %SharedTerms:8
% 59.78/59.87 %goalClause: 5
% 59.78/59.87 %singleGoalClaCount:1
% 59.78/59.87 [1]P1(a1,a2)
% 59.78/59.87 [5]~P1(f6(a4,a1),f6(a4,a2))
% 59.78/59.87 [2]P2(a3,x21,x21)
% 59.78/59.87 [3]P2(f5(x31),x31,a3)
% 59.78/59.87 [4]P2(x41,x42,f6(x41,x42))
% 59.78/59.87 [6]~P2(x61,x62,x64)+P2(x61,x62,x63)+~P1(x64,x63)
% 59.78/59.87 [7]~P2(x73,x74,x71)+P1(x71,x72)+~P2(x73,x74,x72)
% 59.78/59.87 [8]~P2(x86,x84,x81)+P2(x81,x82,x83)+~P2(x84,x82,x85)+~P2(x86,x85,x83)
% 59.78/59.87 [9]~P2(x91,x96,x94)+P2(x91,x92,x93)+~P2(x94,x95,x93)+~P2(x96,x95,x92)
% 59.78/59.87 %EqnAxiom
% 59.78/59.87
% 59.78/59.87 %-------------------------------------------
% 59.78/59.88 cnf(12,plain,
% 59.78/59.88 (P2(a3,a1,a2)),
% 59.78/59.88 inference(scs_inference,[],[2,1,7,6])).
% 59.78/59.88 cnf(13,plain,
% 59.78/59.88 (P2(a3,x131,x131)),
% 59.78/59.88 inference(rename_variables,[],[2])).
% 59.78/59.88 cnf(17,plain,
% 59.78/59.88 (P2(x171,x172,f6(x171,x172))),
% 59.78/59.88 inference(rename_variables,[],[4])).
% 59.78/59.88 cnf(19,plain,
% 59.78/59.88 (P2(a3,f6(a3,a3),a3)),
% 59.78/59.88 inference(scs_inference,[],[2,13,4,17,3,1,7,6,8,9])).
% 59.78/59.88 cnf(24,plain,
% 59.78/59.88 (P1(x241,f6(a3,x241))),
% 59.78/59.88 inference(scs_inference,[],[2,4,7])).
% 59.78/59.88 cnf(41,plain,
% 59.78/59.88 (P2(a3,x411,a3)+~P2(f6(a3,a3),x411,f6(a3,a3))),
% 59.78/59.88 inference(scs_inference,[],[2,4,3,19,7,6,8])).
% 59.78/59.88 cnf(46,plain,
% 59.78/59.88 (P1(a3,f6(f5(x461),x461))),
% 59.78/59.88 inference(scs_inference,[],[3,4,7])).
% 59.78/59.88 cnf(47,plain,
% 59.78/59.88 (P2(x471,x472,f6(x471,x472))),
% 59.78/59.88 inference(rename_variables,[],[4])).
% 59.78/59.88 cnf(49,plain,
% 59.78/59.88 (P2(f5(x491),x491,f6(a3,a3))),
% 59.78/59.88 inference(scs_inference,[],[3,24,4,7,6])).
% 59.78/59.88 cnf(52,plain,
% 59.78/59.88 (P2(a3,x521,f6(f5(a3),x521))),
% 59.78/59.88 inference(scs_inference,[],[3,24,2,4,47,7,6,8])).
% 59.78/59.88 cnf(54,plain,
% 59.78/59.88 (P2(f5(x541),x541,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(56,plain,
% 59.78/59.88 (P2(f5(a3),x561,x561)),
% 59.78/59.88 inference(scs_inference,[],[3,54,24,2,4,47,7,6,8,9])).
% 59.78/59.88 cnf(65,plain,
% 59.78/59.88 (P2(f5(f5(x651)),f6(a3,a3),x651)),
% 59.78/59.88 inference(scs_inference,[],[3,46,2,49,52,7,6,9])).
% 59.78/59.88 cnf(70,plain,
% 59.78/59.88 (P2(f5(x701),f6(x701,x702),x702)),
% 59.78/59.88 inference(scs_inference,[],[3,2,4,9])).
% 59.78/59.88 cnf(71,plain,
% 59.78/59.88 (P2(x711,x712,f6(x711,x712))),
% 59.78/59.88 inference(rename_variables,[],[4])).
% 59.78/59.88 cnf(73,plain,
% 59.78/59.88 (P1(f6(f5(x731),f6(x731,x732)),x732)),
% 59.78/59.88 inference(scs_inference,[],[3,2,4,71,9,7])).
% 59.78/59.88 cnf(76,plain,
% 59.78/59.88 (P1(a3,x761)+~P2(f6(a3,a3),x761,f6(a3,a3))),
% 59.78/59.88 inference(scs_inference,[],[2,41,7])).
% 59.78/59.88 cnf(77,plain,
% 59.78/59.88 (P2(a3,f6(f5(x771),f6(x771,x772)),x772)),
% 59.78/59.88 inference(scs_inference,[],[73,2,6])).
% 59.78/59.88 cnf(78,plain,
% 59.78/59.88 (P2(a3,x781,x781)),
% 59.78/59.88 inference(rename_variables,[],[2])).
% 59.78/59.88 cnf(80,plain,
% 59.78/59.88 (P2(a3,f6(a3,x801),x801)),
% 59.78/59.88 inference(scs_inference,[],[3,73,2,78,70,6,8])).
% 59.78/59.88 cnf(81,plain,
% 59.78/59.88 (P2(f5(x811),f6(x811,x812),x812)),
% 59.78/59.88 inference(rename_variables,[],[70])).
% 59.78/59.88 cnf(82,plain,
% 59.78/59.88 (P2(f5(x821),x821,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(83,plain,
% 59.78/59.88 (P2(a3,x831,x831)),
% 59.78/59.88 inference(rename_variables,[],[2])).
% 59.78/59.88 cnf(85,plain,
% 59.78/59.88 (P2(f5(f5(x851)),x852,f6(x851,x852))),
% 59.78/59.88 inference(scs_inference,[],[3,82,73,2,78,83,70,81,6,8,9])).
% 59.78/59.88 cnf(92,plain,
% 59.78/59.88 (P2(f5(x921),x921,x922)+~P2(f6(a3,a3),x922,f6(a3,a3))),
% 59.78/59.88 inference(scs_inference,[],[3,76,6])).
% 59.78/59.88 cnf(95,plain,
% 59.78/59.88 (P2(f5(x951),x951,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(100,plain,
% 59.78/59.88 (P2(f5(x1001),x1001,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(101,plain,
% 59.78/59.88 (P2(a3,x1011,x1011)),
% 59.78/59.88 inference(rename_variables,[],[2])).
% 59.78/59.88 cnf(103,plain,
% 59.78/59.88 (P2(f5(a3),x1031,f6(f5(x1032),f6(x1032,x1031)))),
% 59.78/59.88 inference(scs_inference,[],[3,95,100,2,101,77,85,7,6,8,9])).
% 59.78/59.88 cnf(109,plain,
% 59.78/59.88 (P2(f5(a3),x1091,f6(f5(x1092),f6(x1092,x1091)))),
% 59.78/59.88 inference(rename_variables,[],[103])).
% 59.78/59.88 cnf(110,plain,
% 59.78/59.88 (P2(f5(x1101),x1101,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(112,plain,
% 59.78/59.88 (P2(f5(x1121),x1121,f6(f5(x1122),f6(x1122,a3)))),
% 59.78/59.88 inference(scs_inference,[],[3,110,103,7,6])).
% 59.78/59.88 cnf(114,plain,
% 59.78/59.88 (P2(f5(f5(a3)),x1141,x1141)),
% 59.78/59.88 inference(scs_inference,[],[3,110,2,56,103,7,6,9])).
% 59.78/59.88 cnf(116,plain,
% 59.78/59.88 (P2(f5(x1161),x1161,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(118,plain,
% 59.78/59.88 (P2(a3,x1181,f6(f5(x1182),f6(x1182,x1181)))),
% 59.78/59.88 inference(scs_inference,[],[3,110,116,2,56,103,109,7,6,9,8])).
% 59.78/59.88 cnf(125,plain,
% 59.78/59.88 (P2(f5(x1251),x1251,a3)),
% 59.78/59.88 inference(rename_variables,[],[3])).
% 59.78/59.88 cnf(127,plain,
% 59.78/59.88 (P2(f5(x1271),x1271,f5(a3))),
% 59.78/59.88 inference(scs_inference,[],[3,125,114,7,6])).
% 59.78/59.88 cnf(140,plain,
% 59.78/59.88 (P2(f5(f5(x1401)),f5(a3),x1401)),
% 59.78/59.88 inference(scs_inference,[],[3,2,127,118,7,9])).
% 59.78/59.88 cnf(159,plain,
% 59.78/59.88 (P2(f5(a3),f6(f5(a3),x1591),x1591)),
% 59.78/59.88 inference(scs_inference,[],[3,2,52,9])).
% 59.78/59.88 cnf(233,plain,
% 59.78/59.88 (P2(x2331,x2332,f6(x2331,x2332))),
% 59.78/59.88 inference(rename_variables,[],[4])).
% 59.78/59.88 cnf(237,plain,
% 59.78/59.88 (P2(x2371,x2372,f6(x2371,x2372))),
% 59.78/59.88 inference(rename_variables,[],[4])).
% 59.78/59.88 cnf(238,plain,
% 59.78/59.88 (P2(x2381,x2382,f6(x2381,x2382))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(240,plain,
% 59.78/59.89 (P2(x2401,x2402,f6(f6(x2401,a3),x2402))),
% 59.78/59.89 inference(scs_inference,[],[4,233,238,237,2,159,52,7,8,9])).
% 59.78/59.89 cnf(247,plain,
% 59.78/59.89 (P2(x2471,x2472,f6(f6(x2471,a3),x2472))),
% 59.78/59.89 inference(rename_variables,[],[240])).
% 59.78/59.89 cnf(251,plain,
% 59.78/59.89 (P2(x2511,x2512,f6(x2511,x2512))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(252,plain,
% 59.78/59.89 (P2(x2521,x2522,f6(x2521,x2522))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(254,plain,
% 59.78/59.89 (P2(x2541,a2,f6(f6(x2541,a3),a1))),
% 59.78/59.89 inference(scs_inference,[],[4,252,251,12,240,247,7,8,9])).
% 59.78/59.89 cnf(294,plain,
% 59.78/59.89 (P2(x2941,x2942,f6(x2941,x2942))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(295,plain,
% 59.78/59.89 (P2(x2951,x2952,f6(x2951,x2952))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(297,plain,
% 59.78/59.89 (P2(x2971,x2972,f6(f6(x2971,a3),f6(a3,x2972)))),
% 59.78/59.89 inference(scs_inference,[],[4,295,294,52,80,8,9])).
% 59.78/59.89 cnf(762,plain,
% 59.78/59.89 (P2(x7621,x7622,f6(x7621,x7622))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(764,plain,
% 59.78/59.89 (P2(a2,x7641,f6(f6(a3,a3),f6(a1,x7641)))),
% 59.78/59.89 inference(scs_inference,[],[12,127,4,762,112,254,240,7,9,8])).
% 59.78/59.89 cnf(771,plain,
% 59.78/59.89 (P2(x7711,x7712,f6(x7711,x7712))),
% 59.78/59.89 inference(rename_variables,[],[4])).
% 59.78/59.89 cnf(780,plain,
% 59.78/59.89 (P2(f6(a3,a3),x7801,x7801)),
% 59.78/59.89 inference(scs_inference,[],[12,2,49,127,4,771,140,297,764,7,6,9,8])).
% 59.78/59.89 cnf(1649,plain,
% 59.78/59.89 (P2(f5(f5(x16491)),f6(a3,a3),x16491)),
% 59.78/59.89 inference(rename_variables,[],[65])).
% 59.78/59.89 cnf(1651,plain,
% 59.78/59.89 (P2(x16511,f5(x16511),f6(a3,a3))),
% 59.78/59.89 inference(scs_inference,[],[65,1649,49,780,1,6,8])).
% 59.78/59.89 cnf(1664,plain,
% 59.78/59.89 (P2(x16641,f5(x16641),f5(a3))),
% 59.78/59.89 inference(scs_inference,[],[65,127,780,1651,92,8])).
% 59.78/59.89 cnf(2159,plain,
% 59.78/59.89 (P2(f5(x21591),f6(x21591,a1),a2)),
% 59.78/59.89 inference(scs_inference,[],[70,1,6])).
% 59.78/59.89 cnf(3202,plain,
% 59.78/59.89 (~P2(f5(a3),f6(a4,a1),f6(a4,a2))),
% 59.78/59.89 inference(scs_inference,[],[5,56,7])).
% 59.78/59.89 cnf(3263,plain,
% 59.78/59.89 ($false),
% 59.78/59.89 inference(scs_inference,[],[3202,1664,2159,4,8]),
% 59.78/59.89 ['proof']).
% 59.78/59.89 % SZS output end Proof
% 59.78/59.89 % Total time :59.190000s
%------------------------------------------------------------------------------