%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN523+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n087.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 : Thu Apr 14 06:42:14 EDT 2016
% Result : CounterSatisfiable 12.21s
% 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 : SYN523+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.22 % Computer : n087.star.cs.uiowa.edu
% 0.02/0.22 % Model : x86_64 x86_64
% 0.02/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.22 % Memory : 32218.75MB
% 0.02/0.22 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.22 % CPULimit : 300
% 0.02/0.22 % DateTime : Sat Apr 9 00:13:24 CDT 2016
% 0.02/0.22 % CPUTime:
% 6.30/5.85 > val it = (): unit
% 6.60/6.11 Trying to find a model that refutes: ~ ((((((((((((((ALL U.
% 6.60/6.11 bnd_ndr1_0 -->
% 6.60/6.11 (((bnd_ndr1_1 U & ~ bnd_c2_2 U bnd_a141) &
% 6.60/6.11 ~ bnd_c5_2 U bnd_a141) &
% 6.60/6.11 ~ bnd_c1_2 U bnd_a141 |
% 6.60/6.11 (bnd_ndr1_1 U & bnd_c3_2 U bnd_a142) &
% 6.60/6.11 ~ bnd_c4_2 U bnd_a142) |
% 6.60/6.11 ~ bnd_c1_1 U) |
% 6.60/6.11 bnd_ndr1_0 & ~ bnd_c1_1 bnd_a143) |
% 6.60/6.11 ~ bnd_c2_0) &
% 6.60/6.11 ((bnd_c5_0 | bnd_c2_0) | bnd_c1_0)) &
% 6.60/6.11 (~ bnd_c4_0 |
% 6.60/6.11 ((bnd_ndr1_0 &
% 6.60/6.11 (ALL V.
% 6.60/6.11 bnd_ndr1_1 bnd_a144 -->
% 6.60/6.11 (bnd_c3_2 bnd_a144 V | bnd_c4_2 bnd_a144 V) |
% 6.60/6.11 ~ bnd_c5_2 bnd_a144 V)) &
% 6.60/6.11 bnd_c5_1 bnd_a144) &
% 6.60/6.11 ~ bnd_c4_1 bnd_a144)) &
% 6.60/6.11 (~ bnd_c1_0 |
% 6.60/6.11 (ALL W.
% 6.60/6.11 bnd_ndr1_0 -->
% 6.60/6.11 (~ bnd_c5_1 W | ~ bnd_c3_1 W) |
% 6.60/6.11 (ALL X. bnd_ndr1_1 W --> bnd_c4_2 W X | bnd_c1_2 W X)))) &
% 6.60/6.11 (((bnd_ndr1_0 &
% 6.60/6.11 (ALL Y.
% 6.60/6.11 bnd_ndr1_1 bnd_a145 -->
% 6.60/6.11 (~ bnd_c2_2 bnd_a145 Y | ~ bnd_c5_2 bnd_a145 Y) |
% 6.60/6.11 ~ bnd_c1_2 bnd_a145 Y)) &
% 6.60/6.11 bnd_c3_1 bnd_a145) &
% 6.60/6.11 ~ bnd_c5_1 bnd_a145 |
% 6.60/6.11 bnd_c2_0)) &
% 6.60/6.11 (((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a146) & bnd_c4_1 bnd_a146 |
% 6.60/6.11 bnd_c4_0) |
% 6.60/6.11 (ALL Z.
% 6.60/6.11 bnd_ndr1_0 -->
% 6.60/6.11 bnd_c5_1 Z |
% 6.60/6.11 ((bnd_ndr1_1 Z & bnd_c3_2 Z bnd_a147) &
% 6.60/6.11 ~ bnd_c1_2 Z bnd_a147) &
% 6.60/6.11 ~ bnd_c5_2 Z bnd_a147))) &
% 6.60/6.11 ((~ bnd_c5_0 | ~ bnd_c1_0) |
% 6.60/6.11 ((bnd_ndr1_0 & bnd_c5_1 bnd_a148) & ~ bnd_c3_1 bnd_a148) &
% 6.60/6.11 ~ bnd_c2_1 bnd_a148)) &
% 6.60/6.11 (((ALL X1.
% 6.60/6.11 bnd_ndr1_0 -->
% 6.60/6.11 ((bnd_ndr1_1 X1 & bnd_c5_2 X1 bnd_a149) &
% 6.60/6.11 bnd_c4_2 X1 bnd_a149 |
% 6.60/6.11 bnd_c4_1 X1) |
% 6.60/6.11 bnd_c3_1 X1) |
% 6.60/6.11 (bnd_ndr1_0 &
% 6.60/6.11 (ALL X2.
% 6.60/6.11 bnd_ndr1_1 bnd_a150 -->
% 6.60/6.11 bnd_c5_2 bnd_a150 X2 | ~ bnd_c4_2 bnd_a150 X2)) &
% 6.60/6.11 ~ bnd_c4_1 bnd_a150) |
% 6.60/6.11 bnd_c3_0)) &
% 6.60/6.11 (~ bnd_c3_0 |
% 6.60/6.11 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a151) & ~ bnd_c3_1 bnd_a151)) &
% 6.60/6.11 ((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a152) & ~ bnd_c1_1 bnd_a152) &
% 6.60/6.11 bnd_c3_1 bnd_a152 |
% 6.60/6.11 bnd_c2_0) |
% 6.60/6.11 (ALL X3. bnd_ndr1_0 --> bnd_c5_1 X3 | bnd_c4_1 X3))) &
% 6.60/6.11 (((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a153) & ~ bnd_c5_1 bnd_a153 |
% 6.60/6.11 ((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a154) & bnd_c1_1 bnd_a154) &
% 6.60/6.11 (ALL X4.
% 6.60/6.11 bnd_ndr1_1 bnd_a154 -->
% 6.60/6.11 ~ bnd_c5_2 bnd_a154 X4 | ~ bnd_c1_2 bnd_a154 X4)) |
% 6.60/6.11 bnd_c3_0)) &
% 6.60/6.11 ((~ bnd_c4_0 |
% 6.60/6.11 (ALL X5. bnd_ndr1_0 --> (bnd_c4_1 X5 | bnd_c5_1 X5) | bnd_c1_1 X5)) |
% 6.60/6.11 (((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a155) & bnd_ndr1_1 bnd_a155) &
% 6.60/6.11 bnd_c1_2 bnd_a155 bnd_a156) &
% 6.60/6.11 bnd_c5_2 bnd_a155 bnd_a156) &
% 6.60/6.11 bnd_c2_2 bnd_a155 bnd_a156) &
% 6.60/6.11 (ALL X6.
% 6.60/6.11 bnd_ndr1_1 bnd_a155 -->
% 6.60/6.11 (~ bnd_c4_2 bnd_a155 X6 | ~ bnd_c2_2 bnd_a155 X6) |
% 6.60/6.11 bnd_c5_2 bnd_a155 X6)))
% 7.40/6.97 Unfolded term: ~ ((((((((((((((ALL U.
% 7.40/6.97 bnd_ndr1_0 -->
% 7.40/6.97 (((bnd_ndr1_1 U & ~ bnd_c2_2 U bnd_a141) &
% 7.40/6.97 ~ bnd_c5_2 U bnd_a141) &
% 7.40/6.97 ~ bnd_c1_2 U bnd_a141 |
% 7.40/6.97 (bnd_ndr1_1 U & bnd_c3_2 U bnd_a142) &
% 7.40/6.97 ~ bnd_c4_2 U bnd_a142) |
% 7.40/6.97 ~ bnd_c1_1 U) |
% 7.40/6.97 bnd_ndr1_0 & ~ bnd_c1_1 bnd_a143) |
% 7.40/6.97 ~ bnd_c2_0) &
% 7.40/6.97 ((bnd_c5_0 | bnd_c2_0) | bnd_c1_0)) &
% 7.40/6.97 (~ bnd_c4_0 |
% 7.40/6.97 ((bnd_ndr1_0 &
% 7.40/6.97 (ALL V.
% 7.40/6.97 bnd_ndr1_1 bnd_a144 -->
% 7.40/6.97 (bnd_c3_2 bnd_a144 V | bnd_c4_2 bnd_a144 V) |
% 7.40/6.97 ~ bnd_c5_2 bnd_a144 V)) &
% 7.40/6.97 bnd_c5_1 bnd_a144) &
% 7.40/6.97 ~ bnd_c4_1 bnd_a144)) &
% 7.40/6.97 (~ bnd_c1_0 |
% 7.40/6.97 (ALL W.
% 7.40/6.97 bnd_ndr1_0 -->
% 7.40/6.97 (~ bnd_c5_1 W | ~ bnd_c3_1 W) |
% 7.40/6.97 (ALL X. bnd_ndr1_1 W --> bnd_c4_2 W X | bnd_c1_2 W X)))) &
% 7.40/6.97 (((bnd_ndr1_0 &
% 7.40/6.97 (ALL Y.
% 7.40/6.97 bnd_ndr1_1 bnd_a145 -->
% 7.40/6.97 (~ bnd_c2_2 bnd_a145 Y | ~ bnd_c5_2 bnd_a145 Y) |
% 7.40/6.97 ~ bnd_c1_2 bnd_a145 Y)) &
% 7.40/6.97 bnd_c3_1 bnd_a145) &
% 7.40/6.97 ~ bnd_c5_1 bnd_a145 |
% 7.40/6.97 bnd_c2_0)) &
% 7.40/6.97 (((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a146) & bnd_c4_1 bnd_a146 |
% 7.40/6.97 bnd_c4_0) |
% 7.40/6.97 (ALL Z.
% 7.40/6.97 bnd_ndr1_0 -->
% 7.40/6.97 bnd_c5_1 Z |
% 7.40/6.97 ((bnd_ndr1_1 Z & bnd_c3_2 Z bnd_a147) &
% 7.40/6.97 ~ bnd_c1_2 Z bnd_a147) &
% 7.40/6.97 ~ bnd_c5_2 Z bnd_a147))) &
% 7.40/6.97 ((~ bnd_c5_0 | ~ bnd_c1_0) |
% 7.40/6.97 ((bnd_ndr1_0 & bnd_c5_1 bnd_a148) & ~ bnd_c3_1 bnd_a148) &
% 7.40/6.97 ~ bnd_c2_1 bnd_a148)) &
% 7.40/6.97 (((ALL X1.
% 7.40/6.97 bnd_ndr1_0 -->
% 7.40/6.97 ((bnd_ndr1_1 X1 & bnd_c5_2 X1 bnd_a149) &
% 7.40/6.97 bnd_c4_2 X1 bnd_a149 |
% 7.40/6.97 bnd_c4_1 X1) |
% 7.40/6.97 bnd_c3_1 X1) |
% 7.40/6.97 (bnd_ndr1_0 &
% 7.40/6.97 (ALL X2.
% 7.40/6.97 bnd_ndr1_1 bnd_a150 -->
% 7.40/6.97 bnd_c5_2 bnd_a150 X2 | ~ bnd_c4_2 bnd_a150 X2)) &
% 7.40/6.97 ~ bnd_c4_1 bnd_a150) |
% 7.40/6.97 bnd_c3_0)) &
% 7.40/6.97 (~ bnd_c3_0 |
% 7.40/6.97 (bnd_ndr1_0 & ~ bnd_c2_1 bnd_a151) & ~ bnd_c3_1 bnd_a151)) &
% 7.40/6.97 ((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a152) & ~ bnd_c1_1 bnd_a152) &
% 7.40/6.97 bnd_c3_1 bnd_a152 |
% 7.40/6.97 bnd_c2_0) |
% 7.40/6.97 (ALL X3. bnd_ndr1_0 --> bnd_c5_1 X3 | bnd_c4_1 X3))) &
% 7.40/6.97 (((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a153) & ~ bnd_c5_1 bnd_a153 |
% 7.40/6.97 ((bnd_ndr1_0 & ~ bnd_c5_1 bnd_a154) & bnd_c1_1 bnd_a154) &
% 7.40/6.97 (ALL X4.
% 7.40/6.97 bnd_ndr1_1 bnd_a154 -->
% 7.40/6.97 ~ bnd_c5_2 bnd_a154 X4 | ~ bnd_c1_2 bnd_a154 X4)) |
% 7.40/6.97 bnd_c3_0)) &
% 7.40/6.97 ((~ bnd_c4_0 |
% 7.40/6.97 (ALL X5. bnd_ndr1_0 --> (bnd_c4_1 X5 | bnd_c5_1 X5) | bnd_c1_1 X5)) |
% 7.40/6.97 (((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a155) & bnd_ndr1_1 bnd_a155) &
% 7.40/6.97 bnd_c1_2 bnd_a155 bnd_a156) &
% 7.40/6.97 bnd_c5_2 bnd_a155 bnd_a156) &
% 7.40/6.97 bnd_c2_2 bnd_a155 bnd_a156) &
% 7.40/6.97 (ALL X6.
% 7.40/6.97 bnd_ndr1_1 bnd_a155 -->
% 7.40/6.97 (~ bnd_c4_2 bnd_a155 X6 | ~ bnd_c2_2 bnd_a155 X6) |
% 7.40/6.97 bnd_c5_2 bnd_a155 X6)))
% 7.40/6.97 Adding axioms...
% 7.40/6.98 Typedef.type_definition_def
% 9.81/9.39 ...done.
% 9.81/9.39 Ground types: ?'b, TPTP_Interpret.ind
% 9.81/9.39 Translating term (sizes: 1, 1) ...
% 12.11/11.62 Invoking SAT solver...
% 12.21/11.72 Model found:
% 12.21/11.72 Size of types: ?'b: 1, TPTP_Interpret.ind: 1
% 12.21/11.72 bnd_a156: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a155: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a154: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a153: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a152: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a151: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c3_0: True
% 12.21/11.72 bnd_a150: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a149: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c2_1: {(??.TPTP_Interpret.ind0, False)}
% 12.21/11.72 bnd_a148: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a147: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a146: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_a145: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c3_1: {(??.TPTP_Interpret.ind0, False)}
% 12.21/11.72 bnd_c4_1: {(??.TPTP_Interpret.ind0, False)}
% 12.21/11.72 bnd_c5_1: {(??.TPTP_Interpret.ind0, True)}
% 12.21/11.72 bnd_a144: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c4_0: False
% 12.21/11.72 bnd_c1_0: False
% 12.21/11.72 bnd_c5_0: True
% 12.21/11.72 bnd_c2_0: True
% 12.21/11.72 bnd_a143: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c1_1: {(??.TPTP_Interpret.ind0, False)}
% 12.21/11.72 bnd_c4_2: {(??.TPTP_Interpret.ind0, {(??.TPTP_Interpret.ind0, False)})}
% 12.21/11.72 bnd_a142: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c3_2: {(??.TPTP_Interpret.ind0, {(??.TPTP_Interpret.ind0, True)})}
% 12.21/11.72 bnd_c1_2: {(??.TPTP_Interpret.ind0, {(??.TPTP_Interpret.ind0, True)})}
% 12.21/11.72 bnd_c5_2: {(??.TPTP_Interpret.ind0, {(??.TPTP_Interpret.ind0, True)})}
% 12.21/11.72 bnd_a141: ??.TPTP_Interpret.ind0
% 12.21/11.72 bnd_c2_2: {(??.TPTP_Interpret.ind0, {(??.TPTP_Interpret.ind0, True)})}
% 12.21/11.72 bnd_ndr1_1: {(??.TPTP_Interpret.ind0, True)}
% 12.21/11.72 bnd_ndr1_0: True
% 12.21/11.72
% 12.21/11.72 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------