%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SEU911^5 : TPTP v6.4.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n048.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 03:59:02 EDT 2016
% Result : CounterSatisfiable 174.52s
% 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.02/0.03 % Problem : SEU911^5 : TPTP v6.4.0. Released v4.0.0.
% 0.02/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.24 % Computer : n048.star.cs.uiowa.edu
% 0.03/0.24 % Model : x86_64 x86_64
% 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.24 % Memory : 32218.75MB
% 0.03/0.24 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.03/0.24 % CPULimit : 300
% 0.03/0.25 % DateTime : Thu Apr 7 12:17:09 CDT 2016
% 0.03/0.25 % CPUTime :
% 6.28/5.87 > val it = (): unit
% 6.49/6.08 Trying to find a model that refutes: (((ALL Xx. bnd_cC Xx --> bnd_cA (bnd_f Xx)) &
% 6.49/6.08 (ALL Xe.
% 6.49/6.08 (ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx.
% 6.49/6.08 X Xx --> (ALL Xt. Xe Xt --> X (%Xz. Xx Xz | Xt = Xz))) -->
% 6.49/6.08 X Xe) &
% 6.49/6.08 (ALL Xx. Xe Xx --> (EX S. bnd_cA S & S Xx)) -->
% 6.49/6.08 (ALL Xx.
% 6.49/6.08 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_f Xx Xx0) --> bnd_cC Xx) &
% 6.49/6.08 (ALL Xx.
% 6.49/6.08 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_f Xx Xx0) -->
% 6.49/6.08 (EX Xe0.
% 6.49/6.08 ((ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx0.
% 6.49/6.08 X Xx0 -->
% 6.49/6.08 (ALL Xt. Xe0 Xt --> X (%Xz. Xx0 Xz | Xt = Xz))) -->
% 6.49/6.08 X Xe0) &
% 6.49/6.08 (ALL Xx0. Xe0 Xx0 --> Xx Xx0)) &
% 6.49/6.08 (ALL Xy.
% 6.49/6.08 bnd_cC Xy & (ALL Xx0. Xe0 Xx0 --> Xy Xx0) -->
% 6.49/6.08 bnd_cC Xy & (ALL Xx0. Xe Xx0 --> bnd_f Xy Xx0)))))) &
% 6.49/6.08 (ALL Xx. bnd_cC Xx --> bnd_cB (bnd_g Xx))) &
% 6.49/6.08 (ALL Xe.
% 6.49/6.08 (ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx. X Xx --> (ALL Xt. Xe Xt --> X (%Xz. Xx Xz | Xt = Xz))) -->
% 6.49/6.08 X Xe) &
% 6.49/6.08 (ALL Xx. Xe Xx --> (EX S. bnd_cB S & S Xx)) -->
% 6.49/6.08 (ALL Xx. bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_g Xx Xx0) --> bnd_cC Xx) &
% 6.49/6.08 (ALL Xx.
% 6.49/6.08 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_g Xx Xx0) -->
% 6.49/6.08 (EX Xe0.
% 6.49/6.08 ((ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx0.
% 6.49/6.08 X Xx0 -->
% 6.49/6.08 (ALL Xt. Xe0 Xt --> X (%Xz. Xx0 Xz | Xt = Xz))) -->
% 6.49/6.08 X Xe0) &
% 6.49/6.08 (ALL Xx0. Xe0 Xx0 --> Xx Xx0)) &
% 6.49/6.08 (ALL Xy.
% 6.49/6.08 bnd_cC Xy & (ALL Xx0. Xe0 Xx0 --> Xy Xx0) -->
% 6.49/6.08 bnd_cC Xy & (ALL Xx0. Xe Xx0 --> bnd_g Xy Xx0))))) -->
% 6.49/6.08 (ALL Xx.
% 6.49/6.08 bnd_cC Xx -->
% 6.49/6.08 (%Xx0. EX S. (EX Xr.
% 6.49/6.08 (EX Xd Xe.
% 6.49/6.08 (((ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx1.
% 6.49/6.08 X Xx1 -->
% 6.49/6.08 (ALL Xt.
% 6.49/6.08 Xd Xt --> X (%Xz. Xx1 Xz | Xt = Xz))) -->
% 6.49/6.08 X Xd) &
% 6.49/6.08 (ALL Xx1. Xd Xx1 --> bnd_f Xx Xx1)) &
% 6.49/6.08 (ALL X.
% 6.49/6.08 X (%Xy. False) &
% 6.49/6.08 (ALL Xx1.
% 6.49/6.08 X Xx1 -->
% 6.49/6.08 (ALL Xt.
% 6.49/6.08 Xe Xt --> X (%Xz. Xx1 Xz | Xt = Xz))) -->
% 6.49/6.08 X Xe)) &
% 6.49/6.08 (ALL Xx1. Xe Xx1 --> bnd_g Xx Xx1) -->
% 6.49/6.08 (ALL Xu Xv. Xr Xu Xv = (Xu = Xd & Xv = Xe))) &
% 6.49/6.08 Xr (%Xx1. False) S) &
% 6.49/6.08 S Xx0) =
% 6.49/6.08 bnd_g Xx)
% 6.68/6.26 Unfolded term: (((ALL Xx. bnd_cC Xx --> bnd_cA (bnd_f Xx)) &
% 6.68/6.26 (ALL Xe.
% 6.68/6.26 (ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx.
% 6.68/6.26 X Xx --> (ALL Xt. Xe Xt --> X (%Xz. Xx Xz | Xt = Xz))) -->
% 6.68/6.26 X Xe) &
% 6.68/6.26 (ALL Xx. Xe Xx --> (EX S. bnd_cA S & S Xx)) -->
% 6.68/6.26 (ALL Xx.
% 6.68/6.26 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_f Xx Xx0) --> bnd_cC Xx) &
% 6.68/6.26 (ALL Xx.
% 6.68/6.26 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_f Xx Xx0) -->
% 6.68/6.26 (EX Xe0.
% 6.68/6.26 ((ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx0.
% 6.68/6.26 X Xx0 -->
% 6.68/6.26 (ALL Xt. Xe0 Xt --> X (%Xz. Xx0 Xz | Xt = Xz))) -->
% 6.68/6.26 X Xe0) &
% 6.68/6.26 (ALL Xx0. Xe0 Xx0 --> Xx Xx0)) &
% 6.68/6.26 (ALL Xy.
% 6.68/6.26 bnd_cC Xy & (ALL Xx0. Xe0 Xx0 --> Xy Xx0) -->
% 6.68/6.26 bnd_cC Xy & (ALL Xx0. Xe Xx0 --> bnd_f Xy Xx0)))))) &
% 6.68/6.26 (ALL Xx. bnd_cC Xx --> bnd_cB (bnd_g Xx))) &
% 6.68/6.26 (ALL Xe.
% 6.68/6.26 (ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx. X Xx --> (ALL Xt. Xe Xt --> X (%Xz. Xx Xz | Xt = Xz))) -->
% 6.68/6.26 X Xe) &
% 6.68/6.26 (ALL Xx. Xe Xx --> (EX S. bnd_cB S & S Xx)) -->
% 6.68/6.26 (ALL Xx. bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_g Xx Xx0) --> bnd_cC Xx) &
% 6.68/6.26 (ALL Xx.
% 6.68/6.26 bnd_cC Xx & (ALL Xx0. Xe Xx0 --> bnd_g Xx Xx0) -->
% 6.68/6.26 (EX Xe0.
% 6.68/6.26 ((ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx0.
% 6.68/6.26 X Xx0 -->
% 6.68/6.26 (ALL Xt. Xe0 Xt --> X (%Xz. Xx0 Xz | Xt = Xz))) -->
% 6.68/6.26 X Xe0) &
% 6.68/6.26 (ALL Xx0. Xe0 Xx0 --> Xx Xx0)) &
% 6.68/6.26 (ALL Xy.
% 6.68/6.26 bnd_cC Xy & (ALL Xx0. Xe0 Xx0 --> Xy Xx0) -->
% 6.68/6.26 bnd_cC Xy & (ALL Xx0. Xe Xx0 --> bnd_g Xy Xx0))))) -->
% 6.68/6.26 (ALL Xx.
% 6.68/6.26 bnd_cC Xx -->
% 6.68/6.26 (%Xx0. EX S. (EX Xr.
% 6.68/6.26 (EX Xd Xe.
% 6.68/6.26 (((ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx1.
% 6.68/6.26 X Xx1 -->
% 6.68/6.26 (ALL Xt.
% 6.68/6.26 Xd Xt --> X (%Xz. Xx1 Xz | Xt = Xz))) -->
% 6.68/6.26 X Xd) &
% 6.68/6.26 (ALL Xx1. Xd Xx1 --> bnd_f Xx Xx1)) &
% 6.68/6.26 (ALL X.
% 6.68/6.26 X (%Xy. False) &
% 6.68/6.26 (ALL Xx1.
% 6.68/6.26 X Xx1 -->
% 6.68/6.26 (ALL Xt.
% 6.68/6.26 Xe Xt --> X (%Xz. Xx1 Xz | Xt = Xz))) -->
% 6.68/6.26 X Xe)) &
% 6.68/6.26 (ALL Xx1. Xe Xx1 --> bnd_g Xx Xx1) -->
% 6.68/6.26 (ALL Xu Xv. Xr Xu Xv = (Xu = Xd & Xv = Xe))) &
% 6.68/6.26 Xr (%Xx1. False) S) &
% 6.68/6.26 S Xx0) =
% 6.68/6.26 bnd_g Xx)
% 6.68/6.26 Adding axioms...
% 6.68/6.27 Typedef.type_definition_def
% 6.88/6.50 Typedef.type_definition_def
% 7.68/7.22 Typedef.type_definition_def
% 8.79/8.35 ...done.
% 8.79/8.35 Ground types: ?'b, bnd_c, bnd_a, bnd_b
% 8.79/8.35 Translating term (sizes: 1, 1, 1, 1) ...
% 174.32/173.39 Invoking SAT solver...
% 174.52/173.52 Model found:
% 174.52/173.52 Size of types: ?'b: 1, bnd_c: 1, bnd_a: 1, bnd_b: 1
% 174.52/173.52 bnd_g: {({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, True)},
% 174.52/173.52 {(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_b0, True)}),
% 174.52/173.52 ({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, False)},
% 174.52/173.52 {(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_b0, False)})}
% 174.52/173.52 bnd_cB: {({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_b0, True)},
% 174.52/173.52 False),
% 174.52/173.52 ({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_b0, False)},
% 174.52/173.52 True)}
% 174.52/173.52 bnd_f: {({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, True)},
% 174.52/173.52 {(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_a0, True)}),
% 174.52/173.52 ({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, False)},
% 174.52/173.52 {(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_a0, False)})}
% 174.52/173.52 bnd_cA: {({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_a0, True)},
% 174.52/173.52 False),
% 174.52/173.52 ({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_a0, False)},
% 174.52/173.52 True)}
% 174.52/173.52 bnd_cC: {({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, True)},
% 174.52/173.52 False),
% 174.52/173.52 ({(??.Scratch_tptp_refute_1552_24498.theBenchmark_46p.bnd_c0, False)},
% 174.52/173.52 True)}
% 174.52/173.52
% 174.52/173.52 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------