%------------------------------------------------------------------------------
% File : Refute---2015
% Problem : PRO007+4 : TPTP v6.4.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : isabelle tptp_refute %d %s
% Computer : n032.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 16091.75MB
% OS : Linux 3.10.0-327.10.1.el7.x86_64
% CPULimit : 300s
% DateTime : Thu Apr 14 02:25:46 EDT 2016
% Result : Timeout 300.08s
% Output : None
% 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 : PRO007+4 : TPTP v6.4.0. Released v4.0.0.
% 0.00/0.04 % Command : isabelle tptp_refute %d %s
% 0.02/0.23 % Computer : n032.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 16091.75MB
% 0.02/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Wed Apr 6 08:40:54 CDT 2016
% 0.02/0.23 % CPUTime :
% 6.30/5.87 > val it = (): unit
% 6.59/6.10 Trying to find a model that refutes: bnd_occurrence_of X105 bnd_tptp0 -->
% 6.59/6.10 (EX X106 X107.
% 6.59/6.10 (((((bnd_occurrence_of X106 bnd_tptp3 & bnd_root_occ X106 X105) &
% 6.59/6.10 (bnd_occurrence_of X107 bnd_tptp1 |
% 6.59/6.10 bnd_occurrence_of X107 bnd_tptp2)) &
% 6.59/6.10 bnd_min_precedes X106 X107 bnd_tptp0) &
% 6.59/6.10 bnd_leaf_occ X107 X105) &
% 6.59/6.10 (bnd_occurrence_of X107 bnd_tptp1 -->
% 6.59/6.10 ~ (EX X108.
% 6.59/6.10 bnd_occurrence_of X108 bnd_tptp2 &
% 6.59/6.10 bnd_min_precedes X106 X108 bnd_tptp0))) &
% 6.59/6.10 (bnd_occurrence_of X107 bnd_tptp2 -->
% 6.59/6.10 ~ (EX X109.
% 6.59/6.10 bnd_occurrence_of X109 bnd_tptp1 &
% 6.59/6.10 bnd_min_precedes X106 X109 bnd_tptp0)))
% 7.48/7.05 Unfolded term: [| ~ bnd_tptp1 = bnd_tptp2; ~ bnd_tptp3 = bnd_tptp2;
% 7.48/7.05 ~ bnd_tptp3 = bnd_tptp1; ~ bnd_tptp4 = bnd_tptp2;
% 7.48/7.05 ~ bnd_tptp4 = bnd_tptp1; ~ bnd_tptp4 = bnd_tptp3; bnd_atomic bnd_tptp3;
% 7.48/7.05 bnd_atomic bnd_tptp2; bnd_atomic bnd_tptp1; bnd_atomic bnd_tptp4;
% 7.48/7.05 ~ bnd_atomic bnd_tptp0; bnd_activity bnd_tptp0;
% 7.48/7.05 ALL X101.
% 7.48/7.05 bnd_occurrence_of X101 bnd_tptp0 -->
% 7.48/7.05 (EX X102 X103 X104.
% 7.48/7.05 (((((bnd_occurrence_of X102 bnd_tptp3 & bnd_root_occ X102 X101) &
% 7.48/7.05 bnd_occurrence_of X103 bnd_tptp4) &
% 7.48/7.05 bnd_next_subocc X102 X103 bnd_tptp0) &
% 7.48/7.05 (bnd_occurrence_of X104 bnd_tptp1 |
% 7.48/7.05 bnd_occurrence_of X104 bnd_tptp2)) &
% 7.48/7.05 bnd_next_subocc X103 X104 bnd_tptp0) &
% 7.48/7.05 bnd_leaf_occ X104 X101);
% 7.48/7.05 ALL X97 X98 X99 X100.
% 7.48/7.05 (bnd_min_precedes X97 X98 X100 & bnd_min_precedes X97 X99 X100) &
% 7.48/7.05 bnd_precedes X98 X99 -->
% 7.48/7.05 bnd_min_precedes X98 X99 X100;
% 7.48/7.05 ALL X94 X95 X96.
% 7.48/7.05 bnd_earlier X94 X95 & bnd_earlier X95 X96 --> bnd_earlier X94 X96;
% 7.48/7.05 ALL X90 X91 X92 X93.
% 7.48/7.05 (bnd_occurrence_of X92 X93 & bnd_root_occ X90 X92) &
% 7.48/7.05 bnd_root_occ X91 X92 -->
% 7.48/7.05 X90 = X91;
% 7.48/7.05 ALL X86 X87 X88 X89.
% 7.48/7.05 ((bnd_occurrence_of X88 X89 & ~ bnd_atomic X89) &
% 7.48/7.05 bnd_leaf_occ X86 X88) &
% 7.48/7.05 bnd_leaf_occ X87 X88 -->
% 7.48/7.05 X86 = X87;
% 7.48/7.05 ALL X82 X83 X84 X85.
% 7.48/7.05 (bnd_min_precedes X82 X83 X84 & bnd_occurrence_of X85 X84) &
% 7.48/7.05 bnd_subactivity_occurrence X83 X85 -->
% 7.48/7.05 bnd_subactivity_occurrence X82 X85;
% 7.48/7.05 ALL X78 X79 X80.
% 7.48/7.05 bnd_next_subocc X78 X79 X80 =
% 7.48/7.05 (bnd_min_precedes X78 X79 X80 &
% 7.48/7.05 ~ (EX X81.
% 7.48/7.05 bnd_min_precedes X78 X81 X80 & bnd_min_precedes X81 X79 X80));
% 7.48/7.05 ALL X75 X76 X77.
% 7.48/7.05 bnd_next_subocc X75 X76 X77 --> bnd_arboreal X75 & bnd_arboreal X76;
% 7.48/7.05 ALL X72 X73 X74. bnd_min_precedes X72 X73 X74 --> bnd_precedes X72 X73;
% 7.48/7.05 ALL X68 X69 X70.
% 7.48/7.05 bnd_min_precedes X68 X69 X70 -->
% 7.48/7.05 (EX X71. bnd_root X71 X70 & bnd_min_precedes X71 X69 X70);
% 7.48/7.05 ALL X65 X66 X67. bnd_min_precedes X65 X66 X67 --> ~ bnd_root X66 X67;
% 7.48/7.05 ALL X63 X64.
% 7.48/7.05 bnd_precedes X63 X64 = (bnd_earlier X63 X64 & bnd_legal X64);
% 7.48/7.05 ALL X61 X62. bnd_earlier X61 X62 --> ~ bnd_earlier X62 X61;
% 7.48/7.05 ALL X58 X59.
% 7.48/7.05 bnd_root_occ X58 X59 =
% 7.48/7.05 (EX X60.
% 7.48/7.05 (bnd_occurrence_of X59 X60 & bnd_subactivity_occurrence X58 X59) &
% 7.48/7.05 bnd_root X58 X60);
% 7.48/7.05 ALL X55 X56.
% 7.48/7.05 bnd_leaf_occ X55 X56 =
% 7.48/7.05 (EX X57.
% 7.48/7.05 (bnd_occurrence_of X56 X57 & bnd_subactivity_occurrence X55 X56) &
% 7.48/7.05 bnd_leaf X55 X57);
% 7.48/7.05 ALL X53 X54. bnd_root X53 X54 --> bnd_legal X53;
% 7.48/7.05 ALL X51 X52.
% 7.48/7.05 bnd_occurrence_of X51 X52 --> bnd_arboreal X51 = bnd_atomic X52;
% 7.48/7.05 ALL X47 X48.
% 7.48/7.05 bnd_leaf X47 X48 =
% 7.48/7.05 ((bnd_root X47 X48 | (EX X49. bnd_min_precedes X49 X47 X48)) &
% 7.48/7.05 ~ (EX X50. bnd_min_precedes X47 X50 X48));
% 7.48/7.05 ALL X44 X45.
% 7.48/7.05 bnd_atocc X44 X45 =
% 7.48/7.05 (EX X46.
% 7.48/7.05 (bnd_subactivity X45 X46 & bnd_atomic X46) &
% 7.48/7.05 bnd_occurrence_of X44 X46);
% 7.48/7.05 ALL X43. bnd_legal X43 --> bnd_arboreal X43;
% 7.48/7.05 ALL X41.
% 7.48/7.05 bnd_activity_occurrence X41 -->
% 7.48/7.05 (EX X42. bnd_activity X42 & bnd_occurrence_of X41 X42);
% 7.48/7.05 ALL X39 X40.
% 7.48/7.05 bnd_subactivity_occurrence X39 X40 -->
% 7.48/7.05 bnd_activity_occurrence X39 & bnd_activity_occurrence X40;
% 7.48/7.05 ALL X35 X36 X37.
% 7.48/7.05 bnd_occurrence_of X35 X37 & bnd_root_occ X36 X35 -->
% 7.48/7.05 ~ (EX X38. bnd_min_precedes X38 X36 X37);
% 7.48/7.05 ALL X31 X32 X33.
% 7.48/7.05 bnd_occurrence_of X31 X33 & bnd_leaf_occ X32 X31 -->
% 7.48/7.05 ~ (EX X34. bnd_min_precedes X32 X34 X33);
% 7.48/7.05 ALL X28 X29 X30.
% 7.48/7.05 bnd_occurrence_of X28 X29 & bnd_occurrence_of X28 X30 --> X29 = X30;
% 7.48/7.05 ALL X25 X26.
% 7.48/7.05 bnd_leaf X25 X26 & ~ bnd_atomic X26 -->
% 7.48/7.05 (EX X27. bnd_occurrence_of X27 X26 & bnd_leaf_occ X25 X27);
% 7.48/7.05 ALL X21 X22 X23.
% 7.48/7.05 bnd_min_precedes X22 X23 X21 -->
% 7.48/7.05 (EX X24.
% 7.48/7.05 (bnd_occurrence_of X24 X21 & bnd_subactivity_occurrence X22 X24) &
% 7.48/7.05 bnd_subactivity_occurrence X23 X24);
% 7.48/7.05 ALL X18 X19.
% 7.48/7.05 bnd_root X19 X18 -->
% 7.48/7.05 (EX X20. bnd_subactivity X20 X18 & bnd_atocc X19 X20);
% 7.48/7.05 ALL X14 X15 X16 X17.
% 7.48/7.05 (((bnd_occurrence_of X15 X14 & bnd_arboreal X16) & bnd_arboreal X17) &
% 7.48/7.05 bnd_subactivity_occurrence X16 X15) &
% 7.48/7.05 bnd_subactivity_occurrence X17 X15 -->
% 7.48/7.05 (bnd_min_precedes X16 X17 X14 | bnd_min_precedes X17 X16 X14) |
% 7.48/7.05 X16 = X17;
% 7.48/7.05 ALL X12 X13.
% 7.48/7.05 bnd_occurrence_of X13 X12 -->
% 7.48/7.05 bnd_activity X12 & bnd_activity_occurrence X13;
% 7.48/7.05 ALL X8 X9 X10 X11.
% 7.48/7.05 (((bnd_occurrence_of X9 X8 & bnd_subactivity_occurrence X10 X9) &
% 7.48/7.05 bnd_leaf_occ X11 X9) &
% 7.48/7.05 bnd_arboreal X10) &
% 7.48/7.05 ~ bnd_min_precedes X10 X11 X8 -->
% 7.48/7.05 X11 = X10;
% 7.48/7.05 ALL X3 X4 X5 X6 X7.
% 7.48/7.05 ((((bnd_occurrence_of X4 X3 & bnd_root_occ X6 X4) &
% 7.48/7.05 bnd_leaf_occ X7 X4) &
% 7.48/7.05 bnd_subactivity_occurrence X5 X4) &
% 7.48/7.05 bnd_min_precedes X6 X5 X3) &
% 7.48/7.05 ~ X5 = X7 -->
% 7.48/7.05 bnd_min_precedes X5 X7 X3;
% 7.48/7.05 ALL X0 X1.
% 7.48/7.05 bnd_occurrence_of X1 X0 & ~ bnd_atomic X0 -->
% 7.48/7.05 (EX X2. bnd_root X2 X0 & bnd_subactivity_occurrence X2 X1) |]
% 7.48/7.05 ==> bnd_occurrence_of X105 bnd_tptp0 -->
% 7.48/7.05 (EX X106 X107.
% 7.48/7.05 (((((bnd_occurrence_of X106 bnd_tptp3 & bnd_root_occ X106 X105) &
% 7.48/7.05 (bnd_occurrence_of X107 bnd_tptp1 |
% 7.48/7.05 bnd_occurrence_of X107 bnd_tptp2)) &
% 7.48/7.05 bnd_min_precedes X106 X107 bnd_tptp0) &
% 7.48/7.05 bnd_leaf_occ X107 X105) &
% 7.48/7.05 (bnd_occurrence_of X107 bnd_tptp1 -->
% 7.48/7.05 ~ (EX X108.
% 7.48/7.05 bnd_occurrence_of X108 bnd_tptp2 &
% 7.48/7.05 bnd_min_precedes X106 X108 bnd_tptp0))) &
% 7.48/7.05 (bnd_occurrence_of X107 bnd_tptp2 -->
% 7.48/7.05 ~ (EX X109.
% 7.48/7.05 bnd_occurrence_of X109 bnd_tptp1 &
% 7.48/7.05 bnd_min_precedes X106 X109 bnd_tptp0)))
% 7.48/7.05 Adding axioms...
% 7.48/7.06 Typedef.type_definition_def
% 12.90/12.42 ...done.
% 12.90/12.42 Ground types: ?'b, TPTP_Interpret.ind
% 12.90/12.42 Translating term (sizes: 1, 1) ...
% 16.70/16.23 Invoking SAT solver...
% 16.70/16.23 No model exists.
% 16.70/16.23 Translating term (sizes: 2, 1) ...
% 21.10/20.65 Invoking SAT solver...
% 21.10/20.66 No model exists.
% 21.10/20.66 Translating term (sizes: 1, 2) ...
% 48.17/47.67 Invoking SAT solver...
% 48.17/47.68 No model exists.
% 48.17/47.68 Translating term (sizes: 3, 1) ...
% 55.09/54.52 Invoking SAT solver...
% 55.09/54.52 No model exists.
% 55.09/54.52 Translating term (sizes: 2, 2) ...
% 89.81/89.16 Invoking SAT solver...
% 89.81/89.16 No model exists.
% 89.81/89.16 Translating term (sizes: 1, 3) ...
% 211.90/210.56 Invoking SAT solver...
% 212.00/210.66 No model exists.
% 212.00/210.66 Translating term (sizes: 4, 1) ...
% 226.01/224.55 Invoking SAT solver...
% 226.01/224.55 No model exists.
% 226.01/224.55 Translating term (sizes: 3, 2) ...
% 300.08/297.92 /export/starexec/sandbox/solver/lib/scripts/run-polyml-5.5.2: line 82: 29596 CPU time limit exceeded (core dumped) "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS
% 300.08/297.92 29597 (core dumped) | { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
% 300.08/297.93 /export/starexec/sandbox/solver/src/HOL/TPTP/lib/Tools/tptp_refute: line 26: 29542 Exit 152 "$ISABELLE_PROCESS" -q -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP
% 300.08/297.93 29543 CPU time limit exceeded (core dumped) | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far. Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^ monotype.$"
%------------------------------------------------------------------------------