%------------------------------------------------------------------------------
% File       : Z3---4.4.1
% Problem    : AGT004+2 : TPTP v6.4.0. Bugfixed v3.1.0.
% Transform  : none
% Format     : tptp
% Command    : z3_tptp -proof -model -t:%d -file:%s

% Computer   : n099.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 Jul 26 10:29:53 EDT 2016

% Result     : Theorem 0.07s
% Output     : Proof 0.07s
% Verified   : 
% Statistics : Number of formulae       :   34 (  34 expanded)
%              Number of leaves         :   19 (  19 expanded)
%              Depth                    :    8
%              Number of atoms          :  133 ( 133 expanded)
%              Number of equality atoms :    0 (   0 expanded)
%              Maximal formula depth    :   12 (   7 average)
%              Maximal term depth       :    1 (   1 average)

% Comments   : 
%------------------------------------------------------------------------------
%----WARNING: Z3---4.4.1 format not known, defaulting to TPTP
tff(accept_number_type,type,(
    accept_number: ( $i * $i ) > $o )).

tff(n5_type,type,(
    n5: $i )).

tff(countryamedicalorganization_type,type,(
    countryamedicalorganization: $i )).

tff(accept_leader_type,type,(
    accept_leader: ( $i * $i ) > $o )).

tff(countryahumanitarianorganization_type,type,(
    countryahumanitarianorganization: $i )).

tff(accept_city_type,type,(
    accept_city: ( $i * $i ) > $o )).

tff(coastvillage_type,type,(
    coastvillage: $i )).

tff(accept_team_type,type,(
    accept_team: ( $i * $i * $i * $i ) > $o )).

tff(1,axiom,(
    ~ accept_city(countryamedicalorganization,coastvillage) ),
    file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax',deduced_13)).

tff(2,plain,
    ( ~ accept_city(countryamedicalorganization,coastvillage)
    | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
    | ~ accept_number(countryamedicalorganization,n5)
    | accept_city(countryamedicalorganization,coastvillage) ),
    inference(tautology,[status(thm)],[])).

tff(3,plain,
    ( ~ accept_city(countryamedicalorganization,coastvillage)
    | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
    | ~ accept_number(countryamedicalorganization,n5) ),
    inference(unit_resolution,[status(thm)],[2,1])).

tff(4,plain,
    ( ~ ~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5)
  <=> accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5) ),
    inference(rewrite,[status(thm)],[])).

tff(5,axiom,(
    ~ ~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',query_4)).

tff(6,plain,(
    accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5) ),
    inference(modus_ponens,[status(thm)],[5,4])).

tff(7,plain,
    ( ~ ( accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5)
      <=> ~ ( ~ accept_city(countryamedicalorganization,coastvillage)
            | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
            | ~ accept_number(countryamedicalorganization,n5) ) )
    | ~ accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5)
    | ~ ( ~ accept_city(countryamedicalorganization,coastvillage)
        | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
        | ~ accept_number(countryamedicalorganization,n5) ) ),
    inference(tautology,[status(thm)],[])).

tff(8,plain,(
    ~ ( accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5)
    <=> ~ ( ~ accept_city(countryamedicalorganization,coastvillage)
          | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
          | ~ accept_number(countryamedicalorganization,n5) ) ) ),
    inference(unit_resolution,[status(thm)],[7,6,3])).

tff(9,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_team(X4,X1,X3,X2)
      <=> ~ ( ~ accept_city(X4,X3)
            | ~ accept_leader(X4,X1)
            | ~ accept_number(X4,X2) ) )
    <=> ( accept_team(X4,X1,X3,X2)
      <=> ~ ( ~ accept_city(X4,X3)
            | ~ accept_leader(X4,X1)
            | ~ accept_number(X4,X2) ) ) ) ),
    inference(reflexivity,[status(thm)],[])).

tff(10,plain,
    ( ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ~ ( ~ accept_city(A,C)
            | ~ accept_leader(A,L)
            | ~ accept_number(A,N) ) )
  <=> ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ~ ( ~ accept_city(A,C)
            | ~ accept_leader(A,L)
            | ~ accept_number(A,N) ) ) ),
    inference(quant_intro,[status(thm)],[9])).

