%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : LAT362+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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 : Sun Jul 17 05:43:25 EDT 2022
% Result : Theorem 0.63s 1.41s
% Output : Proof 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : LAT362+1 : TPTP v8.1.0. Released v3.4.0.
% 0.04/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n004.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 : Thu Jun 30 07:07:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.63/1.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.63/1.42 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.63/1.42
% 0.63/1.42 %-----------------------------------------------------
% 0.63/1.42 fof(t20_waybel34, conjecture, ! [_270785] : (~ v2_setfam_1(_270785) => r2_functor0(k4_waybel34(_270785), k5_waybel34(_270785))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t20_waybel34)).
% 0.63/1.42 fof(cc2_setfam_1, axiom, ! [_271116] : (~ v2_setfam_1(_271116) => ~ v1_xboole_0(_271116)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', cc2_setfam_1)).
% 0.63/1.42 fof(d41_functor0, axiom, ! [_271273] : (~ v3_struct_0(_271273) & v2_altcat_1(_271273) & v12_altcat_1(_271273) & l2_altcat_1(_271273) => ! [_271311] : (~ v3_struct_0(_271311) & v2_altcat_1(_271311) & v12_altcat_1(_271311) & l2_altcat_1(_271311) => (r2_functor0(_271273, _271311) <=> ? [_271359] : (m2_functor0(_271359, _271273, _271311) & v21_functor0(_271359, _271273, _271311) & v16_functor0(_271359, _271273, _271311))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d41_functor0)).
% 0.63/1.42 fof(dt_k4_waybel34, axiom, ! [_271733] : (~ v1_xboole_0(_271733) => ~ v3_struct_0(k4_waybel34(_271733)) & v2_altcat_1(k4_waybel34(_271733)) & v6_altcat_1(k4_waybel34(_271733)) & v11_altcat_1(k4_waybel34(_271733)) & v12_altcat_1(k4_waybel34(_271733)) & v2_yellow21(k4_waybel34(_271733)) & l2_altcat_1(k4_waybel34(_271733))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k4_waybel34)).
% 0.63/1.42 fof(dt_k5_waybel34, axiom, ! [_272096] : (~ v1_xboole_0(_272096) => ~ v3_struct_0(k5_waybel34(_272096)) & v2_altcat_1(k5_waybel34(_272096)) & v6_altcat_1(k5_waybel34(_272096)) & v11_altcat_1(k5_waybel34(_272096)) & v12_altcat_1(k5_waybel34(_272096)) & v2_yellow21(k5_waybel34(_272096)) & l2_altcat_1(k5_waybel34(_272096))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k5_waybel34)).
% 0.63/1.42 fof(dt_k6_waybel34, axiom, ! [_272460] : (~ v2_setfam_1(_272460) => v9_functor0(k6_waybel34(_272460), k4_waybel34(_272460), k5_waybel34(_272460)) & v16_functor0(k6_waybel34(_272460), k4_waybel34(_272460), k5_waybel34(_272460)) & m2_functor0(k6_waybel34(_272460), k4_waybel34(_272460), k5_waybel34(_272460))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k6_waybel34)).
% 0.63/1.42 fof(fc7_waybel34, axiom, ! [_272837] : (~ v2_setfam_1(_272837) => v6_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v8_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v9_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v11_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v12_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v14_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v16_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837)) & v21_functor0(k6_waybel34(_272837), k4_waybel34(_272837), k5_waybel34(_272837))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fc7_waybel34)).
% 0.63/1.42
% 0.63/1.42 cnf(1, plain, [v2_setfam_1(31 ^ [])], clausify(t20_waybel34)).
% 0.63/1.42 cnf(2, plain, [r2_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))], clausify(t20_waybel34)).
% 0.63/1.42 cnf(3, plain, [-(_80128 = _80128)], theory(equality)).
% 0.63/1.42 cnf(4, plain, [-(m2_functor0(_89067, _89234, _89397)), m2_functor0(_88982, _89151, _89316), _88982 = _89067, _89151 = _89234, _89316 = _89397], theory(equality)).
% 0.63/1.42 cnf(5, plain, [-(v16_functor0(_98216, _98383, _98546)), v16_functor0(_98131, _98300, _98465), _98131 = _98216, _98300 = _98383, _98465 = _98546], theory(equality)).
% 0.63/1.42 cnf(6, plain, [-(v21_functor0(_104214, _104381, _104544)), v21_functor0(_104129, _104298, _104463), _104129 = _104214, _104298 = _104381, _104463 = _104544], theory(equality)).
% 0.63/1.42 cnf(7, plain, [-(v2_setfam_1(_137459)), v1_xboole_0(_137459)], clausify(cc2_setfam_1)).
% 0.63/1.42 cnf(8, plain, [l2_altcat_1(_144299), v12_altcat_1(_144299), v2_altcat_1(_144299), -(v3_struct_0(_144299)), l2_altcat_1(_144621), v12_altcat_1(_144621), v2_altcat_1(_144621), -(v3_struct_0(_144621)), -(r2_functor0(_144299, _144621)), m2_functor0(_144980, _144299, _144621), v21_functor0(_144980, _144299, _144621), v16_functor0(_144980, _144299, _144621)], clausify(d41_functor0)).
% 0.63/1.42 cnf(9, plain, [-(v1_xboole_0(_150517)), v3_struct_0(k4_waybel34(_150517))], clausify(dt_k4_waybel34)).
% 0.63/1.42 cnf(10, plain, [-(v1_xboole_0(_150517)), -(v2_altcat_1(k4_waybel34(_150517)))], clausify(dt_k4_waybel34)).
% 0.63/1.42 cnf(11, plain, [-(v1_xboole_0(_150517)), -(v12_altcat_1(k4_waybel34(_150517)))], clausify(dt_k4_waybel34)).
% 0.63/1.42 cnf(12, plain, [-(v1_xboole_0(_150517)), -(l2_altcat_1(k4_waybel34(_150517)))], clausify(dt_k4_waybel34)).
% 0.63/1.42 cnf(13, plain, [-(v1_xboole_0(_151237)), v3_struct_0(k5_waybel34(_151237))], clausify(dt_k5_waybel34)).
% 0.63/1.42 cnf(14, plain, [-(v1_xboole_0(_151237)), -(v2_altcat_1(k5_waybel34(_151237)))], clausify(dt_k5_waybel34)).
% 0.63/1.42 cnf(15, plain, [-(v1_xboole_0(_151237)), -(v12_altcat_1(k5_waybel34(_151237)))], clausify(dt_k5_waybel34)).
% 0.63/1.42 cnf(16, plain, [-(v1_xboole_0(_151237)), -(l2_altcat_1(k5_waybel34(_151237)))], clausify(dt_k5_waybel34)).
% 0.63/1.42 cnf(17, plain, [-(v2_setfam_1(_151957)), -(v16_functor0(k6_waybel34(_151957), k4_waybel34(_151957), k5_waybel34(_151957)))], clausify(dt_k6_waybel34)).
% 0.63/1.42 cnf(18, plain, [-(v2_setfam_1(_151957)), -(m2_functor0(k6_waybel34(_151957), k4_waybel34(_151957), k5_waybel34(_151957)))], clausify(dt_k6_waybel34)).
% 0.63/1.42 cnf(19, plain, [-(v2_setfam_1(_171864)), -(v21_functor0(k6_waybel34(_171864), k4_waybel34(_171864), k5_waybel34(_171864)))], clausify(fc7_waybel34)).
% 0.63/1.42
% 0.63/1.42 cnf('1',plain,[r2_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))],start(2)).
% 0.63/1.42 cnf('1.1',plain,[-(r2_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), l2_altcat_1(k4_waybel34(31 ^ [])), v12_altcat_1(k4_waybel34(31 ^ [])), v2_altcat_1(k4_waybel34(31 ^ [])), -(v3_struct_0(k4_waybel34(31 ^ []))), l2_altcat_1(k5_waybel34(31 ^ [])), v12_altcat_1(k5_waybel34(31 ^ [])), v2_altcat_1(k5_waybel34(31 ^ [])), -(v3_struct_0(k5_waybel34(31 ^ []))), m2_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), v21_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))],extension(8,bind([[_144980, _144299, _144621], [k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.1',plain,[-(l2_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(12,bind([[_150517], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.1.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.1.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.2',plain,[-(v12_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(11,bind([[_150517], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.2.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.2.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.3',plain,[-(v2_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(10,bind([[_150517], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.3.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.3.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.4',plain,[v3_struct_0(k4_waybel34(31 ^ [])), -(v1_xboole_0(31 ^ []))],extension(9,bind([[_150517], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.4.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.4.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.5',plain,[-(l2_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(16,bind([[_151237], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.5.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.5.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.6',plain,[-(v12_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(15,bind([[_151237], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.6.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.6.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.7',plain,[-(v2_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(14,bind([[_151237], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.7.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.7.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.8',plain,[v3_struct_0(k5_waybel34(31 ^ [])), -(v1_xboole_0(31 ^ []))],extension(13,bind([[_151237], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.8.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_137459], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.8.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.9',plain,[-(m2_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), m2_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []), k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []), k5_waybel34(31 ^ []) = k5_waybel34(31 ^ [])],extension(4,bind([[_88982, _89067, _89151, _89234, _89316, _89397], [k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.9.1',plain,[-(m2_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(18,bind([[_151957], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.9.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.9.2',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_80128], [k6_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.9.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_80128], [k4_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.9.4',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_80128], [k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.10',plain,[-(v21_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), v21_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []), k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []), k5_waybel34(31 ^ []) = k5_waybel34(31 ^ [])],extension(6,bind([[_104129, _104214, _104298, _104381, _104463, _104544], [k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.10.1',plain,[-(v21_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(19,bind([[_171864], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.10.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.10.2',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_80128], [k6_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.10.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_80128], [k4_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.10.4',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_80128], [k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.11',plain,[-(v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []), k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []), k5_waybel34(31 ^ []) = k5_waybel34(31 ^ [])],extension(5,bind([[_98131, _98216, _98300, _98383, _98465, _98546], [k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.11.1',plain,[-(v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(17,bind([[_151957], [31 ^ []]]))).
% 0.63/1.42 cnf('1.1.11.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 0.63/1.42 cnf('1.1.11.2',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_80128], [k6_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.11.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_80128], [k4_waybel34(31 ^ [])]]))).
% 0.63/1.42 cnf('1.1.11.4',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_80128], [k5_waybel34(31 ^ [])]]))).
% 0.63/1.42 %-----------------------------------------------------
% 0.63/1.43
% 0.63/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------