%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : SYN529+1 : TPTP v6.4.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n059.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:16 EDT 2016
% Result : CounterSatisfiable 33.50s
% 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 : SYN529+1 : TPTP v6.4.0. Released v2.1.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.03/0.23 % Computer : n059.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.75MB
% 0.03/0.23 % 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 00:13:54 CDT 2016
% 0.03/0.23 % CPUTime:
% 6.24/5.89 > val it = (): unit
% 6.64/6.22 Trying to find a model that refutes: ~ (((((((((((((((((((((((bnd_c2_0 | ~ bnd_c5_0) &
% 6.64/6.22 ((~ bnd_c4_0 | ~ bnd_c3_0) | ~ bnd_c2_0)) &
% 6.64/6.22 ((bnd_c4_0 |
% 6.64/6.22 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a314) &
% 6.64/6.22 ~ bnd_c3_2 bnd_a314 bnd_a315) &
% 6.64/6.22 ~ bnd_c2_2 bnd_a314 bnd_a315) &
% 6.64/6.22 ~ bnd_c1_2 bnd_a314 bnd_a315) &
% 6.64/6.22 bnd_c4_1 bnd_a314) &
% 6.64/6.22 (ALL U.
% 6.64/6.22 bnd_ndr1_1 bnd_a314 -->
% 6.64/6.22 (~ bnd_c1_2 bnd_a314 U | bnd_c4_2 bnd_a314 U) |
% 6.64/6.22 bnd_c3_2 bnd_a314 U)) |
% 6.64/6.22 (ALL V.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 ((ALL W.
% 6.64/6.22 bnd_ndr1_1 V -->
% 6.64/6.22 (bnd_c4_2 V W | bnd_c3_2 V W) |
% 6.64/6.22 bnd_c1_2 V W) |
% 6.64/6.22 ~ bnd_c4_1 V) |
% 6.64/6.22 bnd_c5_1 V))) &
% 6.64/6.22 (((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a316) &
% 6.64/6.22 bnd_ndr1_1 bnd_a316) &
% 6.64/6.22 bnd_c3_2 bnd_a316 bnd_a317) &
% 6.64/6.22 ~ bnd_c4_2 bnd_a316 bnd_a317) &
% 6.64/6.22 bnd_c2_2 bnd_a316 bnd_a317) &
% 6.64/6.22 bnd_c1_1 bnd_a316 |
% 6.64/6.22 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a318) &
% 6.64/6.22 bnd_c4_2 bnd_a318 bnd_a319) &
% 6.64/6.22 bnd_c2_2 bnd_a318 bnd_a319) &
% 6.64/6.22 bnd_ndr1_1 bnd_a318) &
% 6.64/6.22 bnd_c2_2 bnd_a318 bnd_a320) &
% 6.64/6.22 ~ bnd_c4_2 bnd_a318 bnd_a320) |
% 6.64/6.22 ~ bnd_c4_0)) &
% 6.64/6.22 (((ALL X.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 ((ALL Y.
% 6.64/6.22 bnd_ndr1_1 X -->
% 6.64/6.22 (~ bnd_c4_2 X Y | bnd_c2_2 X Y) |
% 6.64/6.22 ~ bnd_c3_2 X Y) |
% 6.64/6.22 ((bnd_ndr1_1 X & ~ bnd_c1_2 X bnd_a321) &
% 6.64/6.22 bnd_c5_2 X bnd_a321) &
% 6.64/6.22 ~ bnd_c2_2 X bnd_a321) |
% 6.64/6.22 ~ bnd_c2_1 X) |
% 6.64/6.22 bnd_c4_0) |
% 6.64/6.22 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a322) &
% 6.64/6.22 bnd_ndr1_1 bnd_a322) &
% 6.64/6.22 ~ bnd_c4_2 bnd_a322 bnd_a323) &
% 6.64/6.22 bnd_c5_2 bnd_a322 bnd_a323) &
% 6.64/6.22 ~ bnd_c1_2 bnd_a322 bnd_a323)) &
% 6.64/6.22 (((ALL Z. bnd_ndr1_0 --> bnd_c1_1 Z | bnd_c5_1 Z) |
% 6.64/6.22 (ALL X1.
% 6.64/6.22 bnd_ndr1_0 --> ~ bnd_c2_1 X1 | bnd_c4_1 X1)) |
% 6.64/6.22 (ALL X2.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 (bnd_c4_1 X2 |
% 6.64/6.22 (ALL X3.
% 6.64/6.22 bnd_ndr1_1 X2 -->
% 6.64/6.22 bnd_c5_2 X2 X3 | bnd_c4_2 X2 X3)) |
% 6.64/6.22 bnd_c2_1 X2))) &
% 6.64/6.22 (bnd_c2_0 | ~ bnd_c3_0)) &
% 6.64/6.22 ((bnd_c5_0 |
% 6.64/6.22 ((((bnd_ndr1_0 &
% 6.64/6.22 (ALL X4.
% 6.64/6.22 bnd_ndr1_1 bnd_a324 -->
% 6.64/6.22 (bnd_c3_2 bnd_a324 X4 | bnd_c2_2 bnd_a324 X4) |
% 6.64/6.22 ~ bnd_c4_2 bnd_a324 X4)) &
% 6.64/6.22 bnd_ndr1_1 bnd_a324) &
% 6.64/6.22 bnd_c1_2 bnd_a324 bnd_a325) &
% 6.64/6.22 bnd_c5_2 bnd_a324 bnd_a325) &
% 6.64/6.22 (ALL X5.
% 6.64/6.22 bnd_ndr1_1 bnd_a324 -->
% 6.64/6.22 bnd_c3_2 bnd_a324 X5 | bnd_c1_2 bnd_a324 X5)) |
% 6.64/6.22 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a326) &
% 6.64/6.22 bnd_c4_1 bnd_a326) &
% 6.64/6.22 bnd_ndr1_1 bnd_a326) &
% 6.64/6.22 ~ bnd_c2_2 bnd_a326 bnd_a327) &
% 6.64/6.22 ~ bnd_c5_2 bnd_a326 bnd_a327) &
% 6.64/6.22 bnd_c3_2 bnd_a326 bnd_a327)) &
% 6.64/6.22 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a328) & bnd_c5_1 bnd_a328 |
% 6.64/6.22 bnd_c4_0) |
% 6.64/6.22 (((bnd_ndr1_0 & bnd_ndr1_1 bnd_a329) &
% 6.64/6.22 ~ bnd_c2_2 bnd_a329 bnd_a330) &
% 6.64/6.22 (ALL X6.
% 6.64/6.22 bnd_ndr1_1 bnd_a329 -->
% 6.64/6.22 (~ bnd_c4_2 bnd_a329 X6 | ~ bnd_c5_2 bnd_a329 X6) |
% 6.64/6.22 bnd_c1_2 bnd_a329 X6)) &
% 6.64/6.22 bnd_c1_1 bnd_a329)) &
% 6.64/6.22 ((~ bnd_c4_0 |
% 6.64/6.22 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a331) &
% 6.64/6.22 bnd_c1_2 bnd_a331 bnd_a332) &
% 6.64/6.22 bnd_c2_2 bnd_a331 bnd_a332) &
% 6.64/6.22 ~ bnd_c5_2 bnd_a331 bnd_a332) &
% 6.64/6.22 bnd_c5_1 bnd_a331) &
% 6.64/6.22 bnd_c3_1 bnd_a331) |
% 6.64/6.22 bnd_ndr1_0 & ~ bnd_c3_1 bnd_a333)) &
% 6.64/6.22 ((ALL X7.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 (bnd_c3_1 X7 |
% 6.64/6.22 (bnd_ndr1_1 X7 & bnd_c4_2 X7 bnd_a334) &
% 6.64/6.22 bnd_c2_2 X7 bnd_a334) |
% 6.64/6.22 bnd_c5_1 X7) |
% 6.64/6.22 bnd_c1_0)) &
% 6.64/6.22 (((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a335) &
% 6.64/6.22 bnd_c4_2 bnd_a335 bnd_a336) &
% 6.64/6.22 bnd_c5_2 bnd_a335 bnd_a336) &
% 6.64/6.22 bnd_c2_2 bnd_a335 bnd_a336) &
% 6.64/6.22 bnd_ndr1_1 bnd_a335) &
% 6.64/6.22 bnd_c1_2 bnd_a335 bnd_a337) &
% 6.64/6.22 bnd_c5_2 bnd_a335 bnd_a337) &
% 6.64/6.22 ~ bnd_c3_2 bnd_a335 bnd_a337 |
% 6.64/6.22 bnd_c4_0) |
% 6.64/6.22 bnd_c5_0)) &
% 6.64/6.22 ((~ bnd_c5_0 |
% 6.64/6.22 (((((bnd_ndr1_0 & bnd_c1_1 bnd_a338) & bnd_c4_1 bnd_a338) &
% 6.64/6.22 bnd_ndr1_1 bnd_a338) &
% 6.64/6.22 bnd_c1_2 bnd_a338 bnd_a339) &
% 6.64/6.22 ~ bnd_c3_2 bnd_a338 bnd_a339) &
% 6.64/6.22 ~ bnd_c4_2 bnd_a338 bnd_a339) |
% 6.64/6.22 (ALL X8.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 ((ALL X9.
% 6.64/6.22 bnd_ndr1_1 X8 -->
% 6.64/6.22 (~ bnd_c3_2 X8 X9 | bnd_c2_2 X8 X9) |
% 6.64/6.22 bnd_c1_2 X8 X9) |
% 6.64/6.22 ((bnd_ndr1_1 X8 & ~ bnd_c4_2 X8 bnd_a340) &
% 6.64/6.22 ~ bnd_c1_2 X8 bnd_a340) &
% 6.64/6.22 bnd_c2_2 X8 bnd_a340) |
% 6.64/6.22 ((bnd_ndr1_1 X8 & bnd_c2_2 X8 bnd_a341) &
% 6.64/6.22 bnd_c4_2 X8 bnd_a341) &
% 6.64/6.22 bnd_c3_2 X8 bnd_a341))) &
% 6.64/6.22 ((bnd_c3_0 | bnd_c5_0) | ~ bnd_c1_0)) &
% 6.64/6.22 (bnd_c4_0 |
% 6.64/6.22 (ALL X10.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 ((bnd_ndr1_1 X10 & bnd_c5_2 X10 bnd_a342) &
% 6.64/6.22 bnd_c2_2 X10 bnd_a342 |
% 6.64/6.22 ~ bnd_c4_1 X10) |
% 6.64/6.22 bnd_c5_1 X10))) &
% 6.64/6.22 ((~ bnd_c3_0 | ~ bnd_c5_0) | bnd_c4_0)) &
% 6.64/6.22 ((ALL X11.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 ((ALL X12.
% 6.64/6.22 bnd_ndr1_1 X11 -->
% 6.64/6.22 (bnd_c4_2 X11 X12 | bnd_c3_2 X11 X12) |
% 6.64/6.22 bnd_c2_2 X11 X12) |
% 6.64/6.22 bnd_c3_1 X11) |
% 6.64/6.22 ~ bnd_c2_1 X11) |
% 6.64/6.22 bnd_c5_0)) &
% 6.64/6.22 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a343) & bnd_c2_1 bnd_a343 |
% 6.64/6.22 bnd_c3_0)) &
% 6.64/6.22 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a344) &
% 6.64/6.22 bnd_c3_2 bnd_a344 bnd_a345) &
% 6.64/6.22 ~ bnd_c1_2 bnd_a344 bnd_a345) &
% 6.64/6.22 ~ bnd_c2_1 bnd_a344) &
% 6.64/6.22 (ALL X13.
% 6.64/6.22 bnd_ndr1_1 bnd_a344 -->
% 6.64/6.22 (~ bnd_c2_2 bnd_a344 X13 | ~ bnd_c1_2 bnd_a344 X13) |
% 6.64/6.22 ~ bnd_c5_2 bnd_a344 X13) |
% 6.64/6.22 bnd_c5_0) |
% 6.64/6.22 ((((bnd_ndr1_0 & bnd_c4_1 bnd_a346) & bnd_ndr1_1 bnd_a346) &
% 6.64/6.22 ~ bnd_c5_2 bnd_a346 bnd_a347) &
% 6.64/6.22 bnd_c1_2 bnd_a346 bnd_a347) &
% 6.64/6.22 bnd_c3_1 bnd_a346)) &
% 6.64/6.22 (((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a348) &
% 6.64/6.22 (ALL X14.
% 6.64/6.22 bnd_ndr1_1 bnd_a348 -->
% 6.64/6.22 (bnd_c5_2 bnd_a348 X14 | ~ bnd_c4_2 bnd_a348 X14) |
% 6.64/6.22 ~ bnd_c2_2 bnd_a348 X14)) &
% 6.64/6.22 bnd_ndr1_1 bnd_a348) &
% 6.64/6.22 ~ bnd_c5_2 bnd_a348 bnd_a349) &
% 6.64/6.22 bnd_c2_2 bnd_a348 bnd_a349 |
% 6.64/6.22 (ALL X15.
% 6.64/6.22 bnd_ndr1_0 -->
% 6.64/6.22 (((bnd_ndr1_1 X15 & bnd_c2_2 X15 bnd_a350) &
% 6.64/6.22 ~ bnd_c3_2 X15 bnd_a350) &
% 6.64/6.22 ~ bnd_c1_2 X15 bnd_a350 |
% 6.64/6.22 ~ bnd_c3_1 X15) |
% 6.64/6.22 (ALL X16.
% 6.64/6.22 bnd_ndr1_1 X15 -->
% 6.64/6.22 (bnd_c1_2 X15 X16 | ~ bnd_c4_2 X15 X16) |
% 6.64/6.22 bnd_c5_2 X15 X16)))) &
% 6.64/6.22 ((bnd_c4_0 | ~ bnd_c1_0) | ~ bnd_c5_0)) &
% 6.64/6.22 (((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a351) & bnd_ndr1_1 bnd_a351) &
% 6.64/6.22 bnd_c2_2 bnd_a351 bnd_a352) &
% 6.64/6.22 ~ bnd_c1_2 bnd_a351 bnd_a352) &
% 6.64/6.22 ~ bnd_c4_2 bnd_a351 bnd_a352) &
% 6.64/6.22 bnd_c4_1 bnd_a351 |
% 6.64/6.22 bnd_c3_0) |
% 6.64/6.22 ((((bnd_ndr1_0 &
% 6.64/6.22 (ALL X17.
% 6.64/6.22 bnd_ndr1_1 bnd_a353 -->
% 6.64/6.22 (~ bnd_c2_2 bnd_a353 X17 | bnd_c3_2 bnd_a353 X17) |
% 6.64/6.22 ~ bnd_c5_2 bnd_a353 X17)) &
% 6.64/6.22 bnd_ndr1_1 bnd_a353) &
% 6.64/6.22 bnd_c2_2 bnd_a353 bnd_a354) &
% 6.64/6.22 bnd_c3_2 bnd_a353 bnd_a354) &
% 6.64/6.22 (ALL X18.
% 6.64/6.22 bnd_ndr1_1 bnd_a353 -->
% 6.64/6.22 (~ bnd_c1_2 bnd_a353 X18 | ~ bnd_c4_2 bnd_a353 X18) |
% 6.64/6.22 bnd_c3_2 bnd_a353 X18))) &
% 6.64/6.22 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a355) & ~ bnd_c4_2 bnd_a355 bnd_a356) &
% 6.64/6.22 ~ bnd_c5_2 bnd_a355 bnd_a356) &
% 6.64/6.22 (ALL X19.
% 6.64/6.22 bnd_ndr1_1 bnd_a355 -->
% 6.64/6.22 bnd_c3_2 bnd_a355 X19 | ~ bnd_c1_2 bnd_a355 X19)) &
% 6.64/6.22 ~ bnd_c3_1 bnd_a355 |
% 6.64/6.22 bnd_c2_0) |
% 6.64/6.22 bnd_c5_0))
% 8.75/8.32 Unfolded term: ~ (((((((((((((((((((((((bnd_c2_0 | ~ bnd_c5_0) &
% 8.75/8.32 ((~ bnd_c4_0 | ~ bnd_c3_0) | ~ bnd_c2_0)) &
% 8.75/8.32 ((bnd_c4_0 |
% 8.75/8.32 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a314) &
% 8.75/8.32 ~ bnd_c3_2 bnd_a314 bnd_a315) &
% 8.75/8.32 ~ bnd_c2_2 bnd_a314 bnd_a315) &
% 8.75/8.32 ~ bnd_c1_2 bnd_a314 bnd_a315) &
% 8.75/8.32 bnd_c4_1 bnd_a314) &
% 8.75/8.32 (ALL U.
% 8.75/8.32 bnd_ndr1_1 bnd_a314 -->
% 8.75/8.32 (~ bnd_c1_2 bnd_a314 U | bnd_c4_2 bnd_a314 U) |
% 8.75/8.32 bnd_c3_2 bnd_a314 U)) |
% 8.75/8.32 (ALL V.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 ((ALL W.
% 8.75/8.32 bnd_ndr1_1 V -->
% 8.75/8.32 (bnd_c4_2 V W | bnd_c3_2 V W) |
% 8.75/8.32 bnd_c1_2 V W) |
% 8.75/8.32 ~ bnd_c4_1 V) |
% 8.75/8.32 bnd_c5_1 V))) &
% 8.75/8.32 (((((((bnd_ndr1_0 & ~ bnd_c4_1 bnd_a316) &
% 8.75/8.32 bnd_ndr1_1 bnd_a316) &
% 8.75/8.32 bnd_c3_2 bnd_a316 bnd_a317) &
% 8.75/8.32 ~ bnd_c4_2 bnd_a316 bnd_a317) &
% 8.75/8.32 bnd_c2_2 bnd_a316 bnd_a317) &
% 8.75/8.32 bnd_c1_1 bnd_a316 |
% 8.75/8.32 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a318) &
% 8.75/8.32 bnd_c4_2 bnd_a318 bnd_a319) &
% 8.75/8.32 bnd_c2_2 bnd_a318 bnd_a319) &
% 8.75/8.32 bnd_ndr1_1 bnd_a318) &
% 8.75/8.32 bnd_c2_2 bnd_a318 bnd_a320) &
% 8.75/8.32 ~ bnd_c4_2 bnd_a318 bnd_a320) |
% 8.75/8.32 ~ bnd_c4_0)) &
% 8.75/8.32 (((ALL X.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 ((ALL Y.
% 8.75/8.32 bnd_ndr1_1 X -->
% 8.75/8.32 (~ bnd_c4_2 X Y | bnd_c2_2 X Y) |
% 8.75/8.32 ~ bnd_c3_2 X Y) |
% 8.75/8.32 ((bnd_ndr1_1 X & ~ bnd_c1_2 X bnd_a321) &
% 8.75/8.32 bnd_c5_2 X bnd_a321) &
% 8.75/8.32 ~ bnd_c2_2 X bnd_a321) |
% 8.75/8.32 ~ bnd_c2_1 X) |
% 8.75/8.32 bnd_c4_0) |
% 8.75/8.32 ((((bnd_ndr1_0 & bnd_c3_1 bnd_a322) &
% 8.75/8.32 bnd_ndr1_1 bnd_a322) &
% 8.75/8.32 ~ bnd_c4_2 bnd_a322 bnd_a323) &
% 8.75/8.32 bnd_c5_2 bnd_a322 bnd_a323) &
% 8.75/8.32 ~ bnd_c1_2 bnd_a322 bnd_a323)) &
% 8.75/8.32 (((ALL Z. bnd_ndr1_0 --> bnd_c1_1 Z | bnd_c5_1 Z) |
% 8.75/8.32 (ALL X1.
% 8.75/8.32 bnd_ndr1_0 --> ~ bnd_c2_1 X1 | bnd_c4_1 X1)) |
% 8.75/8.32 (ALL X2.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 (bnd_c4_1 X2 |
% 8.75/8.32 (ALL X3.
% 8.75/8.32 bnd_ndr1_1 X2 -->
% 8.75/8.32 bnd_c5_2 X2 X3 | bnd_c4_2 X2 X3)) |
% 8.75/8.32 bnd_c2_1 X2))) &
% 8.75/8.32 (bnd_c2_0 | ~ bnd_c3_0)) &
% 8.75/8.32 ((bnd_c5_0 |
% 8.75/8.32 ((((bnd_ndr1_0 &
% 8.75/8.32 (ALL X4.
% 8.75/8.32 bnd_ndr1_1 bnd_a324 -->
% 8.75/8.32 (bnd_c3_2 bnd_a324 X4 | bnd_c2_2 bnd_a324 X4) |
% 8.75/8.32 ~ bnd_c4_2 bnd_a324 X4)) &
% 8.75/8.32 bnd_ndr1_1 bnd_a324) &
% 8.75/8.32 bnd_c1_2 bnd_a324 bnd_a325) &
% 8.75/8.32 bnd_c5_2 bnd_a324 bnd_a325) &
% 8.75/8.32 (ALL X5.
% 8.75/8.32 bnd_ndr1_1 bnd_a324 -->
% 8.75/8.32 bnd_c3_2 bnd_a324 X5 | bnd_c1_2 bnd_a324 X5)) |
% 8.75/8.32 (((((bnd_ndr1_0 & bnd_c2_1 bnd_a326) &
% 8.75/8.32 bnd_c4_1 bnd_a326) &
% 8.75/8.32 bnd_ndr1_1 bnd_a326) &
% 8.75/8.32 ~ bnd_c2_2 bnd_a326 bnd_a327) &
% 8.75/8.32 ~ bnd_c5_2 bnd_a326 bnd_a327) &
% 8.75/8.32 bnd_c3_2 bnd_a326 bnd_a327)) &
% 8.75/8.32 (((bnd_ndr1_0 & ~ bnd_c2_1 bnd_a328) & bnd_c5_1 bnd_a328 |
% 8.75/8.32 bnd_c4_0) |
% 8.75/8.32 (((bnd_ndr1_0 & bnd_ndr1_1 bnd_a329) &
% 8.75/8.32 ~ bnd_c2_2 bnd_a329 bnd_a330) &
% 8.75/8.32 (ALL X6.
% 8.75/8.32 bnd_ndr1_1 bnd_a329 -->
% 8.75/8.32 (~ bnd_c4_2 bnd_a329 X6 | ~ bnd_c5_2 bnd_a329 X6) |
% 8.75/8.32 bnd_c1_2 bnd_a329 X6)) &
% 8.75/8.32 bnd_c1_1 bnd_a329)) &
% 8.75/8.32 ((~ bnd_c4_0 |
% 8.75/8.32 (((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a331) &
% 8.75/8.32 bnd_c1_2 bnd_a331 bnd_a332) &
% 8.75/8.32 bnd_c2_2 bnd_a331 bnd_a332) &
% 8.75/8.32 ~ bnd_c5_2 bnd_a331 bnd_a332) &
% 8.75/8.32 bnd_c5_1 bnd_a331) &
% 8.75/8.32 bnd_c3_1 bnd_a331) |
% 8.75/8.32 bnd_ndr1_0 & ~ bnd_c3_1 bnd_a333)) &
% 8.75/8.32 ((ALL X7.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 (bnd_c3_1 X7 |
% 8.75/8.32 (bnd_ndr1_1 X7 & bnd_c4_2 X7 bnd_a334) &
% 8.75/8.32 bnd_c2_2 X7 bnd_a334) |
% 8.75/8.32 bnd_c5_1 X7) |
% 8.75/8.32 bnd_c1_0)) &
% 8.75/8.32 (((((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a335) &
% 8.75/8.32 bnd_c4_2 bnd_a335 bnd_a336) &
% 8.75/8.32 bnd_c5_2 bnd_a335 bnd_a336) &
% 8.75/8.32 bnd_c2_2 bnd_a335 bnd_a336) &
% 8.75/8.32 bnd_ndr1_1 bnd_a335) &
% 8.75/8.32 bnd_c1_2 bnd_a335 bnd_a337) &
% 8.75/8.32 bnd_c5_2 bnd_a335 bnd_a337) &
% 8.75/8.32 ~ bnd_c3_2 bnd_a335 bnd_a337 |
% 8.75/8.32 bnd_c4_0) |
% 8.75/8.32 bnd_c5_0)) &
% 8.75/8.32 ((~ bnd_c5_0 |
% 8.75/8.32 (((((bnd_ndr1_0 & bnd_c1_1 bnd_a338) & bnd_c4_1 bnd_a338) &
% 8.75/8.32 bnd_ndr1_1 bnd_a338) &
% 8.75/8.32 bnd_c1_2 bnd_a338 bnd_a339) &
% 8.75/8.32 ~ bnd_c3_2 bnd_a338 bnd_a339) &
% 8.75/8.32 ~ bnd_c4_2 bnd_a338 bnd_a339) |
% 8.75/8.32 (ALL X8.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 ((ALL X9.
% 8.75/8.32 bnd_ndr1_1 X8 -->
% 8.75/8.32 (~ bnd_c3_2 X8 X9 | bnd_c2_2 X8 X9) |
% 8.75/8.32 bnd_c1_2 X8 X9) |
% 8.75/8.32 ((bnd_ndr1_1 X8 & ~ bnd_c4_2 X8 bnd_a340) &
% 8.75/8.32 ~ bnd_c1_2 X8 bnd_a340) &
% 8.75/8.32 bnd_c2_2 X8 bnd_a340) |
% 8.75/8.32 ((bnd_ndr1_1 X8 & bnd_c2_2 X8 bnd_a341) &
% 8.75/8.32 bnd_c4_2 X8 bnd_a341) &
% 8.75/8.32 bnd_c3_2 X8 bnd_a341))) &
% 8.75/8.32 ((bnd_c3_0 | bnd_c5_0) | ~ bnd_c1_0)) &
% 8.75/8.32 (bnd_c4_0 |
% 8.75/8.32 (ALL X10.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 ((bnd_ndr1_1 X10 & bnd_c5_2 X10 bnd_a342) &
% 8.75/8.32 bnd_c2_2 X10 bnd_a342 |
% 8.75/8.32 ~ bnd_c4_1 X10) |
% 8.75/8.32 bnd_c5_1 X10))) &
% 8.75/8.32 ((~ bnd_c3_0 | ~ bnd_c5_0) | bnd_c4_0)) &
% 8.75/8.32 ((ALL X11.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 ((ALL X12.
% 8.75/8.32 bnd_ndr1_1 X11 -->
% 8.75/8.32 (bnd_c4_2 X11 X12 | bnd_c3_2 X11 X12) |
% 8.75/8.32 bnd_c2_2 X11 X12) |
% 8.75/8.32 bnd_c3_1 X11) |
% 8.75/8.32 ~ bnd_c2_1 X11) |
% 8.75/8.32 bnd_c5_0)) &
% 8.75/8.32 ((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a343) & bnd_c2_1 bnd_a343 |
% 8.75/8.32 bnd_c3_0)) &
% 8.75/8.32 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a344) &
% 8.75/8.32 bnd_c3_2 bnd_a344 bnd_a345) &
% 8.75/8.32 ~ bnd_c1_2 bnd_a344 bnd_a345) &
% 8.75/8.32 ~ bnd_c2_1 bnd_a344) &
% 8.75/8.32 (ALL X13.
% 8.75/8.32 bnd_ndr1_1 bnd_a344 -->
% 8.75/8.32 (~ bnd_c2_2 bnd_a344 X13 | ~ bnd_c1_2 bnd_a344 X13) |
% 8.75/8.32 ~ bnd_c5_2 bnd_a344 X13) |
% 8.75/8.32 bnd_c5_0) |
% 8.75/8.32 ((((bnd_ndr1_0 & bnd_c4_1 bnd_a346) & bnd_ndr1_1 bnd_a346) &
% 8.75/8.32 ~ bnd_c5_2 bnd_a346 bnd_a347) &
% 8.75/8.32 bnd_c1_2 bnd_a346 bnd_a347) &
% 8.75/8.32 bnd_c3_1 bnd_a346)) &
% 8.75/8.32 (((((bnd_ndr1_0 & ~ bnd_c3_1 bnd_a348) &
% 8.75/8.32 (ALL X14.
% 8.75/8.32 bnd_ndr1_1 bnd_a348 -->
% 8.75/8.32 (bnd_c5_2 bnd_a348 X14 | ~ bnd_c4_2 bnd_a348 X14) |
% 8.75/8.32 ~ bnd_c2_2 bnd_a348 X14)) &
% 8.75/8.32 bnd_ndr1_1 bnd_a348) &
% 8.75/8.32 ~ bnd_c5_2 bnd_a348 bnd_a349) &
% 8.75/8.32 bnd_c2_2 bnd_a348 bnd_a349 |
% 8.75/8.32 (ALL X15.
% 8.75/8.32 bnd_ndr1_0 -->
% 8.75/8.32 (((bnd_ndr1_1 X15 & bnd_c2_2 X15 bnd_a350) &
% 8.75/8.32 ~ bnd_c3_2 X15 bnd_a350) &
% 8.75/8.32 ~ bnd_c1_2 X15 bnd_a350 |
% 8.75/8.32 ~ bnd_c3_1 X15) |
% 8.75/8.32 (ALL X16.
% 8.75/8.32 bnd_ndr1_1 X15 -->
% 8.75/8.32 (bnd_c1_2 X15 X16 | ~ bnd_c4_2 X15 X16) |
% 8.75/8.32 bnd_c5_2 X15 X16)))) &
% 8.75/8.32 ((bnd_c4_0 | ~ bnd_c1_0) | ~ bnd_c5_0)) &
% 8.75/8.32 (((((((bnd_ndr1_0 & ~ bnd_c1_1 bnd_a351) & bnd_ndr1_1 bnd_a351) &
% 8.75/8.32 bnd_c2_2 bnd_a351 bnd_a352) &
% 8.75/8.32 ~ bnd_c1_2 bnd_a351 bnd_a352) &
% 8.75/8.32 ~ bnd_c4_2 bnd_a351 bnd_a352) &
% 8.75/8.32 bnd_c4_1 bnd_a351 |
% 8.75/8.32 bnd_c3_0) |
% 8.75/8.32 ((((bnd_ndr1_0 &
% 8.75/8.32 (ALL X17.
% 8.75/8.32 bnd_ndr1_1 bnd_a353 -->
% 8.75/8.32 (~ bnd_c2_2 bnd_a353 X17 | bnd_c3_2 bnd_a353 X17) |
% 8.75/8.32 ~ bnd_c5_2 bnd_a353 X17)) &
% 8.75/8.32 bnd_ndr1_1 bnd_a353) &
% 8.75/8.32 bnd_c2_2 bnd_a353 bnd_a354) &
% 8.75/8.32 bnd_c3_2 bnd_a353 bnd_a354) &
% 8.75/8.32 (ALL X18.
% 8.75/8.32 bnd_ndr1_1 bnd_a353 -->
% 8.75/8.32 (~ bnd_c1_2 bnd_a353 X18 | ~ bnd_c4_2 bnd_a353 X18) |
% 8.75/8.32 bnd_c3_2 bnd_a353 X18))) &
% 8.75/8.32 ((((((bnd_ndr1_0 & bnd_ndr1_1 bnd_a355) & ~ bnd_c4_2 bnd_a355 bnd_a356) &
% 8.75/8.32 ~ bnd_c5_2 bnd_a355 bnd_a356) &
% 8.75/8.32 (ALL X19.
% 8.75/8.32 bnd_ndr1_1 bnd_a355 -->
% 8.75/8.32 bnd_c3_2 bnd_a355 X19 | ~ bnd_c1_2 bnd_a355 X19)) &
% 8.75/8.32 ~ bnd_c3_1 bnd_a355 |
% 8.75/8.32 bnd_c2_0) |
% 8.75/8.32 bnd_c5_0))
% 8.75/8.32 Adding axioms...
% 8.75/8.37 Typedef.type_definition_def
% 14.95/14.54 ...done.
% 14.95/14.54 Ground types: ?'b, TPTP_Interpret.ind
% 14.95/14.54 Translating term (sizes: 1, 1) ...
% 19.96/19.51 Invoking SAT solver...
% 19.96/19.51 No model exists.
% 19.96/19.51 Translating term (sizes: 2, 1) ...
% 25.58/25.12 Invoking SAT solver...
% 25.58/25.13 No model exists.
% 25.58/25.13 Translating term (sizes: 1, 2) ...
% 33.29/32.87 Invoking SAT solver...
% 33.50/33.09 Model found:
% 33.50/33.09 Size of types: ?'b: 1, TPTP_Interpret.ind: 2
% 33.50/33.09 bnd_a356: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a355: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a354: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a353: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a352: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a351: ??.TPTP_Interpret.ind1
% 33.50/33.09 bnd_a350: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a349: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a348: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a347: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a346: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a345: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a344: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a343: ??.TPTP_Interpret.ind1
% 33.50/33.09 bnd_a342: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a341: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a340: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a339: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a338: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a337: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a336: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a335: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_c1_0: False
% 33.50/33.09 bnd_a334: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a333: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a332: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a331: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a330: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a329: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a328: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a327: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a326: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a325: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a324: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a323: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a322: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_c3_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 33.50/33.09 bnd_c2_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 33.50/33.09 bnd_c5_2: {(??.TPTP_Interpret.ind0,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 33.50/33.09 (??.TPTP_Interpret.ind1,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 33.50/33.09 bnd_a321: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a320: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a319: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a318: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_c1_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, False)}
% 33.50/33.09 bnd_a317: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_a316: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_c5_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 33.50/33.09 bnd_c4_2: {(??.TPTP_Interpret.ind0,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 33.50/33.09 (??.TPTP_Interpret.ind1,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 33.50/33.09 bnd_c4_1: {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}
% 33.50/33.09 bnd_c1_2: {(??.TPTP_Interpret.ind0,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)}),
% 33.50/33.09 (??.TPTP_Interpret.ind1,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, False)})}
% 33.50/33.09 bnd_c2_2: {(??.TPTP_Interpret.ind0,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 33.50/33.09 (??.TPTP_Interpret.ind1,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 33.50/33.09 bnd_a315: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_c3_2: {(??.TPTP_Interpret.ind0,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)}),
% 33.50/33.09 (??.TPTP_Interpret.ind1,
% 33.50/33.09 {(??.TPTP_Interpret.ind0, True), (??.TPTP_Interpret.ind1, True)})}
% 33.50/33.09 bnd_a314: ??.TPTP_Interpret.ind0
% 33.50/33.09 bnd_ndr1_1: {(??.TPTP_Interpret.ind0, False), (??.TPTP_Interpret.ind1, True)}
% 33.50/33.09 bnd_ndr1_0: True
% 33.50/33.09 bnd_c3_0: False
% 33.50/33.09 bnd_c4_0: False
% 33.50/33.09 bnd_c5_0: True
% 33.50/33.09 bnd_c2_0: True
% 33.50/33.09
% 33.50/33.09 % SZS status CounterSatisfiable
%------------------------------------------------------------------------------