tff(11,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_city(X4,X3)
        & accept_leader(X4,X1)
        & accept_number(X4,X2) )
    <=> ~ ( ~ accept_city(X4,X3)
          | ~ accept_leader(X4,X1)
          | ~ accept_number(X4,X2) ) ) ),
    inference(rewrite,[status(thm)],[])).

tff(12,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_team(X4,X1,X3,X2)
      <=> ( accept_city(X4,X3)
          & accept_leader(X4,X1)
          & accept_number(X4,X2) ) )
    <=> ( accept_team(X4,X1,X3,X2)
      <=> ~ ( ~ accept_city(X4,X3)
            | ~ accept_leader(X4,X1)
            | ~ accept_number(X4,X2) ) ) ) ),
    inference(monotonicity,[status(thm)],[11])).

tff(13,plain,
    ( ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ( accept_city(A,C)
          & accept_leader(A,L)
          & accept_number(A,N) ) )
  <=> ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ~ ( ~ accept_city(A,C)
            | ~ accept_leader(A,L)
            | ~ accept_number(A,N) ) ) ),
    inference(quant_intro,[status(thm)],[12])).

tff(14,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_team(X4,X1,X3,X2)
      <=> ( accept_city(X4,X3)
          & accept_leader(X4,X1)
          & accept_number(X4,X2) ) )
    <=> ( accept_team(X4,X1,X3,X2)
      <=> ( accept_city(X4,X3)
          & accept_leader(X4,X1)
          & accept_number(X4,X2) ) ) ) ),
    inference(rewrite,[status(thm)],[])).

tff(15,plain,
    ( ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ( accept_city(A,C)
          & accept_leader(A,L)
          & accept_number(A,N) ) )
  <=> ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ( accept_city(A,C)
          & accept_leader(A,L)
          & accept_number(A,N) ) ) ),
    inference(quant_intro,[status(thm)],[14])).

tff(16,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_city(X4,X3)
        & accept_leader(X4,X1)
        & accept_number(X4,X2) )
    <=> ( accept_city(X4,X3)
        & accept_leader(X4,X1)
        & accept_number(X4,X2) ) ) ),
    inference(rewrite,[status(thm)],[])).

tff(17,plain,(
    ! [X4: $i,X3: $i,X2: $i,X1: $i] :
      ( ( accept_team(X4,X1,X3,X2)
      <=> ( accept_city(X4,X3)
          & accept_leader(X4,X1)
          & accept_number(X4,X2) ) )
    <=> ( accept_team(X4,X1,X3,X2)
      <=> ( accept_city(X4,X3)
          & accept_leader(X4,X1)
          & accept_number(X4,X2) ) ) ) ),
    inference(monotonicity,[status(thm)],[16])).

tff(18,plain,
    ( ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ( accept_city(A,C)
          & accept_leader(A,L)
          & accept_number(A,N) ) )
  <=> ! [A: $i,C: $i,N: $i,L: $i] :
        ( accept_team(A,L,C,N)
      <=> ( accept_city(A,C)
          & accept_leader(A,L)
          & accept_number(A,N) ) ) ),
    inference(quant_intro,[status(thm)],[17])).

tff(19,axiom,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ( accept_city(A,C)
        & accept_leader(A,L)
        & accept_number(A,N) ) ) ),
    file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax',a1_1)).

tff(20,plain,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ( accept_city(A,C)
        & accept_leader(A,L)
        & accept_number(A,N) ) ) ),
    inference(modus_ponens,[status(thm)],[19,18])).

tff(21,plain,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ( accept_city(A,C)
        & accept_leader(A,L)
        & accept_number(A,N) ) ) ),
    inference(modus_ponens,[status(thm)],[20,15])).

tff(22,plain,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ( accept_city(A,C)
        & accept_leader(A,L)
        & accept_number(A,N) ) ) ),
    inference(nnf,[status(sab)],[21])).

tff(23,plain,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ~ ( ~ accept_city(A,C)
          | ~ accept_leader(A,L)
          | ~ accept_number(A,N) ) ) ),
    inference(modus_ponens,[status(thm)],[22,13])).

