%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : AGT024+2 : TPTP v8.1.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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:59 EDT 2022
% Result : Theorem 186.83s 180.67s
% Output : Proof 186.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.13 % Problem : AGT024+2 : TPTP v8.1.0. Bugfixed v3.1.0.
% 0.09/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n023.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 4 03:35:55 EDT 2022
% 0.13/0.35 % CPUTime :
% 186.83/180.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.83/180.68 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 186.83/180.68
% 186.83/180.68 %-----------------------------------------------------
% 186.83/180.68 fof(rdn_positive_less_multi_digit_low, axiom, ! [_120600, _120603, _120606] : (rdn_positive_less(rdnn(_120600), rdnn(_120606)) & rdn_non_zero(_120603) => rdn_positive_less(rdn(rdnn(_120600), _120603), rdn(rdnn(_120606), _120603))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less_multi_digit_low)).
% 186.83/180.68 fof(deduced_206, axiom, accept_population(muslimcountrybhumanitarianorganization, atheist, n78), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax', deduced_206)).
% 186.83/180.68 fof(rdn_positive_less78, axiom, rdn_positive_less(rdnn(n7), rdnn(n8)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less78)).
% 186.83/180.68 fof(a2_7, axiom, ! [_120982] : (accept_population(_120982, atheist, n12) & accept_population(_120982, christian, n3) & accept_population(_120982, muslim, n0) & accept_population(_120982, native, n85) & accept_population(_120982, other, n0) <=> accept_city(_120982, coastvillage)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_7)).
% 186.83/180.68 fof(rdn25, axiom, rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn25)).
% 186.83/180.68 fof(rdn_positive_less67, axiom, rdn_positive_less(rdnn(n6), rdnn(n7)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less67)).
% 186.83/180.68 fof(a2_9, axiom, ! [_121480] : (accept_population(_121480, atheist, n75) & accept_population(_121480, christian, n24) & accept_population(_121480, muslim, n1) & accept_population(_121480, native, n0) & accept_population(_121480, other, n0) <=> accept_city(_121480, towna)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_9)).
% 186.83/180.68 fof(event_172, axiom, accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_172)).
% 186.83/180.68 fof(deduced_366, axiom, ~ accept_city(muslimcountrybhumanitarianorganization, towna), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax', deduced_366)).
% 186.83/180.68 fof(rdn24, axiom, rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn24)).
% 186.83/180.68 fof(event_13, axiom, accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+1.ax', event_13)).
% 186.83/180.68 fof(rdn_digit7, axiom, rdn_non_zero_digit(rdnn(n7)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_digit7)).
% 186.83/180.68 fof(a2_10, axiom, ! [_122263] : (accept_population(_122263, atheist, n75) & accept_population(_122263, christian, n25) & accept_population(_122263, muslim, n0) & accept_population(_122263, native, n0) & accept_population(_122263, other, n0) <=> accept_city(_122263, citya)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_10)).
% 186.83/180.68 fof(a1_1, axiom, ! [_122573, _122576, _122579, _122582] : (accept_team(_122573, _122582, _122576, _122579) <=> accept_city(_122573, _122576) & accept_leader(_122573, _122582) & accept_number(_122573, _122579)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_1)).
% 186.83/180.68 fof(rdn_positive_less56, axiom, rdn_positive_less(rdnn(n5), rdnn(n6)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less56)).
% 186.83/180.68 fof(rdn_digit2, axiom, rdn_non_zero_digit(rdnn(n2)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_digit2)).
% 186.83/180.68 fof(a2_12, axiom, ! [_123025] : (accept_population(_123025, atheist, n78) & accept_population(_123025, christian, n20) & accept_population(_123025, muslim, n1) & accept_population(_123025, native, n0) & accept_population(_123025, other, n1) <=> accept_city(_123025, cityb)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a2_12)).
% 186.83/180.68 fof(deduced_204, axiom, accept_population(muslimcountrybhumanitarianorganization, muslim, n1), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+2.ax', deduced_204)).
% 186.83/180.68 fof(rdn75, axiom, rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn75)).
% 186.83/180.68 fof(query_24, conjecture, ? [_123574] : ~ accept_population(_123574, christian, n25), file('/export/starexec/sandbox/benchmark/theBenchmark.p', query_24)).
% 186.83/180.68 fof(rdn_non_zero_by_digit, axiom, ! [_123848] : (rdn_non_zero_digit(rdnn(_123848)) => rdn_non_zero(rdnn(_123848))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_non_zero_by_digit)).
% 186.83/180.68 fof(rdn78, axiom, rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+0.ax', rdn78)).
% 186.83/180.68 fof(a1_3, axiom, ! [_124154, _124157, _124160, _124163] : (accept_population(_124154, _124163, _124157) & less(_124160, _124157) => accept_population(_124154, _124163, _124160)), file('/export/starexec/sandbox/benchmark/Axioms/AGT001+0.ax', a1_3)).
% 186.83/180.68 fof(rdn_positive_less45, axiom, rdn_positive_less(rdnn(n4), rdnn(n5)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less45)).
% 186.83/180.68 fof(rdn_positive_less_transitivity, axiom, ! [_124443, _124446, _124449] : (rdn_positive_less(rdnn(_124443), rdnn(_124446)) & rdn_positive_less(rdnn(_124446), rdnn(_124449)) => rdn_positive_less(rdnn(_124443), rdnn(_124449))), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', rdn_positive_less_transitivity)).
% 186.83/180.68 fof(less_entry_point_pos_pos, axiom, ! [_124788, _124791, _124794, _124797] : (rdn_translate(_124788, rdn_pos(_124794)) & rdn_translate(_124791, rdn_pos(_124797)) & rdn_positive_less(_124794, _124797) => less(_124788, _124791)), file('/export/starexec/sandbox/benchmark/Axioms/NUM005+1.ax', less_entry_point_pos_pos)).
% 186.83/180.68
% 186.83/180.68 cnf(1, plain, [-(rdn_positive_less(rdn(rdnn(_26230), _26231), rdn(rdnn(_26232), _26231))), rdn_positive_less(rdnn(_26230), rdnn(_26232)), rdn_non_zero(_26231)], clausify(rdn_positive_less_multi_digit_low)).
% 186.83/180.68 cnf(2, plain, [-(accept_population(muslimcountrybhumanitarianorganization, atheist, n78))], clausify(deduced_206)).
% 186.83/180.68 cnf(3, plain, [-(rdn_positive_less(rdnn(n7), rdnn(n8)))], clausify(rdn_positive_less78)).
% 186.83/180.68 cnf(4, plain, [-(accept_population(_17577, other, n0)), accept_city(_17577, coastvillage)], clausify(a2_7)).
% 186.83/180.68 cnf(5, plain, [-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))], clausify(rdn25)).
% 186.83/180.68 cnf(6, plain, [-(rdn_positive_less(rdnn(n6), rdnn(n7)))], clausify(rdn_positive_less67)).
% 186.83/180.68 cnf(7, plain, [-(accept_city(_17631, towna)), accept_population(_17631, atheist, n75), accept_population(_17631, christian, n24), accept_population(_17631, muslim, n1), accept_population(_17631, native, n0), accept_population(_17631, other, n0)], clausify(a2_9)).
% 186.83/180.68 cnf(8, plain, [-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5))], clausify(event_172)).
% 186.83/180.68 cnf(9, plain, [accept_city(muslimcountrybhumanitarianorganization, towna)], clausify(deduced_366)).
% 186.83/180.68 cnf(10, plain, [-(accept_population(_17577, muslim, n0)), accept_city(_17577, coastvillage)], clausify(a2_7)).
% 186.83/180.68 cnf(11, plain, [-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))], clausify(rdn24)).
% 186.83/180.68 cnf(12, plain, [-(accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5))], clausify(event_13)).
% 186.83/180.68 cnf(13, plain, [-(rdn_non_zero_digit(rdnn(n7)))], clausify(rdn_digit7)).
% 186.83/180.68 cnf(14, plain, [-(accept_population(_17658, other, n0)), accept_city(_17658, citya)], clausify(a2_10)).
% 186.83/180.68 cnf(15, plain, [accept_team(_17305, _17308, _17306, _17307), -(accept_city(_17305, _17306))], clausify(a1_1)).
% 186.83/180.68 cnf(16, plain, [-(rdn_positive_less(rdnn(n5), rdnn(n6)))], clausify(rdn_positive_less56)).
% 186.83/180.68 cnf(17, plain, [-(rdn_non_zero_digit(rdnn(n2)))], clausify(rdn_digit2)).
% 186.83/180.68 cnf(18, plain, [-(accept_population(_17712, native, n0)), accept_city(_17712, cityb)], clausify(a2_12)).
% 186.83/180.68 cnf(19, plain, [-(accept_city(_17658, citya)), accept_population(_17658, atheist, n75), accept_population(_17658, christian, n25), accept_population(_17658, muslim, n0), accept_population(_17658, native, n0), accept_population(_17658, other, n0)], clausify(a2_10)).
% 186.83/180.68 cnf(20, plain, [-(accept_population(muslimcountrybhumanitarianorganization, muslim, n1))], clausify(deduced_204)).
% 186.83/180.68 cnf(21, plain, [-(accept_population(_17658, atheist, n75)), accept_city(_17658, citya)], clausify(a2_10)).
% 186.83/180.68 cnf(22, plain, [-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))], clausify(rdn75)).
% 186.83/180.68 cnf(23, plain, [-(accept_population(_26412, christian, n25))], clausify(query_24)).
% 186.83/180.68 cnf(24, plain, [rdn_non_zero_digit(rdnn(_26276)), -(rdn_non_zero(rdnn(_26276)))], clausify(rdn_non_zero_by_digit)).
% 186.83/180.68 cnf(25, plain, [-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))], clausify(rdn78)).
% 186.83/180.68 cnf(26, plain, [-(accept_population(_17341, _17344, _17343)), accept_population(_17341, _17344, _17342), less(_17343, _17342)], clausify(a1_3)).
% 186.83/180.68 cnf(27, plain, [-(rdn_positive_less(rdnn(n4), rdnn(n5)))], clausify(rdn_positive_less45)).
% 186.83/180.68 cnf(28, plain, [-(rdn_positive_less(rdnn(_26180), rdnn(_26182))), rdn_positive_less(rdnn(_26180), rdnn(_26181)), rdn_positive_less(rdnn(_26181), rdnn(_26182))], clausify(rdn_positive_less_transitivity)).
% 186.83/180.68 cnf(29, plain, [-(less(_26302, _26303)), rdn_translate(_26302, rdn_pos(_26304)), rdn_translate(_26303, rdn_pos(_26305)), rdn_positive_less(_26304, _26305)], clausify(less_entry_point_pos_pos)).
% 186.83/180.68
% 186.83/180.68 cnf('1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, christian, n25))],start(23,bind([[_26412], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1',plain,[accept_population(muslimcountrybhumanitarianorganization, christian, n25), -(accept_city(muslimcountrybhumanitarianorganization, citya)), accept_population(muslimcountrybhumanitarianorganization, atheist, n75), accept_population(muslimcountrybhumanitarianorganization, muslim, n0), accept_population(muslimcountrybhumanitarianorganization, native, n0), accept_population(muslimcountrybhumanitarianorganization, other, n0)],extension(19,bind([[_17658], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1',plain,[accept_city(muslimcountrybhumanitarianorganization, citya), -(accept_population(muslimcountrybhumanitarianorganization, other, n0))],extension(14,bind([[_17658], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1.1',plain,[accept_population(muslimcountrybhumanitarianorganization, other, n0), -(accept_city(muslimcountrybhumanitarianorganization, towna)), accept_population(muslimcountrybhumanitarianorganization, atheist, n75), accept_population(muslimcountrybhumanitarianorganization, christian, n24), accept_population(muslimcountrybhumanitarianorganization, muslim, n1), accept_population(muslimcountrybhumanitarianorganization, native, n0)],extension(7,bind([[_17631], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1.1.1',plain,[accept_city(muslimcountrybhumanitarianorganization, towna)],extension(9)).
% 186.83/180.68 cnf('1.1.1.1.2',plain,[-(accept_population(muslimcountrybhumanitarianorganization, atheist, n75)), accept_city(muslimcountrybhumanitarianorganization, citya)],extension(21,bind([[_17658], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1.1.2.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, citya))],reduction('1.1')).
% 186.83/180.68 cnf('1.1.1.1.3',plain,[-(accept_population(muslimcountrybhumanitarianorganization, christian, n24)), accept_population(muslimcountrybhumanitarianorganization, christian, n25), less(n24, n25)],extension(26,bind([[_17341, _17344, _17343, _17342], [muslimcountrybhumanitarianorganization, christian, n24, n25]]))).
% 186.83/180.68 cnf('1.1.1.1.3.1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, christian, n25))],extension(23,bind([[_26412], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1.1.3.2',plain,[-(less(n24, n25)), rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))), rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))), rdn_positive_less(rdn(rdnn(n4), rdnn(n2)), rdn(rdnn(n5), rdnn(n2)))],extension(29,bind([[_26302, _26303, _26304, _26305], [n24, n25, rdn(rdnn(n4), rdnn(n2)), rdn(rdnn(n5), rdnn(n2))]]))).
% 186.83/180.68 cnf('1.1.1.1.3.2.1',plain,[-(rdn_translate(n24, rdn_pos(rdn(rdnn(n4), rdnn(n2)))))],extension(11)).
% 186.83/180.68 cnf('1.1.1.1.3.2.2',plain,[-(rdn_translate(n25, rdn_pos(rdn(rdnn(n5), rdnn(n2)))))],extension(5)).
% 186.83/180.68 cnf('1.1.1.1.3.2.3',plain,[-(rdn_positive_less(rdn(rdnn(n4), rdnn(n2)), rdn(rdnn(n5), rdnn(n2)))), rdn_positive_less(rdnn(n4), rdnn(n5)), rdn_non_zero(rdnn(n2))],extension(1,bind([[_26230, _26232, _26231], [n4, n5, rdnn(n2)]]))).
% 186.83/180.68 cnf('1.1.1.1.3.2.3.1',plain,[-(rdn_positive_less(rdnn(n4), rdnn(n5)))],extension(27)).
% 186.83/180.68 cnf('1.1.1.1.3.2.3.2',plain,[-(rdn_non_zero(rdnn(n2))), rdn_non_zero_digit(rdnn(n2))],extension(24,bind([[_26276], [n2]]))).
% 186.83/180.68 cnf('1.1.1.1.3.2.3.2.1',plain,[-(rdn_non_zero_digit(rdnn(n2)))],extension(17)).
% 186.83/180.68 cnf('1.1.1.1.4',plain,[-(accept_population(muslimcountrybhumanitarianorganization, muslim, n1))],extension(20)).
% 186.83/180.68 cnf('1.1.1.1.5',plain,[-(accept_population(muslimcountrybhumanitarianorganization, native, n0)), accept_city(muslimcountrybhumanitarianorganization, cityb)],extension(18,bind([[_17712], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.1.1.5.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, cityb)), accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5)],extension(15,bind([[_17305, _17308, _17306, _17307], [muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5]]))).
% 186.83/180.68 cnf('1.1.1.1.5.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5))],extension(8)).
% 186.83/180.68 cnf('1.1.2',plain,[-(accept_population(muslimcountrybhumanitarianorganization, atheist, n75)), accept_population(muslimcountrybhumanitarianorganization, atheist, n78), less(n75, n78)],extension(26,bind([[_17341, _17344, _17343, _17342], [muslimcountrybhumanitarianorganization, atheist, n75, n78]]))).
% 186.83/180.68 cnf('1.1.2.1',plain,[-(accept_population(muslimcountrybhumanitarianorganization, atheist, n78))],extension(2)).
% 186.83/180.68 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(29,bind([[_26302, _26303, _26304, _26305], [n75, n78, rdn(rdnn(n5), rdnn(n7)), rdn(rdnn(n8), rdnn(n7))]]))).
% 186.83/180.68 cnf('1.1.2.2.1',plain,[-(rdn_translate(n75, rdn_pos(rdn(rdnn(n5), rdnn(n7)))))],extension(22)).
% 186.83/180.68 cnf('1.1.2.2.2',plain,[-(rdn_translate(n78, rdn_pos(rdn(rdnn(n8), rdnn(n7)))))],extension(25)).
% 186.83/180.68 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(1,bind([[_26230, _26232, _26231], [n5, n8, rdnn(n7)]]))).
% 186.83/180.68 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(28,bind([[_26180, _26181, _26182], [n5, n6, n8]]))).
% 186.83/180.68 cnf('1.1.2.2.3.1.1',plain,[-(rdn_positive_less(rdnn(n5), rdnn(n6)))],extension(16)).
% 186.83/180.68 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(28,bind([[_26180, _26181, _26182], [n6, n7, n8]]))).
% 186.83/180.68 cnf('1.1.2.2.3.1.2.1',plain,[-(rdn_positive_less(rdnn(n6), rdnn(n7)))],extension(6)).
% 186.83/180.68 cnf('1.1.2.2.3.1.2.2',plain,[-(rdn_positive_less(rdnn(n7), rdnn(n8)))],extension(3)).
% 186.83/180.68 cnf('1.1.2.2.3.2',plain,[-(rdn_non_zero(rdnn(n7))), rdn_non_zero_digit(rdnn(n7))],extension(24,bind([[_26276], [n7]]))).
% 186.83/180.68 cnf('1.1.2.2.3.2.1',plain,[-(rdn_non_zero_digit(rdnn(n7)))],extension(13)).
% 186.83/180.68 cnf('1.1.3',plain,[-(accept_population(muslimcountrybhumanitarianorganization, muslim, n0)), accept_city(muslimcountrybhumanitarianorganization, coastvillage)],extension(10,bind([[_17577], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.3.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, coastvillage)), accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5)],extension(15,bind([[_17305, _17308, _17306, _17307], [muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5]]))).
% 186.83/180.68 cnf('1.1.3.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5))],extension(12)).
% 186.83/180.68 cnf('1.1.4',plain,[-(accept_population(muslimcountrybhumanitarianorganization, native, n0)), accept_city(muslimcountrybhumanitarianorganization, cityb)],extension(18,bind([[_17712], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.4.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, cityb)), accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5)],extension(15,bind([[_17305, _17308, _17306, _17307], [muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5]]))).
% 186.83/180.68 cnf('1.1.4.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, countrybhumanitarianorganization, cityb, n5))],extension(8)).
% 186.83/180.68 cnf('1.1.5',plain,[-(accept_population(muslimcountrybhumanitarianorganization, other, n0)), accept_city(muslimcountrybhumanitarianorganization, coastvillage)],extension(4,bind([[_17577], [muslimcountrybhumanitarianorganization]]))).
% 186.83/180.68 cnf('1.1.5.1',plain,[-(accept_city(muslimcountrybhumanitarianorganization, coastvillage)), accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5)],extension(15,bind([[_17305, _17308, _17306, _17307], [muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5]]))).
% 186.83/180.68 cnf('1.1.5.1.1',plain,[-(accept_team(muslimcountrybhumanitarianorganization, christiancountrychumanitarianorganization, coastvillage, n5))],extension(12)).
% 186.83/180.68 %-----------------------------------------------------
% 186.83/180.69
% 186.83/180.69 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------