%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU411+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n006.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:39 EDT 2022
% Result : Theorem 2.00s 2.45s
% Output : Proof 2.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU411+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.14/0.34 % Computer : n006.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 : Mon Jun 20 00:52:10 EDT 2022
% 0.14/0.34 % CPUTime :
% 2.00/2.45 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.00/2.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.00/2.47
% 2.00/2.47 %-----------------------------------------------------
% 2.00/2.47 fof(t20_latsum_1, conjecture, ! [_70981] : (~ v3_struct_0(_70981) & v2_orders_2(_70981) & v3_orders_2(_70981) & v4_orders_2(_70981) & v1_yellow_0(_70981) & v1_lattice3(_70981) & l1_orders_2(_70981) => ! [_71040] : (~ v3_struct_0(_71040) & v2_orders_2(_71040) & v3_orders_2(_71040) & v4_orders_2(_71040) & v1_yellow_0(_71040) & v1_lattice3(_71040) & l1_orders_2(_71040) => ~ v1_xboole_0(k3_xboole_0(u1_struct_0(_70981), u1_struct_0(_71040))) & v1_waybel_0(k3_xboole_0(u1_struct_0(_70981), u1_struct_0(_71040)), _71040) & v12_waybel_0(k3_xboole_0(u1_struct_0(_70981), u1_struct_0(_71040)), _71040) & m1_subset_1(k3_xboole_0(u1_struct_0(_70981), u1_struct_0(_71040)), k1_zfmisc_1(u1_struct_0(_71040))) => r2_hidden(k3_yellow_0(_71040), u1_struct_0(_70981)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t20_latsum_1)).
% 2.00/2.47 fof(d19_waybel_0, axiom, ! [_71914] : (l1_orders_2(_71914) => ! [_71929] : (m1_subset_1(_71929, k1_zfmisc_1(u1_struct_0(_71914))) => (v12_waybel_0(_71929, _71914) <=> ! [_71965] : (m1_subset_1(_71965, u1_struct_0(_71914)) => ! [_71987] : (m1_subset_1(_71987, u1_struct_0(_71914)) => r2_hidden(_71965, _71929) & r1_orders_2(_71914, _71987, _71965) => r2_hidden(_71987, _71929)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d19_waybel_0)).
% 2.00/2.47 fof(d1_xboole_0, axiom, ! [_72344] : (_72344 = k1_xboole_0 <=> ! [_72358] : ~ r2_hidden(_72358, _72344)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_xboole_0)).
% 2.00/2.47 fof(d3_xboole_0, axiom, ! [_72512, _72515, _72518] : (_72518 = k3_xboole_0(_72512, _72515) <=> ! [_72539] : (r2_hidden(_72539, _72518) <=> r2_hidden(_72539, _72512) & r2_hidden(_72539, _72515))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_xboole_0)).
% 2.00/2.47 fof(dt_k3_yellow_0, axiom, ! [_72772] : (l1_orders_2(_72772) => m1_subset_1(k3_yellow_0(_72772), u1_struct_0(_72772))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k3_yellow_0)).
% 2.00/2.47 fof(fc1_xboole_0, axiom, v1_xboole_0(k1_xboole_0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc1_xboole_0)).
% 2.00/2.47 fof(t13_latsum_1, axiom, ! [_72985] : (~ v3_struct_0(_72985) & l1_orders_2(_72985) => ! [_73009] : (~ v3_struct_0(_73009) & l1_orders_2(_73009) => ! [_73033] : (r2_hidden(_73033, k3_xboole_0(u1_struct_0(_72985), u1_struct_0(_73009))) => m1_subset_1(_73033, u1_struct_0(_73009))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t13_latsum_1)).
% 2.00/2.47 fof(t44_yellow_0, axiom, ! [_73326] : (~ v3_struct_0(_73326) & v4_orders_2(_73326) & v1_yellow_0(_73326) & l1_orders_2(_73326) => ! [_73364] : (m1_subset_1(_73364, u1_struct_0(_73326)) => r1_orders_2(_73326, k3_yellow_0(_73326), _73364))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t44_yellow_0)).
% 2.00/2.47
% 2.00/2.47 cnf(1, plain, [v3_struct_0(13 ^ [])], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(2, plain, [-(l1_orders_2(13 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(3, plain, [v3_struct_0(14 ^ [])], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(4, plain, [-(v4_orders_2(14 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(5, plain, [-(v1_yellow_0(14 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(6, plain, [-(l1_orders_2(14 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(7, plain, [v1_xboole_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(8, plain, [-(v12_waybel_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), 14 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(9, plain, [-(m1_subset_1(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), k1_zfmisc_1(u1_struct_0(14 ^ []))))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(10, plain, [r2_hidden(k3_yellow_0(14 ^ []), u1_struct_0(13 ^ []))], clausify(t20_latsum_1)).
% 2.00/2.47 cnf(11, plain, [-(k3_xboole_0(_28881, _29014) = k3_xboole_0(_28948, _29079)), _28881 = _28948, _29014 = _29079], theory(equality)).
% 2.00/2.47 cnf(12, plain, [_29824 = _29873, -(u1_struct_0(_29824) = u1_struct_0(_29873))], theory(equality)).
% 2.00/2.47 cnf(13, plain, [-(_19283 = _19283)], theory(equality)).
% 2.00/2.47 cnf(14, plain, [_19436 = _19481, -(_19481 = _19436)], theory(equality)).
% 2.00/2.47 cnf(15, plain, [-(r2_hidden(_23189, _23320)), r2_hidden(_23122, _23255), _23122 = _23189, _23255 = _23320], theory(equality)).
% 2.00/2.47 cnf(16, plain, [-(v1_xboole_0(_26397)), _26348 = _26397, v1_xboole_0(_26348)], theory(equality)).
% 2.00/2.47 cnf(17, plain, [l1_orders_2(_30874), m1_subset_1(_31011, k1_zfmisc_1(u1_struct_0(_30874))), v12_waybel_0(_31011, _30874), m1_subset_1(_31254, u1_struct_0(_30874)), m1_subset_1(_31405, u1_struct_0(_30874)), -(r2_hidden(_31405, _31011)), r2_hidden(_31254, _31011), r1_orders_2(_30874, _31405, _31254)], clausify(d19_waybel_0)).
% 2.00/2.47 cnf(18, plain, [-(_31971 = k1_xboole_0), -(r2_hidden(3 ^ [_31971], _31971))], clausify(d1_xboole_0)).
% 2.00/2.47 cnf(19, plain, [_32434 = k3_xboole_0(_32295, _32365), r2_hidden(_32598, _32434), -(r2_hidden(_32598, _32295))], clausify(d3_xboole_0)).
% 2.00/2.47 cnf(20, plain, [l1_orders_2(_33379), -(m1_subset_1(k3_yellow_0(_33379), u1_struct_0(_33379)))], clausify(dt_k3_yellow_0)).
% 2.00/2.47 cnf(21, plain, [-(v1_xboole_0(k1_xboole_0))], clausify(fc1_xboole_0)).
% 2.00/2.47 cnf(22, plain, [l1_orders_2(_39212), -(v3_struct_0(_39212)), l1_orders_2(_39402), -(v3_struct_0(_39402)), r2_hidden(_39579, k3_xboole_0(u1_struct_0(_39212), u1_struct_0(_39402))), -(m1_subset_1(_39579, u1_struct_0(_39402)))], clausify(t13_latsum_1)).
% 2.00/2.47 cnf(23, plain, [-(r1_orders_2(_41206, k3_yellow_0(_41206), _41491)), m1_subset_1(_41491, u1_struct_0(_41206)), -(v3_struct_0(_41206)), v4_orders_2(_41206), v1_yellow_0(_41206), l1_orders_2(_41206)], clausify(t44_yellow_0)).
% 2.00/2.47
% 2.00/2.47 cnf('1',plain,[v3_struct_0(14 ^ [])],start(3)).
% 2.00/2.47 cnf('1.1',plain,[-(v3_struct_0(14 ^ [])), l1_orders_2(13 ^ []), -(v3_struct_0(13 ^ [])), l1_orders_2(14 ^ []), r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))), -(m1_subset_1(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], u1_struct_0(14 ^ [])))],extension(22,bind([[_39212, _39579, _39402], [13 ^ [], 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], 14 ^ []]]))).
% 2.00/2.47 cnf('1.1.1',plain,[-(l1_orders_2(13 ^ []))],extension(2)).
% 2.00/2.47 cnf('1.1.2',plain,[v3_struct_0(13 ^ [])],extension(1)).
% 2.00/2.47 cnf('1.1.3',plain,[-(l1_orders_2(14 ^ []))],extension(6)).
% 2.00/2.47 cnf('1.1.4',plain,[-(r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))), r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))), 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))] = 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))],extension(15,bind([[_23122, _23189, _23255, _23320], [3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]))).
% 2.00/2.47 cnf('1.1.4.1',plain,[-(r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))), -(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k1_xboole_0)],extension(18,bind([[_31971], [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]))).
% 2.00/2.47 cnf('1.1.4.1.1',plain,[k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k1_xboole_0, -(k1_xboole_0 = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))],extension(14,bind([[_19481, _19436], [k1_xboole_0, k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]))).
% 2.00/2.47 cnf('1.1.4.1.1.1',plain,[k1_xboole_0 = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), -(v1_xboole_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))), v1_xboole_0(k1_xboole_0)],extension(16,bind([[_26397, _26348], [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), k1_xboole_0]]))).
% 2.00/2.47 cnf('1.1.4.1.1.1.1',plain,[v1_xboole_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))],extension(7)).
% 2.00/2.47 cnf('1.1.4.1.1.1.2',plain,[-(v1_xboole_0(k1_xboole_0))],extension(21)).
% 2.00/2.47 cnf('1.1.4.2',plain,[-(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))] = 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))])],extension(13,bind([[_19283], [3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]]))).
% 2.00/2.47 cnf('1.1.4.3',plain,[-(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))), u1_struct_0(13 ^ []) = u1_struct_0(13 ^ []), u1_struct_0(14 ^ []) = u1_struct_0(14 ^ [])],extension(11,bind([[_28881, _28948, _29014, _29079], [u1_struct_0(13 ^ []), u1_struct_0(13 ^ []), u1_struct_0(14 ^ []), u1_struct_0(14 ^ [])]]))).
% 2.00/2.47 cnf('1.1.4.3.1',plain,[-(u1_struct_0(13 ^ []) = u1_struct_0(13 ^ [])), 13 ^ [] = 13 ^ []],extension(12,bind([[_29824, _29873], [13 ^ [], 13 ^ []]]))).
% 2.00/2.47 cnf('1.1.4.3.1.1',plain,[-(13 ^ [] = 13 ^ [])],extension(13,bind([[_19283], [13 ^ []]]))).
% 2.00/2.47 cnf('1.1.4.3.2',plain,[-(u1_struct_0(14 ^ []) = u1_struct_0(14 ^ [])), 14 ^ [] = 14 ^ []],extension(12,bind([[_29824, _29873], [14 ^ [], 14 ^ []]]))).
% 2.00/2.47 cnf('1.1.4.3.2.1',plain,[-(14 ^ [] = 14 ^ [])],extension(13,bind([[_19283], [14 ^ []]]))).
% 2.00/2.47 cnf('1.1.5',plain,[m1_subset_1(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], u1_struct_0(14 ^ [])), -(r1_orders_2(14 ^ [], k3_yellow_0(14 ^ []), 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))])), -(v3_struct_0(14 ^ [])), v4_orders_2(14 ^ []), v1_yellow_0(14 ^ []), l1_orders_2(14 ^ [])],extension(23,bind([[_41491, _41206], [3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], 14 ^ []]]))).
% 2.00/2.47 cnf('1.1.5.1',plain,[r1_orders_2(14 ^ [], k3_yellow_0(14 ^ []), 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]), l1_orders_2(14 ^ []), m1_subset_1(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), k1_zfmisc_1(u1_struct_0(14 ^ []))), v12_waybel_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), 14 ^ []), m1_subset_1(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], u1_struct_0(14 ^ [])), m1_subset_1(k3_yellow_0(14 ^ []), u1_struct_0(14 ^ [])), -(r2_hidden(k3_yellow_0(14 ^ []), k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))), r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))],extension(17,bind([[_30874, _31405, _31254, _31011], [14 ^ [], k3_yellow_0(14 ^ []), 3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]))).
% 2.00/2.47 cnf('1.1.5.1.1',plain,[-(l1_orders_2(14 ^ []))],extension(6)).
% 2.00/2.47 cnf('1.1.5.1.2',plain,[-(m1_subset_1(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), k1_zfmisc_1(u1_struct_0(14 ^ []))))],extension(9)).
% 2.00/2.47 cnf('1.1.5.1.3',plain,[-(v12_waybel_0(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), 14 ^ []))],extension(8)).
% 2.00/2.47 cnf('1.1.5.1.4',plain,[-(m1_subset_1(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], u1_struct_0(14 ^ [])))],reduction('1.1')).
% 2.00/2.47 cnf('1.1.5.1.5',plain,[-(m1_subset_1(k3_yellow_0(14 ^ []), u1_struct_0(14 ^ []))), l1_orders_2(14 ^ [])],extension(20,bind([[_33379], [14 ^ []]]))).
% 2.00/2.47 cnf('1.1.5.1.5.1',plain,[-(l1_orders_2(14 ^ []))],extension(6)).
% 2.00/2.47 cnf('1.1.5.1.6',plain,[r2_hidden(k3_yellow_0(14 ^ []), k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))), k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), -(r2_hidden(k3_yellow_0(14 ^ []), u1_struct_0(13 ^ [])))],extension(19,bind([[_32434, _32365, _32598, _32295], [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])), u1_struct_0(14 ^ []), k3_yellow_0(14 ^ []), u1_struct_0(13 ^ [])]]))).
% 2.00/2.47 cnf('1.1.5.1.6.1',plain,[-(k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])) = k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ [])))],extension(13,bind([[_19283], [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))]]))).
% 2.00/2.47 cnf('1.1.5.1.6.2',plain,[r2_hidden(k3_yellow_0(14 ^ []), u1_struct_0(13 ^ []))],extension(10)).
% 2.00/2.47 cnf('1.1.5.1.7',plain,[-(r2_hidden(3 ^ [k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))], k3_xboole_0(u1_struct_0(13 ^ []), u1_struct_0(14 ^ []))))],lemmata('1.1')).
% 2.00/2.47 cnf('1.1.5.2',plain,[v3_struct_0(14 ^ [])],extension(3)).
% 2.00/2.47 cnf('1.1.5.3',plain,[-(v4_orders_2(14 ^ []))],extension(4)).
% 2.00/2.47 cnf('1.1.5.4',plain,[-(v1_yellow_0(14 ^ []))],extension(5)).
% 2.00/2.47 cnf('1.1.5.5',plain,[-(l1_orders_2(14 ^ []))],extension(6)).
% 2.00/2.47 %-----------------------------------------------------
% 2.00/2.47
% 2.00/2.47 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------