%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : AGT014+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:45:28 AM UTC 2026
% Result : Theorem 8.43s 3.35s
% Output : Refutation 8.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 400
% Syntax : Number of formulae : 802 ( 766 unt; 0 typ; 0 def)
% Number of atoms : 1036 ( 6 equ; 0 cnn)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 2857 ( 19 ~; 3 |; 180 &;2604 @)
% ( 15 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 68 ( 66 usr; 60 con; 0-3 aty)
% Number of variables : 63 ( 0 ^; 54 !; 9 ?; 63 :)
% Comments :
%------------------------------------------------------------------------------
thf(accept_population_decl,type,
accept_population: $i > $i > $i > $o ).
thf(accept_number_decl,type,
accept_number: $i > $i > $o ).
thf(less_decl,type,
less: $i > $i > $o ).
thf(countryamedicalorganization_decl,type,
countryamedicalorganization: $i ).
thf(n3_decl,type,
n3: $i ).
thf(countrybhumanitarianorganization_decl,type,
countrybhumanitarianorganization: $i ).
thf(accept_leader_decl,type,
accept_leader: $i > $i > $o ).
thf(countryahumanitarianorganization_decl,type,
countryahumanitarianorganization: $i ).
thf(countryafirstaidorganization_decl,type,
countryafirstaidorganization: $i ).
thf(sufferterragovernment_decl,type,
sufferterragovernment: $i ).
thf(n4_decl,type,
n4: $i ).
thf(christiancountrychumanitarianorganization_decl,type,
christiancountrychumanitarianorganization: $i ).
thf(accept_city_decl,type,
accept_city: $i > $i > $o ).
thf(coastvillage_decl,type,
coastvillage: $i ).
thf(countryccivilorganization_decl,type,
countryccivilorganization: $i ).
thf(countrybcivilorganization_decl,type,
countrybcivilorganization: $i ).
thf(countryacivilorganization_decl,type,
countryacivilorganization: $i ).
thf(countrycmedicalorganization_decl,type,
countrycmedicalorganization: $i ).
thf(christiansufferterrahumanitarianorganization_decl,type,
christiansufferterrahumanitarianorganization: $i ).
thf(townc_decl,type,
townc: $i ).
thf(muslimcountrybhumanitarianorganization_decl,type,
muslimcountrybhumanitarianorganization: $i ).
thf(atheist_decl,type,
atheist: $i ).
thf(n30_decl,type,
n30: $i ).
thf(christian_decl,type,
christian: $i ).
thf(n0_decl,type,
n0: $i ).
thf(muslim_decl,type,
muslim: $i ).
thf(n65_decl,type,
n65: $i ).
thf(native_decl,type,
native: $i ).
thf(other_decl,type,
other: $i ).
thf(n5_decl,type,
n5: $i ).
thf(towna_decl,type,
towna: $i ).
thf(cityb_decl,type,
cityb: $i ).
thf(n2_decl,type,
n2: $i ).
thf(n1_decl,type,
n1: $i ).
thf(n78_decl,type,
n78: $i ).
thf(n20_decl,type,
n20: $i ).
thf(n75_decl,type,
n75: $i ).
thf(n24_decl,type,
n24: $i ).
thf(sum_decl,type,
sum: $i > $i > $i > $o ).
thf(less_or_equal_decl,type,
less_or_equal: $i > $i > $o ).
thf(n12_decl,type,
n12: $i ).
thf(n85_decl,type,
n85: $i ).
thf(n100_decl,type,
n100: $i ).
thf(sunsetpoint_decl,type,
sunsetpoint: $i ).
thf(n68_decl,type,
n68: $i ).
thf(n16_decl,type,
n16: $i ).
thf(n11_decl,type,
n11: $i ).
thf(stjosephburgh_decl,type,
stjosephburgh: $i ).
thf(n25_decl,type,
n25: $i ).
thf(citya_decl,type,
citya: $i ).
thf(n70_decl,type,
n70: $i ).
thf(n15_decl,type,
n15: $i ).
thf(n10_decl,type,
n10: $i ).
thf(centrallakecity_decl,type,
centrallakecity: $i ).
thf(n7_decl,type,
n7: $i ).
thf(suffertown_decl,type,
suffertown: $i ).
thf(n8_decl,type,
n8: $i ).
thf(townb_decl,type,
townb: $i ).
thf(n60_decl,type,
n60: $i ).
thf(sunnysideport_decl,type,
sunnysideport: $i ).
thf(n13_decl,type,
n13: $i ).
thf(northport_decl,type,
northport: $i ).
thf(n54_decl,type,
n54: $i ).
thf(n23_decl,type,
n23: $i ).
thf(n9_decl,type,
n9: $i ).
thf(centraltown_decl,type,
centraltown: $i ).
thf(291,axiom,
n0 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_76) ).
thf(809,plain,
n0 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[291]) ).
thf(268,axiom,
n20 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_10) ).
thf(760,plain,
n20 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[268]) ).
thf(50,axiom,
townc @ ( christiancountrychumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_7) ).
thf(479,plain,
townc @ ( christiancountrychumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(302,axiom,
n75 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_276) ).
thf(846,plain,
n75 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[302]) ).
thf(323,axiom,
n0 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_85) ).
thf(893,plain,
n0 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[323]) ).
thf(79,axiom,
! [A: $i] :
( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n24 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( towna @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_9) ).
thf(518,plain,
! [A: $i] :
( ( ( towna @ ( A @ accept_city ) )
=> ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n24 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n24 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( towna @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(379,axiom,
n24 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_287) ).
thf(962,plain,
n24 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[379]) ).
thf(102,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( n1 @ ( A @ sum ) ) ) )
=> ( A @ ( C @ less_or_equal ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_successor) ).
thf(555,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( n1 @ ( A @ sum ) ) ) )
=> ( A @ ( C @ less_or_equal ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(188,axiom,
n4 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_334) ).
thf(666,plain,
n4 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(52,axiom,
n5 @ ( countryamedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_215) ).
thf(481,plain,
n5 @ ( countryamedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(167,axiom,
countryahumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_19) ).
thf(645,plain,
countryahumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(322,axiom,
n85 @ ( native @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_86) ).
thf(892,plain,
n85 @ ( native @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[322]) ).
thf(339,axiom,
n78 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_174) ).
thf(909,plain,
n78 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[339]) ).
thf(159,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less_or_equal ) )
<=> ( ( A = B )
| ( B @ ( A @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_or_equal) ).
thf(628,plain,
! [A: $i,B: $i] :
( ( ( ( A = B )
| ( B @ ( A @ less ) ) )
=> ( B @ ( A @ less_or_equal ) ) )
& ( ( B @ ( A @ less_or_equal ) )
=> ( ( A = B )
| ( B @ ( A @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(205,axiom,
coastvillage @ ( countryahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_27) ).
thf(683,plain,
coastvillage @ ( countryahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[205]) ).
thf(398,axiom,
n78 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_61) ).
thf(994,plain,
n78 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[398]) ).
thf(250,axiom,
n24 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_263) ).
thf(741,plain,
n24 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[250]) ).
thf(33,axiom,
muslimcountrybhumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_123) ).
thf(449,plain,
muslimcountrybhumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(129,axiom,
sufferterragovernment @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_301) ).
thf(597,plain,
sufferterragovernment @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(317,axiom,
n65 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_45) ).
thf(861,plain,
n65 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[317]) ).
thf(5,axiom,
n3 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_335) ).
thf(408,plain,
n3 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(381,axiom,
n1 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_170) ).
thf(977,plain,
n1 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[381]) ).
thf(115,axiom,
countryahumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_8) ).
thf(582,plain,
countryahumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(270,axiom,
n0 @ ( native @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_135) ).
thf(762,plain,
n0 @ ( native @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[270]) ).
thf(321,axiom,
! [A: $i] :
( ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n60 @ ( muslim @ ( A @ accept_population ) ) )
& ( n8 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( sunnysideport @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_3) ).
thf(878,plain,
! [A: $i] :
( ( ( sunnysideport @ ( A @ accept_city ) )
=> ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n60 @ ( muslim @ ( A @ accept_population ) ) )
& ( n8 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n60 @ ( muslim @ ( A @ accept_population ) ) )
& ( n8 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( sunnysideport @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[321]) ).
thf(24,axiom,
n3 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_310) ).
thf(440,plain,
n3 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(177,axiom,
cityb @ ( countryamedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_213) ).
thf(655,plain,
cityb @ ( countryamedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(146,axiom,
~ ( towna @ ( muslimcountrybhumanitarianorganization @ accept_city ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_366) ).
thf(614,plain,
~ ( towna @ ( muslimcountrybhumanitarianorganization @ accept_city ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(199,axiom,
towna @ ( countryacivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_320) ).
thf(677,plain,
towna @ ( countryacivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[199]) ).
thf(81,axiom,
countrycmedicalorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_340) ).
thf(533,plain,
countrycmedicalorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(97,axiom,
countryahumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_129) ).
thf(550,plain,
countryahumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(70,axiom,
countryccivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_130) ).
thf(500,plain,
countryccivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(237,axiom,
n30 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_108) ).
thf(715,plain,
n30 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[237]) ).
thf(220,axiom,
n3 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_204) ).
thf(698,plain,
n3 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[220]) ).
thf(86,axiom,
coastvillage @ ( sufferterragovernment @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_147) ).
thf(538,plain,
coastvillage @ ( sufferterragovernment @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(360,axiom,
n30 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_199) ).
thf(930,plain,
n30 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[360]) ).
thf(192,axiom,
n5 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_267) ).
thf(670,plain,
n5 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(256,axiom,
n20 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_229) ).
thf(747,plain,
n20 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[256]) ).
thf(343,axiom,
n1 @ ( other @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_234) ).
thf(913,plain,
n1 @ ( other @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[343]) ).
thf(328,axiom,
n5 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_15) ).
thf(898,plain,
n5 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[328]) ).
thf(231,axiom,
n85 @ ( native @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_99) ).
thf(709,plain,
n85 @ ( native @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[231]) ).
thf(20,axiom,
n5 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_302) ).
thf(436,plain,
n5 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(173,axiom,
coastvillage @ ( countryafirstaidorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_103) ).
thf(651,plain,
coastvillage @ ( countryafirstaidorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(297,axiom,
n65 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_150) ).
thf(841,plain,
n65 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[297]) ).
thf(14,axiom,
christiancountrychumanitarianorganization @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_28) ).
thf(417,plain,
christiancountrychumanitarianorganization @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(246,axiom,
n85 @ ( native @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_118) ).
thf(724,plain,
n85 @ ( native @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[246]) ).
thf(241,axiom,
n0 @ ( native @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_273) ).
thf(719,plain,
n0 @ ( native @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[241]) ).
thf(74,axiom,
christiancountrychumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_14) ).
thf(504,plain,
christiancountrychumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(364,axiom,
n5 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_105) ).
thf(934,plain,
n5 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[364]) ).
thf(150,axiom,
n4 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_240) ).
thf(619,plain,
n4 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(294,axiom,
n1 @ ( muslim @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_349) ).
thf(838,plain,
n1 @ ( muslim @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[294]) ).
thf(347,axiom,
n78 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_114) ).
thf(917,plain,
n78 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[347]) ).
thf(224,axiom,
n20 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_51) ).
thf(702,plain,
n20 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[224]) ).
thf(260,axiom,
n5 @ ( other @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_177) ).
thf(751,plain,
n5 @ ( other @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[260]) ).
thf(90,axiom,
n4 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_165) ).
thf(542,plain,
n4 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(44,axiom,
countrybcivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_332) ).
thf(460,plain,
countrybcivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(332,axiom,
n0 @ ( other @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_313) ).
thf(902,plain,
n0 @ ( other @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[332]) ).
thf(18,axiom,
! [A: $i] :
( ( ( n5 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n65 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( townc @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_13) ).
thf(421,plain,
! [A: $i] :
( ( ( townc @ ( A @ accept_city ) )
=> ( ( n5 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n65 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n5 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n65 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n30 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( townc @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(138,axiom,
countryahumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_109) ).
thf(606,plain,
countryahumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(278,axiom,
n20 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_235) ).
thf(770,plain,
n20 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[278]) ).
thf(13,axiom,
countryccivilorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_280) ).
thf(416,plain,
countryccivilorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(32,axiom,
n2 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_214) ).
thf(448,plain,
n2 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(160,axiom,
countryacivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_92) ).
thf(638,plain,
countryacivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(309,axiom,
n1 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_190) ).
thf(853,plain,
n1 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[309]) ).
thf(354,axiom,
n0 @ ( native @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_171) ).
thf(924,plain,
n0 @ ( native @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[354]) ).
thf(62,axiom,
townc @ ( countryafirstaidorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_110) ).
thf(492,plain,
townc @ ( countryafirstaidorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(265,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( D @ ( A @ accept_population ) ) ) )
=> ( C @ ( D @ ( A @ accept_population ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_3) ).
thf(756,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( D @ ( A @ accept_population ) ) ) )
=> ( C @ ( D @ ( A @ accept_population ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[265]) ).
thf(123,axiom,
n1 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_345) ).
thf(591,plain,
n1 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(27,axiom,
n2 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_363) ).
thf(443,plain,
n2 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(154,axiom,
countryccivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_155) ).
thf(623,plain,
countryccivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(168,axiom,
n1 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_21) ).
thf(646,plain,
n1 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(55,axiom,
n4 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_327) ).
thf(485,plain,
n4 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(367,axiom,
n5 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_184) ).
thf(937,plain,
n5 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[367]) ).
thf(107,axiom,
townc @ ( countryacivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_79) ).
thf(574,plain,
townc @ ( countryacivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(335,axiom,
n3 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_25) ).
thf(905,plain,
n3 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[335]) ).
thf(51,axiom,
n2 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_322) ).
thf(480,plain,
n2 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(209,axiom,
countryahumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_201) ).
thf(687,plain,
countryahumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[209]) ).
thf(373,axiom,
n0 @ ( native @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_254) ).
thf(956,plain,
n0 @ ( native @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[373]) ).
thf(37,axiom,
towna @ ( sufferterragovernment @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_57) ).
thf(453,plain,
towna @ ( sufferterragovernment @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(282,axiom,
n0 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_5) ).
thf(774,plain,
n0 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[282]) ).
thf(182,axiom,
n1 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_337) ).
thf(660,plain,
n1 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(305,axiom,
n65 @ ( muslim @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_16) ).
thf(849,plain,
n65 @ ( muslim @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[305]) ).
thf(134,axiom,
countryacivilorganization @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_233) ).
thf(602,plain,
countryacivilorganization @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(385,axiom,
n78 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_257) ).
thf(981,plain,
n78 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[385]) ).
thf(274,axiom,
n0 @ ( native @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_348) ).
thf(766,plain,
n0 @ ( native @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[274]) ).
thf(320,axiom,
n78 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_230) ).
thf(877,plain,
n78 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[320]) ).
thf(214,axiom,
towna @ ( countrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_139) ).
thf(692,plain,
towna @ ( countrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[214]) ).
thf(8,axiom,
christiancountrychumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_148) ).
thf(411,plain,
christiancountrychumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(392,axiom,
n1 @ ( other @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_59) ).
thf(988,plain,
n1 @ ( other @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[392]) ).
thf(36,axiom,
coastvillage @ ( countrybcivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_42) ).
thf(452,plain,
coastvillage @ ( countrybcivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(350,axiom,
n0 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_186) ).
thf(920,plain,
n0 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[350]) ).
thf(23,axiom,
countrybhumanitarianorganization @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_238) ).
thf(439,plain,
countrybhumanitarianorganization @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(200,axiom,
muslimcountrybhumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_43) ).
thf(678,plain,
muslimcountrybhumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[200]) ).
thf(183,axiom,
christiancountrychumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_132) ).
thf(661,plain,
christiancountrychumanitarianorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
thf(355,axiom,
n24 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_247) ).
thf(925,plain,
n24 @ ( christian @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[355]) ).
thf(269,axiom,
n85 @ ( native @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_23) ).
thf(761,plain,
n85 @ ( native @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[269]) ).
thf(292,axiom,
! [A: $i] :
( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n10 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n15 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( centrallakecity @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_4) ).
thf(810,plain,
! [A: $i] :
( ( ( centrallakecity @ ( A @ accept_city ) )
=> ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n10 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n15 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n10 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n15 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( centrallakecity @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[292]) ).
thf(82,axiom,
muslimcountrybhumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_2) ).
thf(534,plain,
muslimcountrybhumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(236,axiom,
n1 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_9) ).
thf(714,plain,
n1 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[236]) ).
thf(94,axiom,
~ ( sufferterragovernment @ ( christiansufferterrahumanitarianorganization @ accept_leader ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_82) ).
thf(546,plain,
~ ( sufferterragovernment @ ( christiansufferterrahumanitarianorganization @ accept_leader ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(288,axiom,
n0 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_95) ).
thf(793,plain,
n0 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[288]) ).
thf(340,axiom,
n65 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_106) ).
thf(910,plain,
n65 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[340]) ).
thf(255,axiom,
n0 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_284) ).
thf(746,plain,
n0 @ ( other @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[255]) ).
thf(318,axiom,
n3 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_70) ).
thf(862,plain,
n3 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[318]) ).
thf(130,axiom,
countryacivilorganization @ ( countryamedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_209) ).
thf(598,plain,
countryacivilorganization @ ( countryamedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(374,axiom,
n65 @ ( muslim @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_178) ).
thf(957,plain,
n65 @ ( muslim @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[374]) ).
thf(324,axiom,
n0 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_159) ).
thf(894,plain,
n0 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[324]) ).
thf(4,axiom,
n3 @ ( countryamedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_217) ).
thf(407,plain,
n3 @ ( countryamedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(215,axiom,
sufferterragovernment @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_250) ).
thf(693,plain,
sufferterragovernment @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[215]) ).
thf(346,axiom,
n1 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_204) ).
thf(916,plain,
n1 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[346]) ).
thf(303,axiom,
n65 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_158) ).
thf(847,plain,
n65 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[303]) ).
thf(156,axiom,
n5 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_239) ).
thf(625,plain,
n5 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(187,axiom,
n4 @ ( countryamedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_216) ).
thf(665,plain,
n4 @ ( countryamedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(116,axiom,
countryacivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_117) ).
thf(583,plain,
countryacivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(45,axiom,
townc @ ( countryamedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_20) ).
thf(461,plain,
townc @ ( countryamedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(63,axiom,
n2 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_344) ).
thf(493,plain,
n2 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(204,axiom,
countryahumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_78) ).
thf(682,plain,
countryahumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[204]) ).
thf(98,axiom,
n3 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_304) ).
thf(551,plain,
n3 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(232,axiom,
n0 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_220) ).
thf(710,plain,
n0 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[232]) ).
thf(308,axiom,
n24 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_223) ).
thf(852,plain,
n24 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[308]) ).
thf(19,axiom,
countrybhumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_259) ).
thf(435,plain,
countrybhumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(40,axiom,
n1 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_306) ).
thf(456,plain,
n1 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(298,axiom,
n0 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_119) ).
thf(842,plain,
n0 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[298]) ).
thf(219,axiom,
n4 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_342) ).
thf(697,plain,
n4 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[219]) ).
thf(172,axiom,
n2 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_336) ).
thf(650,plain,
n2 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(247,axiom,
! [A: $i] :
( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n100 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n0 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( sunsetpoint @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_8) ).
thf(725,plain,
! [A: $i] :
( ( ( sunsetpoint @ ( A @ accept_city ) )
=> ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n100 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n0 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n100 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n0 @ ( christian @ ( A @ accept_population ) ) )
& ( n0 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( sunsetpoint @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[247]) ).
thf(384,axiom,
n20 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_60) ).
thf(980,plain,
n20 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[384]) ).
thf(125,axiom,
countryacivilorganization @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_111) ).
thf(593,plain,
countryacivilorganization @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(142,axiom,
sufferterragovernment @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_278) ).
thf(610,plain,
sufferterragovernment @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(17,axiom,
muslimcountrybhumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_183) ).
thf(420,plain,
muslimcountrybhumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(69,axiom,
n2 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_197) ).
thf(499,plain,
n2 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(393,axiom,
n0 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_46) ).
thf(989,plain,
n0 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[393]) ).
thf(313,axiom,
n0 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_272) ).
thf(857,plain,
n0 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[313]) ).
thf(251,axiom,
n5 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_3) ).
thf(742,plain,
n5 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[251]) ).
thf(111,axiom,
n3 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_98) ).
thf(578,plain,
n3 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(58,axiom,
n1 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_271) ).
thf(488,plain,
n1 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(363,axiom,
n75 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_317) ).
thf(933,plain,
n75 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[363]) ).
thf(85,axiom,
townc @ ( muslimcountrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_200) ).
thf(537,plain,
townc @ ( muslimcountrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(191,axiom,
n3 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_227) ).
thf(669,plain,
n3 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(164,axiom,
n2 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_59) ).
thf(642,plain,
n2 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(59,axiom,
countryafirstaidorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_141) ).
thf(489,plain,
countryafirstaidorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(122,axiom,
n2 @ ( countryamedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_218) ).
thf(590,plain,
n2 @ ( countryamedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(201,axiom,
n4 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_268) ).
thf(679,plain,
n4 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[201]) ).
thf(228,axiom,
n30 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_152) ).
thf(706,plain,
n30 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[228]) ).
thf(101,axiom,
n1 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_358) ).
thf(554,plain,
n1 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(262,axiom,
n3 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_101) ).
thf(753,plain,
n3 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[262]) ).
thf(331,axiom,
n1 @ ( other @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_253) ).
thf(901,plain,
n1 @ ( other @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[331]) ).
thf(208,axiom,
n2 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_226) ).
thf(686,plain,
n2 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[208]) ).
thf(153,axiom,
sufferterragovernment @ ( countryamedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_226) ).
thf(622,plain,
sufferterragovernment @ ( countryamedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(389,axiom,
n0 @ ( muslim @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_24) ).
thf(985,plain,
n0 @ ( muslim @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[389]) ).
thf(223,axiom,
n75 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_56) ).
thf(701,plain,
n75 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[223]) ).
thf(76,axiom,
towna @ ( countrycmedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_289) ).
thf(515,plain,
towna @ ( countrycmedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(176,axiom,
countrybhumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_292) ).
thf(654,plain,
countrybhumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(41,axiom,
christiancountrychumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_91) ).
thf(457,plain,
christiancountrychumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(243,axiom,
n85 @ ( native @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_32) ).
thf(721,plain,
n85 @ ( native @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[243]) ).
thf(169,axiom,
countryahumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_161) ).
thf(647,plain,
countryahumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(401,axiom,
n65 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_75) ).
thf(997,plain,
n65 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[401]) ).
thf(388,axiom,
n0 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_126) ).
thf(984,plain,
n0 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[388]) ).
thf(341,axiom,
n5 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_196) ).
thf(911,plain,
n5 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[341]) ).
thf(73,axiom,
countrybhumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_232) ).
thf(503,plain,
countrybhumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(137,axiom,
n5 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_171) ).
thf(605,plain,
n5 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(287,axiom,
n75 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_138) ).
thf(792,plain,
n75 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[287]) ).
thf(368,axiom,
n0 @ ( native @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_261) ).
thf(938,plain,
n0 @ ( native @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[368]) ).
thf(351,axiom,
n24 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_137) ).
thf(921,plain,
n24 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[351]) ).
thf(89,axiom,
cityb @ ( countryahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_237) ).
thf(541,plain,
cityb @ ( countryahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(179,axiom,
n4 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_324) ).
thf(657,plain,
n4 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(273,axiom,
n75 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_224) ).
thf(765,plain,
n75 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[273]) ).
thf(196,axiom,
n2 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_167) ).
thf(674,plain,
n2 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[196]) ).
thf(370,axiom,
n20 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_173) ).
thf(953,plain,
n20 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[370]) ).
thf(356,axiom,
n0 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_87) ).
thf(926,plain,
n0 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[356]) ).
thf(281,axiom,
n0 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_198) ).
thf(773,plain,
n0 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[281]) ).
thf(289,axiom,
n0 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_69) ).
thf(794,plain,
n0 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[289]) ).
thf(119,axiom,
~ ( n5 @ ( countryccivilorganization @ accept_number ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_58) ).
thf(586,plain,
~ ( n5 @ ( countryccivilorganization @ accept_number ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(184,axiom,
n2 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_203) ).
thf(662,plain,
n2 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(240,axiom,
n30 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_18) ).
thf(718,plain,
n30 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[240]) ).
thf(336,axiom,
n1 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_210) ).
thf(906,plain,
n1 @ ( other @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[336]) ).
thf(9,axiom,
coastvillage @ ( countrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_122) ).
thf(412,plain,
coastvillage @ ( countrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(259,axiom,
n0 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_100) ).
thf(750,plain,
n0 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[259]) ).
thf(149,axiom,
n2 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_211) ).
thf(618,plain,
n2 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(293,axiom,
! [A: $i] :
( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n4 @ ( native @ ( A @ accept_population ) ) )
& ( n7 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n65 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( suffertown @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_1) ).
thf(824,plain,
! [A: $i] :
( ( ( suffertown @ ( A @ accept_city ) )
=> ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n4 @ ( native @ ( A @ accept_population ) ) )
& ( n7 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n65 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n4 @ ( native @ ( A @ accept_population ) ) )
& ( n7 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n65 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( suffertown @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[293]) ).
thf(312,axiom,
n30 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_180) ).
thf(856,plain,
n30 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[312]) ).
thf(254,axiom,
n0 @ ( native @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_203) ).
thf(745,plain,
n0 @ ( native @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[254]) ).
thf(106,axiom,
sufferterragovernment @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_353) ).
thf(573,plain,
sufferterragovernment @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(211,axiom,
n5 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_222) ).
thf(689,plain,
n5 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[211]) ).
thf(28,axiom,
christiancountrychumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_73) ).
thf(444,plain,
christiancountrychumanitarianorganization @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(133,axiom,
cityb @ ( countrybcivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_53) ).
thf(601,plain,
cityb @ ( countrybcivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(117,axiom,
countrybhumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_207) ).
thf(584,plain,
countrybhumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(334,axiom,
n0 @ ( other @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_244) ).
thf(904,plain,
n0 @ ( other @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[334]) ).
thf(216,axiom,
towna @ ( countryamedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_227) ).
thf(694,plain,
towna @ ( countryamedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[216]) ).
thf(1,conjecture,
? [A: $i,B: $i,C: $i] :
~ ( C @ ( B @ ( A @ accept_population ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query_14) ).
thf(2,negated_conjecture,
~ ? [A: $i,B: $i,C: $i] :
~ ( C @ ( B @ ( A @ accept_population ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(402,plain,
~ ? [A: $i,B: $i,C: $i] :
~ ( C @ ( B @ ( A @ accept_population ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(299,axiom,
n12 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_97) ).
thf(843,plain,
n12 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[299]) ).
thf(280,axiom,
n30 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_6) ).
thf(772,plain,
n30 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[280]) ).
thf(252,axiom,
n1 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_112) ).
thf(743,plain,
n1 @ ( other @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[252]) ).
thf(112,axiom,
n3 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_343) ).
thf(579,plain,
n3 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(375,axiom,
n30 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_77) ).
thf(958,plain,
n30 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[375]) ).
thf(93,axiom,
sufferterragovernment @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_140) ).
thf(545,plain,
sufferterragovernment @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(10,axiom,
n3 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_215) ).
thf(413,plain,
n3 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(110,axiom,
n1 @ ( countryamedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_219) ).
thf(577,plain,
n1 @ ( countryamedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(233,axiom,
n65 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_125) ).
thf(711,plain,
n65 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[233]) ).
thf(163,axiom,
sufferterragovernment @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_367) ).
thf(641,plain,
sufferterragovernment @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(105,axiom,
n3 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_362) ).
thf(572,plain,
n3 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(143,axiom,
sufferterragovernment @ ( countryccivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_266) ).
thf(611,plain,
sufferterragovernment @ ( countryccivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(349,axiom,
n78 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_206) ).
thf(919,plain,
n78 @ ( atheist @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[349]) ).
thf(226,axiom,
n85 @ ( native @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_143) ).
thf(704,plain,
n85 @ ( native @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[226]) ).
thf(88,axiom,
n2 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_192) ).
thf(540,plain,
n2 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(194,axiom,
n3 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_166) ).
thf(672,plain,
n3 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[194]) ).
thf(29,axiom,
countrybhumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_339) ).
thf(445,plain,
countrybhumanitarianorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(366,axiom,
n3 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_88) ).
thf(936,plain,
n3 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[366]) ).
thf(235,axiom,
n78 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_52) ).
thf(713,plain,
n78 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[235]) ).
thf(68,axiom,
n3 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_234) ).
thf(498,plain,
n3 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(330,axiom,
n1 @ ( other @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_228) ).
thf(900,plain,
n1 @ ( other @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[330]) ).
thf(203,axiom,
countrybhumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_176) ).
thf(681,plain,
countrybhumanitarianorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[203]) ).
thf(16,axiom,
townc @ ( christiansufferterrahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_162) ).
thf(419,plain,
townc @ ( christiansufferterrahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(35,axiom,
towna @ ( countryafirstaidorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_279) ).
thf(451,plain,
towna @ ( countryafirstaidorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(171,axiom,
n2 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_28) ).
thf(649,plain,
n2 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(147,axiom,
cityb @ ( sufferterragovernment @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_258) ).
thf(616,plain,
cityb @ ( sufferterragovernment @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(131,axiom,
n1 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_330) ).
thf(599,plain,
n1 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(319,axiom,
! [A: $i] :
( ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n8 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( townb @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_11) ).
thf(863,plain,
! [A: $i] :
( ( ( townb @ ( A @ accept_city ) )
=> ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n8 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n8 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( townb @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[319]) ).
thf(272,axiom,
n65 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_185) ).
thf(764,plain,
n65 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[272]) ).
thf(383,axiom,
n5 @ ( other @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_74) ).
thf(979,plain,
n5 @ ( other @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[383]) ).
thf(136,axiom,
n2 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_242) ).
thf(604,plain,
n2 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(394,axiom,
n0 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_179) ).
thf(990,plain,
n0 @ ( christian @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[394]) ).
thf(400,axiom,
n5 @ ( other @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_124) ).
thf(996,plain,
n5 @ ( other @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[400]) ).
thf(48,axiom,
n3 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_269) ).
thf(477,plain,
n3 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(64,axiom,
n2 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_183) ).
thf(494,plain,
n2 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(266,axiom,
n5 @ ( other @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_149) ).
thf(758,plain,
n5 @ ( other @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[266]) ).
thf(83,axiom,
countryacivilorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_31) ).
thf(535,plain,
countryacivilorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(141,axiom,
countrybcivilorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_281) ).
thf(609,plain,
countrybcivilorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(126,axiom,
towna @ ( countryccivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_265) ).
thf(594,plain,
towna @ ( countryccivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(152,axiom,
n5 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_308) ).
thf(621,plain,
n5 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(54,axiom,
~ ( coastvillage @ ( countryamedicalorganization @ accept_city ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_13) ).
thf(483,plain,
~ ( coastvillage @ ( countryamedicalorganization @ accept_city ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(325,axiom,
n1 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_297) ).
thf(895,plain,
n1 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[325]) ).
thf(277,axiom,
n85 @ ( native @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_38) ).
thf(769,plain,
n85 @ ( native @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[277]) ).
thf(190,axiom,
n2 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_65) ).
thf(668,plain,
n2 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(314,axiom,
n12 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_71) ).
thf(858,plain,
n12 @ ( atheist @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[314]) ).
thf(99,axiom,
christiancountrychumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_283) ).
thf(552,plain,
christiancountrychumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(304,axiom,
n24 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_80) ).
thf(848,plain,
n24 @ ( christian @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[304]) ).
thf(222,axiom,
n12 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_146) ).
thf(700,plain,
n12 @ ( atheist @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[222]) ).
thf(157,axiom,
n4 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_17) ).
thf(626,plain,
n4 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(345,axiom,
n12 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_35) ).
thf(915,plain,
n12 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[345]) ).
thf(46,axiom,
n1 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_364) ).
thf(462,plain,
n1 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(362,axiom,
n65 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_197) ).
thf(932,plain,
n65 @ ( muslim @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[362]) ).
thf(387,axiom,
n24 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_350) ).
thf(983,plain,
n24 @ ( christian @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[387]) ).
thf(376,axiom,
n5 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_157) ).
thf(959,plain,
n5 @ ( other @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[376]) ).
thf(276,axiom,
n85 @ ( native @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_94) ).
thf(768,plain,
n85 @ ( native @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[276]) ).
thf(217,axiom,
countryahumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_49) ).
thf(695,plain,
countryahumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[217]) ).
thf(39,axiom,
countryahumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_189) ).
thf(455,plain,
countryahumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(140,axiom,
townc @ ( countrycmedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_188) ).
thf(608,plain,
townc @ ( countrycmedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(390,axiom,
n1 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_172) ).
thf(986,plain,
n1 @ ( muslim @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[390]) ).
thf(307,axiom,
n85 @ ( native @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_68) ).
thf(851,plain,
n85 @ ( native @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[307]) ).
thf(175,axiom,
cityb @ ( christiansufferterrahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_175) ).
thf(653,plain,
cityb @ ( christiansufferterrahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(352,axiom,
n24 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_275) ).
thf(922,plain,
n24 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[352]) ).
thf(180,axiom,
townc @ ( sufferterragovernment @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_154) ).
thf(658,plain,
townc @ ( sufferterragovernment @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(342,axiom,
n0 @ ( other @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_134) ).
thf(912,plain,
n0 @ ( other @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[342]) ).
thf(207,axiom,
countryacivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_1) ).
thf(685,plain,
countryacivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[207]) ).
thf(75,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ less ) )
<=> ( ( B != A )
& ~ ( A @ ( B @ less ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less_property) ).
thf(505,plain,
! [A: $i,B: $i] :
( ( ( ( B != A )
& ~ ( A @ ( B @ less ) ) )
=> ( B @ ( A @ less ) ) )
& ( ( B @ ( A @ less ) )
=> ( ( B != A )
& ~ ( A @ ( B @ less ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(22,axiom,
towna @ ( countryahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_251) ).
thf(438,plain,
towna @ ( countryahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(244,axiom,
n78 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_192) ).
thf(722,plain,
n78 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[244]) ).
thf(121,axiom,
countryccivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_325) ).
thf(589,plain,
countryccivilorganization @ ( christiancountrychumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(357,axiom,
n0 @ ( native @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_296) ).
thf(927,plain,
n0 @ ( native @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[357]) ).
thf(258,axiom,
n0 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_17) ).
thf(749,plain,
n0 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[258]) ).
thf(369,axiom,
! [A: $i] :
( ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n15 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n13 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( northport @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_6) ).
thf(939,plain,
! [A: $i] :
( ( ( northport @ ( A @ accept_city ) )
=> ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n15 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n13 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n2 @ ( other @ ( A @ accept_population ) ) )
& ( n15 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n13 @ ( christian @ ( A @ accept_population ) ) )
& ( n70 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( northport @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[369]) ).
thf(263,axiom,
n12 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_26) ).
thf(754,plain,
n12 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[263]) ).
thf(100,axiom,
cityb @ ( countryccivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_64) ).
thf(553,plain,
cityb @ ( countryccivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(42,axiom,
n1 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_323) ).
thf(458,plain,
n1 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(60,axiom,
n3 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_241) ).
thf(490,plain,
n3 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(197,axiom,
townc @ ( countryccivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_181) ).
thf(675,plain,
townc @ ( countryccivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[197]) ).
thf(290,axiom,
! [A: $i] :
( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n25 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( citya @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_10) ).
thf(795,plain,
! [A: $i] :
( ( ( citya @ ( A @ accept_city ) )
=> ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n25 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n25 @ ( christian @ ( A @ accept_population ) ) )
& ( n75 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( citya @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[290]) ).
thf(202,axiom,
cityb @ ( countrycmedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_193) ).
thf(680,plain,
cityb @ ( countrycmedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[202]) ).
thf(185,axiom,
n4 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_361) ).
thf(663,plain,
n4 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(95,axiom,
countrybhumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_116) ).
thf(548,plain,
countrybhumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(170,axiom,
n5 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_73) ).
thf(648,plain,
n5 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(57,axiom,
countrybhumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_282) ).
thf(487,plain,
countrybhumanitarianorganization @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(148,axiom,
n2 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_88) ).
thf(617,plain,
n2 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(77,axiom,
n4 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_235) ).
thf(516,plain,
n4 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(284,axiom,
! [A: $i] :
( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n11 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n16 @ ( christian @ ( A @ accept_population ) ) )
& ( n68 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( stjosephburgh @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_5) ).
thf(776,plain,
! [A: $i] :
( ( ( stjosephburgh @ ( A @ accept_city ) )
=> ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n11 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n16 @ ( christian @ ( A @ accept_population ) ) )
& ( n68 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n4 @ ( other @ ( A @ accept_population ) ) )
& ( n11 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n16 @ ( christian @ ( A @ accept_population ) ) )
& ( n68 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( stjosephburgh @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[284]) ).
thf(212,axiom,
n1 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_243) ).
thf(690,plain,
n1 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[212]) ).
thf(162,axiom,
christiancountrychumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_195) ).
thf(640,plain,
christiancountrychumanitarianorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(227,axiom,
n0 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_144) ).
thf(705,plain,
n0 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[227]) ).
thf(229,axiom,
n12 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_102) ).
thf(707,plain,
n12 @ ( atheist @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[229]) ).
thf(11,axiom,
countryahumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_153) ).
thf(414,plain,
countryahumanitarianorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(371,axiom,
n5 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_44) ).
thf(954,plain,
n5 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[371]) ).
thf(248,axiom,
n20 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_191) ).
thf(739,plain,
n20 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[248]) ).
thf(6,axiom,
countryafirstaidorganization @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_22) ).
thf(409,plain,
countryafirstaidorganization @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(397,axiom,
n3 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_120) ).
thf(993,plain,
n3 @ ( christian @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[397]) ).
thf(234,axiom,
n0 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_39) ).
thf(712,plain,
n0 @ ( muslim @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[234]) ).
thf(103,axiom,
! [A: $i] :
( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n85 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n3 @ ( christian @ ( A @ accept_population ) ) )
& ( n12 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( coastvillage @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_7) ).
thf(557,plain,
! [A: $i] :
( ( ( coastvillage @ ( A @ accept_city ) )
=> ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n85 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n3 @ ( christian @ ( A @ accept_population ) ) )
& ( n12 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n0 @ ( other @ ( A @ accept_population ) ) )
& ( n85 @ ( native @ ( A @ accept_population ) ) )
& ( n0 @ ( muslim @ ( A @ accept_population ) ) )
& ( n3 @ ( christian @ ( A @ accept_population ) ) )
& ( n12 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( coastvillage @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(113,axiom,
countryacivilorganization @ ( countryccivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_65) ).
thf(580,plain,
countryacivilorganization @ ( countryccivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(311,axiom,
n75 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_248) ).
thf(855,plain,
n75 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[311]) ).
thf(195,axiom,
n2 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_357) ).
thf(673,plain,
n2 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(286,axiom,
n75 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_288) ).
thf(791,plain,
n75 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[286]) ).
thf(25,axiom,
n4 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_52) ).
thf(441,plain,
n4 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(118,axiom,
countryamedicalorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_30) ).
thf(585,plain,
countryamedicalorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(239,axiom,
n1 @ ( muslim @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_222) ).
thf(717,plain,
n1 @ ( muslim @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[239]) ).
thf(72,axiom,
cityb @ ( countryafirstaidorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_115) ).
thf(502,plain,
cityb @ ( countryafirstaidorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(296,axiom,
n12 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_89) ).
thf(840,plain,
n12 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[296]) ).
thf(47,axiom,
! [A: $i] :
( ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n78 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( cityb @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_12) ).
thf(463,plain,
! [A: $i] :
( ( ( cityb @ ( A @ accept_city ) )
=> ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n78 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n1 @ ( other @ ( A @ accept_population ) ) )
& ( n0 @ ( native @ ( A @ accept_population ) ) )
& ( n1 @ ( muslim @ ( A @ accept_population ) ) )
& ( n20 @ ( christian @ ( A @ accept_population ) ) )
& ( n78 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( cityb @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(109,axiom,
n5 @ ( christiancountrychumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_341) ).
thf(576,plain,
n5 @ ( christiancountrychumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(165,axiom,
countryacivilorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_252) ).
thf(643,plain,
countryacivilorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(92,axiom,
countrycmedicalorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_194) ).
thf(544,plain,
countrycmedicalorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(337,axiom,
n3 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_145) ).
thf(907,plain,
n3 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[337]) ).
thf(253,axiom,
n0 @ ( native @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_314) ).
thf(744,plain,
n0 @ ( native @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[253]) ).
thf(225,axiom,
n20 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_113) ).
thf(703,plain,
n20 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[225]) ).
thf(178,axiom,
coastvillage @ ( countrycmedicalorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_36) ).
thf(656,plain,
coastvillage @ ( countrycmedicalorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(145,axiom,
sufferterragovernment @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_319) ).
thf(613,plain,
sufferterragovernment @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(132,axiom,
sufferterragovernment @ ( countrycmedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_290) ).
thf(600,plain,
sufferterragovernment @ ( countrycmedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(382,axiom,
n0 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_295) ).
thf(978,plain,
n0 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[382]) ).
thf(127,axiom,
n2 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_311) ).
thf(595,plain,
n2 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(144,axiom,
n3 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_328) ).
thf(612,plain,
n3 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(67,axiom,
countryamedicalorganization @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_29) ).
thf(497,plain,
countryamedicalorganization @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(315,axiom,
n1 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_202) ).
thf(859,plain,
n1 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[315]) ).
thf(395,axiom,
n20 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_211) ).
thf(991,plain,
n20 @ ( christian @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[395]) ).
thf(30,axiom,
cityb @ ( christiancountrychumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_12) ).
thf(446,plain,
cityb @ ( christiancountrychumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(104,axiom,
countrybcivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_156) ).
thf(571,plain,
countrybcivilorganization @ ( muslimcountrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(301,axiom,
n3 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_40) ).
thf(845,plain,
n3 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[301]) ).
thf(158,axiom,
countrybhumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_214) ).
thf(627,plain,
countrybhumanitarianorganization @ ( countryamedicalorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(34,axiom,
towna @ ( countrybcivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_300) ).
thf(450,plain,
towna @ ( countrybcivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(53,axiom,
n5 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_164) ).
thf(482,plain,
n5 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(193,axiom,
townc @ ( countrybcivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_48) ).
thf(671,plain,
townc @ ( countrybcivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(114,axiom,
n5 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_354) ).
thf(581,plain,
n5 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(65,axiom,
countrybcivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_131) ).
thf(495,plain,
countrybcivilorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(267,axiom,
n75 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_299) ).
thf(759,plain,
n75 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[267]) ).
thf(300,axiom,
n75 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_264) ).
thf(844,plain,
n75 @ ( atheist @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[300]) ).
thf(279,axiom,
n1 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_50) ).
thf(771,plain,
n1 @ ( other @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[279]) ).
thf(361,axiom,
n24 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_55) ).
thf(931,plain,
n24 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[361]) ).
thf(87,axiom,
n5 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_54) ).
thf(539,plain,
n5 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(210,axiom,
n5 @ ( countrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_333) ).
thf(688,plain,
n5 @ ( countrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[210]) ).
thf(333,axiom,
n0 @ ( native @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_245) ).
thf(903,plain,
n0 @ ( native @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[333]) ).
thf(378,axiom,
n24 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_316) ).
thf(961,plain,
n24 @ ( christian @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[378]) ).
thf(174,axiom,
n3 @ ( countryccivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_321) ).
thf(652,plain,
n3 @ ( countryccivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(15,axiom,
coastvillage @ ( christiansufferterrahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_90) ).
thf(418,plain,
coastvillage @ ( christiansufferterrahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(399,axiom,
n20 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_256) ).
thf(995,plain,
n20 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[399]) ).
thf(120,axiom,
countrybhumanitarianorganization @ ( countryccivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_63) ).
thf(588,plain,
countrybhumanitarianorganization @ ( countryccivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(221,axiom,
n30 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_47) ).
thf(699,plain,
n30 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[221]) ).
thf(380,axiom,
! [A: $i] :
( ( ( n9 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n3 @ ( muslim @ ( A @ accept_population ) ) )
& ( n23 @ ( christian @ ( A @ accept_population ) ) )
& ( n54 @ ( atheist @ ( A @ accept_population ) ) ) )
<=> ( centraltown @ ( A @ accept_city ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_2) ).
thf(963,plain,
! [A: $i] :
( ( ( centraltown @ ( A @ accept_city ) )
=> ( ( n9 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n3 @ ( muslim @ ( A @ accept_population ) ) )
& ( n23 @ ( christian @ ( A @ accept_population ) ) )
& ( n54 @ ( atheist @ ( A @ accept_population ) ) ) ) )
& ( ( ( n9 @ ( other @ ( A @ accept_population ) ) )
& ( n1 @ ( native @ ( A @ accept_population ) ) )
& ( n3 @ ( muslim @ ( A @ accept_population ) ) )
& ( n23 @ ( christian @ ( A @ accept_population ) ) )
& ( n54 @ ( atheist @ ( A @ accept_population ) ) ) )
=> ( centraltown @ ( A @ accept_city ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[380]) ).
thf(78,axiom,
n2 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_329) ).
thf(517,plain,
n2 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(326,axiom,
n1 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_274) ).
thf(896,plain,
n1 @ ( muslim @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[326]) ).
thf(257,axiom,
n1 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_315) ).
thf(748,plain,
n1 @ ( muslim @ ( countryacivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[257]) ).
thf(344,axiom,
n20 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_205) ).
thf(914,plain,
n20 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[344]) ).
thf(189,axiom,
countryacivilorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_163) ).
thf(667,plain,
countryacivilorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(359,axiom,
n0 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_107) ).
thf(929,plain,
n0 @ ( christian @ ( countryafirstaidorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[359]) ).
thf(49,axiom,
n4 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_309) ).
thf(478,plain,
n4 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(271,axiom,
n78 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_212) ).
thf(763,plain,
n78 @ ( atheist @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[271]) ).
thf(329,axiom,
n75 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_81) ).
thf(899,plain,
n75 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[329]) ).
thf(206,axiom,
countryamedicalorganization @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_66) ).
thf(684,plain,
countryamedicalorganization @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[206]) ).
thf(96,axiom,
countrycmedicalorganization @ ( countrybhumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_133) ).
thf(549,plain,
countrycmedicalorganization @ ( countrybhumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(84,axiom,
n5 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_326) ).
thf(536,plain,
n5 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(238,axiom,
n24 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_298) ).
thf(716,plain,
n24 @ ( christian @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[238]) ).
thf(151,axiom,
n5 @ ( countryahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_89) ).
thf(620,plain,
n5 @ ( countryahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(261,axiom,
n1 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_255) ).
thf(752,plain,
n1 @ ( muslim @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[261]) ).
thf(31,axiom,
n5 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_360) ).
thf(447,plain,
n5 @ ( muslimcountrybhumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(7,axiom,
n4 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_303) ).
thf(410,plain,
n4 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( A @ accept_number ) ) )
=> ( C @ ( A @ accept_number ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_2) ).
thf(405,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( C @ less ) )
& ( B @ ( A @ accept_number ) ) )
=> ( C @ ( A @ accept_number ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(310,axiom,
n1 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_286) ).
thf(854,plain,
n1 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[310]) ).
thf(285,axiom,
n65 @ ( muslim @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_4) ).
thf(790,plain,
n65 @ ( muslim @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[285]) ).
thf(135,axiom,
countryamedicalorganization @ ( sufferterragovernment @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_54) ).
thf(603,plain,
countryamedicalorganization @ ( sufferterragovernment @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(348,axiom,
n0 @ ( native @ ( countryamedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_221) ).
thf(918,plain,
n0 @ ( native @ ( countryamedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[348]) ).
thf(21,axiom,
countryamedicalorganization @ ( countryahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_21) ).
thf(437,plain,
countryamedicalorganization @ ( countryahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(186,axiom,
n2 @ ( countryafirstaidorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_270) ).
thf(664,plain,
n2 @ ( countryafirstaidorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[186]) ).
thf(377,axiom,
n78 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_236) ).
thf(960,plain,
n78 @ ( atheist @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[377]) ).
thf(80,axiom,
n3 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_356) ).
thf(532,plain,
n3 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(218,axiom,
townc @ ( countrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_128) ).
thf(696,plain,
townc @ ( countrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[218]) ).
thf(242,axiom,
n1 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_136) ).
thf(720,plain,
n1 @ ( muslim @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[242]) ).
thf(372,axiom,
n3 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_96) ).
thf(955,plain,
n3 @ ( christian @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[372]) ).
thf(327,axiom,
n0 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_151) ).
thf(897,plain,
n0 @ ( christian @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[327]) ).
thf(275,axiom,
n3 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_34) ).
thf(767,plain,
n3 @ ( christian @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[275]) ).
thf(358,axiom,
n0 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_93) ).
thf(928,plain,
n0 @ ( other @ ( muslimcountrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[358]) ).
thf(12,axiom,
countryacivilorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_37) ).
thf(415,plain,
countryacivilorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(249,axiom,
n0 @ ( native @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_285) ).
thf(740,plain,
n0 @ ( native @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[249]) ).
thf(391,axiom,
n0 @ ( other @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_260) ).
thf(987,plain,
n0 @ ( other @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[391]) ).
thf(108,axiom,
countryccivilorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_291) ).
thf(575,plain,
countryccivilorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(316,axiom,
n30 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_187) ).
thf(860,plain,
n30 @ ( atheist @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[316]) ).
thf(128,axiom,
christiancountrychumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_104) ).
thf(596,plain,
christiancountrychumanitarianorganization @ ( countryafirstaidorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(166,axiom,
n2 @ ( sufferterragovernment @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_305) ).
thf(644,plain,
n2 @ ( sufferterragovernment @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(43,axiom,
towna @ ( christiansufferterrahumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_83) ).
thf(459,plain,
towna @ ( christiansufferterrahumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(245,axiom,
n0 @ ( other @ ( sufferterragovernment @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_142) ).
thf(723,plain,
n0 @ ( other @ ( sufferterragovernment @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[245]) ).
thf(306,axiom,
n1 @ ( muslim @ ( countryahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_246) ).
thf(850,plain,
n1 @ ( muslim @ ( countryahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[306]) ).
thf(386,axiom,
n75 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_351) ).
thf(982,plain,
n75 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[386]) ).
thf(213,axiom,
n1 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_168) ).
thf(691,plain,
n1 @ ( christiansufferterrahumanitarianorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[213]) ).
thf(26,axiom,
cityb @ ( countryacivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_231) ).
thf(442,plain,
cityb @ ( countryacivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(71,axiom,
towna @ ( christiancountrychumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_352) ).
thf(501,plain,
towna @ ( christiancountrychumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(139,axiom,
n5 @ ( countrybcivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',event_45) ).
thf(607,plain,
n5 @ ( countrybcivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(155,axiom,
n1 @ ( countryacivilorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_312) ).
thf(624,plain,
n1 @ ( countryacivilorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(295,axiom,
n0 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_347) ).
thf(839,plain,
n0 @ ( other @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[295]) ).
thf(338,axiom,
n12 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_41) ).
thf(908,plain,
n12 @ ( atheist @ ( countrybcivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[338]) ).
thf(396,axiom,
n30 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_160) ).
thf(992,plain,
n30 @ ( atheist @ ( christiansufferterrahumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[396]) ).
thf(56,axiom,
n4 @ ( countrycmedicalorganization @ accept_number ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_355) ).
thf(486,plain,
n4 @ ( countrycmedicalorganization @ accept_number ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(365,axiom,
n1 @ ( muslim @ ( countryccivilorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_262) ).
thf(935,plain,
n1 @ ( muslim @ ( countryccivilorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[365]) ).
thf(353,axiom,
n78 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_11) ).
thf(923,plain,
n78 @ ( atheist @ ( christiancountrychumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[353]) ).
thf(181,axiom,
countryahumanitarianorganization @ ( countryccivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_182) ).
thf(659,plain,
countryahumanitarianorganization @ ( countryccivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(91,axiom,
christiancountrychumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_293) ).
thf(543,plain,
christiancountrychumanitarianorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(283,axiom,
n12 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_121) ).
thf(775,plain,
n12 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[283]) ).
thf(161,axiom,
coastvillage @ ( countryacivilorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_72) ).
thf(639,plain,
coastvillage @ ( countryacivilorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(61,axiom,
coastvillage @ ( muslimcountrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_98) ).
thf(491,plain,
coastvillage @ ( muslimcountrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(124,axiom,
countrycmedicalorganization @ ( countrybcivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_294) ).
thf(592,plain,
countrycmedicalorganization @ ( countrybcivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(230,axiom,
n0 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_33) ).
thf(708,plain,
n0 @ ( muslim @ ( countrycmedicalorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[230]) ).
thf(264,axiom,
n30 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_127) ).
thf(755,plain,
n30 @ ( atheist @ ( countrybhumanitarianorganization @ accept_population ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[264]) ).
thf(198,axiom,
cityb @ ( muslimcountrybhumanitarianorganization @ accept_city ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_208) ).
thf(676,plain,
cityb @ ( muslimcountrybhumanitarianorganization @ accept_city ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[198]) ).
thf(66,axiom,
countryafirstaidorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_84) ).
thf(496,plain,
countryafirstaidorganization @ ( christiansufferterrahumanitarianorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(38,axiom,
countryafirstaidorganization @ ( countryacivilorganization @ accept_leader ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',deduced_67) ).
thf(454,plain,
countryafirstaidorganization @ ( countryacivilorganization @ accept_leader ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(998,plain,
$false,
inference(e,[status(thm)],[809,760,479,846,893,518,962,555,666,481,645,892,909,628,683,994,741,449,597,861,408,977,582,762,878,440,655,614,677,533,550,500,715,698,538,930,670,747,913,898,709,436,651,841,417,724,719,504,934,619,838,917,702,751,542,460,902,421,606,770,416,448,638,853,924,492,756,591,443,623,646,485,937,574,905,480,687,956,453,774,660,849,602,981,766,877,692,411,988,452,920,439,678,661,925,761,810,534,714,546,793,910,746,862,598,957,894,407,693,916,847,625,665,583,461,493,682,551,710,852,435,456,842,697,650,725,980,593,610,420,499,989,857,742,578,488,933,537,669,642,489,590,679,706,554,753,901,686,622,985,701,515,654,457,721,647,997,984,911,503,605,792,938,921,541,657,765,674,953,926,773,794,586,662,718,906,412,750,618,824,856,745,573,689,444,601,584,904,694,402,843,772,743,579,958,545,413,577,711,641,572,611,919,704,540,672,445,936,713,498,900,681,419,451,649,616,599,863,764,979,604,990,996,477,494,758,535,609,594,621,483,895,769,668,858,552,848,700,626,915,462,932,983,959,768,695,455,608,986,851,653,922,658,912,685,505,438,722,589,927,749,939,754,553,458,490,675,795,680,663,548,648,487,617,516,776,690,640,705,707,414,954,739,409,993,712,557,580,855,673,791,441,585,717,502,840,463,576,643,544,907,744,703,656,613,600,978,595,612,497,859,991,446,571,845,627,450,482,671,581,495,759,844,771,931,539,688,903,961,652,418,995,588,699,963,517,896,748,914,667,929,478,763,899,684,549,536,716,620,752,447,410,405,854,790,603,918,437,664,960,532,696,720,955,897,767,928,415,740,987,575,860,596,644,459,723,850,982,691,442,501,607,624,839,908,992,486,935,923,659,543,775,639,491,592,708,755,676,496,454]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT014+2 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.15/0.40 % Computer : n012.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Sat Sep 26 20:53:36 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.15/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.73/0.88 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.90/1.20 % [INFO] Parsing done (313ms).
% 1.90/1.21 % [INFO] Running in sequential loop mode.
% 2.63/1.55 % [INFO] eprover registered as external prover.
% 2.63/1.56 % [INFO] Scanning for conjecture ...
% 3.22/1.72 % [INFO] Found a conjecture (or negated_conjecture) and 922 axioms. Running axiom selection ...
% 4.09/1.93 % [INFO] Axiom selection finished. Selected 399 axioms (removed 523 axioms).
% 4.62/2.04 % [INFO] Problem is first-order (TPTP FOF).
% 4.62/2.05 % [INFO] Type checking passed.
% 4.62/2.06 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 8.43/3.34 % External prover 'e' found a proof!
% 8.43/3.34 % [INFO] Killing All external provers ...
% 8.43/3.34 % Time passed: 2825ms (effective reasoning time: 2125ms)
% 8.43/3.34 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 8.43/3.35 % Axioms used in derivation (399): deduced_285, deduced_170, deduced_69, event_59, deduced_96, a1_2, deduced_93, deduced_39, deduced_29, deduced_221, deduced_176, deduced_105, event_89, deduced_53, deduced_64, deduced_304, deduced_58, deduced_187, deduced_344, deduced_74, deduced_18, deduced_4, deduced_36, deduced_210, deduced_165, deduced_162, deduced_322, deduced_311, deduced_296, deduced_198, deduced_82, event_45, less_property, deduced_42, deduced_173, deduced_333, deduced_71, event_73, deduced_154, deduced_119, deduced_191, a2_13, deduced_85, deduced_184, deduced_349, deduced_31, deduced_309, a2_4, deduced_47, deduced_20, deduced_209, event_88, deduced_282, deduced_337, deduced_141, deduced_158, deduced_195, deduced_90, deduced_130, deduced_65, deduced_299, event_211, deduced_350, deduced_180, deduced_265, deduced_260, deduced_101, deduced_108, event_52, deduced_293, deduced_28, event_235, deduced_153, deduced_78, deduced_235, deduced_272, deduced_300, deduced_288, deduced_17, deduced_361, deduced_113, deduced_214, deduced_56, event_65, deduced_254, deduced_185, deduced_315, deduced_114, a2_7, deduced_129, deduced_326, deduced_182, deduced_366, deduced_67, deduced_355, a1_3, deduced_7, deduced_48, deduced_124, deduced_98, deduced_37, deduced_163, deduced_192, deduced_171, deduced_239, deduced_34, deduced_125, deduced_19, deduced_59, deduced_263, deduced_211, deduced_25, deduced_87, a2_3, a2_12, deduced_174, deduced_135, deduced_243, deduced_76, deduced_146, deduced_200, event_222, deduced_241, deduced_60, deduced_30, deduced_45, deduced_232, deduced_222, deduced_160, deduced_203, deduced_118, deduced_348, deduced_252, deduced_14, deduced_360, deduced_102, deduced_329, deduced_86, event_203, event_214, deduced_334, deduced_215, deduced_247, deduced_219, deduced_323, deduced_273, deduced_255, deduced_269, deduced_308, deduced_179, deduced_41, deduced_312, deduced_226, deduced_345, deduced_236, deduced_294, deduced_208, deduced_266, deduced_352, deduced_75, deduced_283, deduced_363, deduced_303, deduced_230, deduced_110, event_227, a2_6, deduced_52, deduced_63, deduced_330, deduced_276, deduced_97, deduced_168, deduced_26, deduced_181, deduced_107, deduced_258, deduced_157, deduced_12, a2_8, deduced_143, deduced_140, deduced_121, deduced_8, deduced_23, deduced_341, deduced_290, deduced_150, deduced_196, deduced_132, event_171, deduced_3, deduced_77, deduced_126, deduced_6, deduced_115, deduced_83, deduced_233, deduced_204, deduced_79, deduced_287, deduced_244, deduced_72, deduced_193, deduced_291, deduced_15, deduced_201, deduced_206, deduced_279, deduced_88, deduced_164, deduced_251, deduced_9, deduced_99, deduced_1, event_21, deduced_217, deduced_33, deduced_103, a2_11, deduced_228, deduced_189, deduced_298, deduced_186, deduced_240, deduced_262, deduced_137, deduced_212, deduced_178, deduced_175, deduced_44, deduced_280, deduced_70, deduced_223, deduced_94, deduced_229, deduced_320, deduced_335, deduced_274, deduced_147, a2_2, event_197, event_192, deduced_22, event_28, event_17, deduced_40, deduced_324, deduced_133, deduced_364, deduced_136, deduced_227, deduced_216, deduced_267, a2_9, deduced_81, deduced_256, deduced_259, event_54, deduced_51, deduced_248, deduced_342, deduced_302, deduced_245, event_226, deduced_122, deduced_2, deduced_319, deduced_237, deduced_156, deduced_11, deduced_151, deduced_205, deduced_270, deduced_197, deduced_317, deduced_92, deduced_286, deduced_111, deduced_305, deduced_207, deduced_275, deduced_218, deduced_167, deduced_353, deduced_95, deduced_356, deduced_367, deduced_144, deduced_328, deduced_313, deduced_351, deduced_340, deduced_43, deduced_188, deduced_234, deduced_138, deduced_32, deduced_16, deduced_131, deduced_5, deduced_177, deduced_120, deduced_292, deduced_161, deduced_301, deduced_13, deduced_149, deduced_27, deduced_106, deduced_271, deduced_142, deduced_89, a2_1, deduced_24, deduced_284, deduced_246, deduced_295, deduced_339, deduced_257, deduced_297, deduced_281, deduced_73, deduced_268, deduced_358, deduced_152, deduced_250, event_204, deduced_127, deduced_190, deduced_104, deduced_172, deduced_84, deduced_199, deduced_183, deduced_54, event_183, event_215, deduced_261, event_98, deduced_166, a2_10, a2_5, deduced_116, deduced_362, deduced_306, deduced_123, deduced_354, deduced_21, deduced_264, deduced_343, deduced_194, event_234, deduced_128, deduced_314, deduced_117, less_successor, deduced_46, deduced_224, deduced_148, deduced_100, deduced_109, deduced_50, deduced_112, deduced_155, deduced_231, deduced_325, deduced_91, deduced_80, deduced_213, deduced_10, deduced_139, deduced_332, deduced_253, deduced_66, deduced_310, deduced_238, deduced_357, deduced_347, deduced_220, deduced_35, deduced_134, deduced_49, deduced_57, less_or_equal, deduced_38, deduced_61, deduced_159, deduced_278, deduced_55, deduced_316, deduced_202, deduced_321, deduced_242, deduced_327, deduced_336, deduced_145, deduced_289, deduced_68
% 8.43/3.35 % No. of inferences in proof: 802
% 8.43/3.35 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 2825 ms resp. 2125 ms w/o parsing
% 8.87/3.48 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 8.87/3.49 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------