%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n003.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 : Tue Jul 19 12:02:22 EDT 2022
% Result : Theorem 26.15s 26.30s
% Output : Proof 26.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU374+1 : TPTP v8.1.0. Released v3.3.0.
% 0.04/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jun 19 00:24:58 EDT 2022
% 0.13/0.34 % CPUTime :
% 26.15/26.30 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.15/26.31 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.15/26.32
% 26.15/26.32 %-----------------------------------------------------
% 26.15/26.32 fof(t20_yellow_6, conjecture, ! [_87034] : (one_sorted_str(_87034) => ! [_87049] : (net_str(_87049, _87034) => ! [_87067] : (subnetstr(_87067, _87034, _87049) => ! [_87088] : (element(_87088, the_carrier(_87049)) => ! [_87110] : (element(_87110, the_carrier(_87049)) => ! [_87132] : (element(_87132, the_carrier(_87067)) => ! [_87154] : (element(_87154, the_carrier(_87067)) => _87088 = _87132 & _87110 = _87154 & related(_87067, _87132, _87154) => related(_87049, _87088, _87110)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t20_yellow_6)).
% 26.15/26.32 fof(d8_yellow_6, axiom, ! [_87795] : (one_sorted_str(_87795) => ! [_87810] : (net_str(_87810, _87795) => ! [_87828] : (net_str(_87828, _87795) => (subnetstr(_87828, _87795, _87810) <=> subrelstr(_87828, _87810) & the_mapping(_87795, _87828) = relation_dom_restr_as_relation_of(the_carrier(_87810), the_carrier(_87795), the_mapping(_87795, _87810), the_carrier(_87828)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d8_yellow_6)).
% 26.15/26.32 fof(dt_l1_waybel_0, axiom, ! [_88192] : (one_sorted_str(_88192) => ! [_88207] : (net_str(_88207, _88192) => rel_str(_88207))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_l1_waybel_0)).
% 26.15/26.32 fof(dt_m1_yellow_6, axiom, ! [_88372, _88375] : (one_sorted_str(_88372) & net_str(_88375, _88372) => ! [_88400] : (subnetstr(_88400, _88372, _88375) => net_str(_88400, _88372))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_m1_yellow_6)).
% 26.15/26.32 fof(t60_yellow_0, axiom, ! [_88661] : (rel_str(_88661) => ! [_88676] : (subrelstr(_88676, _88661) => ! [_88694] : (element(_88694, the_carrier(_88661)) => ! [_88716] : (element(_88716, the_carrier(_88661)) => ! [_88738] : (element(_88738, the_carrier(_88676)) => ! [_88760] : (element(_88760, the_carrier(_88676)) => _88738 = _88694 & _88760 = _88716 & related(_88676, _88738, _88760) => related(_88661, _88694, _88716))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t60_yellow_0)).
% 26.15/26.32
% 26.15/26.32 cnf(1, plain, [-(one_sorted_str(19 ^ []))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(2, plain, [-(net_str(20 ^ [], 19 ^ []))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(3, plain, [-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(4, plain, [-(element(22 ^ [], the_carrier(20 ^ [])))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(5, plain, [-(element(23 ^ [], the_carrier(20 ^ [])))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(6, plain, [-(element(24 ^ [], the_carrier(21 ^ [])))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(7, plain, [-(element(25 ^ [], the_carrier(21 ^ [])))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(8, plain, [-(22 ^ [] = 24 ^ [])], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(9, plain, [-(23 ^ [] = 25 ^ [])], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(10, plain, [-(related(21 ^ [], 24 ^ [], 25 ^ []))], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(11, plain, [related(20 ^ [], 22 ^ [], 23 ^ [])], clausify(t20_yellow_6)).
% 26.15/26.32 cnf(12, plain, [_25110 = _25155, -(_25155 = _25110)], theory(equality)).
% 26.15/26.32 cnf(13, plain, [one_sorted_str(_42394), net_str(_42523, _42394), net_str(_42667, _42394), subnetstr(_42667, _42394, _42523), -(subrelstr(_42667, _42523))], clausify(d8_yellow_6)).
% 26.15/26.32 cnf(14, plain, [one_sorted_str(_45153), net_str(_45240, _45153), -(rel_str(_45240))], clausify(dt_l1_waybel_0)).
% 26.15/26.32 cnf(15, plain, [net_str(_46171, _46109), one_sorted_str(_46109), subnetstr(_46344, _46109, _46171), -(net_str(_46344, _46109))], clausify(dt_m1_yellow_6)).
% 26.15/26.32 cnf(16, plain, [rel_str(_58293), subrelstr(_58453, _58293), element(_58628, the_carrier(_58293)), element(_58812, the_carrier(_58293)), element(_58987, the_carrier(_58453)), element(_59153, the_carrier(_58453)), -(related(_58293, _58628, _58812)), _58987 = _58628, _59153 = _58812, related(_58453, _58987, _59153)], clausify(t60_yellow_0)).
% 26.15/26.32
% 26.15/26.32 cnf('1',plain,[related(20 ^ [], 22 ^ [], 23 ^ [])],start(11)).
% 26.15/26.32 cnf('1.1',plain,[-(related(20 ^ [], 22 ^ [], 23 ^ [])), rel_str(20 ^ []), subrelstr(21 ^ [], 20 ^ []), element(22 ^ [], the_carrier(20 ^ [])), element(23 ^ [], the_carrier(20 ^ [])), element(24 ^ [], the_carrier(21 ^ [])), element(25 ^ [], the_carrier(21 ^ [])), 24 ^ [] = 22 ^ [], 25 ^ [] = 23 ^ [], related(21 ^ [], 24 ^ [], 25 ^ [])],extension(16,bind([[_58293, _58628, _58812, _58453, _58987, _59153], [20 ^ [], 22 ^ [], 23 ^ [], 21 ^ [], 24 ^ [], 25 ^ []]]))).
% 26.15/26.32 cnf('1.1.1',plain,[-(rel_str(20 ^ [])), one_sorted_str(19 ^ []), net_str(20 ^ [], 19 ^ [])],extension(14,bind([[_45240, _45153], [20 ^ [], 19 ^ []]]))).
% 26.15/26.32 cnf('1.1.1.1',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 26.15/26.32 cnf('1.1.1.2',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 26.15/26.32 cnf('1.1.2',plain,[-(subrelstr(21 ^ [], 20 ^ [])), one_sorted_str(19 ^ []), net_str(20 ^ [], 19 ^ []), net_str(21 ^ [], 19 ^ []), subnetstr(21 ^ [], 19 ^ [], 20 ^ [])],extension(13,bind([[_42667, _42394, _42523], [21 ^ [], 19 ^ [], 20 ^ []]]))).
% 26.15/26.32 cnf('1.1.2.1',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 26.15/26.32 cnf('1.1.2.2',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 26.15/26.32 cnf('1.1.2.3',plain,[-(net_str(21 ^ [], 19 ^ [])), net_str(20 ^ [], 19 ^ []), one_sorted_str(19 ^ []), subnetstr(21 ^ [], 19 ^ [], 20 ^ [])],extension(15,bind([[_46344, _46109, _46171], [21 ^ [], 19 ^ [], 20 ^ []]]))).
% 26.15/26.32 cnf('1.1.2.3.1',plain,[-(net_str(20 ^ [], 19 ^ []))],extension(2)).
% 26.15/26.32 cnf('1.1.2.3.2',plain,[-(one_sorted_str(19 ^ []))],extension(1)).
% 26.15/26.32 cnf('1.1.2.3.3',plain,[-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))],extension(3)).
% 26.15/26.32 cnf('1.1.2.4',plain,[-(subnetstr(21 ^ [], 19 ^ [], 20 ^ []))],extension(3)).
% 26.15/26.32 cnf('1.1.3',plain,[-(element(22 ^ [], the_carrier(20 ^ [])))],extension(4)).
% 26.15/26.32 cnf('1.1.4',plain,[-(element(23 ^ [], the_carrier(20 ^ [])))],extension(5)).
% 26.15/26.32 cnf('1.1.5',plain,[-(element(24 ^ [], the_carrier(21 ^ [])))],extension(6)).
% 26.15/26.32 cnf('1.1.6',plain,[-(element(25 ^ [], the_carrier(21 ^ [])))],extension(7)).
% 26.15/26.32 cnf('1.1.7',plain,[-(24 ^ [] = 22 ^ []), 22 ^ [] = 24 ^ []],extension(12,bind([[_25110, _25155], [22 ^ [], 24 ^ []]]))).
% 26.15/26.32 cnf('1.1.7.1',plain,[-(22 ^ [] = 24 ^ [])],extension(8)).
% 26.15/26.32 cnf('1.1.8',plain,[-(25 ^ [] = 23 ^ []), 23 ^ [] = 25 ^ []],extension(12,bind([[_25110, _25155], [23 ^ [], 25 ^ []]]))).
% 26.15/26.32 cnf('1.1.8.1',plain,[-(23 ^ [] = 25 ^ [])],extension(9)).
% 26.15/26.32 cnf('1.1.9',plain,[-(related(21 ^ [], 24 ^ [], 25 ^ []))],extension(10)).
% 26.15/26.32 %-----------------------------------------------------
% 26.15/26.32
% 26.15/26.32 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------