%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR113+25 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n018.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:28 EDT 2022
% Result : Theorem 119.71s 116.17s
% Output : Proof 119.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : CSR113+25 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n018.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jun 11 14:44:55 EDT 2022
% 0.13/0.33 % CPUTime :
% 119.71/116.17 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.71/116.18 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 119.71/116.18
% 119.71/116.18 %-----------------------------------------------------
% 119.71/116.18 fof(synth_qa07_003_mw3_112, conjecture, ? [_433898, _433901, _433904, _433907] : (attr(_433901, _433898) & scar(_433904, _433907) & sub(_433898, name_1_1) & val(_433898, usa_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_003_mw3_112)).
% 119.71/116.18 fof(ave07_era5_synth_qa07_003_mw3_112, hypothesis, sub(c53814, freiheitsstatue_1_1) & prop(c53857, hoch_1_1) & sub(c53857, wiedererkennungswert_1_1) & pred(c53870, mensch_1_1) & sub(c53874, symbol_1_1) & attr(c53883, c53884) & sub(c53883, land_1_1) & sub(c53884, name_1_1) & val(c53884, usa_0) & pred(c53927, sternenbanner_1_1) & sub(c53930, uncle_1_1) & attr(c53935, c53936) & sub(c53935, mensch_1_1) & sub(c53936, eigenname_1_1) & val(c53936, sam_0) & tupl_p9(c54159, c53814, c53857, c53870, c53874, c53883, c53927, c53930, c53935) & assoc(freiheitsstatue_1_1, freiheit_1_1) & sub(freiheitsstatue_1_1, statue_1_1) & assoc(sternenbanner_1_1, stern_1_1) & sub(sternenbanner_1_1, banner_1_1) & assoc(wiedererkennungswert_1_1, erkennung_1_1) & assoc(wiedererkennungswert_1_1, re_1_1) & sub(wiedererkennungswert_1_1, wert_1_1) & sort(c53814, d) & card(c53814, int1) & etype(c53814, int0) & fact(c53814, real) & gener(c53814, sp) & quant(c53814, one) & refer(c53814, det) & varia(c53814, con) & sort(freiheitsstatue_1_1, d) & card(freiheitsstatue_1_1, int1) & etype(freiheitsstatue_1_1, int0) & fact(freiheitsstatue_1_1, real) & gener(freiheitsstatue_1_1, ge) & quant(freiheitsstatue_1_1, one) & refer(freiheitsstatue_1_1, refer_c) & varia(freiheitsstatue_1_1, varia_c) & sort(c53857, io) & sort(c53857, oa) & card(c53857, int1) & etype(c53857, int0) & fact(c53857, real) & gener(c53857, sp) & quant(c53857, one) & refer(c53857, indet) & varia(c53857, varia_c) & sort(hoch_1_1, mq) & sort(wiedererkennungswert_1_1, io) & sort(wiedererkennungswert_1_1, oa) & card(wiedererkennungswert_1_1, int1) & etype(wiedererkennungswert_1_1, int0) & fact(wiedererkennungswert_1_1, real) & gener(wiedererkennungswert_1_1, ge) & quant(wiedererkennungswert_1_1, one) & refer(wiedererkennungswert_1_1, refer_c) & varia(wiedererkennungswert_1_1, varia_c) & sort(c53870, d) & card(c53870, cons(x_constant, cons(int1, nil))) & etype(c53870, int1) & fact(c53870, real) & gener(c53870, gener_c) & quant(c53870, many) & refer(c53870, refer_c) & varia(c53870, varia_c) & sort(mensch_1_1, d) & card(mensch_1_1, int1) & etype(mensch_1_1, int0) & fact(mensch_1_1, real) & gener(mensch_1_1, ge) & quant(mensch_1_1, one) & refer(mensch_1_1, refer_c) & varia(mensch_1_1, varia_c) & sort(c53874, io) & card(c53874, int1) & etype(c53874, int0) & fact(c53874, real) & gener(c53874, sp) & quant(c53874, one) & refer(c53874, indet) & varia(c53874, varia_c) & sort(symbol_1_1, io) & card(symbol_1_1, int1) & etype(symbol_1_1, int0) & fact(symbol_1_1, real) & gener(symbol_1_1, ge) & quant(symbol_1_1, one) & refer(symbol_1_1, refer_c) & varia(symbol_1_1, varia_c) & sort(c53883, d) & sort(c53883, io) & card(c53883, int1) & etype(c53883, int0) & fact(c53883, real) & gener(c53883, sp) & quant(c53883, one) & refer(c53883, det) & varia(c53883, con) & sort(c53884, na) & card(c53884, int1) & etype(c53884, int0) & fact(c53884, real) & gener(c53884, sp) & quant(c53884, one) & refer(c53884, indet) & varia(c53884, varia_c) & sort(land_1_1, d) & sort(land_1_1, io) & card(land_1_1, int1) & etype(land_1_1, int0) & fact(land_1_1, real) & gener(land_1_1, ge) & quant(land_1_1, one) & refer(land_1_1, refer_c) & varia(land_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(usa_0, fe) & sort(c53927, d) & card(c53927, cons(x_constant, cons(int1, nil))) & etype(c53927, int1) & fact(c53927, real) & gener(c53927, sp) & quant(c53927, mult) & refer(c53927, det) & varia(c53927, con) & sort(sternenbanner_1_1, d) & card(sternenbanner_1_1, int1) & etype(sternenbanner_1_1, int0) & fact(sternenbanner_1_1, real) & gener(sternenbanner_1_1, ge) & quant(sternenbanner_1_1, one) & refer(sternenbanner_1_1, refer_c) & varia(sternenbanner_1_1, varia_c) & sort(c53930, o) & card(c53930, int1) & etype(c53930, int0) & fact(c53930, real) & gener(c53930, gener_c) & quant(c53930, one) & refer(c53930, refer_c) & varia(c53930, varia_c) & sort(uncle_1_1, o) & card(uncle_1_1, int1) & etype(uncle_1_1, int0) & fact(uncle_1_1, real) & gener(uncle_1_1, ge) & quant(uncle_1_1, one) & refer(uncle_1_1, refer_c) & varia(uncle_1_1, varia_c) & sort(c53935, d) & card(c53935, int1) & etype(c53935, int0) & fact(c53935, real) & gener(c53935, sp) & quant(c53935, one) & refer(c53935, det) & varia(c53935, con) & sort(c53936, na) & card(c53936, int1) & etype(c53936, int0) & fact(c53936, real) & gener(c53936, sp) & quant(c53936, one) & refer(c53936, indet) & varia(c53936, 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(sam_0, fe) & sort(c54159, ent) & card(c54159, card_c) & etype(c54159, etype_c) & fact(c54159, real) & gener(c54159, gener_c) & quant(c54159, quant_c) & refer(c54159, refer_c) & varia(c54159, varia_c) & sort(freiheit_1_1, as) & sort(freiheit_1_1, io) & card(freiheit_1_1, int1) & etype(freiheit_1_1, int0) & fact(freiheit_1_1, real) & gener(freiheit_1_1, ge) & quant(freiheit_1_1, one) & refer(freiheit_1_1, refer_c) & varia(freiheit_1_1, varia_c) & sort(statue_1_1, d) & card(statue_1_1, int1) & etype(statue_1_1, int0) & fact(statue_1_1, real) & gener(statue_1_1, ge) & quant(statue_1_1, one) & refer(statue_1_1, refer_c) & varia(statue_1_1, varia_c) & sort(stern_1_1, d) & card(stern_1_1, int1) & etype(stern_1_1, int0) & fact(stern_1_1, real) & gener(stern_1_1, ge) & quant(stern_1_1, one) & refer(stern_1_1, refer_c) & varia(stern_1_1, varia_c) & sort(banner_1_1, d) & card(banner_1_1, int1) & etype(banner_1_1, int0) & fact(banner_1_1, real) & gener(banner_1_1, ge) & quant(banner_1_1, one) & refer(banner_1_1, refer_c) & varia(banner_1_1, varia_c) & sort(erkennung_1_1, ad) & card(erkennung_1_1, int1) & etype(erkennung_1_1, int0) & fact(erkennung_1_1, real) & gener(erkennung_1_1, ge) & quant(erkennung_1_1, one) & refer(erkennung_1_1, refer_c) & varia(erkennung_1_1, varia_c) & sort(re_1_1, t) & card(re_1_1, int1) & etype(re_1_1, int0) & fact(re_1_1, real) & gener(re_1_1, gener_c) & quant(re_1_1, one) & refer(re_1_1, refer_c) & varia(re_1_1, varia_c) & sort(wert_1_1, io) & sort(wert_1_1, oa) & card(wert_1_1, int1) & etype(wert_1_1, int0) & fact(wert_1_1, real) & gener(wert_1_1, ge) & quant(wert_1_1, one) & refer(wert_1_1, refer_c) & varia(wert_1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 fof(member_first, axiom, ! [_436982, _436985] : member(_436982, cons(_436982, _436985)), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', member_first)).
% 119.71/116.18 fof(attr_name__abk__374rzung_stehen_1_b_f__374r, axiom, ! [_437410, _437413, _437416] : (attr(_437416, _437410) & member(_437413, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))) & sub(_437410, _437413) => ? [_437475] : (mcont(_437475, _437416) & obj(_437475, _437416) & scar(_437475, _437416) & subs(_437475, stehen_1_b))), file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax', attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 119.71/116.18
% 119.71/116.18 cnf(1, plain, [attr(_193165, _193164), scar(_193166, _193167), sub(_193164, name_1_1), val(_193164, usa_0)], clausify(synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(2, plain, [-(attr(c53883, c53884))], clausify(ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(3, plain, [-(sub(c53884, name_1_1))], clausify(ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(4, plain, [-(val(c53884, usa_0))], clausify(ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(5, plain, [-(attr(c53935, c53936))], clausify(ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(6, plain, [-(sub(c53936, eigenname_1_1))], clausify(ave07_era5_synth_qa07_003_mw3_112)).
% 119.71/116.18 cnf(7, plain, [-(member(_129848, cons(_129848, _129849)))], clausify(member_first)).
% 119.71/116.18 cnf(8, plain, [-(scar(52 ^ [_131946, _131945, _131944], _131946)), attr(_131946, _131944), member(_131945, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(_131944, _131945)], clausify(attr_name__abk__374rzung_stehen_1_b_f__374r)).
% 119.71/116.18
% 119.71/116.18 cnf('1',plain,[attr(c53883, c53884), scar(52 ^ [c53935, eigenname_1_1, c53936], c53935), sub(c53884, name_1_1), val(c53884, usa_0)],start(1,bind([[_193165, _193166, _193167, _193164], [c53883, 52 ^ [c53935, eigenname_1_1, c53936], c53935, c53884]]))).
% 119.71/116.18 cnf('1.1',plain,[-(attr(c53883, c53884))],extension(2)).
% 119.71/116.18 cnf('1.2',plain,[-(scar(52 ^ [c53935, eigenname_1_1, c53936], c53935)), attr(c53935, c53936), member(eigenname_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))), sub(c53936, eigenname_1_1)],extension(8,bind([[_131946, _131944, _131945], [c53935, c53936, eigenname_1_1]]))).
% 119.71/116.18 cnf('1.2.1',plain,[-(attr(c53935, c53936))],extension(5)).
% 119.71/116.18 cnf('1.2.2',plain,[-(member(eigenname_1_1, cons(eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil)))))],extension(7,bind([[_129848, _129849], [eigenname_1_1, cons(familiename_1_1, cons(name_1_1, nil))]]))).
% 119.71/116.19 cnf('1.2.3',plain,[-(sub(c53936, eigenname_1_1))],extension(6)).
% 119.71/116.19 cnf('1.3',plain,[-(sub(c53884, name_1_1))],extension(3)).
% 119.71/116.19 cnf('1.4',plain,[-(val(c53884, usa_0))],extension(4)).
% 119.71/116.19 %-----------------------------------------------------
% 119.71/116.19
% 119.71/116.19 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------