%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR114+10 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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 21:16:32 EDT 2022
% Result : Theorem 191.54s 184.90s
% Output : Proof 191.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR114+10 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n017.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Thu Jun 9 19:53:19 EDT 2022
% 0.12/0.33 % CPUTime :
% 191.54/184.90 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 191.54/184.91 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 191.54/184.91
% 191.54/184.91 %-----------------------------------------------------
% 191.54/184.91 fof(ave07_era5_synth_qa07_004_mira_news_613, hypothesis, attr(c40862, c40863) & sub(c40862, stadt__1_1) & sub(c40863, name_1_1) & val(c40863, hallstatt_0) & sub(c40883, titel_1_1) & attch(c40889, c40883) & prop(c40889, c40892) & sub(c40889, st__374ck_1_1) & supl(c40892, neo_1_1, c40893) & attch(c40895, c40889) & prop(c40895, slowenisch__1_1) & sub(c40895, dramatiker_1_1) & attr(c40903, c40904) & attr(c40903, c40905) & sub(c40903, romanautor_1_1) & sub(c40904, eigenname_1_1) & val(c40904, drago_0) & sub(c40905, familiename_1_1) & val(c40905, jancar_0) & subs(c40936, festival_1_1) & attr(c40941, c40947) & prop(c40941, zeitgen__366ssisch_1_1) & sub(c40941, schauspielhaus_1_1) & sub(c40947, name_1_1) & val(c40947, dionisya_0) & prop(c40954, italienisch__1_1) & sub(c40954, stadt__1_1) & pred(c40955, veroli_1_1) & subs(c40962, herstellung_1_1) & attch(c40970, c40962) & prop(c40970, slowenisch__1_1) & sub(c40970, schauspielhaus_1_1) & attr(c40976, c40977) & sub(c40976, stadt__1_1) & sub(c40977, name_1_1) & val(c40977, triest_0) & subs(c40979, debuet_1_1) & attr(c41010, c41011) & prop(c41010, slowenisch__1_1) & sub(c41010, nachrichtenagentur_1_1) & sub(c41011, name_1_1) & val(c41011, sta_0) & tupl_p14(c41050, c40862, c40883, c40892, c40903, c40862, c40936, c40941, c40954, c40955, c40962, c40976, c40979, c41010) & assoc(debuet_1_1, ur_1_1) & subs(debuet_1_1, auff__374hrung_1_1) & assoc(nachrichtenagentur_1_1, nachricht_1_1) & sub(nachrichtenagentur_1_1, agentur_1_1) & sort(c40862, d) & sort(c40862, io) & card(c40862, int1) & etype(c40862, int0) & fact(c40862, real) & gener(c40862, sp) & quant(c40862, one) & refer(c40862, det) & varia(c40862, con) & sort(c40863, na) & card(c40863, int1) & etype(c40863, int0) & fact(c40863, real) & gener(c40863, sp) & quant(c40863, one) & refer(c40863, indet) & varia(c40863, varia_c) & sort(stadt__1_1, d) & sort(stadt__1_1, io) & card(stadt__1_1, int1) & etype(stadt__1_1, int0) & fact(stadt__1_1, real) & gener(stadt__1_1, ge) & quant(stadt__1_1, one) & refer(stadt__1_1, refer_c) & varia(stadt__1_1, varia_c) & sort(name_1_1, na) & card(name_1_1, int1) & etype(name_1_1, int0) & fact(name_1_1, real) & gener(name_1_1, ge) & quant(name_1_1, one) & refer(name_1_1, refer_c) & varia(name_1_1, varia_c) & sort(hallstatt_0, fe) & sort(c40883, d) & sort(c40883, io) & card(c40883, int1) & etype(c40883, int0) & fact(c40883, real) & gener(c40883, sp) & quant(c40883, one) & refer(c40883, det) & varia(c40883, con) & sort(titel_1_1, d) & sort(titel_1_1, io) & card(titel_1_1, int1) & etype(titel_1_1, int0) & fact(titel_1_1, real) & gener(titel_1_1, ge) & quant(titel_1_1, one) & refer(titel_1_1, refer_c) & varia(titel_1_1, varia_c) & sort(c40889, d) & card(c40889, int1) & etype(c40889, int0) & fact(c40889, real) & gener(c40889, sp) & quant(c40889, one) & refer(c40889, det) & varia(c40889, con) & sort(c40892, tq) & sort(st__374ck_1_1, d) & card(st__374ck_1_1, int1) & etype(st__374ck_1_1, int0) & fact(st__374ck_1_1, real) & gener(st__374ck_1_1, ge) & quant(st__374ck_1_1, one) & refer(st__374ck_1_1, refer_c) & varia(st__374ck_1_1, varia_c) & sort(neo_1_1, nq) & sort(c40893, o) & card(c40893, card_c) & etype(c40893, int1) & etype(c40893, int2) & fact(c40893, real) & gener(c40893, gener_c) & quant(c40893, quant_c) & refer(c40893, refer_c) & varia(c40893, varia_c) & sort(c40895, d) & card(c40895, int1) & etype(c40895, int0) & fact(c40895, real) & gener(c40895, sp) & quant(c40895, one) & refer(c40895, det) & varia(c40895, con) & sort(slowenisch__1_1, nq) & sort(dramatiker_1_1, d) & card(dramatiker_1_1, int1) & etype(dramatiker_1_1, int0) & fact(dramatiker_1_1, real) & gener(dramatiker_1_1, ge) & quant(dramatiker_1_1, one) & refer(dramatiker_1_1, refer_c) & varia(dramatiker_1_1, varia_c) & sort(c40903, d) & card(c40903, int1) & etype(c40903, int0) & fact(c40903, real) & gener(c40903, sp) & quant(c40903, one) & refer(c40903, det) & varia(c40903, varia_c) & sort(c40904, na) & card(c40904, int1) & etype(c40904, int0) & fact(c40904, real) & gener(c40904, sp) & quant(c40904, one) & refer(c40904, indet) & varia(c40904, varia_c) & sort(c40905, na) & card(c40905, int1) & etype(c40905, int0) & fact(c40905, real) & gener(c40905, sp) & quant(c40905, one) & refer(c40905, det) & varia(c40905, varia_c) & sort(romanautor_1_1, d) & card(romanautor_1_1, int1) & etype(romanautor_1_1, int0) & fact(romanautor_1_1, real) & gener(romanautor_1_1, ge) & quant(romanautor_1_1, one) & refer(romanautor_1_1, refer_c) & varia(romanautor_1_1, varia_c) & sort(eigenname_1_1, na) & card(eigenname_1_1, int1) & etype(eigenname_1_1, int0) & fact(eigenname_1_1, real) & gener(eigenname_1_1, ge) & quant(eigenname_1_1, one) & refer(eigenname_1_1, refer_c) & varia(eigenname_1_1, varia_c) & sort(drago_0, fe) & sort(familiename_1_1, na) & card(familiename_1_1, int1) & etype(familiename_1_1, int0) & fact(familiename_1_1, real) & gener(familiename_1_1, ge) & quant(familiename_1_1, one) & refer(familiename_1_1, refer_c) & varia(familiename_1_1, varia_c) & sort(jancar_0, fe) & sort(c40936, ad) & card(c40936, int1) & etype(c40936, int0) & fact(c40936, real) & gener(c40936, sp) & quant(c40936, one) & refer(c40936, det) & varia(c40936, con) & sort(festival_1_1, ad) & card(festival_1_1, int1) & etype(festival_1_1, int0) & fact(festival_1_1, real) & gener(festival_1_1, ge) & quant(festival_1_1, one) & refer(festival_1_1, refer_c) & varia(festival_1_1, varia_c) & sort(c40941, d) & sort(c40941, io) & card(c40941, int1) & etype(c40941, int0) & fact(c40941, real) & gener(c40941, sp) & quant(c40941, one) & refer(c40941, det) & varia(c40941, varia_c) & sort(c40947, na) & card(c40947, int1) & etype(c40947, int0) & fact(c40947, real) & gener(c40947, sp) & quant(c40947, one) & refer(c40947, det) & varia(c40947, varia_c) & sort(zeitgen__366ssisch_1_1, nq) & sort(schauspielhaus_1_1, d) & sort(schauspielhaus_1_1, io) & card(schauspielhaus_1_1, int1) & etype(schauspielhaus_1_1, int0) & fact(schauspielhaus_1_1, real) & gener(schauspielhaus_1_1, ge) & quant(schauspielhaus_1_1, one) & refer(schauspielhaus_1_1, refer_c) & varia(schauspielhaus_1_1, varia_c) & sort(dionisya_0, fe) & sort(c40954, d) & sort(c40954, io) & card(c40954, int1) & etype(c40954, int0) & fact(c40954, real) & gener(c40954, sp) & quant(c40954, one) & refer(c40954, det) & varia(c40954, con) & sort(italienisch__1_1, nq) & sort(c40955, o) & card(c40955, cons(x_constant, cons(int1, nil))) & etype(c40955, int1) & fact(c40955, real) & gener(c40955, gener_c) & quant(c40955, mult) & refer(c40955, indet) & varia(c40955, varia_c) & sort(veroli_1_1, o) & card(veroli_1_1, int1) & etype(veroli_1_1, int0) & fact(veroli_1_1, real) & gener(veroli_1_1, ge) & quant(veroli_1_1, one) & refer(veroli_1_1, refer_c) & varia(veroli_1_1, varia_c) & sort(c40962, ad) & card(c40962, int1) & etype(c40962, int0) & fact(c40962, real) & gener(c40962, sp) & quant(c40962, one) & refer(c40962, indet) & varia(c40962, varia_c) & sort(herstellung_1_1, ad) & card(herstellung_1_1, int1) & etype(herstellung_1_1, int0) & fact(herstellung_1_1, real) & gener(herstellung_1_1, ge) & quant(herstellung_1_1, one) & refer(herstellung_1_1, refer_c) & varia(herstellung_1_1, varia_c) & sort(c40970, d) & sort(c40970, io) & card(c40970, int1) & etype(c40970, int0) & fact(c40970, real) & gener(c40970, sp) & quant(c40970, one) & refer(c40970, det) & varia(c40970, con) & sort(c40976, d) & sort(c40976, io) & card(c40976, int1) & etype(c40976, int0) & fact(c40976, real) & gener(c40976, sp) & quant(c40976, one) & refer(c40976, det) & varia(c40976, con) & sort(c40977, na) & card(c40977, int1) & etype(c40977, int0) & fact(c40977, real) & gener(c40977, sp) & quant(c40977, one) & refer(c40977, indet) & varia(c40977, varia_c) & sort(triest_0, fe) & sort(c40979, ad) & card(c40979, int1) & etype(c40979, int0) & fact(c40979, real) & gener(c40979, sp) & quant(c40979, one) & refer(c40979, det) & varia(c40979, con) & sort(debuet_1_1, ad) & card(debuet_1_1, int1) & etype(debuet_1_1, int0) & fact(debuet_1_1, real) & gener(debuet_1_1, ge) & quant(debuet_1_1, one) & refer(debuet_1_1, refer_c) & varia(debuet_1_1, varia_c) & sort(c41010, d) & sort(c41010, io) & card(c41010, int1) & etype(c41010, int0) & fact(c41010, real) & gener(c41010, sp) & quant(c41010, one) & refer(c41010, det) & varia(c41010, con) & sort(c41011, na) & card(c41011, int1) & etype(c41011, int0) & fact(c41011, real) & gener(c41011, sp) & quant(c41011, one) & refer(c41011, indet) & varia(c41011, varia_c) & sort(nachrichtenagentur_1_1, d) & sort(nachrichtenagentur_1_1, io) & card(nachrichtenagentur_1_1, int1) & etype(nachrichtenagentur_1_1, int0) & fact(nachrichtenagentur_1_1, real) & gener(nachrichtenagentur_1_1, ge) & quant(nachrichtenagentur_1_1, one) & refer(nachrichtenagentur_1_1, refer_c) & varia(nachrichtenagentur_1_1, varia_c) & sort(sta_0, fe) & sort(c41050, ent) & card(c41050, card_c) & etype(c41050, etype_c) & fact(c41050, real) & gener(c41050, gener_c) & quant(c41050, quant_c) & refer(c41050, refer_c) & varia(c41050, varia_c) & sort(ur_1_1, o) & card(ur_1_1, int1) & etype(ur_1_1, int0) & fact(ur_1_1, real) & gener(ur_1_1, ge) & quant(ur_1_1, one) & refer(ur_1_1, refer_c) & varia(ur_1_1, varia_c) & sort(auff__374hrung_1_1, ad) & card(auff__374hrung_1_1, int1) & etype(auff__374hrung_1_1, int0) & fact(auff__374hrung_1_1, real) & gener(auff__374hrung_1_1, ge) & quant(auff__374hrung_1_1, one) & refer(auff__374hrung_1_1, refer_c) & varia(auff__374hrung_1_1, varia_c) & sort(nachricht_1_1, ad) & sort(nachricht_1_1, d) & sort(nachricht_1_1, io) & card(nachricht_1_1, int1) & etype(nachricht_1_1, int0) & fact(nachricht_1_1, real) & gener(nachricht_1_1, ge) & quant(nachricht_1_1, one) & refer(nachricht_1_1, refer_c) & varia(nachricht_1_1, varia_c) & sort(agentur_1_1, d) & sort(agentur_1_1, io) & card(agentur_1_1, int1) & etype(agentur_1_1, int0) & fact(agentur_1_1, real) & gener(agentur_1_1, ge) & quant(agentur_1_1, one) & refer(agentur_1_1, refer_c) & varia(agentur_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_004_mira_news_613)).
% 191.54/184.91 fof(synth_qa07_004_mira_news_613, conjecture, ? [_662519, _662522, _662525, _662528, _662531] : (in(_662525, _662519) & attr(_662519, _662522) & loc(_662531, _662525) & scar(_662531, _662528) & sub(_662522, name_1_1) & subs(_662531, stehen_1_1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_004_mira_news_613)).
% 191.54/184.91 fof(state_adjective__in_state, axiom, ! [_662939, _662942, _662945] : (prop(_662939, _662942) & state_adjective_state_binding(_662942, _662945) => ? [_662973, _662976, _662979] : (in(_662979, _662973) & attr(_662973, _662976) & loc(_662939, _662979) & sub(_662973, land_1_1) & sub(_662976, name_1_1) & val(_662976, _662945))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', state_adjective__in_state)).
% 191.54/184.91 fof(loc__stehen_1_1_loc, axiom, ! [_663654, _663657] : (loc(_663654, _663657) => ? [_663675] : (loc(_663675, _663657) & scar(_663675, _663654) & subs(_663675, stehen_1_1))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', loc__stehen_1_1_loc)).
% 191.54/184.91 fof(fact_8972, axiom, state_adjective_state_binding(slowenisch__1_1, slowenien_0), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', fact_8972)).
% 191.54/184.91
% 191.54/184.91 cnf(1, plain, [-(prop(c40895, slowenisch__1_1))], clausify(ave07_era5_synth_qa07_004_mira_news_613)).
% 191.54/184.91 cnf(2, plain, [in(_194495, _194493), attr(_194493, _194494), loc(_194497, _194495), scar(_194497, _194496), sub(_194494, name_1_1), subs(_194497, stehen_1_1)], clausify(synth_qa07_004_mira_news_613)).
% 191.54/184.91 cnf(3, plain, [-(in(50 ^ [_132742, _132741, _132740], 48 ^ [_132742, _132741, _132740])), prop(_132740, _132741), state_adjective_state_binding(_132741, _132742)], clausify(state_adjective__in_state)).
% 191.54/184.91 cnf(4, plain, [loc(_133230, _133231), -(scar(63 ^ [_133231, _133230], _133230))], clausify(loc__stehen_1_1_loc)).
% 191.54/184.91 cnf(5, plain, [-(attr(48 ^ [_132742, _132741, _132740], 49 ^ [_132742, _132741, _132740])), prop(_132740, _132741), state_adjective_state_binding(_132741, _132742)], clausify(state_adjective__in_state)).
% 191.54/184.91 cnf(6, plain, [-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))], clausify(fact_8972)).
% 191.54/184.91 cnf(7, plain, [loc(_133230, _133231), -(loc(63 ^ [_133231, _133230], _133231))], clausify(loc__stehen_1_1_loc)).
% 191.54/184.91 cnf(8, plain, [-(loc(_132740, 50 ^ [_132742, _132741, _132740])), prop(_132740, _132741), state_adjective_state_binding(_132741, _132742)], clausify(state_adjective__in_state)).
% 191.54/184.91 cnf(9, plain, [-(sub(49 ^ [_132742, _132741, _132740], name_1_1)), prop(_132740, _132741), state_adjective_state_binding(_132741, _132742)], clausify(state_adjective__in_state)).
% 191.54/184.91 cnf(10, plain, [loc(_133230, _133231), -(subs(63 ^ [_133231, _133230], stehen_1_1))], clausify(loc__stehen_1_1_loc)).
% 191.54/184.91
% 191.54/184.91 cnf('1',plain,[in(50 ^ [slowenien_0, slowenisch__1_1, c40895], 48 ^ [slowenien_0, slowenisch__1_1, c40895]), attr(48 ^ [slowenien_0, slowenisch__1_1, c40895], 49 ^ [slowenien_0, slowenisch__1_1, c40895]), loc(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], 50 ^ [slowenien_0, slowenisch__1_1, c40895]), scar(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], c40895), sub(49 ^ [slowenien_0, slowenisch__1_1, c40895], name_1_1), subs(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], stehen_1_1)],start(2,bind([[_194493, _194495, _194496, _194494, _194497], [48 ^ [slowenien_0, slowenisch__1_1, c40895], 50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895, 49 ^ [slowenien_0, slowenisch__1_1, c40895], 63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895]]]))).
% 191.54/184.91 cnf('1.1',plain,[-(in(50 ^ [slowenien_0, slowenisch__1_1, c40895], 48 ^ [slowenien_0, slowenisch__1_1, c40895])), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(3,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.1.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.1.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 cnf('1.2',plain,[-(attr(48 ^ [slowenien_0, slowenisch__1_1, c40895], 49 ^ [slowenien_0, slowenisch__1_1, c40895])), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(5,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.2.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.2.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 cnf('1.3',plain,[-(loc(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], 50 ^ [slowenien_0, slowenisch__1_1, c40895])), loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])],extension(7,bind([[_133230, _133231], [c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895]]]))).
% 191.54/184.91 cnf('1.3.1',plain,[-(loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(8,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.3.1.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.3.1.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 cnf('1.4',plain,[-(scar(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], c40895)), loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])],extension(4,bind([[_133230, _133231], [c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895]]]))).
% 191.54/184.91 cnf('1.4.1',plain,[-(loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(8,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.4.1.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.4.1.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 cnf('1.5',plain,[-(sub(49 ^ [slowenien_0, slowenisch__1_1, c40895], name_1_1)), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(9,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.5.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.5.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 cnf('1.6',plain,[-(subs(63 ^ [50 ^ [slowenien_0, slowenisch__1_1, c40895], c40895], stehen_1_1)), loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])],extension(10,bind([[_133230, _133231], [c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895]]]))).
% 191.54/184.91 cnf('1.6.1',plain,[-(loc(c40895, 50 ^ [slowenien_0, slowenisch__1_1, c40895])), prop(c40895, slowenisch__1_1), state_adjective_state_binding(slowenisch__1_1, slowenien_0)],extension(8,bind([[_132740, _132741, _132742], [c40895, slowenisch__1_1, slowenien_0]]))).
% 191.54/184.91 cnf('1.6.1.1',plain,[-(prop(c40895, slowenisch__1_1))],extension(1)).
% 191.54/184.91 cnf('1.6.1.2',plain,[-(state_adjective_state_binding(slowenisch__1_1, slowenien_0))],extension(6)).
% 191.54/184.91 %-----------------------------------------------------
% 191.54/184.92
% 191.54/184.92 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------