%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : CSR115+78 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n029.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:52 EDT 2022
% Result : Theorem 0.63s 1.40s
% Output : Proof 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.12 % Problem : CSR115+78 : TPTP v8.1.0. Released v4.0.0.
% 0.09/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n029.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 : Thu Jun 9 17:51:52 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.63/1.40 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/1.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.63/1.41
% 0.63/1.41 %-----------------------------------------------------
% 0.63/1.41 fof(synth_qa07_007_mira_wp_488_a19984, conjecture, ? [_434642, _434645, _434648, _434651, _434654, _434657] : (attr(_434648, _434645) & attr(_434654, _434657) & obj(_434651, _434642) & sub(_434642, firma_1_1) & sub(_434645, name_1_1) & val(_434645, bmw_0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.41 fof(ave07_era5_synth_qa07_007_mira_wp_488_a19984, hypothesis, attr(c3868, c3869) & sub(c3868, erzeugnis_1_1) & sub(c3869, name_1_1) & val(c3869, mini_0) & attr(c4652, c4653) & sub(c4652, firma_1_1) & sub(c4653, name_1_1) & val(c4653, bmw_0) & pred(c48902, die_1_1) & sub(c48903, firma_1_1) & sub(c48916, sich_1_1) & attch(c48933, c48935) & attr(c48933, c48934) & sub(c48933, einrichtung_1_2) & sub(c48934, name_1_1) & val(c48934, mg_0) & sub(c48935, group_1_1) & attch(c48937, c48935) & attr(c48937, c48938) & sub(c48937, firma_1_1) & sub(c48938, name_1_1) & val(c48938, rover_0) & tupl_p5(c48992, c48902, c48903, c48916, c48935) & obj(c5513, c5557) & ornt(c5513, c5557) & semrel(c5513, c7) & subs(c5513, gehen_1_2) & attr(c5557, c5558) & attr(c5557, c5570) & sub(c5557, firma_1_1) & sub(c5557, land_1_1) & sub(c5558, name_1_1) & val(c5558, rover_0) & sub(c5570, name_1_1) & val(c5570, ford_0) & bei(c5573, c4652) & loc(c7, c5573) & scar(c7, c3868) & subs(c7, bleiben_1_2) & sort(c3868, co) & card(c3868, card_c) & etype(c3868, etype_c) & fact(c3868, real) & gener(c3868, sp) & quant(c3868, quant_c) & refer(c3868, det) & varia(c3868, con) & sort(c3869, na) & card(c3869, int1) & etype(c3869, int0) & fact(c3869, real) & gener(c3869, sp) & quant(c3869, one) & refer(c3869, indet) & varia(c3869, varia_c) & sort(erzeugnis_1_1, co) & card(erzeugnis_1_1, card_c) & etype(erzeugnis_1_1, etype_c) & fact(erzeugnis_1_1, real) & gener(erzeugnis_1_1, ge) & quant(erzeugnis_1_1, quant_c) & refer(erzeugnis_1_1, refer_c) & varia(erzeugnis_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(mini_0, fe) & sort(c4652, d) & sort(c4652, io) & card(c4652, int1) & etype(c4652, int0) & fact(c4652, real) & gener(c4652, sp) & quant(c4652, one) & refer(c4652, det) & varia(c4652, con) & sort(c4653, na) & card(c4653, int1) & etype(c4653, int0) & fact(c4653, real) & gener(c4653, sp) & quant(c4653, one) & refer(c4653, indet) & varia(c4653, varia_c) & sort(firma_1_1, d) & sort(firma_1_1, io) & card(firma_1_1, int1) & etype(firma_1_1, int0) & fact(firma_1_1, real) & gener(firma_1_1, ge) & quant(firma_1_1, one) & refer(firma_1_1, refer_c) & varia(firma_1_1, varia_c) & sort(bmw_0, fe) & sort(c48902, o) & card(c48902, int2000) & etype(c48902, int1) & fact(c48902, real) & gener(c48902, gener_c) & quant(c48902, nfquant) & refer(c48902, refer_c) & varia(c48902, varia_c) & sort(die_1_1, o) & card(die_1_1, int1) & etype(die_1_1, int0) & fact(die_1_1, real) & gener(die_1_1, ge) & quant(die_1_1, one) & refer(die_1_1, refer_c) & varia(die_1_1, varia_c) & sort(c48903, d) & sort(c48903, io) & card(c48903, int1) & etype(c48903, int0) & fact(c48903, real) & gener(c48903, gener_c) & quant(c48903, one) & refer(c48903, refer_c) & varia(c48903, varia_c) & sort(c48916, o) & card(c48916, int1) & etype(c48916, int0) & fact(c48916, real) & gener(c48916, gener_c) & quant(c48916, one) & refer(c48916, refer_c) & varia(c48916, varia_c) & sort(sich_1_1, o) & card(sich_1_1, int1) & etype(sich_1_1, int0) & fact(sich_1_1, real) & gener(sich_1_1, gener_c) & quant(sich_1_1, one) & refer(sich_1_1, refer_c) & varia(sich_1_1, varia_c) & sort(c48933, d) & sort(c48933, io) & card(c48933, int1) & etype(c48933, int1) & fact(c48933, real) & gener(c48933, sp) & quant(c48933, one) & refer(c48933, det) & varia(c48933, con) & sort(c48935, o) & card(c48935, int1) & etype(c48935, int0) & fact(c48935, real) & gener(c48935, sp) & quant(c48935, one) & refer(c48935, det) & varia(c48935, varia_c) & sort(c48934, na) & card(c48934, int1) & etype(c48934, int0) & fact(c48934, real) & gener(c48934, sp) & quant(c48934, one) & refer(c48934, indet) & varia(c48934, varia_c) & sort(einrichtung_1_2, d) & sort(einrichtung_1_2, io) & card(einrichtung_1_2, card_c) & etype(einrichtung_1_2, int1) & fact(einrichtung_1_2, real) & gener(einrichtung_1_2, ge) & quant(einrichtung_1_2, quant_c) & refer(einrichtung_1_2, refer_c) & varia(einrichtung_1_2, varia_c) & sort(mg_0, fe) & sort(group_1_1, o) & card(group_1_1, int1) & etype(group_1_1, int0) & fact(group_1_1, real) & gener(group_1_1, ge) & quant(group_1_1, one) & refer(group_1_1, refer_c) & varia(group_1_1, varia_c) & sort(c48937, d) & sort(c48937, io) & card(c48937, int1) & etype(c48937, int0) & fact(c48937, real) & gener(c48937, sp) & quant(c48937, one) & refer(c48937, det) & varia(c48937, con) & sort(c48938, na) & card(c48938, int1) & etype(c48938, int0) & fact(c48938, real) & gener(c48938, sp) & quant(c48938, one) & refer(c48938, indet) & varia(c48938, varia_c) & sort(rover_0, fe) & sort(c48992, ent) & card(c48992, card_c) & etype(c48992, etype_c) & fact(c48992, real) & gener(c48992, gener_c) & quant(c48992, quant_c) & refer(c48992, refer_c) & varia(c48992, varia_c) & sort(c5513, dn) & fact(c5513, real) & gener(c5513, sp) & sort(c5557, d) & sort(c5557, io) & card(c5557, int1) & etype(c5557, int0) & fact(c5557, real) & gener(c5557, sp) & quant(c5557, one) & refer(c5557, det) & varia(c5557, varia_c) & sort(c7, st) & fact(c7, real) & gener(c7, sp) & sort(gehen_1_2, dn) & fact(gehen_1_2, real) & gener(gehen_1_2, ge) & sort(c5558, na) & card(c5558, int1) & etype(c5558, int0) & fact(c5558, real) & gener(c5558, sp) & quant(c5558, one) & refer(c5558, det) & varia(c5558, varia_c) & sort(c5570, na) & card(c5570, int1) & etype(c5570, int0) & fact(c5570, real) & gener(c5570, sp) & quant(c5570, one) & refer(c5570, indet) & varia(c5570, 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(ford_0, fe) & sort(c5573, l) & card(c5573, int1) & etype(c5573, int0) & fact(c5573, real) & gener(c5573, sp) & quant(c5573, one) & refer(c5573, det) & varia(c5573, con) & sort(bleiben_1_2, st) & fact(bleiben_1_2, real) & gener(bleiben_1_2, ge), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42
% 0.63/1.42 cnf(1, plain, [attr(_193306, _193305), attr(_193308, _193309), obj(_193307, _193304), sub(_193304, firma_1_1), sub(_193305, name_1_1), val(_193305, bmw_0)], clausify(synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(2, plain, [-(attr(c3868, c3869))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(3, plain, [-(attr(c4652, c4653))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(4, plain, [-(sub(c4653, name_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(5, plain, [-(val(c4653, bmw_0))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(6, plain, [-(obj(c5513, c5557))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42 cnf(7, plain, [-(sub(c5557, firma_1_1))], clausify(ave07_era5_synth_qa07_007_mira_wp_488_a19984)).
% 0.63/1.42
% 0.63/1.42 cnf('1',plain,[attr(c4652, c4653), attr(c3868, c3869), obj(c5513, c5557), sub(c5557, firma_1_1), sub(c4653, name_1_1), val(c4653, bmw_0)],start(1,bind([[_193306, _193308, _193309, _193307, _193304, _193305], [c4652, c3868, c3869, c5513, c5557, c4653]]))).
% 0.63/1.42 cnf('1.1',plain,[-(attr(c4652, c4653))],extension(3)).
% 0.63/1.42 cnf('1.2',plain,[-(attr(c3868, c3869))],extension(2)).
% 0.63/1.42 cnf('1.3',plain,[-(obj(c5513, c5557))],extension(6)).
% 0.63/1.42 cnf('1.4',plain,[-(sub(c5557, firma_1_1))],extension(7)).
% 0.63/1.42 cnf('1.5',plain,[-(sub(c4653, name_1_1))],extension(4)).
% 0.63/1.42 cnf('1.6',plain,[-(val(c4653, bmw_0))],extension(5)).
% 0.63/1.42 %-----------------------------------------------------
% 0.63/1.42
% 0.63/1.42 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------