%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LAT376+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art07.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 13:05:09 EST 2010
% Result : Theorem 6.76s
% Output : Solution 6.76s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP19358/LAT376+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP19358/LAT376+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP19358/LAT376+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 19454
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.94 CPU 2.01 WC
% PrfWatch: 3.93 CPU 4.02 WC
% # Preprocessing time : 0.038 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:(~(v2_setfam_1(X1))=>r3_yellow20(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1),k8_waybel34(X1),k9_waybel34(X1))),file('/tmp/SRASS.s.p', t56_waybel34)).
% fof(4, axiom,![X1]:(~(v2_setfam_1(X1))=>(k15_functor0(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1))=k7_waybel34(X1)&k15_functor0(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1))=k6_waybel34(X1))),file('/tmp/SRASS.s.p', t18_waybel34)).
% fof(5, axiom,![X1]:(~(v2_setfam_1(X1))=>~(v1_xboole_0(X1))),file('/tmp/SRASS.s.p', cc2_setfam_1)).
% fof(7, axiom,![X1]:(~(v2_setfam_1(X1))=>((v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&m2_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),file('/tmp/SRASS.s.p', dt_k6_waybel34)).
% fof(8, axiom,![X1]:(~(v2_setfam_1(X1))=>((((~(v3_struct_0(k9_waybel34(X1)))&v2_altcat_1(k9_waybel34(X1)))&v6_altcat_1(k9_waybel34(X1)))&v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))&m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))),file('/tmp/SRASS.s.p', dt_k9_waybel34)).
% fof(21, axiom,![X1]:(~(v1_xboole_0(X1))=>((((~(v3_struct_0(k8_waybel34(X1)))&v2_altcat_1(k8_waybel34(X1)))&v6_altcat_1(k8_waybel34(X1)))&v3_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))&m1_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))),file('/tmp/SRASS.s.p', dt_k8_waybel34)).
% fof(27, axiom,![X1]:(~(v2_setfam_1(X1))=>(((((((v6_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v8_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v11_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v12_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v14_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v21_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),file('/tmp/SRASS.s.p', fc7_waybel34)).
% fof(40, axiom,![X1]:(~(v1_xboole_0(X1))=>((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&l2_altcat_1(k5_waybel34(X1)))),file('/tmp/SRASS.s.p', dt_k5_waybel34)).
% fof(69, axiom,![X1]:(~(v1_xboole_0(X1))=>((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&l2_altcat_1(k4_waybel34(X1)))),file('/tmp/SRASS.s.p', dt_k4_waybel34)).
% fof(76, axiom,![X1]:(~(v2_setfam_1(X1))=>((((((((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v9_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v1_altcat_2(k5_waybel34(X1)))&v2_yellow18(k5_waybel34(X1)))&v3_yellow18(k5_waybel34(X1)))&v4_yellow18(k5_waybel34(X1)))&v1_yellow21(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&v3_yellow21(k5_waybel34(X1)))),file('/tmp/SRASS.s.p', fc6_waybel34)).
% fof(82, axiom,![X1]:(((((~(v3_struct_0(X1))&v2_altcat_1(X1))&v11_altcat_1(X1))&v12_altcat_1(X1))&l2_altcat_1(X1))=>![X2]:(((((~(v3_struct_0(X2))&v2_altcat_1(X2))&v11_altcat_1(X2))&v12_altcat_1(X2))&l2_altcat_1(X2))=>![X3]:((v16_functor0(X3,X1,X2)&m2_functor0(X3,X1,X2))=>(v21_functor0(X3,X1,X2)=>![X4]:((((~(v3_struct_0(X4))&v2_altcat_1(X4))&v3_altcat_2(X4,X1))&m1_altcat_2(X4,X1))=>![X5]:((((~(v3_struct_0(X5))&v2_altcat_1(X5))&v3_altcat_2(X5,X2))&m1_altcat_2(X5,X2))=>(r3_yellow20(X1,X2,X3,X4,X5)=>r3_yellow20(X2,X1,k15_functor0(X1,X2,X3),X5,X4)))))))),file('/tmp/SRASS.s.p', t52_yellow20)).
% fof(92, axiom,![X1]:(~(v2_setfam_1(X1))=>((((((((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v9_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v1_altcat_2(k4_waybel34(X1)))&v2_yellow18(k4_waybel34(X1)))&v3_yellow18(k4_waybel34(X1)))&v4_yellow18(k4_waybel34(X1)))&v1_yellow21(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&v3_yellow21(k4_waybel34(X1)))),file('/tmp/SRASS.s.p', fc5_waybel34)).
% fof(127, conjecture,![X1]:(~(v2_setfam_1(X1))=>r3_yellow20(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1),k9_waybel34(X1),k8_waybel34(X1))),file('/tmp/SRASS.s.p', t57_waybel34)).
% fof(128, negated_conjecture,~(![X1]:(~(v2_setfam_1(X1))=>r3_yellow20(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1),k9_waybel34(X1),k8_waybel34(X1)))),inference(assume_negation,[status(cth)],[127])).
% fof(130, plain,![X1]:(~(v2_setfam_1(X1))=>r3_yellow20(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1),k8_waybel34(X1),k9_waybel34(X1))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(132, plain,![X1]:(~(v2_setfam_1(X1))=>(k15_functor0(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1))=k7_waybel34(X1)&k15_functor0(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1))=k6_waybel34(X1))),inference(fof_simplification,[status(thm)],[4,theory(equality)])).
% fof(133, plain,![X1]:(~(v2_setfam_1(X1))=>~(v1_xboole_0(X1))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(134, plain,![X1]:(~(v2_setfam_1(X1))=>((v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&m2_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(135, plain,![X1]:(~(v2_setfam_1(X1))=>((((~(v3_struct_0(k9_waybel34(X1)))&v2_altcat_1(k9_waybel34(X1)))&v6_altcat_1(k9_waybel34(X1)))&v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))&m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% fof(142, plain,![X1]:(~(v1_xboole_0(X1))=>((((~(v3_struct_0(k8_waybel34(X1)))&v2_altcat_1(k8_waybel34(X1)))&v6_altcat_1(k8_waybel34(X1)))&v3_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))&m1_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))),inference(fof_simplification,[status(thm)],[21,theory(equality)])).
% fof(144, plain,![X1]:(~(v2_setfam_1(X1))=>(((((((v6_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v8_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v11_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v12_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v14_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v21_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(152, plain,![X1]:(~(v1_xboole_0(X1))=>((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&l2_altcat_1(k5_waybel34(X1)))),inference(fof_simplification,[status(thm)],[40,theory(equality)])).
% fof(164, plain,![X1]:(~(v1_xboole_0(X1))=>((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&l2_altcat_1(k4_waybel34(X1)))),inference(fof_simplification,[status(thm)],[69,theory(equality)])).
% fof(167, plain,![X1]:(~(v2_setfam_1(X1))=>((((((((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v9_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v1_altcat_2(k5_waybel34(X1)))&v2_yellow18(k5_waybel34(X1)))&v3_yellow18(k5_waybel34(X1)))&v4_yellow18(k5_waybel34(X1)))&v1_yellow21(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&v3_yellow21(k5_waybel34(X1)))),inference(fof_simplification,[status(thm)],[76,theory(equality)])).
% fof(171, plain,![X1]:(((((~(v3_struct_0(X1))&v2_altcat_1(X1))&v11_altcat_1(X1))&v12_altcat_1(X1))&l2_altcat_1(X1))=>![X2]:(((((~(v3_struct_0(X2))&v2_altcat_1(X2))&v11_altcat_1(X2))&v12_altcat_1(X2))&l2_altcat_1(X2))=>![X3]:((v16_functor0(X3,X1,X2)&m2_functor0(X3,X1,X2))=>(v21_functor0(X3,X1,X2)=>![X4]:((((~(v3_struct_0(X4))&v2_altcat_1(X4))&v3_altcat_2(X4,X1))&m1_altcat_2(X4,X1))=>![X5]:((((~(v3_struct_0(X5))&v2_altcat_1(X5))&v3_altcat_2(X5,X2))&m1_altcat_2(X5,X2))=>(r3_yellow20(X1,X2,X3,X4,X5)=>r3_yellow20(X2,X1,k15_functor0(X1,X2,X3),X5,X4)))))))),inference(fof_simplification,[status(thm)],[82,theory(equality)])).
% fof(172, plain,![X1]:(~(v2_setfam_1(X1))=>((((((((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v9_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v1_altcat_2(k4_waybel34(X1)))&v2_yellow18(k4_waybel34(X1)))&v3_yellow18(k4_waybel34(X1)))&v4_yellow18(k4_waybel34(X1)))&v1_yellow21(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&v3_yellow21(k4_waybel34(X1)))),inference(fof_simplification,[status(thm)],[92,theory(equality)])).
% fof(174, negated_conjecture,~(![X1]:(~(v2_setfam_1(X1))=>r3_yellow20(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1),k9_waybel34(X1),k8_waybel34(X1)))),inference(fof_simplification,[status(thm)],[128,theory(equality)])).
% fof(178, plain,![X1]:(v2_setfam_1(X1)|r3_yellow20(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1),k8_waybel34(X1),k9_waybel34(X1))),inference(fof_nnf,[status(thm)],[130])).
% fof(179, plain,![X2]:(v2_setfam_1(X2)|r3_yellow20(k4_waybel34(X2),k5_waybel34(X2),k6_waybel34(X2),k8_waybel34(X2),k9_waybel34(X2))),inference(variable_rename,[status(thm)],[178])).
% cnf(180,plain,(r3_yellow20(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1),k8_waybel34(X1),k9_waybel34(X1))|v2_setfam_1(X1)),inference(split_conjunct,[status(thm)],[179])).
% fof(187, plain,![X1]:(v2_setfam_1(X1)|(k15_functor0(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1))=k7_waybel34(X1)&k15_functor0(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1))=k6_waybel34(X1))),inference(fof_nnf,[status(thm)],[132])).
% fof(188, plain,![X2]:(v2_setfam_1(X2)|(k15_functor0(k4_waybel34(X2),k5_waybel34(X2),k6_waybel34(X2))=k7_waybel34(X2)&k15_functor0(k5_waybel34(X2),k4_waybel34(X2),k7_waybel34(X2))=k6_waybel34(X2))),inference(variable_rename,[status(thm)],[187])).
% fof(189, plain,![X2]:((k15_functor0(k4_waybel34(X2),k5_waybel34(X2),k6_waybel34(X2))=k7_waybel34(X2)|v2_setfam_1(X2))&(k15_functor0(k5_waybel34(X2),k4_waybel34(X2),k7_waybel34(X2))=k6_waybel34(X2)|v2_setfam_1(X2))),inference(distribute,[status(thm)],[188])).
% cnf(191,plain,(v2_setfam_1(X1)|k15_functor0(k4_waybel34(X1),k5_waybel34(X1),k6_waybel34(X1))=k7_waybel34(X1)),inference(split_conjunct,[status(thm)],[189])).
% fof(192, plain,![X1]:(v2_setfam_1(X1)|~(v1_xboole_0(X1))),inference(fof_nnf,[status(thm)],[133])).
% fof(193, plain,![X2]:(v2_setfam_1(X2)|~(v1_xboole_0(X2))),inference(variable_rename,[status(thm)],[192])).
% cnf(194,plain,(v2_setfam_1(X1)|~v1_xboole_0(X1)),inference(split_conjunct,[status(thm)],[193])).
% fof(198, plain,![X1]:(v2_setfam_1(X1)|((v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&m2_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),inference(fof_nnf,[status(thm)],[134])).
% fof(199, plain,![X2]:(v2_setfam_1(X2)|((v9_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))&v16_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&m2_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))),inference(variable_rename,[status(thm)],[198])).
% fof(200, plain,![X2]:(((v9_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2))&(v16_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(m2_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2))),inference(distribute,[status(thm)],[199])).
% cnf(201,plain,(v2_setfam_1(X1)|m2_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[200])).
% cnf(202,plain,(v2_setfam_1(X1)|v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[200])).
% fof(204, plain,![X1]:(v2_setfam_1(X1)|((((~(v3_struct_0(k9_waybel34(X1)))&v2_altcat_1(k9_waybel34(X1)))&v6_altcat_1(k9_waybel34(X1)))&v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))&m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1)))),inference(fof_nnf,[status(thm)],[135])).
% fof(205, plain,![X2]:(v2_setfam_1(X2)|((((~(v3_struct_0(k9_waybel34(X2)))&v2_altcat_1(k9_waybel34(X2)))&v6_altcat_1(k9_waybel34(X2)))&v3_altcat_2(k9_waybel34(X2),k5_waybel34(X2)))&m1_altcat_2(k9_waybel34(X2),k5_waybel34(X2)))),inference(variable_rename,[status(thm)],[204])).
% fof(206, plain,![X2]:(((((~(v3_struct_0(k9_waybel34(X2)))|v2_setfam_1(X2))&(v2_altcat_1(k9_waybel34(X2))|v2_setfam_1(X2)))&(v6_altcat_1(k9_waybel34(X2))|v2_setfam_1(X2)))&(v3_altcat_2(k9_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(m1_altcat_2(k9_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2))),inference(distribute,[status(thm)],[205])).
% cnf(207,plain,(v2_setfam_1(X1)|m1_altcat_2(k9_waybel34(X1),k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[206])).
% cnf(208,plain,(v2_setfam_1(X1)|v3_altcat_2(k9_waybel34(X1),k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[206])).
% cnf(210,plain,(v2_setfam_1(X1)|v2_altcat_1(k9_waybel34(X1))),inference(split_conjunct,[status(thm)],[206])).
% cnf(211,plain,(v2_setfam_1(X1)|~v3_struct_0(k9_waybel34(X1))),inference(split_conjunct,[status(thm)],[206])).
% fof(272, plain,![X1]:(v1_xboole_0(X1)|((((~(v3_struct_0(k8_waybel34(X1)))&v2_altcat_1(k8_waybel34(X1)))&v6_altcat_1(k8_waybel34(X1)))&v3_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))&m1_altcat_2(k8_waybel34(X1),k4_waybel34(X1)))),inference(fof_nnf,[status(thm)],[142])).
% fof(273, plain,![X2]:(v1_xboole_0(X2)|((((~(v3_struct_0(k8_waybel34(X2)))&v2_altcat_1(k8_waybel34(X2)))&v6_altcat_1(k8_waybel34(X2)))&v3_altcat_2(k8_waybel34(X2),k4_waybel34(X2)))&m1_altcat_2(k8_waybel34(X2),k4_waybel34(X2)))),inference(variable_rename,[status(thm)],[272])).
% fof(274, plain,![X2]:(((((~(v3_struct_0(k8_waybel34(X2)))|v1_xboole_0(X2))&(v2_altcat_1(k8_waybel34(X2))|v1_xboole_0(X2)))&(v6_altcat_1(k8_waybel34(X2))|v1_xboole_0(X2)))&(v3_altcat_2(k8_waybel34(X2),k4_waybel34(X2))|v1_xboole_0(X2)))&(m1_altcat_2(k8_waybel34(X2),k4_waybel34(X2))|v1_xboole_0(X2))),inference(distribute,[status(thm)],[273])).
% cnf(275,plain,(v1_xboole_0(X1)|m1_altcat_2(k8_waybel34(X1),k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[274])).
% cnf(276,plain,(v1_xboole_0(X1)|v3_altcat_2(k8_waybel34(X1),k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[274])).
% cnf(278,plain,(v1_xboole_0(X1)|v2_altcat_1(k8_waybel34(X1))),inference(split_conjunct,[status(thm)],[274])).
% cnf(279,plain,(v1_xboole_0(X1)|~v3_struct_0(k8_waybel34(X1))),inference(split_conjunct,[status(thm)],[274])).
% fof(303, plain,![X1]:(v2_setfam_1(X1)|(((((((v6_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))&v8_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v9_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v11_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v12_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v14_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v16_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))&v21_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1)))),inference(fof_nnf,[status(thm)],[144])).
% fof(304, plain,![X2]:(v2_setfam_1(X2)|(((((((v6_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))&v8_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v9_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v11_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v12_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v14_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v16_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))&v21_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2)))),inference(variable_rename,[status(thm)],[303])).
% fof(305, plain,![X2]:((((((((v6_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2))&(v8_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v9_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v11_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v12_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v14_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v16_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2)))&(v21_functor0(k6_waybel34(X2),k4_waybel34(X2),k5_waybel34(X2))|v2_setfam_1(X2))),inference(distribute,[status(thm)],[304])).
% cnf(306,plain,(v2_setfam_1(X1)|v21_functor0(k6_waybel34(X1),k4_waybel34(X1),k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[305])).
% fof(389, plain,![X1]:(v1_xboole_0(X1)|((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&l2_altcat_1(k5_waybel34(X1)))),inference(fof_nnf,[status(thm)],[152])).
% fof(390, plain,![X2]:(v1_xboole_0(X2)|((((((~(v3_struct_0(k5_waybel34(X2)))&v2_altcat_1(k5_waybel34(X2)))&v6_altcat_1(k5_waybel34(X2)))&v11_altcat_1(k5_waybel34(X2)))&v12_altcat_1(k5_waybel34(X2)))&v2_yellow21(k5_waybel34(X2)))&l2_altcat_1(k5_waybel34(X2)))),inference(variable_rename,[status(thm)],[389])).
% fof(391, plain,![X2]:(((((((~(v3_struct_0(k5_waybel34(X2)))|v1_xboole_0(X2))&(v2_altcat_1(k5_waybel34(X2))|v1_xboole_0(X2)))&(v6_altcat_1(k5_waybel34(X2))|v1_xboole_0(X2)))&(v11_altcat_1(k5_waybel34(X2))|v1_xboole_0(X2)))&(v12_altcat_1(k5_waybel34(X2))|v1_xboole_0(X2)))&(v2_yellow21(k5_waybel34(X2))|v1_xboole_0(X2)))&(l2_altcat_1(k5_waybel34(X2))|v1_xboole_0(X2))),inference(distribute,[status(thm)],[390])).
% cnf(392,plain,(v1_xboole_0(X1)|l2_altcat_1(k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[391])).
% fof(559, plain,![X1]:(v1_xboole_0(X1)|((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&l2_altcat_1(k4_waybel34(X1)))),inference(fof_nnf,[status(thm)],[164])).
% fof(560, plain,![X2]:(v1_xboole_0(X2)|((((((~(v3_struct_0(k4_waybel34(X2)))&v2_altcat_1(k4_waybel34(X2)))&v6_altcat_1(k4_waybel34(X2)))&v11_altcat_1(k4_waybel34(X2)))&v12_altcat_1(k4_waybel34(X2)))&v2_yellow21(k4_waybel34(X2)))&l2_altcat_1(k4_waybel34(X2)))),inference(variable_rename,[status(thm)],[559])).
% fof(561, plain,![X2]:(((((((~(v3_struct_0(k4_waybel34(X2)))|v1_xboole_0(X2))&(v2_altcat_1(k4_waybel34(X2))|v1_xboole_0(X2)))&(v6_altcat_1(k4_waybel34(X2))|v1_xboole_0(X2)))&(v11_altcat_1(k4_waybel34(X2))|v1_xboole_0(X2)))&(v12_altcat_1(k4_waybel34(X2))|v1_xboole_0(X2)))&(v2_yellow21(k4_waybel34(X2))|v1_xboole_0(X2)))&(l2_altcat_1(k4_waybel34(X2))|v1_xboole_0(X2))),inference(distribute,[status(thm)],[560])).
% cnf(562,plain,(v1_xboole_0(X1)|l2_altcat_1(k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[561])).
% fof(589, plain,![X1]:(v2_setfam_1(X1)|((((((((((((~(v3_struct_0(k5_waybel34(X1)))&v2_altcat_1(k5_waybel34(X1)))&v6_altcat_1(k5_waybel34(X1)))&v9_altcat_1(k5_waybel34(X1)))&v11_altcat_1(k5_waybel34(X1)))&v12_altcat_1(k5_waybel34(X1)))&v1_altcat_2(k5_waybel34(X1)))&v2_yellow18(k5_waybel34(X1)))&v3_yellow18(k5_waybel34(X1)))&v4_yellow18(k5_waybel34(X1)))&v1_yellow21(k5_waybel34(X1)))&v2_yellow21(k5_waybel34(X1)))&v3_yellow21(k5_waybel34(X1)))),inference(fof_nnf,[status(thm)],[167])).
% fof(590, plain,![X2]:(v2_setfam_1(X2)|((((((((((((~(v3_struct_0(k5_waybel34(X2)))&v2_altcat_1(k5_waybel34(X2)))&v6_altcat_1(k5_waybel34(X2)))&v9_altcat_1(k5_waybel34(X2)))&v11_altcat_1(k5_waybel34(X2)))&v12_altcat_1(k5_waybel34(X2)))&v1_altcat_2(k5_waybel34(X2)))&v2_yellow18(k5_waybel34(X2)))&v3_yellow18(k5_waybel34(X2)))&v4_yellow18(k5_waybel34(X2)))&v1_yellow21(k5_waybel34(X2)))&v2_yellow21(k5_waybel34(X2)))&v3_yellow21(k5_waybel34(X2)))),inference(variable_rename,[status(thm)],[589])).
% fof(591, plain,![X2]:(((((((((((((~(v3_struct_0(k5_waybel34(X2)))|v2_setfam_1(X2))&(v2_altcat_1(k5_waybel34(X2))|v2_setfam_1(X2)))&(v6_altcat_1(k5_waybel34(X2))|v2_setfam_1(X2)))&(v9_altcat_1(k5_waybel34(X2))|v2_setfam_1(X2)))&(v11_altcat_1(k5_waybel34(X2))|v2_setfam_1(X2)))&(v12_altcat_1(k5_waybel34(X2))|v2_setfam_1(X2)))&(v1_altcat_2(k5_waybel34(X2))|v2_setfam_1(X2)))&(v2_yellow18(k5_waybel34(X2))|v2_setfam_1(X2)))&(v3_yellow18(k5_waybel34(X2))|v2_setfam_1(X2)))&(v4_yellow18(k5_waybel34(X2))|v2_setfam_1(X2)))&(v1_yellow21(k5_waybel34(X2))|v2_setfam_1(X2)))&(v2_yellow21(k5_waybel34(X2))|v2_setfam_1(X2)))&(v3_yellow21(k5_waybel34(X2))|v2_setfam_1(X2))),inference(distribute,[status(thm)],[590])).
% cnf(599,plain,(v2_setfam_1(X1)|v12_altcat_1(k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[591])).
% cnf(600,plain,(v2_setfam_1(X1)|v11_altcat_1(k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[591])).
% cnf(603,plain,(v2_setfam_1(X1)|v2_altcat_1(k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[591])).
% cnf(604,plain,(v2_setfam_1(X1)|~v3_struct_0(k5_waybel34(X1))),inference(split_conjunct,[status(thm)],[591])).
% fof(641, plain,![X1]:(((((v3_struct_0(X1)|~(v2_altcat_1(X1)))|~(v11_altcat_1(X1)))|~(v12_altcat_1(X1)))|~(l2_altcat_1(X1)))|![X2]:(((((v3_struct_0(X2)|~(v2_altcat_1(X2)))|~(v11_altcat_1(X2)))|~(v12_altcat_1(X2)))|~(l2_altcat_1(X2)))|![X3]:((~(v16_functor0(X3,X1,X2))|~(m2_functor0(X3,X1,X2)))|(~(v21_functor0(X3,X1,X2))|![X4]:((((v3_struct_0(X4)|~(v2_altcat_1(X4)))|~(v3_altcat_2(X4,X1)))|~(m1_altcat_2(X4,X1)))|![X5]:((((v3_struct_0(X5)|~(v2_altcat_1(X5)))|~(v3_altcat_2(X5,X2)))|~(m1_altcat_2(X5,X2)))|(~(r3_yellow20(X1,X2,X3,X4,X5))|r3_yellow20(X2,X1,k15_functor0(X1,X2,X3),X5,X4)))))))),inference(fof_nnf,[status(thm)],[171])).
% fof(642, plain,![X6]:(((((v3_struct_0(X6)|~(v2_altcat_1(X6)))|~(v11_altcat_1(X6)))|~(v12_altcat_1(X6)))|~(l2_altcat_1(X6)))|![X7]:(((((v3_struct_0(X7)|~(v2_altcat_1(X7)))|~(v11_altcat_1(X7)))|~(v12_altcat_1(X7)))|~(l2_altcat_1(X7)))|![X8]:((~(v16_functor0(X8,X6,X7))|~(m2_functor0(X8,X6,X7)))|(~(v21_functor0(X8,X6,X7))|![X9]:((((v3_struct_0(X9)|~(v2_altcat_1(X9)))|~(v3_altcat_2(X9,X6)))|~(m1_altcat_2(X9,X6)))|![X10]:((((v3_struct_0(X10)|~(v2_altcat_1(X10)))|~(v3_altcat_2(X10,X7)))|~(m1_altcat_2(X10,X7)))|(~(r3_yellow20(X6,X7,X8,X9,X10))|r3_yellow20(X7,X6,k15_functor0(X6,X7,X8),X10,X9)))))))),inference(variable_rename,[status(thm)],[641])).
% fof(643, plain,![X6]:![X7]:![X8]:![X9]:![X10]:(((((((((v3_struct_0(X10)|~(v2_altcat_1(X10)))|~(v3_altcat_2(X10,X7)))|~(m1_altcat_2(X10,X7)))|(~(r3_yellow20(X6,X7,X8,X9,X10))|r3_yellow20(X7,X6,k15_functor0(X6,X7,X8),X10,X9)))|(((v3_struct_0(X9)|~(v2_altcat_1(X9)))|~(v3_altcat_2(X9,X6)))|~(m1_altcat_2(X9,X6))))|~(v21_functor0(X8,X6,X7)))|(~(v16_functor0(X8,X6,X7))|~(m2_functor0(X8,X6,X7))))|((((v3_struct_0(X7)|~(v2_altcat_1(X7)))|~(v11_altcat_1(X7)))|~(v12_altcat_1(X7)))|~(l2_altcat_1(X7))))|((((v3_struct_0(X6)|~(v2_altcat_1(X6)))|~(v11_altcat_1(X6)))|~(v12_altcat_1(X6)))|~(l2_altcat_1(X6)))),inference(shift_quantors,[status(thm)],[642])).
% cnf(644,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v3_struct_0(X4)|r3_yellow20(X2,X1,k15_functor0(X1,X2,X3),X5,X4)|v3_struct_0(X5)|~l2_altcat_1(X1)|~v12_altcat_1(X1)|~v11_altcat_1(X1)|~v2_altcat_1(X1)|~l2_altcat_1(X2)|~v12_altcat_1(X2)|~v11_altcat_1(X2)|~v2_altcat_1(X2)|~m2_functor0(X3,X1,X2)|~v16_functor0(X3,X1,X2)|~v21_functor0(X3,X1,X2)|~m1_altcat_2(X4,X1)|~v3_altcat_2(X4,X1)|~v2_altcat_1(X4)|~r3_yellow20(X1,X2,X3,X4,X5)|~m1_altcat_2(X5,X2)|~v3_altcat_2(X5,X2)|~v2_altcat_1(X5)),inference(split_conjunct,[status(thm)],[643])).
% fof(694, plain,![X1]:(v2_setfam_1(X1)|((((((((((((~(v3_struct_0(k4_waybel34(X1)))&v2_altcat_1(k4_waybel34(X1)))&v6_altcat_1(k4_waybel34(X1)))&v9_altcat_1(k4_waybel34(X1)))&v11_altcat_1(k4_waybel34(X1)))&v12_altcat_1(k4_waybel34(X1)))&v1_altcat_2(k4_waybel34(X1)))&v2_yellow18(k4_waybel34(X1)))&v3_yellow18(k4_waybel34(X1)))&v4_yellow18(k4_waybel34(X1)))&v1_yellow21(k4_waybel34(X1)))&v2_yellow21(k4_waybel34(X1)))&v3_yellow21(k4_waybel34(X1)))),inference(fof_nnf,[status(thm)],[172])).
% fof(695, plain,![X2]:(v2_setfam_1(X2)|((((((((((((~(v3_struct_0(k4_waybel34(X2)))&v2_altcat_1(k4_waybel34(X2)))&v6_altcat_1(k4_waybel34(X2)))&v9_altcat_1(k4_waybel34(X2)))&v11_altcat_1(k4_waybel34(X2)))&v12_altcat_1(k4_waybel34(X2)))&v1_altcat_2(k4_waybel34(X2)))&v2_yellow18(k4_waybel34(X2)))&v3_yellow18(k4_waybel34(X2)))&v4_yellow18(k4_waybel34(X2)))&v1_yellow21(k4_waybel34(X2)))&v2_yellow21(k4_waybel34(X2)))&v3_yellow21(k4_waybel34(X2)))),inference(variable_rename,[status(thm)],[694])).
% fof(696, plain,![X2]:(((((((((((((~(v3_struct_0(k4_waybel34(X2)))|v2_setfam_1(X2))&(v2_altcat_1(k4_waybel34(X2))|v2_setfam_1(X2)))&(v6_altcat_1(k4_waybel34(X2))|v2_setfam_1(X2)))&(v9_altcat_1(k4_waybel34(X2))|v2_setfam_1(X2)))&(v11_altcat_1(k4_waybel34(X2))|v2_setfam_1(X2)))&(v12_altcat_1(k4_waybel34(X2))|v2_setfam_1(X2)))&(v1_altcat_2(k4_waybel34(X2))|v2_setfam_1(X2)))&(v2_yellow18(k4_waybel34(X2))|v2_setfam_1(X2)))&(v3_yellow18(k4_waybel34(X2))|v2_setfam_1(X2)))&(v4_yellow18(k4_waybel34(X2))|v2_setfam_1(X2)))&(v1_yellow21(k4_waybel34(X2))|v2_setfam_1(X2)))&(v2_yellow21(k4_waybel34(X2))|v2_setfam_1(X2)))&(v3_yellow21(k4_waybel34(X2))|v2_setfam_1(X2))),inference(distribute,[status(thm)],[695])).
% cnf(704,plain,(v2_setfam_1(X1)|v12_altcat_1(k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[696])).
% cnf(705,plain,(v2_setfam_1(X1)|v11_altcat_1(k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[696])).
% cnf(708,plain,(v2_setfam_1(X1)|v2_altcat_1(k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[696])).
% cnf(709,plain,(v2_setfam_1(X1)|~v3_struct_0(k4_waybel34(X1))),inference(split_conjunct,[status(thm)],[696])).
% fof(843, negated_conjecture,?[X1]:(~(v2_setfam_1(X1))&~(r3_yellow20(k5_waybel34(X1),k4_waybel34(X1),k7_waybel34(X1),k9_waybel34(X1),k8_waybel34(X1)))),inference(fof_nnf,[status(thm)],[174])).
% fof(844, negated_conjecture,?[X2]:(~(v2_setfam_1(X2))&~(r3_yellow20(k5_waybel34(X2),k4_waybel34(X2),k7_waybel34(X2),k9_waybel34(X2),k8_waybel34(X2)))),inference(variable_rename,[status(thm)],[843])).
% fof(845, negated_conjecture,(~(v2_setfam_1(esk31_0))&~(r3_yellow20(k5_waybel34(esk31_0),k4_waybel34(esk31_0),k7_waybel34(esk31_0),k9_waybel34(esk31_0),k8_waybel34(esk31_0)))),inference(skolemize,[status(esa)],[844])).
% cnf(846,negated_conjecture,(~r3_yellow20(k5_waybel34(esk31_0),k4_waybel34(esk31_0),k7_waybel34(esk31_0),k9_waybel34(esk31_0),k8_waybel34(esk31_0))),inference(split_conjunct,[status(thm)],[845])).
% cnf(847,negated_conjecture,(~v2_setfam_1(esk31_0)),inference(split_conjunct,[status(thm)],[845])).
% cnf(861,negated_conjecture,(~v1_xboole_0(esk31_0)),inference(spm,[status(thm)],[847,194,theory(equality)])).
% cnf(1233,plain,(v3_struct_0(X1)|v3_struct_0(X2)|v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~v12_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~v2_altcat_1(k5_waybel34(X3))|~v2_altcat_1(k4_waybel34(X3))|~m2_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v16_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(spm,[status(thm)],[644,191,theory(equality)])).
% cnf(5990,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~v12_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(k5_waybel34(X3))|~v2_altcat_1(k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~m2_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[1233,202])).
% cnf(5991,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~v12_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(k5_waybel34(X3))|~v2_altcat_1(k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5990,201])).
% cnf(5992,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~v12_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(k5_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5991,708])).
% cnf(5993,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~v12_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5992,603])).
% cnf(5994,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~v12_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5993,704])).
% cnf(5995,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~v21_functor0(k6_waybel34(X3),k4_waybel34(X3),k5_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5994,599])).
% cnf(5996,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~v11_altcat_1(k4_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5995,306])).
% cnf(5997,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~v11_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5996,705])).
% cnf(5998,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(k4_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5997,600])).
% cnf(5999,plain,(v3_struct_0(k5_waybel34(X3))|v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5998,709])).
% cnf(6000,plain,(v3_struct_0(X1)|v3_struct_0(X2)|r3_yellow20(k5_waybel34(X3),k4_waybel34(X3),k7_waybel34(X3),X1,X2)|v2_setfam_1(X3)|~l2_altcat_1(k5_waybel34(X3))|~l2_altcat_1(k4_waybel34(X3))|~m1_altcat_2(X1,k5_waybel34(X3))|~m1_altcat_2(X2,k4_waybel34(X3))|~v3_altcat_2(X1,k5_waybel34(X3))|~v3_altcat_2(X2,k4_waybel34(X3))|~v2_altcat_1(X1)|~v2_altcat_1(X2)|~r3_yellow20(k4_waybel34(X3),k5_waybel34(X3),k6_waybel34(X3),X2,X1)),inference(csr,[status(thm)],[5999,604])).
% cnf(6001,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|v2_setfam_1(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v3_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))|~r3_yellow20(k4_waybel34(esk31_0),k5_waybel34(esk31_0),k6_waybel34(esk31_0),k8_waybel34(esk31_0),k9_waybel34(esk31_0))),inference(spm,[status(thm)],[846,6000,theory(equality)])).
% cnf(6003,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v3_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))|~r3_yellow20(k4_waybel34(esk31_0),k5_waybel34(esk31_0),k6_waybel34(esk31_0),k8_waybel34(esk31_0),k9_waybel34(esk31_0))),inference(sr,[status(thm)],[6001,847,theory(equality)])).
% cnf(56190,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|v2_setfam_1(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v3_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[6003,180,theory(equality)])).
% cnf(56191,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v3_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56190,847,theory(equality)])).
% cnf(56192,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|v1_xboole_0(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56191,276,theory(equality)])).
% cnf(56193,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v3_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56192,861,theory(equality)])).
% cnf(56194,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|v2_setfam_1(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56193,208,theory(equality)])).
% cnf(56195,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~m1_altcat_2(k8_waybel34(esk31_0),k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56194,847,theory(equality)])).
% cnf(56196,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|v1_xboole_0(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56195,275,theory(equality)])).
% cnf(56197,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~m1_altcat_2(k9_waybel34(esk31_0),k5_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56196,861,theory(equality)])).
% cnf(56198,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|v2_setfam_1(esk31_0)|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56197,207,theory(equality)])).
% cnf(56199,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|~l2_altcat_1(k5_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56198,847,theory(equality)])).
% cnf(56200,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|v1_xboole_0(esk31_0)|~l2_altcat_1(k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56199,392,theory(equality)])).
% cnf(56201,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|~l2_altcat_1(k4_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56200,861,theory(equality)])).
% cnf(56202,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|v1_xboole_0(esk31_0)|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(spm,[status(thm)],[56201,562,theory(equality)])).
% cnf(56203,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))|~v2_altcat_1(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56202,861,theory(equality)])).
% cnf(56204,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|v1_xboole_0(esk31_0)|~v2_altcat_1(k9_waybel34(esk31_0))),inference(spm,[status(thm)],[56203,278,theory(equality)])).
% cnf(56205,negated_conjecture,(v3_struct_0(k8_waybel34(esk31_0))|v3_struct_0(k9_waybel34(esk31_0))|~v2_altcat_1(k9_waybel34(esk31_0))),inference(sr,[status(thm)],[56204,861,theory(equality)])).
% cnf(56206,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))|v2_setfam_1(esk31_0)),inference(spm,[status(thm)],[56205,210,theory(equality)])).
% cnf(56207,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))|v3_struct_0(k8_waybel34(esk31_0))),inference(sr,[status(thm)],[56206,847,theory(equality)])).
% cnf(56208,negated_conjecture,(v1_xboole_0(esk31_0)|v3_struct_0(k9_waybel34(esk31_0))),inference(spm,[status(thm)],[279,56207,theory(equality)])).
% cnf(56209,negated_conjecture,(v3_struct_0(k9_waybel34(esk31_0))),inference(sr,[status(thm)],[56208,861,theory(equality)])).
% cnf(56210,negated_conjecture,(v2_setfam_1(esk31_0)),inference(spm,[status(thm)],[211,56209,theory(equality)])).
% cnf(56212,negated_conjecture,($false),inference(sr,[status(thm)],[56210,847,theory(equality)])).
% cnf(56213,negated_conjecture,($false),56212,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 9506
% # ...of these trivial : 0
% # ...subsumed : 4597
% # ...remaining for further processing: 4909
% # Other redundant clauses eliminated : 3
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 117
% # Backward-rewritten : 11
% # Generated clauses : 49954
% # ...of the previous two non-trivial : 49234
% # Contextual simplify-reflections : 4811
% # Paramodulations : 49926
% # Factorizations : 0
% # Equation resolutions : 19
% # Current number of processed clauses: 4481
% # Positive orientable unit clauses: 59
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 13
% # Non-unit-clauses : 4409
% # Current number of unprocessed clauses: 36815
% # ...number of literals in the above : 130894
% # Clause-clause subsumption calls (NU) : 9025187
% # Rec. Clause-clause subsumption calls : 4046843
% # Unit Clause-clause subsumption calls : 1540
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 980 leaves, 4.89+/-20.435 terms/leaf
% # Paramod-from index: 491 leaves, 3.90+/-16.929 terms/leaf
% # Paramod-into index: 848 leaves, 5.14+/-21.845 terms/leaf
% # -------------------------------------------------
% # User time : 4.572 s
% # System time : 0.077 s
% # Total time : 4.649 s
% # Maximum resident set size: 0 pages
% PrfWatch: 5.42 CPU 5.52 WC
% FINAL PrfWatch: 5.42 CPU 5.52 WC
% SZS output end Solution for /tmp/SystemOnTPTP19358/LAT376+1.tptp
%
%------------------------------------------------------------------------------