%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : AGT009+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 04:57:39 AM UTC 2025
% Result : Theorem 0.85s 1.08s
% Output : Proof 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 128
% Syntax : Number of formulae : 296 ( 74 unt; 0 typ; 0 def)
% Number of atoms : 2356 ( 0 equ)
% Maximal formula atoms : 16 ( 7 avg)
% Number of connectives : 3403 (1494 ~;1069 |; 434 &)
% ( 382 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of FOOLs : 151 ( 151 fml; 0 var)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-4 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 647 ( 561 !; 0 ?; 647 :)
% Comments :
%------------------------------------------------------------------------------
tff(less_type,type,
less: ( $i * $i ) > $o ).
tff(n25_type,type,
n25: $i ).
tff(n24_type,type,
n24: $i ).
tff(accept_population_type,type,
accept_population: ( $i * $i * $i ) > $o ).
tff(christian_type,type,
christian: $i ).
tff(muslimcountrybhumanitarianorganization_type,type,
muslimcountrybhumanitarianorganization: $i ).
tff(n0_type,type,
n0: $i ).
tff(other_type,type,
other: $i ).
tff(native_type,type,
native: $i ).
tff(muslim_type,type,
muslim: $i ).
tff(n75_type,type,
n75: $i ).
tff(atheist_type,type,
atheist: $i ).
tff(accept_city_type,type,
accept_city: ( $i * $i ) > $o ).
tff(citya_type,type,
citya: $i ).
tff(accept_number_type,type,
accept_number: ( $i * $i ) > $o ).
tff(n2_type,type,
n2: $i ).
tff(accept_leader_type,type,
accept_leader: ( $i * $i ) > $o ).
tff(countrybhumanitarianorganization_type,type,
countrybhumanitarianorganization: $i ).
tff(accept_team_type,type,
accept_team: ( $i * $i * $i * $i ) > $o ).
tff(n1_type,type,
n1: $i ).
tff(towna_type,type,
towna: $i ).
tff(countryacivilorganization_type,type,
countryacivilorganization: $i ).
tff(any_agent_in_all_proposed_teams_type,type,
any_agent_in_all_proposed_teams: ( $i * $i * $i ) > $o ).
tff(the_agent_not_in_any_proposed_teams_type,type,
the_agent_not_in_any_proposed_teams: ( $i * $i * $i ) > $o ).
tff(n85_type,type,
n85: $i ).
tff(n3_type,type,
n3: $i ).
tff(n12_type,type,
n12: $i ).
tff(coastvillage_type,type,
coastvillage: $i ).
tff(n5_type,type,
n5: $i ).
tff(christiancountrychumanitarianorganization_type,type,
christiancountrychumanitarianorganization: $i ).
tff(n20_type,type,
n20: $i ).
tff(n78_type,type,
n78: $i ).
tff(cityb_type,type,
cityb: $i ).
tff(n4_type,type,
n4: $i ).
tff(n65_type,type,
n65: $i ).
tff(n30_type,type,
n30: $i ).
tff(townc_type,type,
townc: $i ).
tff(countryahumanitarianorganization_type,type,
countryahumanitarianorganization: $i ).
tff(the_agent_in_all_proposed_teams_type,type,
the_agent_in_all_proposed_teams: ( $i * $i * $i ) > $o ).
tff(rdn_positive_less_type,type,
rdn_positive_less: ( $i * $i ) > $o ).
tff(rdn_type,type,
rdn: ( $i * $i ) > $i ).
tff(rdnn_type,type,
rdnn: $i > $i ).
tff(rdn_non_zero_type,type,
rdn_non_zero: $i > $o ).
tff(rdn_non_zero_digit_type,type,
rdn_non_zero_digit: $i > $o ).
tff(rdn_translate_type,type,
rdn_translate: ( $i * $i ) > $o ).
tff(rdn_pos_type,type,
rdn_pos: $i > $i ).
tff(1,plain,
^ [A: $i] :
refl(( ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
inference(bind,[status(th)],[]) ).
tff(2,plain,
( ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) ),
inference(quant_intro,[status(thm)],[1]) ).
tff(3,plain,
^ [A: $i] :
trans(trans(monotonicity(rewrite(( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ( ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
rewrite(( ( ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
rewrite(( ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
inference(bind,[status(th)],[]) ).
tff(4,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ) ),
inference(quant_intro,[status(thm)],[3]) ).
tff(5,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(6,plain,
^ [A: $i] :
rewrite(( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ) )),
inference(bind,[status(th)],[]) ).
tff(7,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ) ),
inference(quant_intro,[status(thm)],[6]) ).
tff(8,axiom,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_10) ).
tff(9,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
inference(modus_ponens,[status(thm)],[8,7]) ).
tff(10,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
inference(modus_ponens,[status(thm)],[9,5]) ).
tff(11,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n25)
& accept_population(A,muslim,n0)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
inference(skolemize,[status(sab)],[10]) ).
tff(12,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
inference(modus_ponens,[status(thm)],[11,4]) ).
tff(13,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) ),
inference(modus_ponens,[status(thm)],[12,2]) ).
tff(14,plain,
( ~ ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n25)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,citya) )
| ~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,citya) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(15,plain,
~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,citya) ),
inference(unit_resolution,[status(thm)],[14,13]) ).
tff(16,plain,
^ [A: $i,C: $i,N: $i,L: $i] :
refl(( ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
<=> ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) )),
inference(bind,[status(th)],[]) ).
tff(17,plain,
( ! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
<=> ! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) ),
inference(quant_intro,[status(thm)],[16]) ).
tff(18,plain,
^ [A: $i,C: $i,N: $i,L: $i] :
trans(trans(monotonicity(rewrite(( ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) )
<=> ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) ) )),
( ( accept_team(A,L,C,N)
<=> ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) ) )
<=> ( accept_team(A,L,C,N)
<=> ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) ) ) )),
rewrite(( ( accept_team(A,L,C,N)
<=> ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) ) )
<=> ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) )),
( ( accept_team(A,L,C,N)
<=> ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) ) )
<=> ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) )),
rewrite(( ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
<=> ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) )),
( ( accept_team(A,L,C,N)
<=> ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) ) )
<=> ~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) )),
inference(bind,[status(th)],[]) ).
tff(19,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_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ) ),
inference(quant_intro,[status(thm)],[18]) ).
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) ) )
<=> ! [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(rewrite,[status(thm)],[]) ).
tff(21,plain,
^ [A: $i,C: $i,N: $i,L: $i] :
rewrite(( ( accept_team(A,L,C,N)
<=> ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) ) )
<=> ( accept_team(A,L,C,N)
<=> ( accept_city(A,C)
& accept_leader(A,L)
& accept_number(A,N) ) ) )),
inference(bind,[status(th)],[]) ).
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) ) )
<=> ! [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)],[21]) ).
tff(23,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/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_1) ).
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,22]) ).
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) ) ),
inference(modus_ponens,[status(thm)],[24,20]) ).
tff(26,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(skolemize,[status(sab)],[25]) ).
tff(27,plain,
! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ),
inference(modus_ponens,[status(thm)],[26,19]) ).
tff(28,plain,
! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) ),
inference(modus_ponens,[status(thm)],[27,17]) ).
tff(29,plain,
( ~ ! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
| ~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(30,plain,
~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ),
inference(unit_resolution,[status(thm)],[29,28]) ).
tff(31,plain,
( accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2)
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ),
inference(rewrite,[status(thm)],[]) ).
tff(32,plain,
( ~ ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2)
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ),
inference(rewrite,[status(thm)],[]) ).
tff(33,axiom,
~ ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_9) ).
tff(34,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(modus_ponens,[status(thm)],[33,32]) ).
tff(35,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2),
inference(modus_ponens,[status(thm)],[34,31]) ).
tff(36,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) )
| ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) ),
inference(tautology,[status(thm)],[]) ).
tff(37,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,citya,n2) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) ) ),
inference(unit_resolution,[status(thm)],[36,35]) ).
tff(38,plain,
~ ( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2) ),
inference(unit_resolution,[status(thm)],[37,30]) ).
tff(39,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,citya)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n2)
| accept_city(muslimcountrybhumanitarianorganization,citya) ),
inference(tautology,[status(thm)],[]) ).
tff(40,plain,
accept_city(muslimcountrybhumanitarianorganization,citya),
inference(unit_resolution,[status(thm)],[39,38]) ).
tff(41,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,citya) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
| ~ accept_city(muslimcountrybhumanitarianorganization,citya) ),
inference(tautology,[status(thm)],[]) ).
tff(42,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,citya) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ) ),
inference(unit_resolution,[status(thm)],[41,40]) ).
tff(43,plain,
~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(unit_resolution,[status(thm)],[42,15]) ).
tff(44,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| accept_population(muslimcountrybhumanitarianorganization,christian,n25) ),
inference(tautology,[status(thm)],[]) ).
tff(45,plain,
accept_population(muslimcountrybhumanitarianorganization,christian,n25),
inference(unit_resolution,[status(thm)],[44,43]) ).
tff(46,plain,
^ [A: $i] :
refl(( ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
inference(bind,[status(th)],[]) ).
tff(47,plain,
( ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) ),
inference(quant_intro,[status(thm)],[46]) ).
tff(48,plain,
^ [A: $i] :
trans(trans(monotonicity(rewrite(( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ( ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
rewrite(( ( ~ ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
rewrite(( ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
inference(bind,[status(th)],[]) ).
tff(49,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ) ),
inference(quant_intro,[status(thm)],[48]) ).
tff(50,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(51,plain,
^ [A: $i] :
rewrite(( ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ) )),
inference(bind,[status(th)],[]) ).
tff(52,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ) ),
inference(quant_intro,[status(thm)],[51]) ).
tff(53,axiom,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_9) ).
tff(54,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
inference(modus_ponens,[status(thm)],[53,52]) ).
tff(55,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
inference(modus_ponens,[status(thm)],[54,50]) ).
tff(56,plain,
! [A: $i] :
( ( accept_population(A,atheist,n75)
& accept_population(A,christian,n24)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
inference(skolemize,[status(sab)],[55]) ).
tff(57,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
inference(modus_ponens,[status(thm)],[56,49]) ).
tff(58,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) ),
inference(modus_ponens,[status(thm)],[57,47]) ).
tff(59,plain,
( ~ ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n75)
| ~ accept_population(A,christian,n24)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,towna) )
| ~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,towna) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(60,plain,
~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,towna) ),
inference(unit_resolution,[status(thm)],[59,58]) ).
tff(61,plain,
( any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
<=> any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ),
inference(rewrite,[status(thm)],[]) ).
tff(62,axiom,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_12) ).
tff(63,plain,
any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(modus_ponens,[status(thm)],[62,61]) ).
tff(64,plain,
^ [A: $i,L: $i,C: $i] :
refl(( ( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
<=> ( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ) )),
inference(bind,[status(th)],[]) ).
tff(65,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ) ),
inference(quant_intro,[status(thm)],[64]) ).
tff(66,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(67,plain,
^ [A: $i,L: $i,C: $i] :
rewrite(( ( any_agent_in_all_proposed_teams(A,L,C)
=> accept_leader(A,L) )
<=> ( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ) )),
inference(bind,[status(th)],[]) ).
tff(68,plain,
( ! [A: $i,L: $i,C: $i] :
( any_agent_in_all_proposed_teams(A,L,C)
=> accept_leader(A,L) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ) ),
inference(quant_intro,[status(thm)],[67]) ).
tff(69,axiom,
! [A: $i,L: $i,C: $i] :
( any_agent_in_all_proposed_teams(A,L,C)
=> accept_leader(A,L) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_5) ).
tff(70,plain,
! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ),
inference(modus_ponens,[status(thm)],[69,68]) ).
tff(71,plain,
! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ),
inference(modus_ponens,[status(thm)],[70,66]) ).
tff(72,plain,
! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ),
inference(skolemize,[status(sab)],[71]) ).
tff(73,plain,
! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) ),
inference(modus_ponens,[status(thm)],[72,65]) ).
tff(74,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
| ~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
| ~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(75,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
| ~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ),
inference(quant_inst,[status(thm)],[]) ).
tff(76,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ any_agent_in_all_proposed_teams(A,L,C)
| accept_leader(A,L) )
| ~ any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ),
inference(modus_ponens,[status(thm)],[75,74]) ).
tff(77,plain,
accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization),
inference(unit_resolution,[status(thm)],[76,73,63]) ).
tff(78,plain,
( the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
<=> the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna) ),
inference(rewrite,[status(thm)],[]) ).
tff(79,axiom,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_11) ).
tff(80,plain,
the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna),
inference(modus_ponens,[status(thm)],[79,78]) ).
tff(81,plain,
^ [A: $i,L: $i,C: $i] :
refl(( ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
<=> ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )),
inference(bind,[status(th)],[]) ).
tff(82,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ),
inference(quant_intro,[status(thm)],[81]) ).
tff(83,plain,
^ [A: $i,L: $i,C: $i] :
trans(monotonicity(trans(monotonicity(rewrite(( ( accept_city(A,C)
& accept_leader(A,L) )
<=> ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L) ) )),
( ~ ( accept_city(A,C)
& accept_leader(A,L) )
<=> ~ ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L) ) )),
rewrite(( ~ ~ ( ~ accept_city(A,C)
| ~ accept_leader(A,L) )
<=> ( ~ accept_city(A,C)
| ~ accept_leader(A,L) ) )),
( ~ ( accept_city(A,C)
& accept_leader(A,L) )
<=> ( ~ accept_city(A,C)
| ~ accept_leader(A,L) ) )),
( ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_city(A,C)
| ~ accept_leader(A,L) ) )),
rewrite(( ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_city(A,C)
| ~ accept_leader(A,L) )
<=> ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )),
( ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )),
inference(bind,[status(th)],[]) ).
tff(84,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ),
inference(quant_intro,[status(thm)],[83]) ).
tff(85,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(86,plain,
^ [A: $i,L: $i,C: $i] :
rewrite(( ( the_agent_not_in_any_proposed_teams(A,L,C)
=> ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ) )),
inference(bind,[status(th)],[]) ).
tff(87,plain,
( ! [A: $i,L: $i,C: $i] :
( the_agent_not_in_any_proposed_teams(A,L,C)
=> ~ ( accept_city(A,C)
& accept_leader(A,L) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ) ),
inference(quant_intro,[status(thm)],[86]) ).
tff(88,axiom,
! [A: $i,L: $i,C: $i] :
( the_agent_not_in_any_proposed_teams(A,L,C)
=> ~ ( accept_city(A,C)
& accept_leader(A,L) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_6) ).
tff(89,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ),
inference(modus_ponens,[status(thm)],[88,87]) ).
tff(90,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ),
inference(modus_ponens,[status(thm)],[89,85]) ).
tff(91,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ ( accept_city(A,C)
& accept_leader(A,L) ) ),
inference(skolemize,[status(sab)],[90]) ).
tff(92,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ),
inference(modus_ponens,[status(thm)],[91,84]) ).
tff(93,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) ),
inference(modus_ponens,[status(thm)],[92,82]) ).
tff(94,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(95,plain,
( ( ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) )
<=> ( ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(96,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ) ),
inference(monotonicity,[status(thm)],[95]) ).
tff(97,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ) ),
inference(transitivity,[status(thm)],[96,94]) ).
tff(98,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,towna) ),
inference(quant_inst,[status(thm)],[]) ).
tff(99,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_not_in_any_proposed_teams(A,L,C)
| ~ accept_leader(A,L)
| ~ accept_city(A,C) )
| ~ accept_city(muslimcountrybhumanitarianorganization,towna)
| ~ the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization,countryacivilorganization,towna)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryacivilorganization) ),
inference(modus_ponens,[status(thm)],[98,97]) ).
tff(100,plain,
~ accept_city(muslimcountrybhumanitarianorganization,towna),
inference(unit_resolution,[status(thm)],[99,93,80,77]) ).
tff(101,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,towna) )
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| accept_city(muslimcountrybhumanitarianorganization,towna) ),
inference(tautology,[status(thm)],[]) ).
tff(102,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,towna) )
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(unit_resolution,[status(thm)],[101,100]) ).
tff(103,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(unit_resolution,[status(thm)],[102,60]) ).
tff(104,plain,
^ [A: $i] :
refl(( ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
inference(bind,[status(th)],[]) ).
tff(105,plain,
( ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) ),
inference(quant_intro,[status(thm)],[104]) ).
tff(106,plain,
^ [A: $i] :
trans(trans(monotonicity(rewrite(( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> ~ ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) ) )),
( ( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ( ~ ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
rewrite(( ( ~ ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
( ( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
rewrite(( ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
( ( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
inference(bind,[status(th)],[]) ).
tff(107,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) ),
inference(quant_intro,[status(thm)],[106]) ).
tff(108,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(109,plain,
^ [A: $i] :
rewrite(( ( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) )),
inference(bind,[status(th)],[]) ).
tff(110,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ) ),
inference(quant_intro,[status(thm)],[109]) ).
tff(111,axiom,
! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_7) ).
tff(112,plain,
! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
inference(modus_ponens,[status(thm)],[111,110]) ).
tff(113,plain,
! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
inference(modus_ponens,[status(thm)],[112,108]) ).
tff(114,plain,
! [A: $i] :
( ( accept_population(A,atheist,n12)
& accept_population(A,christian,n3)
& accept_population(A,muslim,n0)
& accept_population(A,native,n85)
& accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
inference(skolemize,[status(sab)],[113]) ).
tff(115,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
inference(modus_ponens,[status(thm)],[114,107]) ).
tff(116,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) ),
inference(modus_ponens,[status(thm)],[115,105]) ).
tff(117,plain,
( ~ ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n12)
| ~ accept_population(A,christian,n3)
| ~ accept_population(A,muslim,n0)
| ~ accept_population(A,native,n85)
| ~ accept_population(A,other,n0) )
<=> accept_city(A,coastvillage) )
| ~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,coastvillage) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(118,plain,
~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,coastvillage) ),
inference(unit_resolution,[status(thm)],[117,116]) ).
tff(119,plain,
( ~ ! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
| ~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) )
<=> accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(120,plain,
~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) )
<=> accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ),
inference(unit_resolution,[status(thm)],[119,28]) ).
tff(121,plain,
( accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5)
<=> accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ),
inference(rewrite,[status(thm)],[]) ).
tff(122,axiom,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_13) ).
tff(123,plain,
accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5),
inference(modus_ponens,[status(thm)],[122,121]) ).
tff(124,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) )
<=> accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) )
| ~ accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) ),
inference(tautology,[status(thm)],[]) ).
tff(125,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) )
<=> accept_team(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization,coastvillage,n5) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) ) ),
inference(unit_resolution,[status(thm)],[124,123]) ).
tff(126,plain,
~ ( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5) ),
inference(unit_resolution,[status(thm)],[125,120]) ).
tff(127,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage)
| ~ accept_leader(muslimcountrybhumanitarianorganization,christiancountrychumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n5)
| accept_city(muslimcountrybhumanitarianorganization,coastvillage) ),
inference(tautology,[status(thm)],[]) ).
tff(128,plain,
accept_city(muslimcountrybhumanitarianorganization,coastvillage),
inference(unit_resolution,[status(thm)],[127,126]) ).
tff(129,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,coastvillage) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
| ~ accept_city(muslimcountrybhumanitarianorganization,coastvillage) ),
inference(tautology,[status(thm)],[]) ).
tff(130,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
<=> accept_city(muslimcountrybhumanitarianorganization,coastvillage) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ) ),
inference(unit_resolution,[status(thm)],[129,128]) ).
tff(131,plain,
~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(unit_resolution,[status(thm)],[130,118]) ).
tff(132,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n12)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n3)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n85)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(tautology,[status(thm)],[]) ).
tff(133,plain,
accept_population(muslimcountrybhumanitarianorganization,other,n0),
inference(unit_resolution,[status(thm)],[132,131]) ).
tff(134,plain,
^ [A: $i] :
refl(( ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
inference(bind,[status(th)],[]) ).
tff(135,plain,
( ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) ),
inference(quant_intro,[status(thm)],[134]) ).
tff(136,plain,
^ [A: $i] :
trans(trans(monotonicity(rewrite(( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> ~ ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) ) )),
( ( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ( ~ ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
rewrite(( ( ~ ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
( ( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
rewrite(( ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
( ( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
inference(bind,[status(th)],[]) ).
tff(137,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) ),
inference(quant_intro,[status(thm)],[136]) ).
tff(138,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(139,plain,
^ [A: $i] :
rewrite(( ( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) )),
inference(bind,[status(th)],[]) ).
tff(140,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ) ),
inference(quant_intro,[status(thm)],[139]) ).
tff(141,axiom,
! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_12) ).
tff(142,plain,
! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
inference(modus_ponens,[status(thm)],[141,140]) ).
tff(143,plain,
! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
inference(modus_ponens,[status(thm)],[142,138]) ).
tff(144,plain,
! [A: $i] :
( ( accept_population(A,atheist,n78)
& accept_population(A,christian,n20)
& accept_population(A,muslim,n1)
& accept_population(A,native,n0)
& accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
inference(skolemize,[status(sab)],[143]) ).
tff(145,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
inference(modus_ponens,[status(thm)],[144,137]) ).
tff(146,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) ),
inference(modus_ponens,[status(thm)],[145,135]) ).
tff(147,plain,
( ~ ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n78)
| ~ accept_population(A,christian,n20)
| ~ accept_population(A,muslim,n1)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n1) )
<=> accept_city(A,cityb) )
| ~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) )
<=> accept_city(muslimcountrybhumanitarianorganization,cityb) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(148,plain,
~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) )
<=> accept_city(muslimcountrybhumanitarianorganization,cityb) ),
inference(unit_resolution,[status(thm)],[147,146]) ).
tff(149,plain,
( ~ ! [A: $i,C: $i,N: $i,L: $i] :
~ ( ( ~ accept_city(A,C)
| ~ accept_leader(A,L)
| ~ accept_number(A,N) )
<=> accept_team(A,L,C,N) )
| ~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(150,plain,
~ ( ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ),
inference(unit_resolution,[status(thm)],[149,28]) ).
tff(151,plain,
( accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4)
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ),
inference(rewrite,[status(thm)],[]) ).
tff(152,axiom,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_8) ).
tff(153,plain,
accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4),
inference(modus_ponens,[status(thm)],[152,151]) ).
tff(154,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) )
| ~ accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) ),
inference(tautology,[status(thm)],[]) ).
tff(155,plain,
( ( ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) )
<=> accept_team(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization,cityb,n4) )
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) ) ),
inference(unit_resolution,[status(thm)],[154,153]) ).
tff(156,plain,
~ ( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4) ),
inference(unit_resolution,[status(thm)],[155,150]) ).
tff(157,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,cityb)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countrybhumanitarianorganization)
| ~ accept_number(muslimcountrybhumanitarianorganization,n4)
| accept_city(muslimcountrybhumanitarianorganization,cityb) ),
inference(tautology,[status(thm)],[]) ).
tff(158,plain,
accept_city(muslimcountrybhumanitarianorganization,cityb),
inference(unit_resolution,[status(thm)],[157,156]) ).
tff(159,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) )
<=> accept_city(muslimcountrybhumanitarianorganization,cityb) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) )
| ~ accept_city(muslimcountrybhumanitarianorganization,cityb) ),
inference(tautology,[status(thm)],[]) ).
tff(160,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) )
<=> accept_city(muslimcountrybhumanitarianorganization,cityb) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) ) ),
inference(unit_resolution,[status(thm)],[159,158]) ).
tff(161,plain,
~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1) ),
inference(unit_resolution,[status(thm)],[160,148]) ).
tff(162,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n78)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n20)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n1)
| accept_population(muslimcountrybhumanitarianorganization,muslim,n1) ),
inference(tautology,[status(thm)],[]) ).
tff(163,plain,
accept_population(muslimcountrybhumanitarianorganization,muslim,n1),
inference(unit_resolution,[status(thm)],[162,161]) ).
tff(164,plain,
^ [A: $i] :
refl(( ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
inference(bind,[status(th)],[]) ).
tff(165,plain,
( ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) ),
inference(quant_intro,[status(thm)],[164]) ).
tff(166,plain,
^ [A: $i] :
trans(trans(monotonicity(rewrite(( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> ~ ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) ) )),
( ( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ( ~ ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
rewrite(( ( ~ ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
( ( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
rewrite(( ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
( ( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
inference(bind,[status(th)],[]) ).
tff(167,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ) ),
inference(quant_intro,[status(thm)],[166]) ).
tff(168,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(169,plain,
^ [A: $i] :
rewrite(( ( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ) )),
inference(bind,[status(th)],[]) ).
tff(170,plain,
( ! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) )
<=> ! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ) ),
inference(quant_intro,[status(thm)],[169]) ).
tff(171,axiom,
! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a2_13) ).
tff(172,plain,
! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
inference(modus_ponens,[status(thm)],[171,170]) ).
tff(173,plain,
! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
inference(modus_ponens,[status(thm)],[172,168]) ).
tff(174,plain,
! [A: $i] :
( ( accept_population(A,atheist,n30)
& accept_population(A,christian,n0)
& accept_population(A,muslim,n65)
& accept_population(A,native,n0)
& accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
inference(skolemize,[status(sab)],[173]) ).
tff(175,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
inference(modus_ponens,[status(thm)],[174,167]) ).
tff(176,plain,
! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) ),
inference(modus_ponens,[status(thm)],[175,165]) ).
tff(177,plain,
( ~ ! [A: $i] :
~ ( ( ~ accept_population(A,atheist,n30)
| ~ accept_population(A,christian,n0)
| ~ accept_population(A,muslim,n65)
| ~ accept_population(A,native,n0)
| ~ accept_population(A,other,n5) )
<=> accept_city(A,townc) )
| ~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) )
<=> accept_city(muslimcountrybhumanitarianorganization,townc) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(178,plain,
~ ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) )
<=> accept_city(muslimcountrybhumanitarianorganization,townc) ),
inference(unit_resolution,[status(thm)],[177,176]) ).
tff(179,plain,
( the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
<=> the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc) ),
inference(rewrite,[status(thm)],[]) ).
tff(180,axiom,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+1.ax',event_104) ).
tff(181,plain,
the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc),
inference(modus_ponens,[status(thm)],[180,179]) ).
tff(182,plain,
^ [A: $i,L: $i,C: $i] :
refl(( ( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
<=> ( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ) )),
inference(bind,[status(th)],[]) ).
tff(183,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ) ),
inference(quant_intro,[status(thm)],[182]) ).
tff(184,plain,
^ [A: $i,L: $i,C: $i] :
rewrite(( ( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) )
<=> ( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ) )),
inference(bind,[status(th)],[]) ).
tff(185,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ) ),
inference(quant_intro,[status(thm)],[184]) ).
tff(186,plain,
( ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(187,plain,
^ [A: $i,L: $i,C: $i] :
rewrite(( ( the_agent_in_all_proposed_teams(A,L,C)
=> ( accept_leader(A,L)
& accept_city(A,C) ) )
<=> ( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ) )),
inference(bind,[status(th)],[]) ).
tff(188,plain,
( ! [A: $i,L: $i,C: $i] :
( the_agent_in_all_proposed_teams(A,L,C)
=> ( accept_leader(A,L)
& accept_city(A,C) ) )
<=> ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ) ),
inference(quant_intro,[status(thm)],[187]) ).
tff(189,axiom,
! [A: $i,L: $i,C: $i] :
( the_agent_in_all_proposed_teams(A,L,C)
=> ( accept_leader(A,L)
& accept_city(A,C) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_4) ).
tff(190,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ),
inference(modus_ponens,[status(thm)],[189,188]) ).
tff(191,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ),
inference(modus_ponens,[status(thm)],[190,186]) ).
tff(192,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ( accept_leader(A,L)
& accept_city(A,C) ) ),
inference(skolemize,[status(sab)],[191]) ).
tff(193,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ),
inference(modus_ponens,[status(thm)],[192,185]) ).
tff(194,plain,
! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) ),
inference(modus_ponens,[status(thm)],[193,183]) ).
tff(195,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(196,plain,
( ( ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,townc) ) )
<=> ( ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(197,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,townc) ) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) ) ),
inference(monotonicity,[status(thm)],[196]) ).
tff(198,plain,
( ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,townc) ) )
<=> ( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) ) ),
inference(transitivity,[status(thm)],[197,195]) ).
tff(199,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization)
| ~ accept_city(muslimcountrybhumanitarianorganization,townc) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(200,plain,
( ~ ! [A: $i,L: $i,C: $i] :
( ~ the_agent_in_all_proposed_teams(A,L,C)
| ~ ( ~ accept_leader(A,L)
| ~ accept_city(A,C) ) )
| ~ the_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization,countryahumanitarianorganization,townc)
| ~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ) ),
inference(modus_ponens,[status(thm)],[199,198]) ).
tff(201,plain,
~ ( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization) ),
inference(unit_resolution,[status(thm)],[200,194,181]) ).
tff(202,plain,
( ~ accept_city(muslimcountrybhumanitarianorganization,townc)
| ~ accept_leader(muslimcountrybhumanitarianorganization,countryahumanitarianorganization)
| accept_city(muslimcountrybhumanitarianorganization,townc) ),
inference(tautology,[status(thm)],[]) ).
tff(203,plain,
accept_city(muslimcountrybhumanitarianorganization,townc),
inference(unit_resolution,[status(thm)],[202,201]) ).
tff(204,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) )
<=> accept_city(muslimcountrybhumanitarianorganization,townc) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) )
| ~ accept_city(muslimcountrybhumanitarianorganization,townc) ),
inference(tautology,[status(thm)],[]) ).
tff(205,plain,
( ( ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) )
<=> accept_city(muslimcountrybhumanitarianorganization,townc) )
| ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) ) ),
inference(unit_resolution,[status(thm)],[204,203]) ).
tff(206,plain,
~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5) ),
inference(unit_resolution,[status(thm)],[205,178]) ).
tff(207,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n30)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n65)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n5)
| accept_population(muslimcountrybhumanitarianorganization,native,n0) ),
inference(tautology,[status(thm)],[]) ).
tff(208,plain,
accept_population(muslimcountrybhumanitarianorganization,native,n0),
inference(unit_resolution,[status(thm)],[207,206]) ).
tff(209,plain,
( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0)
| accept_population(muslimcountrybhumanitarianorganization,atheist,n75) ),
inference(tautology,[status(thm)],[]) ).
tff(210,plain,
accept_population(muslimcountrybhumanitarianorganization,atheist,n75),
inference(unit_resolution,[status(thm)],[209,43]) ).
tff(211,plain,
( ~ ( ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) )
| ~ accept_population(muslimcountrybhumanitarianorganization,atheist,n75)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,muslim,n1)
| ~ accept_population(muslimcountrybhumanitarianorganization,native,n0)
| ~ accept_population(muslimcountrybhumanitarianorganization,other,n0) ),
inference(tautology,[status(thm)],[]) ).
tff(212,plain,
~ accept_population(muslimcountrybhumanitarianorganization,christian,n24),
inference(unit_resolution,[status(thm)],[211,210,208,163,133,103]) ).
tff(213,plain,
^ [A: $i,N: $i,M: $i,P: $i] :
refl(( ( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
<=> ( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
inference(bind,[status(th)],[]) ).
tff(214,plain,
( ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
<=> ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ) ),
inference(quant_intro,[status(thm)],[213]) ).
tff(215,plain,
^ [A: $i,N: $i,M: $i,P: $i] :
trans(monotonicity(trans(monotonicity(rewrite(( ( accept_population(A,P,N)
& less(M,N) )
<=> ~ ( ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
( ~ ( accept_population(A,P,N)
& less(M,N) )
<=> ~ ~ ( ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
rewrite(( ~ ~ ( ~ accept_population(A,P,N)
| ~ less(M,N) )
<=> ( ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
( ~ ( accept_population(A,P,N)
& less(M,N) )
<=> ( ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
( ( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) )
<=> ( ~ accept_population(A,P,N)
| ~ less(M,N)
| accept_population(A,P,M) ) )),
rewrite(( ( ~ accept_population(A,P,N)
| ~ less(M,N)
| accept_population(A,P,M) )
<=> ( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
( ( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) )
<=> ( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ) )),
inference(bind,[status(th)],[]) ).
tff(216,plain,
( ! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) )
<=> ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ) ),
inference(quant_intro,[status(thm)],[215]) ).
tff(217,plain,
( ! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) )
<=> ! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(218,plain,
^ [A: $i,N: $i,M: $i,P: $i] :
rewrite(( ( ( accept_population(A,P,N)
& less(M,N) )
=> accept_population(A,P,M) )
<=> ( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ) )),
inference(bind,[status(th)],[]) ).
tff(219,plain,
( ! [A: $i,N: $i,M: $i,P: $i] :
( ( accept_population(A,P,N)
& less(M,N) )
=> accept_population(A,P,M) )
<=> ! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ) ),
inference(quant_intro,[status(thm)],[218]) ).
tff(220,axiom,
! [A: $i,N: $i,M: $i,P: $i] :
( ( accept_population(A,P,N)
& less(M,N) )
=> accept_population(A,P,M) ),
file('/export/starexec/sandbox2/benchmark/Axioms/AGT001+0.ax',a1_3) ).
tff(221,plain,
! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ),
inference(modus_ponens,[status(thm)],[220,219]) ).
tff(222,plain,
! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ),
inference(modus_ponens,[status(thm)],[221,217]) ).
tff(223,plain,
! [A: $i,N: $i,M: $i,P: $i] :
( ~ ( accept_population(A,P,N)
& less(M,N) )
| accept_population(A,P,M) ),
inference(skolemize,[status(sab)],[222]) ).
tff(224,plain,
! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ),
inference(modus_ponens,[status(thm)],[223,216]) ).
tff(225,plain,
! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) ),
inference(modus_ponens,[status(thm)],[224,214]) ).
tff(226,plain,
( ( ~ ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
| accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ less(n24,n25) )
<=> ( ~ ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
| accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ less(n24,n25) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(227,plain,
( ~ ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
| accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ less(n24,n25) ),
inference(quant_inst,[status(thm)],[]) ).
tff(228,plain,
( ~ ! [A: $i,N: $i,M: $i,P: $i] :
( accept_population(A,P,M)
| ~ accept_population(A,P,N)
| ~ less(M,N) )
| accept_population(muslimcountrybhumanitarianorganization,christian,n24)
| ~ accept_population(muslimcountrybhumanitarianorganization,christian,n25)
| ~ less(n24,n25) ),
inference(modus_ponens,[status(thm)],[227,226]) ).
tff(229,plain,
~ less(n24,n25),
inference(unit_resolution,[status(thm)],[228,225,212,45]) ).
tff(230,plain,
^ [X: $i] :
refl(( ( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
<=> ( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ) )),
inference(bind,[status(th)],[]) ).
tff(231,plain,
( ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
<=> ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ) ),
inference(quant_intro,[status(thm)],[230]) ).
tff(232,plain,
( ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
<=> ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(233,plain,
^ [X: $i] :
rewrite(( ( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) )
<=> ( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ) )),
inference(bind,[status(th)],[]) ).
tff(234,plain,
( ! [X: $i] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) )
<=> ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ) ),
inference(quant_intro,[status(thm)],[233]) ).
tff(235,axiom,
! [X: $i] :
( rdn_non_zero_digit(rdnn(X))
=> rdn_non_zero(rdnn(X)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_non_zero_by_digit) ).
tff(236,plain,
! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(modus_ponens,[status(thm)],[235,234]) ).
tff(237,plain,
! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(modus_ponens,[status(thm)],[236,232]) ).
tff(238,plain,
! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(skolemize,[status(sab)],[237]) ).
tff(239,plain,
! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) ),
inference(modus_ponens,[status(thm)],[238,231]) ).
tff(240,plain,
( rdn_non_zero_digit(rdnn(n2))
<=> rdn_non_zero_digit(rdnn(n2)) ),
inference(rewrite,[status(thm)],[]) ).
tff(241,axiom,
rdn_non_zero_digit(rdnn(n2)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_digit2) ).
tff(242,plain,
rdn_non_zero_digit(rdnn(n2)),
inference(modus_ponens,[status(thm)],[241,240]) ).
tff(243,plain,
( ( ~ ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
| rdn_non_zero(rdnn(n2))
| ~ rdn_non_zero_digit(rdnn(n2)) )
<=> ( ~ ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
| rdn_non_zero(rdnn(n2))
| ~ rdn_non_zero_digit(rdnn(n2)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(244,plain,
( ~ ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
| rdn_non_zero(rdnn(n2))
| ~ rdn_non_zero_digit(rdnn(n2)) ),
inference(quant_inst,[status(thm)],[]) ).
tff(245,plain,
( ~ ! [X: $i] :
( rdn_non_zero(rdnn(X))
| ~ rdn_non_zero_digit(rdnn(X)) )
| rdn_non_zero(rdnn(n2))
| ~ rdn_non_zero_digit(rdnn(n2)) ),
inference(modus_ponens,[status(thm)],[244,243]) ).
tff(246,plain,
rdn_non_zero(rdnn(n2)),
inference(unit_resolution,[status(thm)],[245,242,239]) ).
tff(247,plain,
^ [Ds: $i,O: $i,Db: $i] :
refl(( ( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
<=> ( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
inference(bind,[status(th)],[]) ).
tff(248,plain,
( ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
<=> ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) ),
inference(quant_intro,[status(thm)],[247]) ).
tff(249,plain,
^ [Ds: $i,O: $i,Db: $i] :
trans(monotonicity(trans(monotonicity(rewrite(( ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
<=> ~ ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
<=> ~ ~ ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
rewrite(( ~ ~ ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
<=> ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
<=> ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
( ( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O)
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ) )),
rewrite(( ( ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O)
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
( ( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) )),
inference(bind,[status(th)],[]) ).
tff(250,plain,
( ! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ) ),
inference(quant_intro,[status(thm)],[249]) ).
tff(251,plain,
( ! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(252,plain,
^ [Ds: $i,O: $i,Db: $i] :
rewrite(( ( ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ) )),
inference(bind,[status(th)],[]) ).
tff(253,plain,
( ! [Ds: $i,O: $i,Db: $i] :
( ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) )
<=> ! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ) ),
inference(quant_intro,[status(thm)],[252]) ).
tff(254,axiom,
! [Ds: $i,O: $i,Db: $i] :
( ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
=> rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less_multi_digit_low) ).
tff(255,plain,
! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
inference(modus_ponens,[status(thm)],[254,253]) ).
tff(256,plain,
! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
inference(modus_ponens,[status(thm)],[255,251]) ).
tff(257,plain,
! [Ds: $i,O: $i,Db: $i] :
( ~ ( rdn_positive_less(rdnn(Ds),rdnn(Db))
& rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O)) ),
inference(skolemize,[status(sab)],[256]) ).
tff(258,plain,
! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ),
inference(modus_ponens,[status(thm)],[257,250]) ).
tff(259,plain,
! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) ),
inference(modus_ponens,[status(thm)],[258,248]) ).
tff(260,plain,
( rdn_positive_less(rdnn(n4),rdnn(n5))
<=> rdn_positive_less(rdnn(n4),rdnn(n5)) ),
inference(rewrite,[status(thm)],[]) ).
tff(261,axiom,
rdn_positive_less(rdnn(n4),rdnn(n5)),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',rdn_positive_less45) ).
tff(262,plain,
rdn_positive_less(rdnn(n4),rdnn(n5)),
inference(modus_ponens,[status(thm)],[261,260]) ).
tff(263,plain,
( ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) )
<=> ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(264,plain,
( ( rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2)) )
<=> ( ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(265,plain,
( ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2)) )
<=> ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ) ),
inference(monotonicity,[status(thm)],[264]) ).
tff(266,plain,
( ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2)) )
<=> ( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ) ),
inference(transitivity,[status(thm)],[265,263]) ).
tff(267,plain,
( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2)) ),
inference(quant_inst,[status(thm)],[]) ).
tff(268,plain,
( ~ ! [Ds: $i,O: $i,Db: $i] :
( rdn_positive_less(rdn(rdnn(Ds),O),rdn(rdnn(Db),O))
| ~ rdn_positive_less(rdnn(Ds),rdnn(Db))
| ~ rdn_non_zero(O) )
| ~ rdn_positive_less(rdnn(n4),rdnn(n5))
| ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ),
inference(modus_ponens,[status(thm)],[267,266]) ).
tff(269,plain,
( ~ rdn_non_zero(rdnn(n2))
| rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ),
inference(unit_resolution,[status(thm)],[268,262,259]) ).
tff(270,plain,
rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))),
inference(unit_resolution,[status(thm)],[269,246]) ).
tff(271,plain,
^ [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
refl(( ( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
<=> ( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
inference(bind,[status(th)],[]) ).
tff(272,plain,
( ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
<=> ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) ),
inference(quant_intro,[status(thm)],[271]) ).
tff(273,plain,
^ [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
trans(monotonicity(trans(monotonicity(rewrite(( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
<=> ~ ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
<=> ~ ~ ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
rewrite(( ~ ~ ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
<=> ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
<=> ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
( ( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) )
<=> ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y)
| less(X,Y) ) )),
rewrite(( ( ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y)
| less(X,Y) )
<=> ( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
( ( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) )
<=> ( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) )),
inference(bind,[status(th)],[]) ).
tff(274,plain,
( ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) )
<=> ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ) ),
inference(quant_intro,[status(thm)],[273]) ).
tff(275,plain,
( ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) )
<=> ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(276,plain,
^ [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
trans(monotonicity(rewrite(( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
<=> ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) ) )),
( ( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) )
<=> ( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) ) )),
rewrite(( ( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) )
<=> ( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ) )),
( ( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) )
<=> ( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ) )),
inference(bind,[status(th)],[]) ).
tff(277,plain,
( ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) )
<=> ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ) ),
inference(quant_intro,[status(thm)],[276]) ).
tff(278,axiom,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
=> less(X,Y) ),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+1.ax',less_entry_point_pos_pos) ).
tff(279,plain,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ),
inference(modus_ponens,[status(thm)],[278,277]) ).
tff(280,plain,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ),
inference(modus_ponens,[status(thm)],[279,275]) ).
tff(281,plain,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( ~ ( rdn_translate(X,rdn_pos(RDN_X))
& rdn_translate(Y,rdn_pos(RDN_Y))
& rdn_positive_less(RDN_X,RDN_Y) )
| less(X,Y) ),
inference(skolemize,[status(sab)],[280]) ).
tff(282,plain,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ),
inference(modus_ponens,[status(thm)],[281,274]) ).
tff(283,plain,
! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) ),
inference(modus_ponens,[status(thm)],[282,272]) ).
tff(284,plain,
( rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
<=> rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ),
inference(rewrite,[status(thm)],[]) ).
tff(285,axiom,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn25) ).
tff(286,plain,
rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))),
inference(modus_ponens,[status(thm)],[285,284]) ).
tff(287,plain,
( rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
<=> rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))) ),
inference(rewrite,[status(thm)],[]) ).
tff(288,axiom,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
file('/export/starexec/sandbox2/benchmark/Axioms/NUM005+0.ax',rdn24) ).
tff(289,plain,
rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2)))),
inference(modus_ponens,[status(thm)],[288,287]) ).
tff(290,plain,
( ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) )
<=> ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(291,plain,
( ( less(n24,n25)
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) )
<=> ( less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(292,plain,
( ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) )
<=> ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ) ),
inference(monotonicity,[status(thm)],[291]) ).
tff(293,plain,
( ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) )
<=> ( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ) ),
inference(transitivity,[status(thm)],[292,290]) ).
tff(294,plain,
( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2))))
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2))) ),
inference(quant_inst,[status(thm)],[]) ).
tff(295,plain,
( ~ ! [X: $i,Y: $i,RDN_X: $i,RDN_Y: $i] :
( less(X,Y)
| ~ rdn_translate(X,rdn_pos(RDN_X))
| ~ rdn_translate(Y,rdn_pos(RDN_Y))
| ~ rdn_positive_less(RDN_X,RDN_Y) )
| less(n24,n25)
| ~ rdn_positive_less(rdn(rdnn(n4),rdnn(n2)),rdn(rdnn(n5),rdnn(n2)))
| ~ rdn_translate(n24,rdn_pos(rdn(rdnn(n4),rdnn(n2))))
| ~ rdn_translate(n25,rdn_pos(rdn(rdnn(n5),rdnn(n2)))) ),
inference(modus_ponens,[status(thm)],[294,293]) ).
tff(296,plain,
$false,
inference(unit_resolution,[status(thm)],[295,289,286,283,270,229]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : AGT009+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% 0.03/0.11 % Command : run_E %s %d THM
% 0.11/0.31 % Computer : n006.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu Jun 19 10:42:50 EDT 2025
% 0.11/0.31 % CPUTime :
% 0.85/1.08 % SZS status Theorem
% 0.85/1.08 % SZS output start Proof
% See solution above
% 0.92/1.13 % E exiting
%------------------------------------------------------------------------------