%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : COM014+1 : TPTP v6.4.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n067.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Tue Apr 12 12:12:01 EDT 2016
% Result : CounterSatisfiable 132.17s
% Output : Assurance 0s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM014+1 : TPTP v6.4.0. Released v4.0.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.22 % Computer : n067.star.cs.uiowa.edu
% 0.03/0.22 % Model : x86_64 x86_64
% 0.03/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.22 % Memory : 32218.75MB
% 0.03/0.22 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Sat Apr 9 06:28:39 CDT 2016
% 0.03/0.23 % CPUTime :
% 6.31/5.84 > val it = (): unit
% 6.51/6.04 Trying to find a model that refutes: (bnd_aRewritingSystem0 W0 & bnd_isTerminating0 W0) &
% 6.51/6.04 bnd_isLocallyConfluent0 W0 -->
% 6.51/6.04 bnd_isConfluent0 W0
% 6.91/6.51 Unfolded term: [| ALL W0 W1.
% 6.91/6.51 bnd_aElement0 W0 & bnd_aRewritingSystem0 W1 -->
% 6.91/6.51 (ALL W2.
% 6.91/6.51 bnd_aNormalFormOfIn0 W2 W0 W1 =
% 6.91/6.51 ((bnd_aElement0 W2 & bnd_sdtmndtasgtdt0 W0 W1 W2) &
% 6.91/6.51 ~ (EX W3. bnd_aReductOfIn0 W3 W2 W1)));
% 6.91/6.51 ALL W0.
% 6.91/6.51 bnd_aRewritingSystem0 W0 -->
% 6.91/6.51 bnd_isTerminating0 W0 =
% 6.91/6.51 (ALL W1 W2.
% 6.91/6.51 bnd_aElement0 W1 & bnd_aElement0 W2 -->
% 6.91/6.51 bnd_sdtmndtplgtdt0 W1 W0 W2 --> bnd_iLess0 W2 W1);
% 6.91/6.51 ALL W0.
% 6.91/6.51 bnd_aRewritingSystem0 W0 -->
% 6.91/6.51 bnd_isLocallyConfluent0 W0 =
% 6.91/6.51 (ALL W1 W2 W3.
% 6.91/6.51 (((bnd_aElement0 W1 & bnd_aElement0 W2) & bnd_aElement0 W3) &
% 6.91/6.51 bnd_aReductOfIn0 W2 W1 W0) &
% 6.91/6.51 bnd_aReductOfIn0 W3 W1 W0 -->
% 6.91/6.51 (EX W4.
% 6.91/6.51 (bnd_aElement0 W4 & bnd_sdtmndtasgtdt0 W2 W0 W4) &
% 6.91/6.51 bnd_sdtmndtasgtdt0 W3 W0 W4));
% 6.91/6.51 ALL W0.
% 6.91/6.51 bnd_aRewritingSystem0 W0 -->
% 6.91/6.51 bnd_isConfluent0 W0 =
% 6.91/6.51 (ALL W1 W2 W3.
% 6.91/6.51 (((bnd_aElement0 W1 & bnd_aElement0 W2) & bnd_aElement0 W3) &
% 6.91/6.51 bnd_sdtmndtasgtdt0 W1 W0 W2) &
% 6.91/6.51 bnd_sdtmndtasgtdt0 W1 W0 W3 -->
% 6.91/6.51 (EX W4.
% 6.91/6.51 (bnd_aElement0 W4 & bnd_sdtmndtasgtdt0 W2 W0 W4) &
% 6.91/6.51 bnd_sdtmndtasgtdt0 W3 W0 W4));
% 6.91/6.51 ALL W0 W1 W2.
% 6.91/6.51 (bnd_aElement0 W0 & bnd_aRewritingSystem0 W1) & bnd_aElement0 W2 -->
% 6.91/6.51 bnd_sdtmndtasgtdt0 W0 W1 W2 = (W0 = W2 | bnd_sdtmndtplgtdt0 W0 W1 W2);
% 6.91/6.51 ALL W0 W1 W2.
% 6.91/6.51 (bnd_aElement0 W0 & bnd_aRewritingSystem0 W1) & bnd_aElement0 W2 -->
% 6.91/6.51 bnd_sdtmndtplgtdt0 W0 W1 W2 =
% 6.91/6.51 (bnd_aReductOfIn0 W2 W0 W1 |
% 6.91/6.51 (EX W3.
% 6.91/6.51 (bnd_aElement0 W3 & bnd_aReductOfIn0 W3 W0 W1) &
% 6.91/6.51 bnd_sdtmndtplgtdt0 W3 W1 W2));
% 6.91/6.51 ALL W0.
% 6.91/6.51 bnd_aRewritingSystem0 W0 & bnd_isTerminating0 W0 -->
% 6.91/6.51 (ALL W1. bnd_aElement0 W1 --> (EX W2. bnd_aNormalFormOfIn0 W2 W1 W0));
% 6.91/6.51 ALL W0 W1 W2 W3.
% 6.91/6.51 ((bnd_aElement0 W0 & bnd_aRewritingSystem0 W1) & bnd_aElement0 W2) &
% 6.91/6.51 bnd_aElement0 W3 -->
% 6.91/6.51 bnd_sdtmndtasgtdt0 W0 W1 W2 & bnd_sdtmndtasgtdt0 W2 W1 W3 -->
% 6.91/6.51 bnd_sdtmndtasgtdt0 W0 W1 W3;
% 6.91/6.51 ALL W0 W1 W2 W3.
% 6.91/6.51 ((bnd_aElement0 W0 & bnd_aRewritingSystem0 W1) & bnd_aElement0 W2) &
% 6.91/6.51 bnd_aElement0 W3 -->
% 6.91/6.51 bnd_sdtmndtplgtdt0 W0 W1 W2 & bnd_sdtmndtplgtdt0 W2 W1 W3 -->
% 6.91/6.51 bnd_sdtmndtplgtdt0 W0 W1 W3;
% 6.91/6.51 ALL W0 W1 W2.
% 6.91/6.51 (bnd_aElement0 W0 & bnd_aRewritingSystem0 W1) & bnd_aElement0 W2 -->
% 6.91/6.51 bnd_sdtmndtplgtdt0 W0 W1 W2 --> True;
% 6.91/6.51 ALL W0 W1.
% 6.91/6.51 bnd_aElement0 W0 & bnd_aElement0 W1 --> bnd_iLess0 W0 W1 --> True;
% 6.91/6.51 ALL W0 W1.
% 6.91/6.51 bnd_aElement0 W0 & bnd_aRewritingSystem0 W1 -->
% 6.91/6.51 (ALL W2. bnd_aReductOfIn0 W2 W0 W1 --> bnd_aElement0 W2);
% 6.91/6.51 ALL W0. bnd_aRewritingSystem0 W0 --> True;
% 6.91/6.51 ALL W0. bnd_aElement0 W0 --> True |]
% 6.91/6.51 ==> (bnd_aRewritingSystem0 W0 & bnd_isTerminating0 W0) &
% 6.91/6.51 bnd_isLocallyConfluent0 W0 -->
% 6.91/6.51 bnd_isConfluent0 W0
% 6.91/6.51 Adding axioms...
% 7.02/6.51 Typedef.type_definition_def
% 9.32/8.87 ...done.
% 9.32/8.87 Ground types: ?'b, TPTP_Interpret.ind
% 9.32/8.87 Translating term (sizes: 1, 1) ...
% 11.32/10.81 Invoking SAT solver...
% 11.32/10.81 No model exists.
% 11.32/10.81 Translating term (sizes: 2, 1) ...
% 13.92/13.40 Invoking SAT solver...
% 13.92/13.40 No model exists.
% 13.92/13.40 Translating term (sizes: 1, 2) ...
% 29.25/28.77 Invoking SAT solver...
% 29.45/28.91 No model exists.
% 29.45/28.91 Translating term (sizes: 3, 1) ...
% 34.26/33.74 Invoking SAT solver...
% 34.26/33.74 No model exists.
% 34.26/33.74 Translating term (sizes: 2, 2) ...
% 57.42/56.80 Invoking SAT solver...
% 57.42/56.80 No model exists.
% 57.42/56.80 Translating term (sizes: 1, 3) ...
% 131.37/130.51 Invoking SAT solver...
% 132.17/131.37 Model found:
% 132.17/131.37 Size of types: ?'b: 1, TPTP_Interpret.ind: 3
% 132.17/131.37 W0: ??.TPTP_Interpret.ind2
% 132.17/131.37 bnd_isConfluent0: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}
% 132.17/131.37 bnd_isLocallyConfluent0: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}
% 132.17/131.37 bnd_iLess0: {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)})}
% 132.17/131.37 bnd_sdtmndtplgtdt0: {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})})}
% 132.17/131.37 bnd_isTerminating0: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}
% 132.17/131.37 bnd_aReductOfIn0: {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})})}
% 132.17/131.37 bnd_sdtmndtasgtdt0: {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)})})}
% 132.17/131.37 bnd_aNormalFormOfIn0: {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)})}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}),
% 132.17/131.37 (??.TPTP_Interpret.ind1,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, False)}),
% 132.17/131.37 (??.TPTP_Interpret.ind2,
% 132.17/131.37 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)})})}
% 132.17/131.37 bnd_aRewritingSystem0: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}
% 132.17/131.37 bnd_aElement0: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True),
% 132.17/131.37 (??.TPTP_Interpret.ind2, True)}
% 132.17/131.37
% 132.17/131.37 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------