%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : CSR115+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n007.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 : Fri Jul 15 03:18:10 EDT 2022 % Result : Theorem 0.46s 0.81s % Output : CNFRefutation 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.14 % Problem : CSR115+4 : TPTP v8.1.0. Released v4.0.0. % 0.13/0.15 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.16/0.37 % Computer : n007.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 600 % 0.16/0.37 % DateTime : Sat Jun 11 12:30:07 EDT 2022 % 0.16/0.37 % CPUTime : % 0.41/0.56 # SinE strategy is gf500_h_gu_R04_F100_L20000 % 0.41/0.56 # Auto-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN % 0.41/0.56 # and selection function SelectComplexExceptUniqMaxHorn. % 0.41/0.56 # % 0.41/0.56 # Presaturation interreduction done % 0.41/0.56 # Number of axioms: 402 Number of unprocessed: 328 % 0.41/0.56 # Tableaux proof search. % 0.41/0.56 # APR header successfully linked. % 0.41/0.56 # Hello from C++ % 0.44/0.60 # The folding up rule is enabled... % 0.44/0.60 # Local unification is enabled... % 0.44/0.60 # Any saturation attempts will use folding labels... % 0.44/0.60 # 328 beginning clauses after preprocessing and clausification % 0.44/0.60 # Creating start rules for all 1 conjectures. % 0.44/0.60 # There are 1 start rule candidates: % 0.44/0.60 # Found 165 unit axioms. % 0.44/0.60 # 1 start rule tableaux created. % 0.44/0.60 # 163 extension rule candidate clauses % 0.44/0.60 # 165 unit axiom clauses % 0.44/0.60 % 0.44/0.60 # Requested 8, 32 cores available to the main process. % 0.44/0.60 # There are not enough tableaux to fork, creating more from the initial 1 % 0.44/0.60 # Ran out of tableaux, making start rules for all clauses % 0.44/0.60 # Returning from population with 329 new_tableaux and 0 remaining starting tableaux. % 0.44/0.60 # We now have 329 tableaux to operate on % 0.46/0.81 # There were 1 total branch saturation attempts. % 0.46/0.81 # There were 0 of these attempts blocked. % 0.46/0.81 # There were 0 deferred branch saturation attempts. % 0.46/0.81 # There were 0 free duplicated saturations. % 0.46/0.81 # There were 1 total successful branch saturations. % 0.46/0.81 # There were 0 successful branch saturations in interreduction. % 0.46/0.81 # There were 0 successful branch saturations on the branch. % 0.46/0.81 # There were 1 successful branch saturations after the branch. % 0.46/0.81 # SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.81 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.81 # Begin clausification derivation % 0.46/0.81 % 0.46/0.81 # End clausification derivation % 0.46/0.81 # Begin listing active clauses obtained from FOF to CNF conversion % 0.46/0.81 cnf(i_0_39, hypothesis, (gener(mark_1_1,ge))). % 0.46/0.81 cnf(i_0_34, hypothesis, (gener(c2403,sp))). % 0.46/0.81 cnf(i_0_26, hypothesis, (gener(beitrag_1_1,ge))). % 0.46/0.81 cnf(i_0_17, hypothesis, (gener(c2409,gener_c))). % 0.46/0.81 cnf(i_0_10, hypothesis, (gener(million_1_1,ge))). % 0.46/0.81 cnf(i_0_5, hypothesis, (gener(c2590,gener_c))). % 0.46/0.81 cnf(i_0_158, plain, (subsort(X1,X1))). % 0.46/0.81 cnf(i_0_61, plain, (gener_less(ge,gener_c))). % 0.46/0.81 cnf(i_0_62, plain, (gener_less(sp,gener_c))). % 0.46/0.81 cnf(i_0_31, hypothesis, (varia(c2403,varia_c))). % 0.46/0.81 cnf(i_0_23, hypothesis, (varia(beitrag_1_1,varia_c))). % 0.46/0.81 cnf(i_0_14, hypothesis, (varia(c2409,con))). % 0.46/0.81 cnf(i_0_2, hypothesis, (varia(c2590,varia_c))). % 0.46/0.81 cnf(i_0_51, plain, (varia_less(var,varia_c))). % 0.46/0.81 cnf(i_0_52, plain, (varia_less(con,varia_c))). % 0.46/0.81 cnf(i_0_41, hypothesis, (fact(c2383,real))). % 0.46/0.81 cnf(i_0_35, hypothesis, (fact(c2403,real))). % 0.46/0.81 cnf(i_0_27, hypothesis, (fact(beitrag_1_1,real))). % 0.46/0.81 cnf(i_0_18, hypothesis, (fact(c2409,real))). % 0.46/0.81 cnf(i_0_6, hypothesis, (fact(c2590,real))). % 0.46/0.81 cnf(i_0_65, plain, (fact_less(real,fact_c))). % 0.46/0.81 cnf(i_0_97, plain, (fact_less(nonreal,fact_c))). % 0.46/0.81 cnf(i_0_98, plain, (fact_less(hypo,fact_c))). % 0.46/0.81 cnf(i_0_32, hypothesis, (refer(c2403,indet))). % 0.46/0.81 cnf(i_0_24, hypothesis, (refer(beitrag_1_1,refer_c))). % 0.46/0.81 cnf(i_0_15, hypothesis, (refer(c2409,refer_c))). % 0.46/0.81 cnf(i_0_3, hypothesis, (refer(c2590,refer_c))). % 0.46/0.81 cnf(i_0_55, plain, (refer_less(det,refer_c))). % 0.46/0.81 cnf(i_0_56, plain, (refer_less(indet,refer_c))). % 0.46/0.81 cnf(i_0_37, hypothesis, (card(c2403,int1))). % 0.46/0.81 cnf(i_0_29, hypothesis, (card(beitrag_1_1,int1))). % 0.46/0.81 cnf(i_0_20, hypothesis, (card(c2409,card_c))). % 0.46/0.81 cnf(i_0_12, hypothesis, (card(c2406,int12))). % 0.46/0.81 cnf(i_0_8, hypothesis, (card(c2590,card_c))). % 0.46/0.81 cnf(i_0_33, hypothesis, (quant(c2403,one))). % 0.46/0.81 cnf(i_0_25, hypothesis, (quant(beitrag_1_1,one))). % 0.46/0.81 cnf(i_0_16, hypothesis, (quant(c2409,quant_c))). % 0.46/0.81 cnf(i_0_4, hypothesis, (quant(c2590,quant_c))). % 0.46/0.81 cnf(i_0_36, hypothesis, (etype(c2403,int0))). % 0.46/0.81 cnf(i_0_28, hypothesis, (etype(beitrag_1_1,int0))). % 0.46/0.81 cnf(i_0_19, hypothesis, (etype(c2409,etype_c))). % 0.46/0.81 cnf(i_0_7, hypothesis, (etype(c2590,etype_c))). % 0.46/0.81 cnf(i_0_42, hypothesis, (sort(c2383,me))). % 0.46/0.81 cnf(i_0_40, hypothesis, (sort(mark_1_1,me))). % 0.46/0.81 cnf(i_0_38, hypothesis, (sort(c2403,io))). % 0.46/0.81 cnf(i_0_30, hypothesis, (sort(beitrag_1_1,io))). % 0.46/0.81 cnf(i_0_22, hypothesis, (sort(c2409,co))). % 0.46/0.81 cnf(i_0_21, hypothesis, (sort(c2409,m))). % 0.46/0.81 cnf(i_0_13, hypothesis, (sort(c2406,nu))). % 0.46/0.81 cnf(i_0_11, hypothesis, (sort(million_1_1,me))). % 0.46/0.81 cnf(i_0_9, hypothesis, (sort(c2590,ent))). % 0.46/0.81 cnf(i_0_82, plain, (direct_subsort(o,ent))). % 0.46/0.81 cnf(i_0_91, plain, (direct_subsort(co,o))). % 0.46/0.81 cnf(i_0_92, plain, (direct_subsort(s,co))). % 0.46/0.81 cnf(i_0_93, plain, (direct_subsort(d,co))). % 0.46/0.81 cnf(i_0_160, plain, (direct_subsort(ab,o))). % 0.46/0.81 cnf(i_0_191, plain, (direct_subsort(at,ab))). % 0.46/0.81 cnf(i_0_314, plain, (direct_subsort(oa,at))). % 0.46/0.81 cnf(i_0_315, plain, (direct_subsort(na,at))). % 0.46/0.81 cnf(i_0_95, plain, (direct_subsort(io,ab))). % 0.46/0.81 cnf(i_0_192, plain, (direct_subsort(abs,ab))). % 0.46/0.81 cnf(i_0_316, plain, (direct_subsort(ad,abs))). % 0.46/0.81 cnf(i_0_317, plain, (direct_subsort(as,abs))). % 0.46/0.81 cnf(i_0_83, plain, (direct_subsort(si,ent))). % 0.46/0.81 cnf(i_0_161, plain, (direct_subsort(st,si))). % 0.46/0.81 cnf(i_0_162, plain, (direct_subsort(dy,si))). % 0.46/0.81 cnf(i_0_282, plain, (direct_subsort(da,dy))). % 0.46/0.81 cnf(i_0_283, plain, (direct_subsort(dn,dy))). % 0.46/0.81 cnf(i_0_84, plain, (direct_subsort(sd,ent))). % 0.46/0.81 cnf(i_0_163, plain, (direct_subsort(t,sd))). % 0.46/0.81 cnf(i_0_164, plain, (direct_subsort(md,sd))). % 0.46/0.81 cnf(i_0_165, plain, (direct_subsort(l,sd))). % 0.46/0.81 cnf(i_0_85, plain, (direct_subsort(ql,ent))). % 0.46/0.81 cnf(i_0_166, plain, (direct_subsort(p,ql))). % 0.46/0.81 cnf(i_0_284, plain, (direct_subsort(gq,p))). % 0.46/0.81 cnf(i_0_393, plain, (direct_subsort(mq,gq))). % 0.46/0.81 cnf(i_0_394, plain, (direct_subsort(nq,gq))). % 0.46/0.81 cnf(i_0_285, plain, (direct_subsort(tq,p))). % 0.46/0.81 cnf(i_0_167, plain, (direct_subsort(rq,ql))). % 0.46/0.81 cnf(i_0_168, plain, (direct_subsort(fq,ql))). % 0.46/0.81 cnf(i_0_286, plain, (direct_subsort(aq,fq))). % 0.46/0.81 cnf(i_0_287, plain, (direct_subsort(oq,fq))). % 0.46/0.81 cnf(i_0_86, plain, (direct_subsort(gr,ent))). % 0.46/0.81 cnf(i_0_169, plain, (direct_subsort(lg,gr))). % 0.46/0.81 cnf(i_0_170, plain, (direct_subsort(ng,gr))). % 0.46/0.81 cnf(i_0_87, plain, (direct_subsort(qn,ent))). % 0.46/0.81 cnf(i_0_90, plain, (direct_subsort(m,qn))). % 0.46/0.81 cnf(i_0_88, plain, (direct_subsort(me,qn))). % 0.46/0.81 cnf(i_0_171, plain, (direct_subsort(qf,qn))). % 0.46/0.81 cnf(i_0_172, plain, (direct_subsort(nn,qf))). % 0.46/0.81 cnf(i_0_89, plain, (direct_subsort(nu,qf))). % 0.46/0.81 cnf(i_0_371, plain, (sub(herrscher__1_1,an_f__374hrer_1_1))). % 0.46/0.81 cnf(i_0_370, plain, (sub(be_gr__374nder_1_1,an_f__374hrer_1_1))). % 0.46/0.81 cnf(i_0_281, plain, (sub(euland_1_1,land_1_1))). % 0.46/0.81 cnf(i_0_240, plain, (sub(filmpreis_1_1,preis_1_1))). % 0.46/0.81 cnf(i_0_400, plain, (sub(fruehjahr_1_1,jahr__1_1))). % 0.46/0.81 cnf(i_0_390, plain, (sub(landesvater_1_1,oberhaupt_1_1))). % 0.46/0.81 cnf(i_0_361, plain, (sub(literaturnobelpreis_1_1,nobelpreis_1_1))). % 0.46/0.81 cnf(i_0_241, plain, (sub(singlepreis_1_1,preis_1_1))). % 0.46/0.81 cnf(i_0_399, plain, (sub(unkinderhilfswerk_1_1,hilfswerk_1_1))). % 0.46/0.81 cnf(i_0_319, plain, (sub(killerin_1_1,killer_1_1))). % 0.46/0.81 cnf(i_0_397, plain, (sub(kriegerin_1_1,krieger__1_1))). % 0.46/0.81 cnf(i_0_391, plain, (sub(regierungschefin_1_1,landesvater_1_1))). % 0.46/0.81 cnf(i_0_401, plain, (sub(schiller_jahr_1_1,jahr__1_1))). % 0.46/0.81 cnf(i_0_46, hypothesis, (sub(c2383,mark_1_1))). % 0.46/0.81 cnf(i_0_45, hypothesis, (sub(c2403,beitrag_1_1))). % 0.46/0.81 cnf(i_0_380, plain, (chea(befahren_1_1,befahren_2_1))). % 0.46/0.81 cnf(i_0_381, plain, (chea(befahren_1_1,befahrung_1_1))). % 0.46/0.81 cnf(i_0_382, plain, (chea(befahren_1_1,betreten_3_1))). % 0.46/0.81 cnf(i_0_383, plain, (chea(befahren_1_1,betretung_1_1))). % 0.46/0.81 cnf(i_0_330, plain, (chea(aufrufen_1_1,aufruf_1_1))). % 0.46/0.81 cnf(i_0_363, plain, (chea(lancieren_1_1,lancieren_2_1))). % 0.46/0.81 cnf(i_0_364, plain, (chea(lancieren_1_1,lancierung_1_1))). % 0.46/0.81 cnf(i_0_332, plain, (chea(propagieren_1_1,propagation_1_1))). % 0.46/0.81 cnf(i_0_333, plain, (chea(propagieren_1_1,propagieren_2_1))). % 0.46/0.81 cnf(i_0_334, plain, (chea(propagieren_1_1,propagierung_1_1))). % 0.46/0.81 cnf(i_0_362, plain, (chea(auszeichnen_1_1,auszeichnung_1_2))). % 0.46/0.81 cnf(i_0_350, plain, (chea(aufstellen_1_3,nomination_1_1))). % 0.46/0.81 cnf(i_0_351, plain, (chea(aufstellen_1_3,nominierung_1_1))). % 0.46/0.81 cnf(i_0_200, plain, (chea(abmurksen_1_1,toetung_1_1))). % 0.46/0.81 cnf(i_0_196, plain, (chea(sterben_1_1,ableben_2_1))). % 0.46/0.81 cnf(i_0_217, plain, (chea(abknallen_1_1,abknallen_2_1))). % 0.46/0.81 cnf(i_0_218, plain, (chea(abknallen_1_1,erschie__337en_2_1))). % 0.46/0.81 cnf(i_0_219, plain, (chea(abknallen_1_1,erschie__337ung_1_1))). % 0.46/0.81 cnf(i_0_220, plain, (chea(abknallen_1_1,totschie__337en_2_1))). % 0.46/0.81 cnf(i_0_242, plain, (chea(verunfallen_1_1,verungl__374cken_2_1))). % 0.46/0.81 cnf(i_0_318, plain, (chea(ableben_1_1,ableben_2_1))). % 0.46/0.81 cnf(i_0_384, plain, (chea(besitzen_1_1,besitzen_2_1))). % 0.46/0.81 cnf(i_0_385, plain, (chea(besitzen_1_1,besitzung_1_1))). % 0.46/0.81 cnf(i_0_402, plain, (chea(erleben_1_1,erleben_2_1))). % 0.46/0.81 cnf(i_0_320, plain, (chea(totschlagen_1_1,toetung_1_1))). % 0.46/0.81 cnf(i_0_303, plain, (assoc(euland_1_1,eu_0))). % 0.46/0.81 cnf(i_0_365, plain, (assoc(filmpreis_1_1,film_1_1))). % 0.46/0.81 cnf(i_0_279, plain, (assoc(landesvater_1_1,land_1_1))). % 0.46/0.81 cnf(i_0_366, plain, (assoc(singlepreis_1_1,single_1_1))). % 0.46/0.81 cnf(i_0_398, plain, (assoc(unkinderhilfswerk_1_1,kind_1_1))). % 0.46/0.81 cnf(i_0_304, plain, (assoc(unkinderhilfswerk_1_1,l__344ndergemeinschaft_1_1))). % 0.46/0.81 cnf(i_0_309, plain, (temporal_attribute(jahr__1_1,dummy_0))). % 0.46/0.81 cnf(i_0_310, plain, (temporal_attribute(monat_1_1,dummy_0))). % 0.46/0.81 cnf(i_0_311, plain, (temporal_attribute(tag_1_1,dummy_0))). % 0.46/0.81 cnf(i_0_312, plain, (temporal_attribute(woche_1_1,dummy_0))). % 0.46/0.81 cnf(i_0_280, plain, (local_in_stereotype(stadt__1_1,land_1_1))). % 0.46/0.81 cnf(i_0_288, plain, (local_in_stereotype(sekretariat_1_1,stadt__1_1))). % 0.46/0.81 cnf(i_0_331, plain, (purp(lebenshaus_1_1,leben_2_5))). % 0.46/0.81 cnf(i_0_289, plain, (ort_adjektiv_ort(m__374nchener_1_1,m__374nchen_0))). % 0.46/0.81 cnf(i_0_290, plain, (ort_adjektiv_ort(salzburger_1_1,salzburg_0))). % 0.46/0.81 cnf(i_0_301, plain, (partei_adj_partei(sozialdemokratisch__1_1,spd_0))). % 0.46/0.81 cnf(i_0_313, plain, (distrib_obj(erleben_1_1,dummy_0))). % 0.46/0.81 cnf(i_0_387, plain, (impl(national__1_1,konservativ__1_1))). % 0.46/0.81 cnf(i_0_388, plain, (impl(national__1_1,patriotisch__1_1))). % 0.46/0.81 cnf(i_0_386, plain, (impl(chauvinistisch__1_1,national__1_1))). % 0.46/0.81 cnf(i_0_199, plain, (agtrel(abmurksen_1_1,killer_1_1))). % 0.46/0.81 cnf(i_0_272, plain, (scarrel(besitzen_1_1,besitzer__1_1))). % 0.46/0.81 cnf(i_0_187, plain, (named_entity_type(eu_0,organisation_1_1))). % 0.46/0.81 cnf(i_0_188, plain, (named_entity_type(l__344ndergemeinschaft_1_1,organisation_1_1))). % 0.46/0.81 cnf(i_0_305, plain, (named_entity_type(cdu_0,partei_1_1))). % 0.46/0.81 cnf(i_0_306, plain, (named_entity_type(csu_0,partei_1_1))). % 0.46/0.81 cnf(i_0_307, plain, (named_entity_type(fdp_0,partei_1_1))). % 0.46/0.81 cnf(i_0_308, plain, (named_entity_type(kpd_0,partei_1_1))). % 0.46/0.81 cnf(i_0_302, plain, (named_entity_type(oas_0,organisation_1_1))). % 0.46/0.81 cnf(i_0_189, plain, (named_entity_type(spd_0,partei_1_1))). % 0.46/0.81 cnf(i_0_44, hypothesis, (quant_p3(c2409,c2406,million_1_1))). % 0.46/0.81 cnf(i_0_358, plain, (member(X1,cons(X1,X2)))). % 0.46/0.81 cnf(i_0_43, hypothesis, (tupl_p4(c2590,c2383,c2403,c2409))). % 0.46/0.81 cnf(i_0_1, negated_conjecture, (~obj(X1,X2))). % 0.46/0.81 cnf(i_0_63, plain, (has_fact_leq(X1,X2)|~fact(X1,X2))). % 0.46/0.81 cnf(i_0_257, plain, (flp(X1,X2)|~an(X1,X2))). % 0.46/0.81 cnf(i_0_256, plain, (flp(X1,X2)|~bei(X1,X2))). % 0.46/0.81 cnf(i_0_59, plain, (has_gener_leq(X1,X2)|~gener(X1,X2))). % 0.46/0.81 cnf(i_0_49, plain, (has_varia_leq(X1,X2)|~varia(X1,X2))). % 0.46/0.81 cnf(i_0_53, plain, (has_refer_leq(X1,X2)|~refer(X1,X2))). % 0.46/0.81 cnf(i_0_79, plain, (has_card_leq(X1,X2)|~card(X1,X2))). % 0.46/0.81 cnf(i_0_80, plain, (has_card_leq(X1,card_c)|~card(X1,X2))). % 0.46/0.81 cnf(i_0_57, plain, (has_quant_leq(X1,X2)|~quant(X1,X2))). % 0.46/0.81 cnf(i_0_77, plain, (has_etype_leq(X1,X2)|~etype(X1,X2))). % 0.46/0.81 cnf(i_0_249, plain, (assoc(X1,X2)|~attch(X2,X1))). % 0.46/0.81 cnf(i_0_258, plain, (flp(X1,X2)|~in(X1,X2))). % 0.46/0.81 cnf(i_0_58, plain, (has_quant_leq(X1,quant_c)|~quant(X1,X2))). % 0.46/0.81 cnf(i_0_78, plain, (has_etype_leq(X1,etype_c)|~etype(X1,X2))). % 0.46/0.81 cnf(i_0_273, plain, (prop(X1,national__1_1)|~attch(X2,X1)|~sub(X2,land_1_1))). % 0.46/0.81 cnf(i_0_376, plain, (subs(esk49_2(X1,X2),befinden_1_2)|~loc(X1,X2))). % 0.46/0.81 cnf(i_0_360, plain, (benf(X1,X2)|~assoc(X1,X2)|~sub(X1,nobelpreis_1_1))). % 0.46/0.81 cnf(i_0_369, plain, (itms(X1,X2,X3)|~itms(X1,X3,X2))). % 0.46/0.81 cnf(i_0_60, plain, (has_gener_leq(X1,X2)|~gener_less(X3,X2)|~gener(X1,X3))). % 0.46/0.81 cnf(i_0_50, plain, (has_varia_leq(X1,X2)|~varia_less(X3,X2)|~varia(X1,X3))). % 0.46/0.81 cnf(i_0_352, plain, (subr(esk46_2(X1,X2),sub_0)|~sub(X1,X2))). % 0.46/0.81 cnf(i_0_359, plain, (member(X1,cons(X2,X3))|~member(X1,X3))). % 0.46/0.81 cnf(i_0_378, plain, (loc(esk49_2(X1,X2),X2)|~loc(X1,X2))). % 0.46/0.81 cnf(i_0_377, plain, (scar(esk49_2(X1,X2),X1)|~loc(X1,X2))). % 0.46/0.81 cnf(i_0_354, plain, (arg1(esk46_2(X1,X2),X1)|~sub(X1,X2))). % 0.46/0.81 cnf(i_0_64, plain, (has_fact_leq(X1,X2)|~fact_less(X3,X2)|~fact(X1,X3))). % 0.46/0.81 cnf(i_0_353, plain, (arg2(esk46_2(X1,X2),X2)|~sub(X1,X2))). % 0.46/0.81 cnf(i_0_54, plain, (has_refer_leq(X1,X2)|~refer_less(X3,X2)|~refer(X1,X3))). % 0.46/0.81 cnf(i_0_159, plain, (subsort(X1,X2)|~direct_subsort(X1,X3)|~subsort(X3,X2))). % 0.46/0.81 cnf(i_0_81, plain, (sort_leq(X1,X2)|~subsort(X3,X2)|~sort(X1,X3))). % 0.46/0.81 cnf(i_0_96, plain, (sub(X1,X2)|~sub(X3,X2)|~sub(X1,X3))). % 0.46/0.81 cnf(i_0_75, plain, (~loc(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.81 cnf(i_0_243, plain, (pred(X1,X2)|~pred(X1,X3)|~sub(X3,X2))). % 0.46/0.81 cnf(i_0_99, plain, (subs(X1,X2)|~subs(X3,X2)|~subs(X1,X3))). % 0.46/0.81 cnf(i_0_130, plain, (preds(X1,X2)|~preds(X1,X3)|~subs(X3,X2))). % 0.46/0.81 cnf(i_0_104, plain, (temp(X1,X2)|~temp(X3,X2)|~hsit(X3,X1))). % 0.46/0.81 cnf(i_0_193, plain, (temp(X1,X2)|~rslt(X3,X1)|~temp(X3,X2))). % 0.46/0.81 cnf(i_0_194, plain, (temp(X1,X2)|~chea(X3,X1)|~temp(X3,X2))). % 0.46/0.81 cnf(i_0_195, plain, (temp(X1,X2)|~chea(X1,X3)|~temp(X3,X2))). % 0.46/0.81 cnf(i_0_105, plain, (loc(X1,X2)|~loc(X3,X2)|~hsit(X3,X1))). % 0.46/0.81 cnf(i_0_149, plain, (loc(X1,X2)|~chea(X3,X1)|~loc(X3,X2))). % 0.46/0.81 cnf(i_0_106, plain, (subs(esk5_2(X1,X2),sterben_1_1)|~aff(X2,X1)|~subs(X2,abmurksen_1_1))). % 0.46/0.81 cnf(i_0_150, plain, (loc(X1,X2)|~chea(X1,X3)|~loc(X3,X2))). % 0.46/0.81 cnf(i_0_198, plain, (aff(X1,X2)|~aff(X3,X2)|~chea(X1,X3))). % 0.46/0.81 cnf(i_0_197, plain, (aff(X1,X2)|~aff(X3,X2)|~chea(X3,X1))). % 0.46/0.81 cnf(i_0_202, plain, (agt(X1,X2)|~agt(X3,X2)|~chea(X1,X3))). % 0.46/0.81 cnf(i_0_201, plain, (agt(X1,X2)|~agt(X3,X2)|~chea(X3,X1))). % 0.46/0.81 cnf(i_0_121, plain, (subs(esk9_2(X1,X2),sterben_1_1)|~exp(X2,X1)|~subs(X2,verunfallen_1_1))). % 0.46/0.81 cnf(i_0_70, plain, (hsit(X1,esk1_1(X1))|~subs(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.81 cnf(i_0_67, plain, (hsit(X1,esk1_1(X1))|~preds(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.81 cnf(i_0_71, plain, (exp(esk1_1(X1),X1)|~subs(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.81 cnf(i_0_250, plain, (subs(esk28_2(X1,X2),angeh__366ren_1_1)|~attch(X2,X1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_69, plain, (subs(esk1_1(X1),eintreffen_1_2)|~subs(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.82 cnf(i_0_66, plain, (subs(esk1_1(X1),eintreffen_1_2)|~preds(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.82 cnf(i_0_68, plain, (exp(esk1_1(X1),X1)|~preds(X1,X2)|~has_fact_leq(X1,real))). % 0.46/0.82 cnf(i_0_107, plain, (hsit(X1,esk5_2(X2,X1))|~aff(X1,X2)|~subs(X1,abmurksen_1_1))). % 0.46/0.82 cnf(i_0_379, plain, (loc(X1,X2)|~scar(X3,X1)|~loc(X3,X2)|~subs(X3,befinden_1_2))). % 0.46/0.82 cnf(i_0_122, plain, (hsit(X1,esk9_2(X2,X1))|~exp(X1,X2)|~subs(X1,verunfallen_1_1))). % 0.46/0.82 cnf(i_0_108, plain, (aff(esk5_2(X1,X2),X1)|~aff(X2,X1)|~subs(X2,abmurksen_1_1))). % 0.46/0.82 cnf(i_0_123, plain, (aff(esk9_2(X1,X2),X1)|~exp(X2,X1)|~subs(X2,verunfallen_1_1))). % 0.46/0.82 cnf(i_0_252, plain, (scar(esk28_2(X1,X2),X2)|~attch(X2,X1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_251, plain, (sspe(esk28_2(X1,X2),X1)|~attch(X2,X1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_154, plain, (sub(esk11_3(X1,X2,X3),land_1_1)|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_153, plain, (sub(esk12_3(X1,X2,X3),name_1_1)|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_175, plain, (sub(esk14_3(X1,X2,X3),name_1_1)|~ort_adjektiv_ort(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_174, plain, (sub(esk16_3(X1,X2,X3),stadt__1_1)|~ort_adjektiv_ort(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_125, plain, (sub(X1,X2)|~ctxt(X3,X4)|~exp(X3,X1)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_182, plain, (sub(esk18_3(X1,X2,X3),einrichtung_1_2)|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_72, plain, (hsit(X1,X2)|~exp(X1,X2)|~preds(X2,X3)|~subs(X1,eintreffen_1_2)|~has_fact_leq(X2,real))). % 0.46/0.82 cnf(i_0_389, plain, (prop_p3(X1,X2,X3)|~impl(X4,X2)|~prop_p3(X1,X4,X3))). % 0.46/0.82 cnf(i_0_126, plain, (sub(X1,X2)|~ctxt(X3,X4)|~agt(X3,X1)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_124, plain, (sub(X1,X2)|~mexp(X3,X1)|~ctxt(X3,X4)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_181, plain, (sub(esk19_3(X1,X2,X3),name_1_1)|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_180, plain, (subs(esk17_3(X1,X2,X3),angeh__366ren_1_1)|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_155, plain, (loc(X1,esk13_3(X1,X2,X3))|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_176, plain, (loc(X1,esk15_3(X2,X3,X1))|~ort_adjektiv_ort(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_245, plain, (pred(esk27_3(X1,X2,X3),X3)|~state_adjective_inhabitant_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_128, plain, (pred(X1,X2)|~ctxt(X3,X4)|~exp(X3,X1)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_102, plain, (subs(esk4_3(X1,X2,X3),X3)|~chea(X3,X2)|~subs(X1,X2))). % 0.46/0.82 cnf(i_0_129, plain, (pred(X1,X2)|~ctxt(X3,X4)|~agt(X3,X1)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_127, plain, (pred(X1,X2)|~mexp(X3,X1)|~ctxt(X3,X4)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_136, plain, (attch(X1,X2)|~in(X3,X1)|~loc(X2,X3)|~subs(X2,X4))). % 0.46/0.82 cnf(i_0_134, plain, (attch(X1,X2)|~an(X3,X1)|~loc(X2,X3)|~subs(X2,X4))). % 0.46/0.82 cnf(i_0_246, plain, (attch(esk27_3(X1,X2,X3),X1)|~state_adjective_inhabitant_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_103, plain, (chea(esk4_3(X1,X2,X3),X1)|~chea(X3,X2)|~subs(X1,X2))). % 0.46/0.82 cnf(i_0_184, plain, (scar(esk17_3(X1,X2,X3),X3)|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_152, plain, (val(esk12_3(X1,X2,X3),X3)|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_173, plain, (val(esk14_3(X1,X2,X3),X2)|~ort_adjektiv_ort(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_132, plain, (attch(X1,X2)|~bei(X3,X1)|~loc(X2,X3)|~subs(X2,X4))). % 0.46/0.82 cnf(i_0_179, plain, (val(esk19_3(X1,X2,X3),X2)|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_135, plain, (attch(X1,X2)|~in(X3,X1)|~loc(X2,X3)|~preds(X2,X4))). % 0.46/0.82 cnf(i_0_133, plain, (attch(X1,X2)|~an(X3,X1)|~loc(X2,X3)|~preds(X2,X4))). % 0.46/0.82 cnf(i_0_131, plain, (attch(X1,X2)|~bei(X3,X1)|~loc(X2,X3)|~preds(X2,X4))). % 0.46/0.82 cnf(i_0_244, plain, (prop(X1,X2)|~state_adjective_inhabitant_binding(X2,X3)|~attch(X4,X1)|~pred(X4,X3))). % 0.46/0.82 cnf(i_0_101, plain, (chea(X1,esk3_2(X1,X2))|~chea(X3,X2)|~subs(X1,X3))). % 0.46/0.82 cnf(i_0_100, plain, (subs(esk3_2(X1,X2),X2)|~chea(X3,X2)|~subs(X1,X3))). % 0.46/0.82 cnf(i_0_253, plain, (subs(esk29_2(X1,X2),angeh__366ren_1_1)|~attch(X1,X2)|~sub(X2,an_f__374hrer_1_1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_255, plain, (scar(esk29_2(X1,X2),X2)|~attch(X1,X2)|~sub(X2,an_f__374hrer_1_1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_73, plain, (hsit(X1,X2)|~exp(X1,X2)|~subs(X1,eintreffen_1_2)|~subs(X2,X3)|~has_fact_leq(X2,real))). % 0.46/0.82 cnf(i_0_254, plain, (sspe(esk29_2(X1,X2),X1)|~attch(X1,X2)|~sub(X2,an_f__374hrer_1_1)|~sub(X1,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_395, plain, (sub(X1,X2)|~has_sort_leq(X3,oq)|~pmod(X4,X3,X2)|~sub(X1,X4))). % 0.46/0.82 cnf(i_0_396, plain, (pred(X1,X2)|~has_sort_leq(X3,oq)|~pmod(X4,X3,X2)|~pred(X1,X4))). % 0.46/0.82 cnf(i_0_247, plain, (sub(X1,X2)|~itms(X3,X1,X4)|~pred(X3,X2)|~sub(X1,X5))). % 0.46/0.82 cnf(i_0_248, plain, (pred(X1,X2)|~itms(X3,X1,X4)|~pred(X1,X5)|~pred(X3,X2))). % 0.46/0.82 cnf(i_0_296, plain, (~sspe(X1,X2)|~scar(X1,X3)|~subs(X1,angeh__366ren_1_1))). % 0.46/0.82 cnf(i_0_337, plain, (~arg2(X1,X2)|~arg1(X1,X3)|~subs(X1,hei__337en_1_1))). % 0.46/0.82 cnf(i_0_345, plain, (~subr(X1,sub_0)|~arg2(X1,X2)|~arg1(X1,X3))). % 0.46/0.82 cnf(i_0_190, plain, (temp(X1,X2)|~temporal_attribute(X3,dummy_0)|~attr(X4,X2)|~temp(X1,X4)|~sub(X2,X3))). % 0.46/0.82 cnf(i_0_278, plain, (attch(esk34_3(X1,X2,X3),X1)|~prop_p3(X1,X2,X4)|~state_adjective_state_binding(X2,X3))). % 0.46/0.82 cnf(i_0_274, plain, (val(esk35_3(X1,X2,X3),X3)|~prop_p3(X1,X2,X4)|~state_adjective_state_binding(X2,X3))). % 0.46/0.82 cnf(i_0_94, plain, (sub(X1,X2)|~named_entity_type(X3,X2)|~val(X4,X3)|~attr(X1,X4)|~sub(X4,name_1_1)|~has_etype_leq(X1,int0))). % 0.46/0.82 cnf(i_0_110, plain, (hsit(X1,esk6_3(X2,X1,X3))|~agt(X1,X2)|~aff(X1,X3)|~subs(X1,abknallen_1_1))). % 0.46/0.82 cnf(i_0_205, plain, (hsit(X1,esk20_3(X1,X2,X3))|~mcont(X1,X3)|~agt(X1,X2)|~subs(X1,propagieren_1_1))). % 0.46/0.82 cnf(i_0_276, plain, (sub(esk34_3(X1,X2,X3),land_1_1)|~prop_p3(X1,X2,X4)|~state_adjective_state_binding(X2,X3))). % 0.46/0.82 cnf(i_0_275, plain, (sub(esk35_3(X1,X2,X3),name_1_1)|~prop_p3(X1,X2,X4)|~state_adjective_state_binding(X2,X3))). % 0.46/0.82 cnf(i_0_213, plain, (sub(X1,X2)|~agtrel(X3,X2)|~agt(X4,X1)|~rslt(X4,X5)|~subs(X4,X3)|~sub(X4,X3))). % 0.46/0.82 cnf(i_0_109, plain, (subs(esk6_3(X1,X2,X3),abmurksen_1_1)|~agt(X2,X1)|~aff(X2,X3)|~subs(X2,abknallen_1_1))). % 0.46/0.82 cnf(i_0_203, plain, (subs(esk20_3(X1,X2,X3),aufrufen_1_1)|~mcont(X1,X3)|~agt(X1,X2)|~subs(X1,propagieren_1_1))). % 0.46/0.82 cnf(i_0_215, plain, (pred(X1,X2)|~agtrel(X3,X2)|~agt(X4,X1)|~rslt(X4,X5)|~subs(X4,X3)|~pred(X4,X3))). % 0.46/0.82 cnf(i_0_112, plain, (aff(esk6_3(X1,X2,X3),X3)|~agt(X2,X1)|~aff(X2,X3)|~subs(X2,abknallen_1_1))). % 0.46/0.82 cnf(i_0_111, plain, (agt(esk6_3(X1,X2,X3),X1)|~agt(X2,X1)|~aff(X2,X3)|~subs(X2,abknallen_1_1))). % 0.46/0.82 cnf(i_0_206, plain, (agt(esk20_3(X1,X2,X3),X2)|~mcont(X1,X3)|~agt(X1,X2)|~subs(X1,propagieren_1_1))). % 0.46/0.82 cnf(i_0_214, plain, (attch(X1,X2)|~agtrel(X3,X4)|~agt(X5,X1)|~rslt(X5,X2)|~subs(X5,X3)|~sub(X5,X3))). % 0.46/0.82 cnf(i_0_204, plain, (purp(esk20_3(X1,X2,X3),X3)|~mcont(X1,X3)|~agt(X1,X2)|~subs(X1,propagieren_1_1))). % 0.46/0.82 cnf(i_0_148, plain, (~scarrel(X1,X2)|~attch(X3,X4)|~sub(X3,X2))). % 0.46/0.82 cnf(i_0_142, plain, (~scarrel(X1,X2)|~attch(X3,X4)|~pred(X3,X2))). % 0.46/0.82 cnf(i_0_145, plain, (~scarrel(X1,X2)|~attch(X3,X4)|~subs(X3,X2))). % 0.46/0.82 cnf(i_0_139, plain, (~scarrel(X1,X2)|~attch(X3,X4)|~preds(X3,X2))). % 0.46/0.82 cnf(i_0_216, plain, (attch(X1,X2)|~agtrel(X3,X4)|~agt(X5,X1)|~rslt(X5,X2)|~subs(X5,X3)|~pred(X5,X3))). % 0.46/0.82 cnf(i_0_156, plain, (attr(esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_367, plain, (agt(X1,X2)|~distrib_agt(X3,X4)|~itms(X5,X2,X6)|~agt(X1,X5)|~subs(X1,X3))). % 0.46/0.82 cnf(i_0_177, plain, (attr(esk16_3(X1,X2,X3),esk14_3(X1,X2,X3))|~ort_adjektiv_ort(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_185, plain, (attr(esk18_3(X1,X2,X3),esk19_3(X1,X2,X3))|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_210, plain, (subs(esk21_4(X1,X2,X3,X4),X1)|~agtrel(X1,X2)|~attch(X4,X3)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_207, plain, (subs(esk21_4(X1,X2,X3,X4),X1)|~agtrel(X1,X2)|~attch(X4,X3)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_211, plain, (rslt(esk21_4(X1,X2,X3,X4),X3)|~agtrel(X1,X2)|~attch(X4,X3)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_208, plain, (rslt(esk21_4(X1,X2,X3,X4),X3)|~agtrel(X1,X2)|~attch(X4,X3)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_157, plain, (in(esk13_3(X1,X2,X3),esk11_3(X1,X2,X3))|~state_adjective_state_binding(X2,X3)|~prop(X1,X2))). % 0.46/0.82 cnf(i_0_151, plain, (prop(X1,X2)|~state_adjective_state_binding(X2,X3)|~val(X4,X3)|~in(X5,X6)|~attr(X6,X4)|~loc(X1,X5)|~sub(X4,name_1_1)|~sub(X6,land_1_1))). % 0.46/0.82 cnf(i_0_178, plain, (in(esk15_3(X1,X2,X3),esk16_3(X1,X2,X3))|~ort_adjektiv_ort(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_212, plain, (agt(esk21_4(X1,X2,X3,X4),X4)|~agtrel(X1,X2)|~attch(X4,X3)|~sub(X4,X2))). % 0.46/0.82 cnf(i_0_209, plain, (agt(esk21_4(X1,X2,X3,X4),X4)|~agtrel(X1,X2)|~attch(X4,X3)|~pred(X4,X2))). % 0.46/0.82 cnf(i_0_266, plain, (scar(esk32_3(X1,X2,X3),X3)|~in(X1,X2)|~loc(X3,X1)|~sub(X3,mitglied_1_1)|~sub(X2,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_265, plain, (sspe(esk32_3(X1,X2,X3),X2)|~in(X1,X2)|~loc(X3,X1)|~sub(X3,mitglied_1_1)|~sub(X2,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_183, plain, (sspe(esk17_3(X1,X2,X3),esk18_3(X1,X2,X3))|~partei_adj_partei(X1,X2)|~prop(X3,X1))). % 0.46/0.82 cnf(i_0_264, plain, (subs(esk32_3(X1,X2,X3),angeh__366ren_1_1)|~in(X1,X2)|~loc(X3,X1)|~sub(X3,mitglied_1_1)|~sub(X2,einrichtung_1_2))). % 0.46/0.82 cnf(i_0_324, plain, (~purp(X1,X2)|~agt(X1,X3)|~subs(X1,aufrufen_1_1))). % 0.46/0.82 cnf(i_0_355, plain, (subs(esk47_3(X1,X2,X3),hei__337en_1_1)|~attr(X3,X1)|~sub(X1,X2)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))). % 0.46/0.82 cnf(i_0_392, plain, (loc(X1,X2)|~local_in_stereotype(X3,X4)|~dircl(X5,X6)|~dircl(X5,X7)|~in(X6,X2)|~in(X7,X1)|~sub(X2,X4)|~sub(X1,X3))). % 0.46/0.82 cnf(i_0_277, plain, (attr(esk34_3(X1,X2,X3),esk35_3(X1,X2,X3))|~prop_p3(X1,X2,X4)|~state_adjective_state_binding(X2,X3))). % 0.46/0.82 cnf(i_0_357, plain, (arg1(esk47_3(X1,X2,X3),X3)|~attr(X3,X1)|~sub(X1,X2)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))). % 0.46/0.82 cnf(i_0_356, plain, (arg2(esk47_3(X1,X2,X3),X3)|~attr(X3,X1)|~sub(X1,X2)|~member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))))). % 0.46/0.82 cnf(i_0_236, plain, (subs(esk26_4(X1,X2,X3,X4),aufrufen_1_1)|~ornt(X2,X1)|~mcont(X1,X4)|~agt(X2,X3)|~subs(X2,lancieren_1_1)|~sub(X1,aufruf_1_1))). % 0.46/0.82 cnf(i_0_238, plain, (hsit(X1,esk26_4(X2,X1,X3,X4))|~ornt(X1,X2)|~mcont(X2,X4)|~agt(X1,X3)|~subs(X1,lancieren_1_1)|~sub(X2,aufruf_1_1))). % 0.46/0.82 cnf(i_0_300, plain, (agt(X1,X2)|~agt(X1,X3)|~attch(X2,X3)|~sub(X2,einrichtung_1_2)|~sub(X3,X4)|~member(X4,cons(krieger__1_1,cons(trupp_1_1,nil))))). % 0.46/0.82 cnf(i_0_239, plain, (agt(esk26_4(X1,X2,X3,X4),X3)|~ornt(X2,X1)|~mcont(X1,X4)|~agt(X2,X3)|~subs(X2,lancieren_1_1)|~sub(X1,aufruf_1_1))). % 0.46/0.82 cnf(i_0_237, plain, (purp(esk26_4(X1,X2,X3,X4),X4)|~ornt(X2,X1)|~mcont(X1,X4)|~agt(X2,X3)|~subs(X2,lancieren_1_1)|~sub(X1,aufruf_1_1))). % 0.46/0.82 cnf(i_0_374, plain, (hsit(X1,esk48_5(X2,X1,X3,X4,X5))|~origl(X4,X2)|~arg2(X1,X5)|~arg1(X1,X4)|~flp(X2,X3)|~subs(X1,stammen_1_2))). % 0.46/0.82 cnf(i_0_375, plain, (agt(esk48_5(X1,X2,X3,X4,X5),X4)|~origl(X4,X1)|~arg2(X2,X5)|~arg1(X2,X4)|~flp(X1,X3)|~subs(X2,stammen_1_2))). % 0.46/0.82 cnf(i_0_373, plain, (origl(esk48_5(X1,X2,X3,X4,X5),X5)|~origl(X4,X1)|~arg2(X2,X5)|~arg1(X2,X4)|~flp(X1,X3)|~subs(X2,stammen_1_2))). % 0.46/0.82 cnf(i_0_372, plain, (subs(esk48_5(X1,X2,X3,X4,X5),kommen_1_1)|~origl(X4,X1)|~arg2(X2,X5)|~arg1(X2,X4)|~flp(X1,X3)|~subs(X2,stammen_1_2))). % 0.46/0.82 cnf(i_0_230, plain, (~ctxt(X1,X2)|~ornt(X1,X3)|~subs(X1,auszeichnen_1_1)|~sub(X2,X4)|~member(X4,cons(nobelpreis_1_1,cons(preis_1_1,nil))))). % 0.46/0.82 cnf(i_0_299, plain, (agt(X1,X2)|~agt(X1,X3)|~attch(X2,X3)|~pred(X3,X4)|~sub(X2,einrichtung_1_2)|~member(X4,cons(krieger__1_1,cons(trupp_1_1,nil))))). % 0.46/0.82 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 0.46/0.82 # Begin printing tableau % 0.46/0.82 # Found 4 steps % 0.46/0.82 cnf(i_0_27, hypothesis, (fact(beitrag_1_1,real)), inference(start_rule)). % 0.46/0.82 cnf(i_0_996, plain, (fact(beitrag_1_1,real)), inference(extension_rule, [i_0_63])). % 0.46/0.82 cnf(i_0_99173, plain, (has_fact_leq(beitrag_1_1,real)), inference(extension_rule, [i_0_75])). % 0.46/0.82 cnf(i_0_99217, plain, (~loc(beitrag_1_1,X4)), inference(etableau_closure_rule, [i_0_99217, ...])). % 0.46/0.82 # End printing tableau % 0.46/0.82 # SZS output end % 0.46/0.82 # Branches closed with saturation will be marked with an "s" % 0.46/0.83 # Child (374) has found a proof. % 0.46/0.83 % 0.46/0.84 # Proof search is over... % 0.46/0.84 # Freeing feature tree %------------------------------------------------------------------------------