%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : AGT020+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 12:00:58 EDT 2022
% Result : Theorem 227.58s 218.77s
% Output : Proof 227.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : AGT020+1 : TPTP v8.1.0. Bugfixed v3.1.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.35 % Computer : n024.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 600
% 0.12/0.35 % DateTime : Sat Jun 4 05:01:21 EDT 2022
% 0.12/0.35 % CPUTime :
% 227.58/218.77 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 227.60/218.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 227.60/218.78
% 227.60/218.78 %-----------------------------------------------------
% 227.60/218.78 fof(rdn_positive_less78, axiom, rdn_positive_less(rdnn(n7), rdnn(n8)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less78)).
% 227.60/218.78 fof(event_173, axiom, accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_173)).
% 227.60/218.78 fof(event_13, axiom, accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_13)).
% 227.60/218.78 fof(rdn_positive_less67, axiom, rdn_positive_less(rdnn(n6), rdnn(n7)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less67)).
% 227.60/218.78 fof(a2_7, axiom, ! [_373224] : (accept_population(_373224, atheist, n12) & accept_population(_373224, christian, n3) & accept_population(_373224, muslim, n0) & accept_population(_373224, native, n85) & accept_population(_373224, other, n0) <=> accept_city(_373224, coastvillage)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_7)).
% 227.60/218.78 fof(a2_12, axiom, ! [_373515] : (accept_population(_373515, atheist, n78) & accept_population(_373515, christian, n20) & accept_population(_373515, muslim, n1) & accept_population(_373515, native, n0) & accept_population(_373515, other, n1) <=> accept_city(_373515, cityb)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_12)).
% 227.60/218.78 fof(a1_6, axiom, ! [_373869, _373872, _373875] : (the_agent_not_in_any_proposed_teams(_373869, _373872, _373875) => ~ (accept_city(_373869, _373875) & accept_leader(_373869, _373872))), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_6)).
% 227.60/218.78 fof(rdn_extra_digits_positive_less, axiom, ! [_374096, _374099, _374102] : (rdn_non_zero(_374102) => rdn_positive_less(rdnn(_374096), rdn(rdnn(_374099), _374102))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_extra_digits_positive_less)).
% 227.60/218.78 fof(a1_1, axiom, ! [_374316, _374319, _374322, _374325] : (accept_team(_374316, _374325, _374319, _374322) <=> accept_city(_374316, _374319) & accept_leader(_374316, _374325) & accept_number(_374316, _374322)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_1)).
% 227.60/218.78 fof(rdn_positive_less01, axiom, rdn_positive_less(rdnn(n0), rdnn(n1)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less01)).
% 227.60/218.78 fof(less_entry_point_pos_pos, axiom, ! [_374649, _374652, _374655, _374658] : (rdn_translate(_374649, rdn_pos(_374655)) & rdn_translate(_374652, rdn_pos(_374658)) & rdn_positive_less(_374655, _374658) => less(_374649, _374652)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', less_entry_point_pos_pos)).
% 227.60/218.78 fof(event_11, axiom, the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_11)).
% 227.60/218.78 fof(a1_3, axiom, ! [_374970, _374973, _374976, _374979] : (accept_population(_374970, _374979, _374973) & less(_374976, _374973) => accept_population(_374970, _374979, _374976)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_3)).
% 227.60/218.78 fof(rdn75, axiom, rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn75)).
% 227.60/218.78 fof(rdn85, axiom, rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn85)).
% 227.60/218.78 fof(rdn_digit8, axiom, rdn_non_zero_digit(rdnn(n8)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_digit8)).
% 227.60/218.78 fof(rdn_positive_less_multi_digit_low, axiom, ! [_375514, _375517, _375520] : (rdn_positive_less(rdnn(_375514), rdnn(_375520)) & rdn_non_zero(_375517) => rdn_positive_less(rdn(rdnn(_375514), _375517), rdn(rdnn(_375520), _375517))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less_multi_digit_low)).
% 227.60/218.78 fof(a1_5, axiom, ! [_375774, _375777, _375780] : (any_agent_in_all_proposed_teams(_375774, _375777, _375780) => accept_leader(_375774, _375777)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_5)).
% 227.60/218.78 fof(a2_9, axiom, ! [_375956] : (accept_population(_375956, atheist, n75) & accept_population(_375956, christian, n24) & accept_population(_375956, muslim, n1) & accept_population(_375956, native, n0) & accept_population(_375956, other, n0) <=> accept_city(_375956, towna)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_9)).
% 227.60/218.78 fof(query_20, conjecture, ? [_376272, _376275] : ~ accept_population(_376272, christian, _376275), file('/export/starexec/sandbox/benchmark/theBenchmark.p', query_20)).
% 227.60/218.78 fof(rdn1, axiom, rdn_translate(n1, rdn_pos(rdnn(n1))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn1)).
% 227.60/218.78 fof(rdn_non_zero_by_digit, axiom, ! [_376553] : (rdn_non_zero_digit(rdnn(_376553)) => rdn_non_zero(rdnn(_376553))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_non_zero_by_digit)).
% 227.60/218.78 fof(rdn_digit7, axiom, rdn_non_zero_digit(rdnn(n7)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_digit7)).
% 227.60/218.78 fof(rdn_positive_less56, axiom, rdn_positive_less(rdnn(n5), rdnn(n6)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less56)).
% 227.60/218.78 fof(rdn78, axiom, rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn78)).
% 227.60/218.78 fof(event_12, axiom, any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_12)).
% 227.60/218.78 fof(rdn0, axiom, rdn_translate(n0, rdn_pos(rdnn(n0))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn0)).
% 227.60/218.78 fof(rdn_positive_less_transitivity, axiom, ! [_377039, _377042, _377045] : (rdn_positive_less(rdnn(_377039), rdnn(_377042)) & rdn_positive_less(rdnn(_377042), rdnn(_377045)) => rdn_positive_less(rdnn(_377039), rdnn(_377045))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less_transitivity)).
% 227.60/218.78
% 227.60/218.78 cnf(1, plain, [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], clausify(rdn_positive_less78)).
% 227.60/218.78 cnf(2, plain, [-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6))], clausify(event_173)).
% 227.60/218.78 cnf(3, plain, [-(accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5))], clausify(event_13)).
% 227.60/218.78 cnf(4, plain, [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], clausify(rdn_positive_less67)).
% 227.60/218.78 cnf(5, plain, [-(9 ^ [_128469]), -(accept_population(_128469, native, n85))], clausify(a2_7)).
% 227.60/218.78 cnf(6, plain, [-(14 ^ [_132364]), -(accept_population(_132364, atheist, n78))], clausify(a2_12)).
% 227.60/218.78 cnf(7, plain, [14 ^ [_132364], accept_city(_132364, cityb)], clausify(a2_12)).
% 227.60/218.78 cnf(8, plain, [-(14 ^ [_132364]), -(accept_population(_132364, muslim, n1))], clausify(a2_12)).
% 227.60/218.78 cnf(9, plain, [the_agent_not_in_any_proposed_teams(_122953, _123012, _123070), accept_city(_122953, _123070), accept_leader(_122953, _123012)], clausify(a1_6)).
% 227.60/218.78 cnf(10, plain, [rdn_non_zero(_252446), -(rdn_positive_less(rdnn(_252335), rdn(rdnn(_252391), _252446)))], clausify(rdn_extra_digits_positive_less)).
% 227.60/218.78 cnf(11, plain, [9 ^ [_128469], accept_city(_128469, coastvillage)], clausify(a2_7)).
% 227.60/218.78 cnf(12, plain, [accept_team(_120190, _120394, _120259, _120327), 1 ^ [_120394, _120327, _120259, _120190]], clausify(a1_1)).
% 227.60/218.78 cnf(13, plain, [-(1 ^ [_120394, _120327, _120259, _120190]), -(accept_city(_120190, _120259))], clausify(a1_1)).
% 227.60/218.78 cnf(14, plain, [-(14 ^ [_132364]), -(accept_population(_132364, other, n1))], clausify(a2_12)).
% 227.60/218.78 cnf(15, plain, [-(rdn_positive_less(rdnn(n0), rdnn(n1)))], clausify(rdn_positive_less01)).
% 227.60/218.78 cnf(16, plain, [-(less(_253349, _253420)), rdn_translate(_253349, rdn_pos(_253490)), rdn_translate(_253420, rdn_pos(_253559)), rdn_positive_less(_253490, _253559)], clausify(less_entry_point_pos_pos)).
% 227.60/218.78 cnf(17, plain, [-(the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna))], clausify(event_11)).
% 227.60/218.78 cnf(18, plain, [-(accept_population(_121390, _121576, _121515)), accept_population(_121390, _121576, _121453), less(_121515, _121453)], clausify(a1_3)).
% 227.60/218.78 cnf(19, plain, [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], clausify(rdn75)).
% 227.60/218.78 cnf(20, plain, [-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))], clausify(rdn85)).
% 227.60/218.78 cnf(21, plain, [-(rdn_non_zero_digit(rdnn(n8)))], clausify(rdn_digit8)).
% 227.60/218.78 cnf(22, plain, [-(rdn_positive_less(rdn(rdnn(_251712), _251781), rdn(rdnn(_251849), _251781))), rdn_positive_less(rdnn(_251712), rdnn(_251849)), rdn_non_zero(_251781)], clausify(rdn_positive_less_multi_digit_low)).
% 227.60/218.78 cnf(23, plain, [any_agent_in_all_proposed_teams(_122535, _122586, _122636), -(accept_leader(_122535, _122586))], clausify(a1_5)).
% 227.60/218.78 cnf(24, plain, [-(accept_city(_130027, towna)), accept_population(_130027, atheist, n75), accept_population(_130027, christian, n24), accept_population(_130027, muslim, n1), accept_population(_130027, native, n0), accept_population(_130027, other, n0)], clausify(a2_9)).
% 227.60/218.78 cnf(25, plain, [-(accept_population(_257148, christian, _257191))], clausify(query_20)).
% 227.60/218.78 cnf(26, plain, [-(rdn_translate(n1, rdn_pos(rdnn(n1))))], clausify(rdn1)).
% 227.60/218.78 cnf(27, plain, [rdn_non_zero_digit(rdnn(_252776)), -(rdn_non_zero(rdnn(_252776)))], clausify(rdn_non_zero_by_digit)).
% 227.60/218.78 cnf(28, plain, [-(rdn_non_zero_digit(rdnn(n7)))], clausify(rdn_digit7)).
% 227.60/218.78 cnf(29, plain, [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], clausify(rdn_positive_less56)).
% 227.60/218.78 cnf(30, plain, [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], clausify(rdn78)).
% 227.60/218.78 cnf(31, plain, [-(any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna))], clausify(event_12)).
% 227.60/218.78 cnf(32, plain, [-(rdn_translate(n0, rdn_pos(rdnn(n0))))], clausify(rdn0)).
% 227.60/218.78 cnf(33, plain, [-(rdn_positive_less(rdnn(_250518), rdnn(_250653))), rdn_positive_less(rdnn(_250518), rdnn(_250586)), rdn_positive_less(rdnn(_250586), rdnn(_250653))], clausify(rdn_positive_less_transitivity)).
% 227.60/218.78
% 227.60/218.78 cnf('1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, christian, n24))],start(25,bind([[_257148, _257191], [muslimcountrybhumanitarianorganization, n24]]))).
% 227.60/218.78 cnf('1.1',plain,[accept_population(muslimcountrybhumanitarianorganization, christian, n24), -(accept_city(muslimcountrybhumanitarianorganization, towna)), accept_population(muslimcountrybhumanitarianorganization, atheist, n75), accept_population(muslimcountrybhumanitarianorganization, muslim, n1), accept_population(muslimcountrybhumanitarianorganization, native, n0), accept_population(muslimcountrybhumanitarianorganization, other, n0)],extension(24,bind([[_130027], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.1',plain,[accept_city(muslimcountrybhumanitarianorganization, towna), the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna), accept_leader(muslimcountrybhumanitarianorganization, countryacivilorganization)],extension(9,bind([[_123070, _122953, _123012], [towna, muslimcountrybhumanitarianorganization, countryacivilorganization]]))).
% 227.60/218.78 cnf('1.1.1.1',plain,[-(the_agent_not_in_any_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna))],extension(17)).
% 227.60/218.78 cnf('1.1.1.2',plain,[-(accept_leader(muslimcountrybhumanitarianorganization, countryacivilorganization)), any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna)],extension(23,bind([[_122535, _122586, _122636], [muslimcountrybhumanitarianorganization, countryacivilorganization, towna]]))).
% 227.60/218.78 cnf('1.1.1.2.1',plain,[-(any_agent_in_all_proposed_teams(muslimcountrybhumanitarianorganization, countryacivilorganization, towna))],extension(31)).
% 227.60/218.78 cnf('1.1.2',plain,[-(accept_population(muslimcountrybhumanitarianorganization, atheist, n75)), accept_population(muslimcountrybhumanitarianorganization, atheist, n78), less(n75, n78)],extension(18,bind([[_121390, _121576, _121515, _121453], [muslimcountrybhumanitarianorganization, atheist, n75, n78]]))).
% 227.60/218.78 cnf('1.1.2.1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, atheist, n78)), -(14 ^ [muslimcountrybhumanitarianorganization])],extension(6,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.2.1.1',plain,[14 ^ [muslimcountrybhumanitarianorganization], accept_city(muslimcountrybhumanitarianorganization, cityb)],extension(7,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.2.1.1.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, cityb)), -(1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization])],extension(13,bind([[_120394, _120327, _120259, _120190], [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.2.1.1.1.1',plain,[1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization], accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6)],extension(12,bind([[_120190, _120394, _120259, _120327], [muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6]]))).
% 227.60/218.78 cnf('1.1.2.1.1.1.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6))],extension(2)).
% 227.60/218.78 cnf('1.1.2.2',plain,[-(less(n75, n78)), rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))), rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))), rdn_positive_less(rdn(rdnn(n5), rdnn(n7)), rdn(rdnn(n8), rdnn(n7)))],extension(16,bind([[_253349, _253420, _253490, _253559], [n75, n78, rdn(rdnn(n5), rdnn(n7)), rdn(rdnn(n8), rdnn(n7))]]))).
% 227.60/218.78 cnf('1.1.2.2.1',plain,[-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))],extension(19)).
% 227.60/218.78 cnf('1.1.2.2.2',plain,[-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))],extension(30)).
% 227.60/218.78 cnf('1.1.2.2.3',plain,[-(rdn_positive_less(rdn(rdnn(n5), rdnn(n7)), rdn(rdnn(n8), rdnn(n7)))), rdn_positive_less(rdnn(n5), rdnn(n8)), rdn_non_zero(rdnn(n7))],extension(22,bind([[_251712, _251849, _251781], [n5, n8, rdnn(n7)]]))).
% 227.60/218.78 cnf('1.1.2.2.3.1',plain,[-(rdn_positive_less(rdnn(n5), rdnn(n8))), rdn_positive_less(rdnn(n5), rdnn(n6)), rdn_positive_less(rdnn(n6), rdnn(n8))],extension(33,bind([[_250518, _250586, _250653], [n5, n6, n8]]))).
% 227.60/218.78 cnf('1.1.2.2.3.1.1',plain,[-(rdn_positive_less(rdnn(n5), rdnn(n6)))],extension(29)).
% 227.60/218.78 cnf('1.1.2.2.3.1.2',plain,[-(rdn_positive_less(rdnn(n6), rdnn(n8))), rdn_positive_less(rdnn(n6), rdnn(n7)), rdn_positive_less(rdnn(n7), rdnn(n8))],extension(33,bind([[_250518, _250586, _250653], [n6, n7, n8]]))).
% 227.60/218.78 cnf('1.1.2.2.3.1.2.1',plain,[-(rdn_positive_less(rdnn(n6), rdnn(n7)))],extension(4)).
% 227.60/218.78 cnf('1.1.2.2.3.1.2.2',plain,[-(rdn_positive_less(rdnn(n7), rdnn(n8)))],extension(1)).
% 227.60/218.78 cnf('1.1.2.2.3.2',plain,[-(rdn_non_zero(rdnn(n7))), rdn_non_zero_digit(rdnn(n7))],extension(27,bind([[_252776], [n7]]))).
% 227.60/218.78 cnf('1.1.2.2.3.2.1',plain,[-(rdn_non_zero_digit(rdnn(n7)))],extension(28)).
% 227.60/218.78 cnf('1.1.3',plain,[-(accept_population(muslimcountrybhumanitarianorganization, muslim, n1)), -(14 ^ [muslimcountrybhumanitarianorganization])],extension(8,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.3.1',plain,[14 ^ [muslimcountrybhumanitarianorganization], accept_city(muslimcountrybhumanitarianorganization, cityb)],extension(7,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.3.1.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, cityb)), -(1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization])],extension(13,bind([[_120394, _120327, _120259, _120190], [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.3.1.1.1',plain,[1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization], accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6)],extension(12,bind([[_120190, _120394, _120259, _120327], [muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6]]))).
% 227.60/218.78 cnf('1.1.3.1.1.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6))],extension(2)).
% 227.60/218.78 cnf('1.1.4',plain,[-(accept_population(muslimcountrybhumanitarianorganization, native, n0)), accept_population(muslimcountrybhumanitarianorganization, native, n85), less(n0, n85)],extension(18,bind([[_121390, _121576, _121515, _121453], [muslimcountrybhumanitarianorganization, native, n0, n85]]))).
% 227.60/218.78 cnf('1.1.4.1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, native, n85)), -(9 ^ [muslimcountrybhumanitarianorganization])],extension(5,bind([[_128469], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.4.1.1',plain,[9 ^ [muslimcountrybhumanitarianorganization], accept_city(muslimcountrybhumanitarianorganization, coastvillage)],extension(11,bind([[_128469], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.4.1.1.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, coastvillage)), -(1 ^ [christiancountrychumanitarianorganization, n5, coastvillage, muslimcountrybhumanitarianorganization])],extension(13,bind([[_120394, _120327, _120259, _120190], [christiancountrychumanitarianorganization, n5, coastvillage, muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.4.1.1.1.1',plain,[1 ^ [christiancountrychumanitarianorganization, n5, coastvillage, muslimcountrybhumanitarianorganization], accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5)],extension(12,bind([[_120190, _120394, _120259, _120327], [muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5]]))).
% 227.60/218.78 cnf('1.1.4.1.1.1.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5))],extension(3)).
% 227.60/218.78 cnf('1.1.4.2',plain,[-(less(n0, n85)), rdn_translate(n0, rdn_pos(rdnn(n0))), rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))), rdn_positive_less(rdnn(n0), rdn(rdnn(n5), rdnn(n8)))],extension(16,bind([[_253349, _253420, _253490, _253559], [n0, n85, rdnn(n0), rdn(rdnn(n5), rdnn(n8))]]))).
% 227.60/218.78 cnf('1.1.4.2.1',plain,[-(rdn_translate(n0, rdn_pos(rdnn(n0))))],extension(32)).
% 227.60/218.78 cnf('1.1.4.2.2',plain,[-(rdn_translate(n85, rdn_pos(rdn(rdnn(n5), rdnn(n8)))))],extension(20)).
% 227.60/218.78 cnf('1.1.4.2.3',plain,[-(rdn_positive_less(rdnn(n0), rdn(rdnn(n5), rdnn(n8)))), rdn_non_zero(rdnn(n8))],extension(10,bind([[_252335, _252391, _252446], [n0, n5, rdnn(n8)]]))).
% 227.60/218.78 cnf('1.1.4.2.3.1',plain,[-(rdn_non_zero(rdnn(n8))), rdn_non_zero_digit(rdnn(n8))],extension(27,bind([[_252776], [n8]]))).
% 227.60/218.78 cnf('1.1.4.2.3.1.1',plain,[-(rdn_non_zero_digit(rdnn(n8)))],extension(21)).
% 227.60/218.78 cnf('1.1.5',plain,[-(accept_population(muslimcountrybhumanitarianorganization, other, n0)), accept_population(muslimcountrybhumanitarianorganization, other, n1), less(n0, n1)],extension(18,bind([[_121390, _121576, _121515, _121453], [muslimcountrybhumanitarianorganization, other, n0, n1]]))).
% 227.60/218.78 cnf('1.1.5.1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, other, n1)), -(14 ^ [muslimcountrybhumanitarianorganization])],extension(14,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.5.1.1',plain,[14 ^ [muslimcountrybhumanitarianorganization], accept_city(muslimcountrybhumanitarianorganization, cityb)],extension(7,bind([[_132364], [muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.5.1.1.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, cityb)), -(1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization])],extension(13,bind([[_120394, _120327, _120259, _120190], [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization]]))).
% 227.60/218.78 cnf('1.1.5.1.1.1.1',plain,[1 ^ [countrybhumanitarianorganization, n6, cityb, muslimcountrybhumanitarianorganization], accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6)],extension(12,bind([[_120190, _120394, _120259, _120327], [muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6]]))).
% 227.60/218.78 cnf('1.1.5.1.1.1.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n6))],extension(2)).
% 227.60/218.78 cnf('1.1.5.2',plain,[-(less(n0, n1)), rdn_translate(n0, rdn_pos(rdnn(n0))), rdn_translate(n1, rdn_pos(rdnn(n1))), rdn_positive_less(rdnn(n0), rdnn(n1))],extension(16,bind([[_253349, _253420, _253490, _253559], [n0, n1, rdnn(n0), rdnn(n1)]]))).
% 227.60/218.78 cnf('1.1.5.2.1',plain,[-(rdn_translate(n0, rdn_pos(rdnn(n0))))],extension(32)).
% 227.60/218.78 cnf('1.1.5.2.2',plain,[-(rdn_translate(n1, rdn_pos(rdnn(n1))))],extension(26)).
% 227.60/218.78 cnf('1.1.5.2.3',plain,[-(rdn_positive_less(rdnn(n0), rdnn(n1)))],extension(15)).
% 227.60/218.78 %-----------------------------------------------------
% 227.60/218.79
% 227.60/218.79 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------