tff(24,plain,(
    ! [A: $i,C: $i,N: $i,L: $i] :
      ( accept_team(A,L,C,N)
    <=> ~ ( ~ accept_city(A,C)
          | ~ accept_leader(A,L)
          | ~ accept_number(A,N) ) ) ),
    inference(modus_ponens,[status(thm)],[23,10])).

tff(25,plain,
    ( ~ ! [A: $i,C: $i,N: $i,L: $i] :
          ( accept_team(A,L,C,N)
        <=> ~ ( ~ accept_city(A,C)
              | ~ accept_leader(A,L)
              | ~ accept_number(A,N) ) )
    | ( accept_team(countryamedicalorganization,countryahumanitarianorganization,coastvillage,n5)
    <=> ~ ( ~ accept_city(countryamedicalorganization,coastvillage)
          | ~ accept_leader(countryamedicalorganization,countryahumanitarianorganization)
          | ~ accept_number(countryamedicalorganization,n5) ) ) ),
    inference(quant_inst,[status(thm)],[])).

tff(26,plain,(
    $false ),
    inference(unit_resolution,[status(thm)],[25,24,8])).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem    : AGT004+2 : TPTP v6.4.0. Bugfixed v3.1.0.
% 0.00/0.04  % Command    : z3_tptp -proof -model -t:%d -file:%s
% 0.02/0.23  % Computer   : n099.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     : 32218.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   : Thu Jul 21 10:50:24 CDT 2016
% 0.02/0.23  % CPUTime    : 
% 0.07/0.33  % SZS status Theorem
% 0.07/0.33  % SZS output start Proof
% 0.07/0.33  tff(accept_number_type, type, (
% 0.07/0.33     accept_number: ( $i * $i ) > $o)).
% 0.07/0.33  tff(n5_type, type, (
% 0.07/0.33     n5: $i)).
% 0.07/0.33  tff(countryamedicalorganization_type, type, (
% 0.07/0.33     countryamedicalorganization: $i)).
% 0.07/0.33  tff(accept_leader_type, type, (
% 0.07/0.33     accept_leader: ( $i * $i ) > $o)).
% 0.07/0.33  tff(countryahumanitarianorganization_type, type, (
% 0.07/0.33     countryahumanitarianorganization: $i)).
% 0.07/0.33  tff(accept_city_type, type, (
% 0.07/0.33     accept_city: ( $i * $i ) > $o)).
% 0.07/0.33  tff(coastvillage_type, type, (
% 0.07/0.33     coastvillage: $i)).
% 0.07/0.33  tff(accept_team_type, type, (
% 0.07/0.33     accept_team: ( $i * $i * $i * $i ) > $o)).
% 0.07/0.33  tff(1,axiom,((~accept_city(countryamedicalorganization, coastvillage))), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax','deduced_13')).
% 0.07/0.33  tff(2,plain,
% 0.07/0.33      ((((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))) | accept_city(countryamedicalorganization, coastvillage))),
% 0.07/0.33      inference(tautology,[status(thm)],[])).
% 0.07/0.33  tff(3,plain,
% 0.07/0.33      (((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))),
% 0.07/0.33      inference(unit_resolution,[status(thm)],[2, 1])).
% 0.07/0.33  tff(4,plain,
% 0.07/0.33      (((~(~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5))) <=> accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5))),
% 0.07/0.33      inference(rewrite,[status(thm)],[])).
% 0.07/0.33  tff(5,axiom,((~(~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','query_4')).
% 0.07/0.33  tff(6,plain,
% 0.07/0.33      (accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)),
% 0.07/0.33      inference(modus_ponens,[status(thm)],[5, 4])).
% 0.07/0.33  tff(7,plain,
% 0.07/0.33      (((~(accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))))) | (~accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5)) | (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5)))))),
% 0.07/0.33      inference(tautology,[status(thm)],[])).
% 0.07/0.33  tff(8,plain,
% 0.07/0.33      ((~(accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))))))),
% 0.07/0.33      inference(unit_resolution,[status(thm)],[7, 6, 3])).
% 0.07/0.33  tff(9,plain,
% 0.07/0.33      (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))) <=> (accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))))),
% 0.07/0.33      inference(reflexivity,[status(thm)],[])).
% 0.07/0.33  tff(10,plain,
% 0.07/0.33      ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))))),
% 0.07/0.33      inference(quant_intro,[status(thm)],[9])).
% 0.07/0.33  tff(11,plain,
% 0.07/0.33      (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2)) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2)))))),
% 0.07/0.33      inference(rewrite,[status(thm)],[])).
% 0.07/0.33  tff(12,plain,
% 0.07/0.33      (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (~((~accept_city(X4, X3)) | (~accept_leader(X4, X1)) | (~accept_number(X4, X2))))))),
% 0.07/0.35      inference(monotonicity,[status(thm)],[11])).
% 0.07/0.35  tff(13,plain,
% 0.07/0.35      ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N))))))),
% 0.07/0.35      inference(quant_intro,[status(thm)],[12])).
% 0.07/0.35  tff(14,plain,
% 0.07/0.35      (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))))),
% 0.07/0.35      inference(rewrite,[status(thm)],[])).
% 0.07/0.35  tff(15,plain,
% 0.07/0.35      ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))))),
% 0.07/0.35      inference(quant_intro,[status(thm)],[14])).
% 0.07/0.35  tff(16,plain,
% 0.07/0.35      (![X4: $i, X3: $i, X2: $i, X1: $i] : (((accept_city(X4, X3) & accept_leader(X4, X1)) & accept_number(X4, X2)) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2)))),
% 0.07/0.35      inference(rewrite,[status(thm)],[])).
% 0.07/0.35  tff(17,plain,
% 0.07/0.35      (![X4: $i, X3: $i, X2: $i, X1: $i] : ((accept_team(X4, X1, X3, X2) <=> ((accept_city(X4, X3) & accept_leader(X4, X1)) & accept_number(X4, X2))) <=> (accept_team(X4, X1, X3, X2) <=> (accept_city(X4, X3) & accept_leader(X4, X1) & accept_number(X4, X2))))),
% 0.07/0.35      inference(monotonicity,[status(thm)],[16])).
% 0.07/0.35  tff(18,plain,
% 0.07/0.35      ((![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> ((accept_city(A, C) & accept_leader(A, L)) & accept_number(A, N))) <=> ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N))))),
% 0.07/0.35      inference(quant_intro,[status(thm)],[17])).
% 0.07/0.35  tff(19,axiom,(![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> ((accept_city(A, C) & accept_leader(A, L)) & accept_number(A, N)))), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax','a1_1')).
% 0.07/0.35  tff(20,plain,
% 0.07/0.35      (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))),
% 0.07/0.35      inference(modus_ponens,[status(thm)],[19, 18])).
% 0.07/0.35  tff(21,plain,
% 0.07/0.35      (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))),
% 0.07/0.35      inference(modus_ponens,[status(thm)],[20, 15])).
% 0.07/0.35  tff(22,plain,(
% 0.07/0.35      ![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (accept_city(A, C) & accept_leader(A, L) & accept_number(A, N)))),
% 0.07/0.35      inference(nnf,[status(sab)],[21])).
% 0.07/0.35  tff(23,plain,
% 0.07/0.35      (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))),
% 0.07/0.35      inference(modus_ponens,[status(thm)],[22, 13])).
% 0.07/0.35  tff(24,plain,
% 0.07/0.35      (![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))),
% 0.07/0.35      inference(modus_ponens,[status(thm)],[23, 10])).
% 0.07/0.35  tff(25,plain,
% 0.07/0.35      (((~![A: $i, C: $i, N: $i, L: $i] : (accept_team(A, L, C, N) <=> (~((~accept_city(A, C)) | (~accept_leader(A, L)) | (~accept_number(A, N)))))) | (accept_team(countryamedicalorganization, countryahumanitarianorganization, coastvillage, n5) <=> (~((~accept_city(countryamedicalorganization, coastvillage)) | (~accept_leader(countryamedicalorganization, countryahumanitarianorganization)) | (~accept_number(countryamedicalorganization, n5))))))),
% 0.07/0.35      inference(quant_inst,[status(thm)],[])).
% 0.07/0.35  tff(26,plain,
% 0.07/0.35      ($false),
% 0.07/0.35      inference(unit_resolution,[status(thm)],[25, 24, 8])).
% 0.07/0.35  % SZS output end Proof
%------------------------------------------------------------------------------
