%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : LAT376+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:39 EDT 2022
% Result : Theorem 10.54s 10.69s
% Output : Proof 10.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : LAT376+1 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n004.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Wed Jun 29 08:28:38 EDT 2022
% 0.11/0.33 % CPUTime :
% 10.54/10.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.54/10.70 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.54/10.70
% 10.54/10.70 %-----------------------------------------------------
% 10.54/10.70 fof(t57_waybel34, conjecture, ! [_350717] : (~ v2_setfam_1(_350717) => r3_yellow20(k5_waybel34(_350717), k4_waybel34(_350717), k7_waybel34(_350717), k9_waybel34(_350717), k8_waybel34(_350717))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t57_waybel34)).
% 10.54/10.70 fof(cc2_setfam_1, axiom, ! [_351112] : (~ v2_setfam_1(_351112) => ~ v1_xboole_0(_351112)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cc2_setfam_1)).
% 10.54/10.70 fof(dt_k4_waybel34, axiom, ! [_351297] : (~ v1_xboole_0(_351297) => ~ v3_struct_0(k4_waybel34(_351297)) & v2_altcat_1(k4_waybel34(_351297)) & v6_altcat_1(k4_waybel34(_351297)) & v11_altcat_1(k4_waybel34(_351297)) & v12_altcat_1(k4_waybel34(_351297)) & v2_yellow21(k4_waybel34(_351297)) & l2_altcat_1(k4_waybel34(_351297))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k4_waybel34)).
% 10.54/10.70 fof(dt_k5_waybel34, axiom, ! [_351671] : (~ v1_xboole_0(_351671) => ~ v3_struct_0(k5_waybel34(_351671)) & v2_altcat_1(k5_waybel34(_351671)) & v6_altcat_1(k5_waybel34(_351671)) & v11_altcat_1(k5_waybel34(_351671)) & v12_altcat_1(k5_waybel34(_351671)) & v2_yellow21(k5_waybel34(_351671)) & l2_altcat_1(k5_waybel34(_351671))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k5_waybel34)).
% 10.54/10.70 fof(dt_k6_waybel34, axiom, ! [_352046] : (~ v2_setfam_1(_352046) => v9_functor0(k6_waybel34(_352046), k4_waybel34(_352046), k5_waybel34(_352046)) & v16_functor0(k6_waybel34(_352046), k4_waybel34(_352046), k5_waybel34(_352046)) & m2_functor0(k6_waybel34(_352046), k4_waybel34(_352046), k5_waybel34(_352046))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k6_waybel34)).
% 10.54/10.70 fof(dt_k8_waybel34, axiom, ! [_352354] : (~ v1_xboole_0(_352354) => ~ v3_struct_0(k8_waybel34(_352354)) & v2_altcat_1(k8_waybel34(_352354)) & v6_altcat_1(k8_waybel34(_352354)) & v3_altcat_2(k8_waybel34(_352354), k4_waybel34(_352354)) & m1_altcat_2(k8_waybel34(_352354), k4_waybel34(_352354))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k8_waybel34)).
% 10.54/10.70 fof(dt_k9_waybel34, axiom, ! [_352687] : (~ v2_setfam_1(_352687) => ~ v3_struct_0(k9_waybel34(_352687)) & v2_altcat_1(k9_waybel34(_352687)) & v6_altcat_1(k9_waybel34(_352687)) & v3_altcat_2(k9_waybel34(_352687), k5_waybel34(_352687)) & m1_altcat_2(k9_waybel34(_352687), k5_waybel34(_352687))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k9_waybel34)).
% 10.54/10.70 fof(fc7_waybel34, axiom, ! [_353094] : (~ v2_setfam_1(_353094) => v6_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v8_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v9_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v11_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v12_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v14_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v16_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094)) & v21_functor0(k6_waybel34(_353094), k4_waybel34(_353094), k5_waybel34(_353094))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc7_waybel34)).
% 10.54/10.70 fof(t18_waybel34, axiom, ! [_353773] : (~ v2_setfam_1(_353773) => k15_functor0(k4_waybel34(_353773), k5_waybel34(_353773), k6_waybel34(_353773)) = k7_waybel34(_353773) & k15_functor0(k5_waybel34(_353773), k4_waybel34(_353773), k7_waybel34(_353773)) = k6_waybel34(_353773)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t18_waybel34)).
% 10.54/10.70 fof(t52_yellow20, axiom, ! [_354052] : (~ v3_struct_0(_354052) & v2_altcat_1(_354052) & v11_altcat_1(_354052) & v12_altcat_1(_354052) & l2_altcat_1(_354052) => ! [_354097] : (~ v3_struct_0(_354097) & v2_altcat_1(_354097) & v11_altcat_1(_354097) & v12_altcat_1(_354097) & l2_altcat_1(_354097) => ! [_354142] : (v16_functor0(_354142, _354052, _354097) & m2_functor0(_354142, _354052, _354097) => v21_functor0(_354142, _354052, _354097) => ! [_354189] : (~ v3_struct_0(_354189) & v2_altcat_1(_354189) & v3_altcat_2(_354189, _354052) & m1_altcat_2(_354189, _354052) => ! [_354233] : (~ v3_struct_0(_354233) & v2_altcat_1(_354233) & v3_altcat_2(_354233, _354097) & m1_altcat_2(_354233, _354097) => r3_yellow20(_354052, _354097, _354142, _354189, _354233) => r3_yellow20(_354097, _354052, k15_functor0(_354052, _354097, _354142), _354233, _354189)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t52_yellow20)).
% 10.54/10.70 fof(t56_waybel34, axiom, ! [_354911] : (~ v2_setfam_1(_354911) => r3_yellow20(k4_waybel34(_354911), k5_waybel34(_354911), k6_waybel34(_354911), k8_waybel34(_354911), k9_waybel34(_354911))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t56_waybel34)).
% 10.54/10.70
% 10.54/10.70 cnf(1, plain, [v2_setfam_1(31 ^ [])], clausify(t57_waybel34)).
% 10.54/10.70 cnf(2, plain, [r3_yellow20(k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k7_waybel34(31 ^ []), k9_waybel34(31 ^ []), k8_waybel34(31 ^ []))], clausify(t57_waybel34)).
% 10.54/10.70 cnf(3, plain, [-(_101194 = _101194)], theory(equality)).
% 10.54/10.70 cnf(4, plain, [-(m2_functor0(_110757, _110924, _111087)), m2_functor0(_110672, _110841, _111006), _110672 = _110757, _110841 = _110924, _111006 = _111087], theory(equality)).
% 10.54/10.70 cnf(5, plain, [-(r3_yellow20(_115585, _115824, _116059, _116290, _116517)), r3_yellow20(_115464, _115705, _115942, _116175, _116404), _115464 = _115585, _115705 = _115824, _115942 = _116059, _116175 = _116290, _116404 = _116517], theory(equality)).
% 10.54/10.70 cnf(6, plain, [-(v21_functor0(_127311, _127478, _127641)), v21_functor0(_127226, _127395, _127560), _127226 = _127311, _127395 = _127478, _127560 = _127641], theory(equality)).
% 10.54/10.70 cnf(7, plain, [-(v2_setfam_1(_164966)), v1_xboole_0(_164966)], clausify(cc2_setfam_1)).
% 10.54/10.70 cnf(8, plain, [-(v1_xboole_0(_184456)), v3_struct_0(k4_waybel34(_184456))], clausify(dt_k4_waybel34)).
% 10.54/10.70 cnf(9, plain, [-(v1_xboole_0(_184456)), -(v2_altcat_1(k4_waybel34(_184456)))], clausify(dt_k4_waybel34)).
% 10.54/10.70 cnf(10, plain, [-(v1_xboole_0(_184456)), -(v11_altcat_1(k4_waybel34(_184456)))], clausify(dt_k4_waybel34)).
% 10.54/10.70 cnf(11, plain, [-(v1_xboole_0(_184456)), -(v12_altcat_1(k4_waybel34(_184456)))], clausify(dt_k4_waybel34)).
% 10.54/10.70 cnf(12, plain, [-(v1_xboole_0(_184456)), -(l2_altcat_1(k4_waybel34(_184456)))], clausify(dt_k4_waybel34)).
% 10.54/10.70 cnf(13, plain, [-(v1_xboole_0(_185176)), v3_struct_0(k5_waybel34(_185176))], clausify(dt_k5_waybel34)).
% 10.54/10.70 cnf(14, plain, [-(v1_xboole_0(_185176)), -(v2_altcat_1(k5_waybel34(_185176)))], clausify(dt_k5_waybel34)).
% 10.54/10.70 cnf(15, plain, [-(v1_xboole_0(_185176)), -(v11_altcat_1(k5_waybel34(_185176)))], clausify(dt_k5_waybel34)).
% 10.54/10.70 cnf(16, plain, [-(v1_xboole_0(_185176)), -(v12_altcat_1(k5_waybel34(_185176)))], clausify(dt_k5_waybel34)).
% 10.54/10.70 cnf(17, plain, [-(v1_xboole_0(_185176)), -(l2_altcat_1(k5_waybel34(_185176)))], clausify(dt_k5_waybel34)).
% 10.54/10.70 cnf(18, plain, [-(v2_setfam_1(_185896)), -(v16_functor0(k6_waybel34(_185896), k4_waybel34(_185896), k5_waybel34(_185896)))], clausify(dt_k6_waybel34)).
% 10.54/10.70 cnf(19, plain, [-(v2_setfam_1(_185896)), -(m2_functor0(k6_waybel34(_185896), k4_waybel34(_185896), k5_waybel34(_185896)))], clausify(dt_k6_waybel34)).
% 10.54/10.70 cnf(20, plain, [-(v1_xboole_0(_187286)), v3_struct_0(k8_waybel34(_187286))], clausify(dt_k8_waybel34)).
% 10.54/10.70 cnf(21, plain, [-(v1_xboole_0(_187286)), -(v2_altcat_1(k8_waybel34(_187286)))], clausify(dt_k8_waybel34)).
% 10.54/10.70 cnf(22, plain, [-(v1_xboole_0(_187286)), -(v3_altcat_2(k8_waybel34(_187286), k4_waybel34(_187286)))], clausify(dt_k8_waybel34)).
% 10.54/10.70 cnf(23, plain, [-(v1_xboole_0(_187286)), -(m1_altcat_2(k8_waybel34(_187286), k4_waybel34(_187286)))], clausify(dt_k8_waybel34)).
% 10.54/10.70 cnf(24, plain, [-(v2_setfam_1(_187934)), v3_struct_0(k9_waybel34(_187934))], clausify(dt_k9_waybel34)).
% 10.54/10.70 cnf(25, plain, [-(v2_setfam_1(_187934)), -(v2_altcat_1(k9_waybel34(_187934)))], clausify(dt_k9_waybel34)).
% 10.54/10.70 cnf(26, plain, [-(v2_setfam_1(_187934)), -(v3_altcat_2(k9_waybel34(_187934), k5_waybel34(_187934)))], clausify(dt_k9_waybel34)).
% 10.54/10.70 cnf(27, plain, [-(v2_setfam_1(_187934)), -(m1_altcat_2(k9_waybel34(_187934), k5_waybel34(_187934)))], clausify(dt_k9_waybel34)).
% 10.54/10.70 cnf(28, plain, [-(v2_setfam_1(_208422)), -(v21_functor0(k6_waybel34(_208422), k4_waybel34(_208422), k5_waybel34(_208422)))], clausify(fc7_waybel34)).
% 10.54/10.70 cnf(29, plain, [-(v2_setfam_1(_225019)), -(k15_functor0(k4_waybel34(_225019), k5_waybel34(_225019), k6_waybel34(_225019)) = k7_waybel34(_225019))], clausify(t18_waybel34)).
% 10.54/10.70 cnf(30, plain, [l2_altcat_1(_227157), v12_altcat_1(_227157), v11_altcat_1(_227157), v2_altcat_1(_227157), -(v3_struct_0(_227157)), l2_altcat_1(_227616), v12_altcat_1(_227616), v11_altcat_1(_227616), v2_altcat_1(_227616), -(v3_struct_0(_227616)), m2_functor0(_228047, _227157, _227616), v16_functor0(_228047, _227157, _227616), v21_functor0(_228047, _227157, _227616), m1_altcat_2(_228496, _227157), v3_altcat_2(_228496, _227157), v2_altcat_1(_228496), -(v3_struct_0(_228496)), -(r3_yellow20(_227616, _227157, k15_functor0(_227157, _227616, _228047), _228866, _228496)), r3_yellow20(_227157, _227616, _228047, _228496, _228866), -(v3_struct_0(_228866)), v2_altcat_1(_228866), v3_altcat_2(_228866, _227616), m1_altcat_2(_228866, _227616)], clausify(t52_yellow20)).
% 10.54/10.70 cnf(31, plain, [-(v2_setfam_1(_229860)), -(r3_yellow20(k4_waybel34(_229860), k5_waybel34(_229860), k6_waybel34(_229860), k8_waybel34(_229860), k9_waybel34(_229860)))], clausify(t56_waybel34)).
% 10.54/10.70
% 10.54/10.70 cnf('1',plain,[v2_setfam_1(31 ^ [])],start(1)).
% 10.54/10.70 cnf('1.1',plain,[-(v2_setfam_1(31 ^ [])), -(v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])))],extension(18,bind([[_185896], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1',plain,[v16_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ [])), l2_altcat_1(k4_waybel34(31 ^ [])), v12_altcat_1(k4_waybel34(31 ^ [])), v11_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 ^ [])), v11_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 ^ [])), m1_altcat_2(k8_waybel34(31 ^ []), k4_waybel34(31 ^ [])), v3_altcat_2(k8_waybel34(31 ^ []), k4_waybel34(31 ^ [])), v2_altcat_1(k8_waybel34(31 ^ [])), -(v3_struct_0(k8_waybel34(31 ^ []))), -(r3_yellow20(k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k15_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ [])), k9_waybel34(31 ^ []), k8_waybel34(31 ^ []))), r3_yellow20(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ [])), -(v3_struct_0(k9_waybel34(31 ^ []))), v2_altcat_1(k9_waybel34(31 ^ [])), v3_altcat_2(k9_waybel34(31 ^ []), k5_waybel34(31 ^ [])), m1_altcat_2(k9_waybel34(31 ^ []), k5_waybel34(31 ^ []))],extension(30,bind([[_227157, _228047, _228496, _228866, _227616], [k4_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.1',plain,[-(l2_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(12,bind([[_184456], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.1.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.1.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.2',plain,[-(v12_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(11,bind([[_184456], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.2.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.2.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.3',plain,[-(v11_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(10,bind([[_184456], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.3.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.3.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.4',plain,[-(v2_altcat_1(k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(9,bind([[_184456], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.4.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.4.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.5',plain,[v3_struct_0(k4_waybel34(31 ^ [])), -(v1_xboole_0(31 ^ []))],extension(8,bind([[_184456], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.5.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.5.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.6',plain,[-(l2_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(17,bind([[_185176], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.6.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.6.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.7',plain,[-(v12_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(16,bind([[_185176], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.7.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.7.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.8',plain,[-(v11_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(15,bind([[_185176], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.8.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.8.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.9',plain,[-(v2_altcat_1(k5_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(14,bind([[_185176], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.9.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.9.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.10',plain,[v3_struct_0(k5_waybel34(31 ^ [])), -(v1_xboole_0(31 ^ []))],extension(13,bind([[_185176], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.10.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.10.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.11',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([[_110672, _110757, _110841, _110924, _111006, _111087], [k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.11.1',plain,[-(m2_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(19,bind([[_185896], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.11.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.11.2',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_101194], [k6_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.11.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_101194], [k4_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.11.4',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_101194], [k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.12',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([[_127226, _127311, _127395, _127478, _127560, _127641], [k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.12.1',plain,[-(v21_functor0(k6_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(28,bind([[_208422], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.12.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.12.2',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_101194], [k6_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.12.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_101194], [k4_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.12.4',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_101194], [k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.13',plain,[-(m1_altcat_2(k8_waybel34(31 ^ []), k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(23,bind([[_187286], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.13.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.13.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.14',plain,[-(v3_altcat_2(k8_waybel34(31 ^ []), k4_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(22,bind([[_187286], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.14.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.14.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.15',plain,[-(v2_altcat_1(k8_waybel34(31 ^ []))), -(v1_xboole_0(31 ^ []))],extension(21,bind([[_187286], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.15.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.15.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.16',plain,[v3_struct_0(k8_waybel34(31 ^ [])), -(v1_xboole_0(31 ^ []))],extension(20,bind([[_187286], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.16.1',plain,[v1_xboole_0(31 ^ []), -(v2_setfam_1(31 ^ []))],extension(7,bind([[_164966], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.16.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.17',plain,[r3_yellow20(k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k15_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ [])), k9_waybel34(31 ^ []), k8_waybel34(31 ^ [])), -(r3_yellow20(k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k7_waybel34(31 ^ []), k9_waybel34(31 ^ []), k8_waybel34(31 ^ []))), k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []), k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []), k15_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ [])) = k7_waybel34(31 ^ []), k9_waybel34(31 ^ []) = k9_waybel34(31 ^ []), k8_waybel34(31 ^ []) = k8_waybel34(31 ^ [])],extension(5,bind([[_115464, _115585, _115705, _115824, _115942, _116059, _116175, _116290, _116404, _116517], [k5_waybel34(31 ^ []), k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k15_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ [])), k7_waybel34(31 ^ []), k9_waybel34(31 ^ []), k9_waybel34(31 ^ []), k8_waybel34(31 ^ []), k8_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.17.1',plain,[r3_yellow20(k5_waybel34(31 ^ []), k4_waybel34(31 ^ []), k7_waybel34(31 ^ []), k9_waybel34(31 ^ []), k8_waybel34(31 ^ []))],extension(2)).
% 10.54/10.70 cnf('1.1.1.17.2',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_101194], [k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.17.3',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_101194], [k4_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.17.4',plain,[-(k15_functor0(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ [])) = k7_waybel34(31 ^ [])), -(v2_setfam_1(31 ^ []))],extension(29,bind([[_225019], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.17.4.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.17.5',plain,[-(k9_waybel34(31 ^ []) = k9_waybel34(31 ^ []))],extension(3,bind([[_101194], [k9_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.17.6',plain,[-(k8_waybel34(31 ^ []) = k8_waybel34(31 ^ []))],extension(3,bind([[_101194], [k8_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18',plain,[-(r3_yellow20(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ []))), r3_yellow20(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ [])), k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []), k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []), k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []), k8_waybel34(31 ^ []) = k8_waybel34(31 ^ []), k9_waybel34(31 ^ []) = k9_waybel34(31 ^ [])],extension(5,bind([[_115464, _115585, _115705, _115824, _115942, _116059, _116175, _116290, _116404, _116517], [k4_waybel34(31 ^ []), k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ []), k9_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18.1',plain,[-(r3_yellow20(k4_waybel34(31 ^ []), k5_waybel34(31 ^ []), k6_waybel34(31 ^ []), k8_waybel34(31 ^ []), k9_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(31,bind([[_229860], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.18.1.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.18.2',plain,[-(k4_waybel34(31 ^ []) = k4_waybel34(31 ^ []))],extension(3,bind([[_101194], [k4_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18.3',plain,[-(k5_waybel34(31 ^ []) = k5_waybel34(31 ^ []))],extension(3,bind([[_101194], [k5_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18.4',plain,[-(k6_waybel34(31 ^ []) = k6_waybel34(31 ^ []))],extension(3,bind([[_101194], [k6_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18.5',plain,[-(k8_waybel34(31 ^ []) = k8_waybel34(31 ^ []))],extension(3,bind([[_101194], [k8_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.18.6',plain,[-(k9_waybel34(31 ^ []) = k9_waybel34(31 ^ []))],extension(3,bind([[_101194], [k9_waybel34(31 ^ [])]]))).
% 10.54/10.70 cnf('1.1.1.19',plain,[v3_struct_0(k9_waybel34(31 ^ [])), -(v2_setfam_1(31 ^ []))],extension(24,bind([[_187934], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.19.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.20',plain,[-(v2_altcat_1(k9_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(25,bind([[_187934], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.20.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.21',plain,[-(v3_altcat_2(k9_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(26,bind([[_187934], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.21.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 cnf('1.1.1.22',plain,[-(m1_altcat_2(k9_waybel34(31 ^ []), k5_waybel34(31 ^ []))), -(v2_setfam_1(31 ^ []))],extension(27,bind([[_187934], [31 ^ []]]))).
% 10.54/10.70 cnf('1.1.1.22.1',plain,[v2_setfam_1(31 ^ [])],extension(1)).
% 10.54/10.70 %-----------------------------------------------------
% 10.54/10.71
% 10.54/10.71 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------