%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR116+7 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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:17:03 EDT 2022
% Result : Theorem 113.77s 110.26s
% Output : Proof 113.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : CSR116+7 : TPTP v8.1.0. Released v4.0.0.
% 0.06/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 600
% 0.14/0.34 % DateTime : Fri Jun 10 19:19:44 EDT 2022
% 0.14/0.34 % CPUTime :
% 113.77/110.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.77/110.27 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.77/110.27
% 113.77/110.27 %-----------------------------------------------------
% 113.77/110.27 fof(synth_qa07_010_mira_news_1614, conjecture, ? [_428813, _428816, _428819, _428822, _428825, _428828, _428831, _428834, _428837] : (pmod(_428837, erst_1_1, pr__344sident_1_1) & arg1(_428822, _428813) & arg2(_428822, _428825) & attr(_428813, _428816) & attr(_428813, _428819) & attr(_428828, _428831) & obj(_428834, _428813) & prop(_428825, schwarz_1_1) & rslt(_428834, _428822) & sub(_428816, familiename_1_1) & sub(_428819, eigenname_1_1) & sub(_428825, _428837) & subr(_428822, rprs_0) & subs(_428834, w__344hlen_1_2) & val(_428816, mandela_0) & val(_428819, nelson_0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', synth_qa07_010_mira_news_1614)).
% 113.77/110.27 fof(ave07_era5_synth_qa07_010_mira_news_1614, hypothesis, attr(c12, c13) & attr(c12, c14) & sub(c12, mensch_1_1) & sub(c13, eigenname_1_1) & val(c13, nelson_0) & sub(c14, familiename_1_1) & val(c14, mandela_0) & prop(c18, neugew__344hlt_1_1) & sub(c18, abgeordneten_haus_1_2) & prop(c25, schwarz_1_1) & sub(c25, c27) & pmod(c27, erst_1_1, pr__344sident_1_1) & attch(c33, c25) & sub(c33, land_1_1) & agt(c38, c18) & obj(c38, c12) & rslt(c38, c47) & subs(c38, w__344hlen_1_2) & temp(c38, c5) & arg1(c47, c12) & arg2(c47, c25) & subr(c47, rprs_0) & sub(c5, montag__1_1) & sort(c12, d) & card(c12, int1) & etype(c12, int0) & fact(c12, real) & gener(c12, sp) & quant(c12, one) & refer(c12, det) & varia(c12, con) & sort(c13, na) & card(c13, int1) & etype(c13, int0) & fact(c13, real) & gener(c13, sp) & quant(c13, one) & refer(c13, indet) & varia(c13, varia_c) & sort(c14, na) & card(c14, int1) & etype(c14, int0) & fact(c14, real) & gener(c14, sp) & quant(c14, one) & refer(c14, indet) & varia(c14, 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(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(nelson_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(mandela_0, fe) & sort(c18, d) & sort(c18, io) & card(c18, int1) & etype(c18, int0) & fact(c18, real) & gener(c18, sp) & quant(c18, one) & refer(c18, det) & varia(c18, con) & sort(neugew__344hlt_1_1, gq) & sort(abgeordneten_haus_1_2, d) & sort(abgeordneten_haus_1_2, io) & card(abgeordneten_haus_1_2, int1) & etype(abgeordneten_haus_1_2, int0) & fact(abgeordneten_haus_1_2, real) & gener(abgeordneten_haus_1_2, ge) & quant(abgeordneten_haus_1_2, one) & refer(abgeordneten_haus_1_2, refer_c) & varia(abgeordneten_haus_1_2, varia_c) & sort(c25, d) & card(c25, int1) & etype(c25, int0) & fact(c25, real) & gener(c25, sp) & quant(c25, one) & refer(c25, det) & varia(c25, con) & sort(schwarz_1_1, tq) & sort(c27, d) & card(c27, int1) & etype(c27, int0) & fact(c27, real) & gener(c27, ge) & quant(c27, one) & refer(c27, refer_c) & varia(c27, varia_c) & sort(erst_1_1, oq) & card(erst_1_1, int1) & sort(pr__344sident_1_1, d) & card(pr__344sident_1_1, int1) & etype(pr__344sident_1_1, int0) & fact(pr__344sident_1_1, real) & gener(pr__344sident_1_1, ge) & quant(pr__344sident_1_1, one) & refer(pr__344sident_1_1, refer_c) & varia(pr__344sident_1_1, varia_c) & sort(c33, d) & sort(c33, io) & card(c33, int1) & etype(c33, int0) & fact(c33, real) & gener(c33, sp) & quant(c33, one) & refer(c33, det) & varia(c33, con) & 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(c38, da) & fact(c38, real) & gener(c38, sp) & sort(c47, st) & fact(c47, real) & gener(c47, sp) & sort(w__344hlen_1_2, da) & fact(w__344hlen_1_2, real) & gener(w__344hlen_1_2, ge) & sort(c5, ta) & card(c5, int1) & etype(c5, int0) & fact(c5, real) & gener(c5, sp) & quant(c5, one) & refer(c5, det) & varia(c5, con) & sort(rprs_0, st) & fact(rprs_0, real) & gener(rprs_0, gener_c) & sort(montag__1_1, ta) & card(montag__1_1, int1) & etype(montag__1_1, int0) & fact(montag__1_1, real) & gener(montag__1_1, ge) & quant(montag__1_1, one) & refer(montag__1_1, refer_c) & varia(montag__1_1, varia_c), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27
% 113.77/110.27 cnf(1, plain, [pmod(_192492, erst_1_1, pr__344sident_1_1), arg1(_192487, _192484), arg2(_192487, _192488), attr(_192484, _192485), attr(_192484, _192486), attr(_192489, _192490), obj(_192491, _192484), prop(_192488, schwarz_1_1), rslt(_192491, _192487), sub(_192485, familiename_1_1), sub(_192486, eigenname_1_1), sub(_192488, _192492), subr(_192487, rprs_0), subs(_192491, w__344hlen_1_2), val(_192485, mandela_0), val(_192486, nelson_0)], clausify(synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(2, plain, [-(attr(c12, c13))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(3, plain, [-(attr(c12, c14))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(4, plain, [-(sub(c13, eigenname_1_1))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(5, plain, [-(val(c13, nelson_0))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(6, plain, [-(sub(c14, familiename_1_1))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(7, plain, [-(val(c14, mandela_0))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(8, plain, [-(prop(c25, schwarz_1_1))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(9, plain, [-(sub(c25, c27))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(10, plain, [-(pmod(c27, erst_1_1, pr__344sident_1_1))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(11, plain, [-(obj(c38, c12))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(12, plain, [-(rslt(c38, c47))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(13, plain, [-(subs(c38, w__344hlen_1_2))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(14, plain, [-(arg1(c47, c12))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(15, plain, [-(arg2(c47, c25))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27 cnf(16, plain, [-(subr(c47, rprs_0))], clausify(ave07_era5_synth_qa07_010_mira_news_1614)).
% 113.77/110.27
% 113.77/110.27 cnf('1',plain,[pmod(c27, erst_1_1, pr__344sident_1_1), arg1(c47, c12), arg2(c47, c25), attr(c12, c14), attr(c12, c13), attr(c12, c13), obj(c38, c12), prop(c25, schwarz_1_1), rslt(c38, c47), sub(c14, familiename_1_1), sub(c13, eigenname_1_1), sub(c25, c27), subr(c47, rprs_0), subs(c38, w__344hlen_1_2), val(c14, mandela_0), val(c13, nelson_0)],start(1,bind([[_192489, _192490, _192484, _192488, _192492, _192487, _192491, _192485, _192486], [c12, c13, c12, c25, c27, c47, c38, c14, c13]]))).
% 113.77/110.27 cnf('1.1',plain,[-(pmod(c27, erst_1_1, pr__344sident_1_1))],extension(10)).
% 113.77/110.27 cnf('1.2',plain,[-(arg1(c47, c12))],extension(14)).
% 113.77/110.27 cnf('1.3',plain,[-(arg2(c47, c25))],extension(15)).
% 113.77/110.27 cnf('1.4',plain,[-(attr(c12, c14))],extension(3)).
% 113.77/110.27 cnf('1.5',plain,[-(attr(c12, c13))],extension(2)).
% 113.77/110.27 cnf('1.6',plain,[-(attr(c12, c13))],extension(2)).
% 113.77/110.27 cnf('1.7',plain,[-(obj(c38, c12))],extension(11)).
% 113.77/110.27 cnf('1.8',plain,[-(prop(c25, schwarz_1_1))],extension(8)).
% 113.77/110.27 cnf('1.9',plain,[-(rslt(c38, c47))],extension(12)).
% 113.77/110.27 cnf('1.10',plain,[-(sub(c14, familiename_1_1))],extension(6)).
% 113.77/110.27 cnf('1.11',plain,[-(sub(c13, eigenname_1_1))],extension(4)).
% 113.77/110.27 cnf('1.12',plain,[-(sub(c25, c27))],extension(9)).
% 113.77/110.27 cnf('1.13',plain,[-(subr(c47, rprs_0))],extension(16)).
% 113.77/110.27 cnf('1.14',plain,[-(subs(c38, w__344hlen_1_2))],extension(13)).
% 113.77/110.27 cnf('1.15',plain,[-(val(c14, mandela_0))],extension(7)).
% 113.77/110.27 cnf('1.16',plain,[-(val(c13, nelson_0))],extension(5)).
% 113.77/110.27 %-----------------------------------------------------
% 113.77/110.28
% 113.77/110.28 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------