%------------------------------------------------------------------------------
% File : CiME---2.01
% Problem : ALG236-1 : TPTP v6.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : tptp2X_and_run_cime %s
% Computer : n106.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32286.75MB
% OS : Linux 2.6.32-431.11.2.el6.x86_64
% CPULimit : 300s
% DateTime : Tue Jun 10 00:18:18 EDT 2014
% Result : Unsatisfiable 18.96s
% Output : Refutation 18.96s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % Problem : ALG236-1 : TPTP v6.0.0. Released v4.0.0.
% % Command : tptp2X_and_run_cime %s
% % Computer : n106.star.cs.uiowa.edu
% % Model : x86_64 x86_64
% % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% % Memory : 32286.75MB
% % OS : Linux 2.6.32-431.11.2.el6.x86_64
% % CPULimit : 300
% % DateTime : Fri Jun 6 06:04:23 CDT 2014
% % CPUTime : 18.96
% Processing problem /tmp/CiME_25050_n106.star.cs.uiowa.edu
% #verbose 1;
% let F = signature " e,d,c,b,a : constant; mult : 2;";
% let X = vars "A B C D";
% let Axioms = equations F X "
% mult(A,mult(B,mult(A,B))) = mult(A,B);
% mult(A,mult(B,mult(C,D))) = mult(C,mult(B,mult(A,D)));
% mult(mult(A,mult(B,mult(C,B))),D) = mult(A,mult(D,mult(mult(C,B),D)));
% ";
%
% let s1 = status F "
% e lr_lex;
% d lr_lex;
% c lr_lex;
% b lr_lex;
% a lr_lex;
% mult lr_lex;
% ";
%
% let p1 = precedence F "
% mult > a > b > c > d > e";
%
% let s2 = status F "
% e mul;
% d mul;
% c mul;
% b mul;
% a mul;
% mult mul;
% ";
%
% let p2 = precedence F "
% mult > a = b = c = d = e";
%
% let o_auto = AUTO Axioms;
%
% let o = LEX o_auto (LEX (ACRPO s1 p1) (ACRPO s2 p2));
%
% let Conjectures = equations F X " mult(mult(a,b),mult(c,mult(d,e))) = mult(a,mult(c,mult(mult(d,b),e)));"
% ;
% (*
% let Red_Axioms = normalize_equations Defining_rules Axioms;
%
% let Red_Conjectures = normalize_equations Defining_rules Conjectures;
% *)
% #time on;
%
% let res = prove_conj_by_ordered_completion o Axioms Conjectures;
%
% #time off;
%
%
% let status = if res then "unsatisfiable" else "satisfiable";
% #quit;
% Verbose level is now 1
%
% F : signature = <signature>
% X : variable_set = <variable set>
%
% Axioms : (F,X) equations = { mult(A,mult(B,mult(A,B))) = mult(A,B),
% mult(A,mult(B,mult(C,D))) =
% mult(C,mult(B,mult(A,D))),
% mult(mult(A,mult(B,mult(C,B))),D) =
% mult(A,mult(D,mult(mult(C,B),D))) }
% (3 equation(s))
% s1 : F status = <status>
% p1 : F precedence = <precedence>
% s2 : F status = <status>
% p2 : F precedence = <precedence>
% o_auto : F term_ordering = <term ordering>
% o : F term_ordering = <term ordering>
% Conjectures : (F,X) equations = { mult(mult(a,b),mult(c,mult(d,e))) =
% mult(a,mult(c,mult(mult(d,b),e))) }
% (1 equation(s))
% time is now on
%
% Initializing completion ...
% New rule produced : [1] mult(A,mult(B,mult(A,B))) -> mult(A,B)
% Current number of equations to process: 0
% Current number of ordered equations: 4
% Current number of rules: 1
% New rule produced :
% [2] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(B,mult(A,D)))
% The conjecture has been reduced.
% Conjecture is now:
% mult(d,mult(c,mult(mult(a,b),e))) = mult(a,mult(c,mult(mult(d,b),e)))
%
% Current number of equations to process: 1
% Current number of ordered equations: 2
% Current number of rules: 2
% New rule produced :
% [3] mult(A,mult(D,mult(mult(C,B),D))) <-> mult(mult(A,mult(B,mult(C,B))),D)
% Current number of equations to process: 5
% Current number of ordered equations: 3
% Current number of rules: 3
% New rule produced :
% [4] mult(mult(A,mult(B,mult(C,B))),D) <-> mult(A,mult(D,mult(mult(C,B),D)))
% Current number of equations to process: 5
% Current number of ordered equations: 2
% Current number of rules: 4
% New rule produced :
% [5] mult(C,mult(B,mult(A,mult(B,C)))) -> mult(A,mult(B,C))
% Current number of equations to process: 5
% Current number of ordered equations: 1
% Current number of rules: 5
% New rule produced :
% [6] mult(A,mult(mult(B,mult(A,B)),mult(A,B))) -> mult(A,B)
% Current number of equations to process: 5
% Current number of ordered equations: 0
% Current number of rules: 6
% New rule produced :
% [7] mult(A,mult(C,mult(mult(A,B),C))) -> mult(mult(A,B),C)
% Current number of equations to process: 25
% Current number of ordered equations: 0
% Current number of rules: 7
% New rule produced :
% [8] mult(mult(A,mult(B,A)),mult(B,A)) -> mult(A,mult(B,A))
% Rule [6] mult(A,mult(mult(B,mult(A,B)),mult(A,B))) -> mult(A,B) collapsed.
% Current number of equations to process: 74
% Current number of ordered equations: 0
% Current number of rules: 7
% New rule produced :
% [9] mult(mult(A,B),mult(C,mult(A,C))) -> mult(mult(A,B),C)
% Current number of equations to process: 73
% Current number of ordered equations: 0
% Current number of rules: 8
% New rule produced : [10] mult(mult(mult(A,B),C),C) -> mult(mult(A,B),C)
% Current number of equations to process: 82
% Current number of ordered equations: 0
% Current number of rules: 9
% New rule produced : [11] mult(A,mult(mult(B,A),A)) -> mult(A,mult(B,A))
% Current number of equations to process: 99
% Current number of ordered equations: 0
% Current number of rules: 10
% New rule produced : [12] mult(mult(A,B),B) -> mult(A,B)
% Rule [8] mult(mult(A,mult(B,A)),mult(B,A)) -> mult(A,mult(B,A)) collapsed.
% Rule [10] mult(mult(mult(A,B),C),C) -> mult(mult(A,B),C) collapsed.
% Rule [11] mult(A,mult(mult(B,A),A)) -> mult(A,mult(B,A)) collapsed.
% Current number of equations to process: 145
% Current number of ordered equations: 0
% Current number of rules: 8
% New rule produced :
% [13] mult(A,mult(B,mult(A,mult(B,C)))) -> mult(A,mult(B,C))
% Current number of equations to process: 153
% Current number of ordered equations: 0
% Current number of rules: 9
% New rule produced :
% [14] mult(A,mult(B,mult(C,B))) <-> mult(mult(C,B),mult(B,mult(A,B)))
% Current number of equations to process: 165
% Current number of ordered equations: 1
% Current number of rules: 10
% New rule produced :
% [15] mult(mult(C,B),mult(B,mult(A,B))) <-> mult(A,mult(B,mult(C,B)))
% Current number of equations to process: 165
% Current number of ordered equations: 0
% Current number of rules: 11
% New rule produced :
% [16] mult(A,mult(B,mult(C,D))) <-> mult(mult(C,D),mult(B,mult(A,D)))
% Rule [14] mult(A,mult(B,mult(C,B))) <-> mult(mult(C,B),mult(B,mult(A,B)))
% collapsed.
% Current number of equations to process: 182
% Current number of ordered equations: 1
% Current number of rules: 11
% New rule produced :
% [17] mult(mult(C,D),mult(B,mult(A,D))) <-> mult(A,mult(B,mult(C,D)))
% Rule [15] mult(mult(C,B),mult(B,mult(A,B))) <-> mult(A,mult(B,mult(C,B)))
% collapsed.
% Current number of equations to process: 203
% Current number of ordered equations: 0
% Current number of rules: 11
% New rule produced :
% [18] mult(mult(A,B),mult(B,mult(C,B))) -> mult(A,mult(B,mult(C,B)))
% Current number of equations to process: 227
% Current number of ordered equations: 0
% Current number of rules: 12
% Rule [16] mult(A,mult(B,mult(C,D))) <-> mult(mult(C,D),mult(B,mult(A,D))) is composed into
% [16] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(B,mult(A,D)))
% New rule produced :
% [19] mult(mult(A,D),mult(B,mult(C,D))) -> mult(A,mult(B,mult(C,D)))
% Rule [17] mult(mult(C,D),mult(B,mult(A,D))) <-> mult(A,mult(B,mult(C,D)))
% collapsed.
% Rule [18] mult(mult(A,B),mult(B,mult(C,B))) -> mult(A,mult(B,mult(C,B)))
% collapsed.
% Current number of equations to process: 226
% Current number of ordered equations: 0
% Current number of rules: 11
% New rule produced :
% [20]
% mult(A,mult(B,mult(C,mult(D,V_4)))) <-> mult(C,mult(D,mult(A,mult(B,V_4))))
% Current number of equations to process: 280
% Current number of ordered equations: 0
% Current number of rules: 12
% New rule produced :
% [21] mult(mult(A,B),mult(C,mult(D,C))) <-> mult(mult(D,mult(B,mult(A,B))),C)
% Current number of equations to process: 322
% Current number of ordered equations: 1
% Current number of rules: 13
% New rule produced :
% [22] mult(mult(D,mult(B,mult(A,B))),C) <-> mult(mult(A,B),mult(C,mult(D,C)))
% Current number of equations to process: 322
% Current number of ordered equations: 0
% Current number of rules: 14
% New rule produced :
% [23] mult(C,mult(D,mult(mult(A,B),D))) <-> mult(mult(A,mult(B,mult(C,B))),D)
% Current number of equations to process: 418
% Current number of ordered equations: 1
% Current number of rules: 15
% New rule produced :
% [24] mult(mult(A,mult(B,mult(C,B))),D) <-> mult(C,mult(D,mult(mult(A,B),D)))
% Current number of equations to process: 418
% Current number of ordered equations: 0
% Current number of rules: 16
% New rule produced :
% [25] mult(mult(A,B),mult(D,mult(C,D))) <-> mult(mult(A,mult(B,mult(C,B))),D)
% Current number of equations to process: 525
% Current number of ordered equations: 1
% Current number of rules: 17
% New rule produced :
% [26] mult(mult(A,mult(B,mult(C,B))),D) <-> mult(mult(A,B),mult(D,mult(C,D)))
% Current number of equations to process: 525
% Current number of ordered equations: 0
% Current number of rules: 18
% New rule produced :
% [27] mult(A,mult(B,mult(mult(C,D),B))) <-> mult(C,mult(B,mult(mult(A,D),B)))
% Current number of equations to process: 655
% Current number of ordered equations: 0
% Current number of rules: 19
% New rule produced :
% [28] mult(A,mult(C,mult(mult(D,B),C))) <-> mult(mult(A,B),mult(C,mult(D,C)))
% Current number of equations to process: 718
% Current number of ordered equations: 1
% Current number of rules: 20
% New rule produced :
% [29] mult(mult(A,B),mult(C,mult(D,C))) <-> mult(A,mult(C,mult(mult(D,B),C)))
% Current number of equations to process: 718
% Current number of ordered equations: 0
% Current number of rules: 21
% New rule produced :
% [30] mult(mult(A,B),mult(C,mult(D,C))) <-> mult(mult(D,B),mult(C,mult(A,C)))
% Current number of equations to process: 855
% Current number of ordered equations: 0
% Current number of rules: 22
% New rule produced :
% [31] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(B,mult(A,mult(D,mult(C,D)))))
% Current number of equations to process: 925
% Current number of ordered equations: 1
% Current number of rules: 23
% New rule produced :
% [32] mult(C,mult(B,mult(A,mult(D,mult(C,D))))) <-> mult(A,mult(B,mult(C,D)))
% Current number of equations to process: 925
% Current number of ordered equations: 0
% Current number of rules: 24
% New rule produced :
% [33] mult(C,mult(D,mult(A,mult(B,mult(C,D))))) -> mult(A,mult(B,mult(C,D)))
% Current number of equations to process: 1060
% Current number of ordered equations: 0
% Current number of rules: 25
% New rule produced :
% [34] mult(A,mult(B,mult(mult(mult(A,C),D),B))) -> mult(mult(mult(A,C),D),B)
% Current number of equations to process: 1149
% Current number of ordered equations: 0
% Current number of rules: 26
% New rule produced :
% [35] mult(D,mult(B,mult(A,mult(mult(B,C),D)))) -> mult(A,mult(mult(B,C),D))
% Current number of equations to process: 1233
% Current number of ordered equations: 0
% Current number of rules: 27
% New rule produced :
% [36] mult(A,mult(B,mult(mult(C,mult(D,A)),B))) -> mult(mult(C,mult(D,A)),B)
% Current number of equations to process: 1322
% Current number of ordered equations: 0
% Current number of rules: 28
% New rule produced :
% [37] mult(A,mult(B,mult(C,B))) <-> mult(C,mult(mult(B,mult(C,B)),mult(A,B)))
% Current number of equations to process: 1415
% Current number of ordered equations: 1
% Current number of rules: 29
% New rule produced :
% [38] mult(C,mult(mult(B,mult(C,B)),mult(A,B))) <-> mult(A,mult(B,mult(C,B)))
% Current number of equations to process: 1415
% Current number of ordered equations: 0
% Current number of rules: 30
% New rule produced :
% [39] mult(mult(A,mult(B,C)),mult(D,mult(C,D))) -> mult(mult(A,mult(B,C)),D)
% Current number of equations to process: 1541
% Current number of ordered equations: 0
% Current number of rules: 31
% New rule produced :
% [40] mult(A,mult(mult(B,C),D)) <-> mult(D,mult(mult(B,C),mult(A,mult(B,D))))
% Current number of equations to process: 1636
% Current number of ordered equations: 1
% Current number of rules: 32
% New rule produced :
% [41] mult(D,mult(mult(B,C),mult(A,mult(B,D)))) <-> mult(A,mult(mult(B,C),D))
% Current number of equations to process: 1636
% Current number of ordered equations: 0
% Current number of rules: 33
% New rule produced :
% [42] mult(mult(A,B),mult(D,mult(mult(A,C),D))) <-> mult(mult(mult(A,B),C),D)
% Current number of equations to process: 1859
% Current number of ordered equations: 1
% Current number of rules: 34
% New rule produced :
% [43] mult(mult(mult(A,B),C),D) <-> mult(mult(A,B),mult(D,mult(mult(A,C),D)))
% Current number of equations to process: 1859
% Current number of ordered equations: 0
% Current number of rules: 35
% New rule produced :
% [44] mult(mult(mult(A,B),C),D) <-> mult(mult(mult(A,C),B),D)
% Current number of equations to process: 1893
% Current number of ordered equations: 0
% Current number of rules: 36
% New rule produced :
% [45]
% mult(mult(mult(mult(A,C),D),B),V_4) <-> mult(mult(mult(mult(A,B),C),D),V_4)
% Current number of equations to process: 2296
% Current number of ordered equations: 1
% Current number of rules: 37
% New rule produced :
% [46]
% mult(mult(mult(mult(A,B),C),D),V_4) <-> mult(mult(mult(mult(A,C),D),B),V_4)
% Current number of equations to process: 2296
% Current number of ordered equations: 0
% Current number of rules: 38
% New rule produced :
% [47]
% mult(mult(mult(mult(A,B),C),D),V_4) <-> mult(mult(mult(mult(A,D),C),B),V_4)
% Current number of equations to process: 2632
% Current number of ordered equations: 0
% Current number of rules: 39
% New rule produced :
% [48] mult(mult(mult(A,B),C),mult(D,mult(A,D))) -> mult(mult(mult(A,B),C),D)
% Current number of equations to process: 2936
% Current number of ordered equations: 0
% Current number of rules: 40
% New rule produced :
% [49] mult(A,mult(B,mult(mult(C,mult(D,C)),B))) <-> mult(mult(A,mult(D,C)),B)
% Current number of equations to process: 3062
% Current number of ordered equations: 1
% Current number of rules: 41
% New rule produced :
% [50] mult(mult(A,mult(D,C)),B) <-> mult(A,mult(B,mult(mult(C,mult(D,C)),B)))
% Current number of equations to process: 3062
% Current number of ordered equations: 0
% Current number of rules: 42
% New rule produced :
% [51] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(mult(B,mult(C,D)),mult(A,D)))
% Rule
% [37] mult(A,mult(B,mult(C,B))) <-> mult(C,mult(mult(B,mult(C,B)),mult(A,B)))
% collapsed.
% Current number of equations to process: 3363
% Current number of ordered equations: 1
% Current number of rules: 42
% New rule produced :
% [52] mult(C,mult(mult(B,mult(C,D)),mult(A,D))) <-> mult(A,mult(B,mult(C,D)))
% Rule
% [38] mult(C,mult(mult(B,mult(C,B)),mult(A,B))) <-> mult(A,mult(B,mult(C,B)))
% collapsed.
% Current number of equations to process: 3363
% Current number of ordered equations: 0
% Current number of rules: 42
% New rule produced :
% [53] mult(A,mult(mult(B,mult(A,mult(B,C))),C)) -> mult(A,mult(B,C))
% Current number of equations to process: 3386
% Current number of ordered equations: 0
% Current number of rules: 43
% New rule produced :
% [54] mult(A,mult(B,mult(A,mult(C,mult(D,B))))) -> mult(A,mult(C,mult(D,B)))
% Current number of equations to process: 3781
% Current number of ordered equations: 0
% Current number of rules: 44
% New rule produced :
% [55] mult(A,mult(B,mult(A,mult(C,D)))) <-> mult(D,mult(B,mult(A,mult(C,D))))
% Current number of equations to process: 3795
% Current number of ordered equations: 1
% Current number of rules: 45
% New rule produced :
% [56] mult(D,mult(B,mult(A,mult(C,D)))) <-> mult(A,mult(B,mult(A,mult(C,D))))
% Current number of equations to process: 3795
% Current number of ordered equations: 0
% Current number of rules: 46
% New rule produced :
% [57] mult(A,mult(B,mult(A,mult(C,D)))) <-> mult(D,mult(C,mult(A,mult(B,D))))
% Current number of equations to process: 3929
% Current number of ordered equations: 1
% Current number of rules: 47
% New rule produced :
% [58] mult(D,mult(C,mult(A,mult(B,D)))) <-> mult(A,mult(B,mult(A,mult(C,D))))
% Current number of equations to process: 3929
% Current number of ordered equations: 0
% Current number of rules: 48
% New rule produced :
% [59] mult(A,mult(B,mult(C,mult(D,C)))) <-> mult(A,mult(B,mult(A,mult(D,C))))
% Current number of equations to process: 4083
% Current number of ordered equations: 1
% Current number of rules: 49
% New rule produced :
% [60] mult(A,mult(B,mult(A,mult(D,C)))) <-> mult(A,mult(B,mult(C,mult(D,C))))
% Current number of equations to process: 4083
% Current number of ordered equations: 0
% Current number of rules: 50
% New rule produced :
% [61] mult(A,mult(B,mult(C,mult(D,C)))) <-> mult(A,mult(D,mult(A,mult(B,C))))
% Current number of equations to process: 4141
% Current number of ordered equations: 1
% Current number of rules: 51
% New rule produced :
% [62] mult(A,mult(D,mult(A,mult(B,C)))) <-> mult(A,mult(B,mult(C,mult(D,C))))
% Current number of equations to process: 4141
% Current number of ordered equations: 0
% Current number of rules: 52
% New rule produced :
% [63] mult(A,mult(B,mult(A,mult(mult(B,C),D)))) -> mult(A,mult(mult(B,C),D))
% Current number of equations to process: 2910
% Current number of ordered equations: 0
% Current number of rules: 53
% New rule produced :
% [64] mult(A,mult(B,mult(C,mult(B,mult(A,D))))) -> mult(A,mult(B,mult(C,D)))
% Current number of equations to process: 3088
% Current number of ordered equations: 0
% Current number of rules: 54
% New rule produced :
% [65] mult(A,mult(B,mult(mult(A,C),mult(B,D)))) -> mult(mult(A,C),mult(B,D))
% Current number of equations to process: 3281
% Current number of ordered equations: 0
% Current number of rules: 55
% New rule produced :
% [66] mult(mult(A,B),mult(C,mult(A,mult(C,D)))) -> mult(mult(A,B),mult(C,D))
% Current number of equations to process: 3485
% Current number of ordered equations: 0
% Current number of rules: 56
% New rule produced :
% [67] mult(mult(A,mult(B,C)),mult(mult(B,D),C)) -> mult(A,mult(mult(B,D),C))
% Current number of equations to process: 3683
% Current number of ordered equations: 0
% Current number of rules: 57
% New rule produced :
% [68] mult(mult(D,mult(B,mult(A,B))),mult(C,D)) -> mult(mult(A,B),mult(C,D))
% Current number of equations to process: 3911
% Current number of ordered equations: 0
% Current number of rules: 58
% New rule produced :
% [69] mult(mult(A,C),mult(D,mult(mult(A,B),D))) <-> mult(mult(mult(A,B),C),D)
% Current number of equations to process: 4075
% Current number of ordered equations: 3
% Current number of rules: 59
% New rule produced :
% [70] mult(mult(A,mult(B,C)),D) <-> mult(mult(C,mult(B,C)),mult(D,mult(A,D)))
% Current number of equations to process: 4075
% Current number of ordered equations: 2
% Current number of rules: 60
% New rule produced :
% [71] mult(mult(C,mult(B,C)),mult(D,mult(A,D))) <-> mult(mult(A,mult(B,C)),D)
% Current number of equations to process: 4075
% Current number of ordered equations: 1
% Current number of rules: 61
% New rule produced :
% [72] mult(mult(mult(A,B),C),D) <-> mult(mult(A,C),mult(D,mult(mult(A,B),D)))
% Current number of equations to process: 4075
% Current number of ordered equations: 0
% Current number of rules: 62
% New rule produced :
% [73] mult(mult(A,mult(B,mult(D,B))),mult(C,D)) -> mult(mult(A,B),mult(C,D))
% Current number of equations to process: 2487
% Current number of ordered equations: 0
% Current number of rules: 63
% New rule produced :
% [74] mult(A,mult(C,mult(mult(D,B),mult(C,D)))) <-> mult(mult(A,B),mult(C,D))
% Current number of equations to process: 2664
% Current number of ordered equations: 1
% Current number of rules: 64
% New rule produced :
% [75] mult(mult(A,B),mult(C,D)) <-> mult(A,mult(C,mult(mult(D,B),mult(C,D))))
% Current number of equations to process: 2664
% Current number of ordered equations: 0
% Current number of rules: 65
% New rule produced :
% [76]
% mult(A,mult(B,mult(mult(C,D),V_4))) <-> mult(mult(A,D),mult(B,mult(C,V_4)))
% Rule
% [28] mult(A,mult(C,mult(mult(D,B),C))) <-> mult(mult(A,B),mult(C,mult(D,C)))
% collapsed.
% The conjecture has been reduced.
% Conjecture is now:
% Trivial
%
% Current number of equations to process: 2671
% Current number of ordered equations: 1
% Current number of rules: 65
% The current conjecture is true and the solution is the identity
% % SZS output start Refutation
%
% The following 16 rules have been used:
% [1]
% mult(A,mult(B,mult(A,B))) -> mult(A,B); trace = in the starting set
% [2] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(B,mult(A,D))); trace = in the starting set
% [3] mult(A,mult(D,mult(mult(C,B),D))) <-> mult(mult(A,mult(B,mult(C,B))),D); trace = in the starting set
% [4] mult(mult(A,mult(B,mult(C,B))),D) <-> mult(A,mult(D,mult(mult(C,B),D))); trace = in the starting set
% [5] mult(C,mult(B,mult(A,mult(B,C)))) -> mult(A,mult(B,C)); trace = Cp of 2 and 1
% [6] mult(A,mult(mult(B,mult(A,B)),mult(A,B))) -> mult(A,B); trace = Self cp of 1
% [7] mult(A,mult(C,mult(mult(A,B),C))) -> mult(mult(A,B),C); trace = Cp of 4 and 1
% [8] mult(mult(A,mult(B,A)),mult(B,A)) -> mult(A,mult(B,A)); trace = Cp of 6 and 5
% [11] mult(A,mult(mult(B,A),A)) -> mult(A,mult(B,A)); trace = Cp of 8 and 7
% [12] mult(mult(A,B),B) -> mult(A,B); trace = Cp of 11 and 7
% [16] mult(A,mult(B,mult(C,D))) <-> mult(C,mult(B,mult(A,D))); trace = Cp of 12 and 2
% [22] mult(mult(D,mult(B,mult(A,B))),C) <-> mult(mult(A,B),mult(C,mult(D,C))); trace = Cp of 3 and 2
% [24] mult(mult(A,mult(B,mult(C,B))),D) <-> mult(C,mult(D,mult(mult(A,B),D))); trace = Cp of 4 and 2
% [29] mult(mult(A,B),mult(C,mult(D,C))) <-> mult(A,mult(C,mult(mult(D,B),C))); trace = Cp of 24 and 22
% [74] mult(A,mult(C,mult(mult(D,B),mult(C,D)))) <-> mult(mult(A,B),mult(C,D)); trace = Self cp of 29
% [76] mult(A,mult(B,mult(mult(C,D),V_4))) <->
% mult(mult(A,D),mult(B,mult(C,V_4))); trace = Cp of 74 and 16
% % SZS output end Refutation
% All conjectures have been proven
%
% Execution time: 17.820000 sec
% res : bool = true
% time is now off
%
% status : string = "unsatisfiable"
% % SZS status Unsatisfiable
% CiME interrupted
%
% EOF
%------------------------------------------------------------------------------