LisaST---0.9.THM-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : LisaST---0.9
% Problem  : KRS133+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n016.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sun Sep 27 07:45:13 AM UTC 2026

% Result   : Theorem 29.86s 29.19s
% Output   : CNFRefutation 29.92s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : KRS133+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04  % Command  : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38   % Computer : n016.cluster.edu
% 0.09/5.38   % Model    : x86_64 x86_64
% 0.09/5.38   % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38   % Memory   : 8046.5625MB
% 0.09/5.38   % OS       : Linux 6.8.0-71-generic
% 0.07/25.31  % CPULimit : 300
% 0.07/25.31  % WCLimit  : 300
% 0.07/25.31  % DateTime : Fri Sep 25 19:41:45 UTC 2026
% 0.07/25.31  % CPUTime  : 
% 0.07/25.31  Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.86/29.19  % SZS status Theorem for theBenchmark.p
% 29.86/29.19  % SZS output start CNFRefutation for theBenchmark.p
% 29.86/29.19  fof(axiom_0, axiom, ! [X0] : ((cowlThing(X0) & ~cowlNothing(X0)))).
% 29.86/29.19  fof(axiom_1, axiom, ! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0)))).
% 29.86/29.19  fof(axiom_3, axiom, ! [X0] : ((cAgamidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u0')))).
% 29.86/29.19  fof(axiom_4, axiom, ! [X0] : ((cAgamidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_6, axiom, ! [X0] : ((cAmphisbaenidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u1')))).
% 29.86/29.19  fof(axiom_7, axiom, ! [X0] : ((cAmphisbaenidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_9, axiom, ! [X0] : ((cAnomalepidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u2')))).
% 29.86/29.19  fof(axiom_10, axiom, ! [X0] : ((cAnomalepidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_12, axiom, ! [X0] : ((cBipedidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u3')))).
% 29.86/29.19  fof(axiom_13, axiom, ! [X0] : ((cBipedidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_15, axiom, ! [X0] : ((cCordylidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u4')))).
% 29.86/29.19  fof(axiom_16, axiom, ! [X0] : ((cCordylidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_18, axiom, ! [X0] : ((cCrocodylidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u5')))).
% 29.86/29.19  fof(axiom_19, axiom, ! [X0] : ((cCrocodylidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_21, axiom, ! [X0] : ((cEmydidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u6')))).
% 29.86/29.19  fof(axiom_22, axiom, ! [X0] : ((cEmydidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_24, axiom, ! [X0] : ((cGekkonidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u7')))).
% 29.86/29.19  fof(axiom_25, axiom, ! [X0] : ((cGekkonidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_27, axiom, ! [X0] : ((cLeptotyphlopidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u8')))).
% 29.86/29.19  fof(axiom_28, axiom, ! [X0] : ((cLeptotyphlopidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_30, axiom, ! [X0] : ((cLoxocemidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u9')))).
% 29.86/29.19  fof(axiom_31, axiom, ! [X0] : ((cLoxocemidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_32, axiom, ! [X0] : ((cReptile(X0) => (? [X1] : 'rfamily$uname'(X0,X1) & ! [X1] : ! [X2] : ((('rfamily$uname'(X0,X1) & 'rfamily$uname'(X0,X2)) => X1 = X2)))))).
% 29.86/29.19  fof(axiom_34, axiom, ! [X0] : ((cSphenodontidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u10')))).
% 29.86/29.19  fof(axiom_35, axiom, ! [X0] : ((cSphenodontidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_37, axiom, ! [X0] : ((cXantusiidae(X0) => 'rfamily$uname'(X0,'xsd$ustring$u11')))).
% 29.86/29.19  fof(axiom_38, axiom, ! [X0] : ((cXantusiidae(X0) => cReptile(X0)))).
% 29.86/29.19  fof(axiom_39, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u1').
% 29.86/29.19  fof(axiom_40, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u2').
% 29.86/29.19  fof(axiom_41, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u3').
% 29.86/29.19  fof(axiom_42, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u4').
% 29.86/29.19  fof(axiom_43, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u5').
% 29.86/29.19  fof(axiom_44, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_45, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_46, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_47, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_48, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_49, axiom, 'xsd$ustring$u0' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_50, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u2').
% 29.86/29.19  fof(axiom_51, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u3').
% 29.86/29.19  fof(axiom_52, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u4').
% 29.86/29.19  fof(axiom_53, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u5').
% 29.86/29.19  fof(axiom_54, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_55, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_56, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_57, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_58, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_59, axiom, 'xsd$ustring$u1' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_60, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u3').
% 29.86/29.19  fof(axiom_61, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u4').
% 29.86/29.19  fof(axiom_62, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u5').
% 29.86/29.19  fof(axiom_63, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_64, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_65, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_66, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_67, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_68, axiom, 'xsd$ustring$u2' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_69, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u4').
% 29.86/29.19  fof(axiom_70, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u5').
% 29.86/29.19  fof(axiom_71, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_72, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_73, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_74, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_75, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_76, axiom, 'xsd$ustring$u3' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_77, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u5').
% 29.86/29.19  fof(axiom_78, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_79, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_80, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_81, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_82, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_83, axiom, 'xsd$ustring$u4' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_84, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u6').
% 29.86/29.19  fof(axiom_85, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_86, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_87, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_88, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_89, axiom, 'xsd$ustring$u5' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_90, axiom, 'xsd$ustring$u6' != 'xsd$ustring$u7').
% 29.86/29.19  fof(axiom_91, axiom, 'xsd$ustring$u6' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_92, axiom, 'xsd$ustring$u6' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_93, axiom, 'xsd$ustring$u6' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_94, axiom, 'xsd$ustring$u6' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_95, axiom, 'xsd$ustring$u7' != 'xsd$ustring$u8').
% 29.86/29.19  fof(axiom_96, axiom, 'xsd$ustring$u7' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_97, axiom, 'xsd$ustring$u7' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_98, axiom, 'xsd$ustring$u7' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_99, axiom, 'xsd$ustring$u8' != 'xsd$ustring$u9').
% 29.86/29.19  fof(axiom_100, axiom, 'xsd$ustring$u8' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_101, axiom, 'xsd$ustring$u8' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_102, axiom, 'xsd$ustring$u9' != 'xsd$ustring$u10').
% 29.86/29.19  fof(axiom_103, axiom, 'xsd$ustring$u9' != 'xsd$ustring$u11').
% 29.86/29.19  fof(axiom_104, axiom, 'xsd$ustring$u10' != 'xsd$ustring$u11').
% 29.86/29.19  fof(the_axiom, conjecture, (! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cBipedidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cCrocodylidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cCrocodylidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cBipedidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cXantusiidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cEmydidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cSphenodontidae(X0))) & ! [X0] : ~((cAmphisbaenidae(X0) & cAgamidae(X0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 29.86/29.19  fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((cowlThing(X0) & ~cowlNothing(X0))) & (! [X0] : (('xsd$ustring'(X0) <=> ~'xsd$uinteger'(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cBipedidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cCrocodylidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cCrocodylidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cGekkonidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cBipedidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cBipedidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAmphisbaenidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cSphenodontidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cEmydidae(X0))) & (! [X0] : ~((cAmphisbaenidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cCordylidae(X0) & cCrocodylidae(X0))) & (! [X0] : ~((cXantusiidae(X0) & cAnomalepidae(X0))) & (! [X0] : ~((cAnomalepidae(X0) & cSphenodontidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cXantusiidae(X0))) & (! [X0] : ~((cGekkonidae(X0) & cAgamidae(X0))) & (! [X0] : ~((cAgamidae(X0) & cCordylidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cEmydidae(X0) & cLoxocemidae(X0))) & (! [X0] : ~((cLeptotyphlopidae(X0) & cSphenodontidae(X0))) & ! [X0] : ~((cAmphisbaenidae(X0) & cAgamidae(X0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [the_axiom])).
% 29.86/29.19  cnf(c19, plain, cowlThing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 29.86/29.19  cnf(c20, plain, ~cowlNothing(X0), inference(clausification, [status(esa)], [axiom_0])).
% 29.86/29.19  cnf(c21, plain, ~'xsd$ustring'(X0) | ~'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 29.86/29.19  cnf(c22, plain, 'xsd$ustring'(X0) | 'xsd$uinteger'(X0), inference(clausification, [status(esa)], [axiom_1])).
% 29.86/29.19  cnf(c24, plain, ~cAgamidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u0'), inference(clausification, [status(esa)], [axiom_3])).
% 29.86/29.19  cnf(c25, plain, ~cAgamidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_4])).
% 29.86/29.19  cnf(c27, plain, ~cAmphisbaenidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u1'), inference(clausification, [status(esa)], [axiom_6])).
% 29.86/29.19  cnf(c28, plain, ~cAmphisbaenidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_7])).
% 29.86/29.19  cnf(c30, plain, ~cAnomalepidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u2'), inference(clausification, [status(esa)], [axiom_9])).
% 29.86/29.19  cnf(c31, plain, ~cAnomalepidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_10])).
% 29.86/29.19  cnf(c33, plain, ~cBipedidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u3'), inference(clausification, [status(esa)], [axiom_12])).
% 29.86/29.19  cnf(c34, plain, ~cBipedidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_13])).
% 29.86/29.19  cnf(c36, plain, ~cCordylidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u4'), inference(clausification, [status(esa)], [axiom_15])).
% 29.86/29.19  cnf(c37, plain, ~cCordylidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_16])).
% 29.86/29.19  cnf(c39, plain, ~cCrocodylidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u5'), inference(clausification, [status(esa)], [axiom_18])).
% 29.86/29.19  cnf(c40, plain, ~cCrocodylidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_19])).
% 29.86/29.19  cnf(c42, plain, ~cEmydidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u6'), inference(clausification, [status(esa)], [axiom_21])).
% 29.86/29.19  cnf(c43, plain, ~cEmydidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_22])).
% 29.86/29.19  cnf(c45, plain, ~cGekkonidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u7'), inference(clausification, [status(esa)], [axiom_24])).
% 29.86/29.19  cnf(c46, plain, ~cGekkonidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_25])).
% 29.86/29.19  cnf(c48, plain, ~cLeptotyphlopidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u8'), inference(clausification, [status(esa)], [axiom_27])).
% 29.86/29.19  cnf(c49, plain, ~cLeptotyphlopidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_28])).
% 29.86/29.19  cnf(c51, plain, ~cLoxocemidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u9'), inference(clausification, [status(esa)], [axiom_30])).
% 29.86/29.19  cnf(c52, plain, ~cLoxocemidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_31])).
% 29.86/29.19  cnf(c54, plain, ~cReptile(X0) | ~'rfamily$uname'(X0,X1) | ~'rfamily$uname'(X0,X2) | X1 = X2, inference(clausification, [status(esa)], [axiom_32])).
% 29.86/29.19  cnf(c56, plain, ~cSphenodontidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u10'), inference(clausification, [status(esa)], [axiom_34])).
% 29.86/29.19  cnf(c57, plain, ~cSphenodontidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_35])).
% 29.86/29.19  cnf(c59, plain, ~cXantusiidae(X0) | 'rfamily$uname'(X0,'xsd$ustring$u11'), inference(clausification, [status(esa)], [axiom_37])).
% 29.86/29.19  cnf(c60, plain, ~cXantusiidae(X0) | cReptile(X0), inference(clausification, [status(esa)], [axiom_38])).
% 29.86/29.19  cnf(c61, plain, 'xsd$ustring$u0' != 'xsd$ustring$u1', inference(clausification, [status(esa)], [axiom_39])).
% 29.86/29.19  cnf(c62, plain, 'xsd$ustring$u0' != 'xsd$ustring$u2', inference(clausification, [status(esa)], [axiom_40])).
% 29.86/29.19  cnf(c63, plain, 'xsd$ustring$u0' != 'xsd$ustring$u3', inference(clausification, [status(esa)], [axiom_41])).
% 29.86/29.19  cnf(c64, plain, 'xsd$ustring$u0' != 'xsd$ustring$u4', inference(clausification, [status(esa)], [axiom_42])).
% 29.86/29.19  cnf(c65, plain, 'xsd$ustring$u0' != 'xsd$ustring$u5', inference(clausification, [status(esa)], [axiom_43])).
% 29.86/29.19  cnf(c66, plain, 'xsd$ustring$u0' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_44])).
% 29.86/29.19  cnf(c67, plain, 'xsd$ustring$u0' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_45])).
% 29.86/29.19  cnf(c68, plain, 'xsd$ustring$u0' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_46])).
% 29.86/29.19  cnf(c69, plain, 'xsd$ustring$u0' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_47])).
% 29.86/29.19  cnf(c70, plain, 'xsd$ustring$u0' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_48])).
% 29.86/29.19  cnf(c71, plain, 'xsd$ustring$u0' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_49])).
% 29.86/29.19  cnf(c72, plain, 'xsd$ustring$u1' != 'xsd$ustring$u2', inference(clausification, [status(esa)], [axiom_50])).
% 29.86/29.19  cnf(c73, plain, 'xsd$ustring$u1' != 'xsd$ustring$u3', inference(clausification, [status(esa)], [axiom_51])).
% 29.86/29.19  cnf(c74, plain, 'xsd$ustring$u1' != 'xsd$ustring$u4', inference(clausification, [status(esa)], [axiom_52])).
% 29.86/29.19  cnf(c75, plain, 'xsd$ustring$u1' != 'xsd$ustring$u5', inference(clausification, [status(esa)], [axiom_53])).
% 29.86/29.19  cnf(c76, plain, 'xsd$ustring$u1' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_54])).
% 29.86/29.19  cnf(c77, plain, 'xsd$ustring$u1' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_55])).
% 29.86/29.19  cnf(c78, plain, 'xsd$ustring$u1' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_56])).
% 29.86/29.19  cnf(c79, plain, 'xsd$ustring$u1' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_57])).
% 29.86/29.19  cnf(c80, plain, 'xsd$ustring$u1' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_58])).
% 29.86/29.19  cnf(c81, plain, 'xsd$ustring$u1' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_59])).
% 29.86/29.19  cnf(c82, plain, 'xsd$ustring$u2' != 'xsd$ustring$u3', inference(clausification, [status(esa)], [axiom_60])).
% 29.86/29.19  cnf(c83, plain, 'xsd$ustring$u2' != 'xsd$ustring$u4', inference(clausification, [status(esa)], [axiom_61])).
% 29.86/29.19  cnf(c84, plain, 'xsd$ustring$u2' != 'xsd$ustring$u5', inference(clausification, [status(esa)], [axiom_62])).
% 29.86/29.19  cnf(c85, plain, 'xsd$ustring$u2' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_63])).
% 29.86/29.19  cnf(c86, plain, 'xsd$ustring$u2' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_64])).
% 29.86/29.19  cnf(c87, plain, 'xsd$ustring$u2' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_65])).
% 29.86/29.19  cnf(c88, plain, 'xsd$ustring$u2' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_66])).
% 29.86/29.19  cnf(c89, plain, 'xsd$ustring$u2' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_67])).
% 29.86/29.19  cnf(c90, plain, 'xsd$ustring$u2' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_68])).
% 29.86/29.19  cnf(c91, plain, 'xsd$ustring$u3' != 'xsd$ustring$u4', inference(clausification, [status(esa)], [axiom_69])).
% 29.86/29.19  cnf(c92, plain, 'xsd$ustring$u3' != 'xsd$ustring$u5', inference(clausification, [status(esa)], [axiom_70])).
% 29.86/29.19  cnf(c93, plain, 'xsd$ustring$u3' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_71])).
% 29.86/29.19  cnf(c94, plain, 'xsd$ustring$u3' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_72])).
% 29.86/29.19  cnf(c95, plain, 'xsd$ustring$u3' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_73])).
% 29.86/29.19  cnf(c96, plain, 'xsd$ustring$u3' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_74])).
% 29.86/29.19  cnf(c97, plain, 'xsd$ustring$u3' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_75])).
% 29.86/29.19  cnf(c98, plain, 'xsd$ustring$u3' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_76])).
% 29.86/29.19  cnf(c99, plain, 'xsd$ustring$u4' != 'xsd$ustring$u5', inference(clausification, [status(esa)], [axiom_77])).
% 29.86/29.19  cnf(c100, plain, 'xsd$ustring$u4' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_78])).
% 29.86/29.19  cnf(c101, plain, 'xsd$ustring$u4' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_79])).
% 29.86/29.19  cnf(c102, plain, 'xsd$ustring$u4' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_80])).
% 29.86/29.19  cnf(c103, plain, 'xsd$ustring$u4' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_81])).
% 29.86/29.19  cnf(c104, plain, 'xsd$ustring$u4' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_82])).
% 29.86/29.19  cnf(c105, plain, 'xsd$ustring$u4' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_83])).
% 29.86/29.19  cnf(c106, plain, 'xsd$ustring$u5' != 'xsd$ustring$u6', inference(clausification, [status(esa)], [axiom_84])).
% 29.86/29.19  cnf(c107, plain, 'xsd$ustring$u5' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_85])).
% 29.86/29.19  cnf(c108, plain, 'xsd$ustring$u5' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_86])).
% 29.86/29.19  cnf(c109, plain, 'xsd$ustring$u5' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_87])).
% 29.86/29.19  cnf(c110, plain, 'xsd$ustring$u5' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_88])).
% 29.86/29.19  cnf(c111, plain, 'xsd$ustring$u5' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_89])).
% 29.86/29.19  cnf(c112, plain, 'xsd$ustring$u6' != 'xsd$ustring$u7', inference(clausification, [status(esa)], [axiom_90])).
% 29.86/29.19  cnf(c113, plain, 'xsd$ustring$u6' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_91])).
% 29.86/29.19  cnf(c114, plain, 'xsd$ustring$u6' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_92])).
% 29.86/29.19  cnf(c115, plain, 'xsd$ustring$u6' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_93])).
% 29.86/29.19  cnf(c116, plain, 'xsd$ustring$u6' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_94])).
% 29.86/29.19  cnf(c117, plain, 'xsd$ustring$u7' != 'xsd$ustring$u8', inference(clausification, [status(esa)], [axiom_95])).
% 29.86/29.19  cnf(c118, plain, 'xsd$ustring$u7' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_96])).
% 29.86/29.19  cnf(c119, plain, 'xsd$ustring$u7' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_97])).
% 29.86/29.19  cnf(c120, plain, 'xsd$ustring$u7' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_98])).
% 29.86/29.19  cnf(c121, plain, 'xsd$ustring$u8' != 'xsd$ustring$u9', inference(clausification, [status(esa)], [axiom_99])).
% 29.86/29.19  cnf(c122, plain, 'xsd$ustring$u8' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_100])).
% 29.86/29.19  cnf(c123, plain, 'xsd$ustring$u8' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_101])).
% 29.86/29.19  cnf(c124, plain, 'xsd$ustring$u9' != 'xsd$ustring$u10', inference(clausification, [status(esa)], [axiom_102])).
% 29.86/29.19  cnf(c125, plain, 'xsd$ustring$u9' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_103])).
% 29.86/29.19  cnf(c126, plain, 'xsd$ustring$u10' != 'xsd$ustring$u11', inference(clausification, [status(esa)], [axiom_104])).
% 29.86/29.19  cnf(c128, plain, ~X0 | ~cowlThing(sK103) | ~'xsd$uinteger'(sK104) | 'xsd$ustring'(sK104) | cowlNothing(sK103), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c129, plain, ~X0 | 'xsd$uinteger'(sK104) | ~cowlThing(sK103) | ~'xsd$ustring'(sK104) | cowlNothing(sK103), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c131, plain, X0 | cLeptotyphlopidae(sK105) | cAmphisbaenidae(sK106), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c132, plain, X0 | cLeptotyphlopidae(sK105) | cAgamidae(sK106), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c133, plain, X0 | cSphenodontidae(sK105) | cAmphisbaenidae(sK106), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c134, plain, X0 | cSphenodontidae(sK105) | cAgamidae(sK106), inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c135, plain, X0 | cLeptotyphlopidae(sK107) | cEmydidae(sK108) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c136, plain, X0 | cLeptotyphlopidae(sK107) | cLoxocemidae(sK108) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c137, plain, X0 | cLoxocemidae(sK107) | cEmydidae(sK108) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c138, plain, X0 | cLoxocemidae(sK107) | cLoxocemidae(sK108) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c139, plain, X0 | cGekkonidae(sK109) | cAgamidae(sK110) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c140, plain, X0 | cGekkonidae(sK109) | cCordylidae(sK110) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c141, plain, X0 | cAgamidae(sK109) | cAgamidae(sK110) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c142, plain, X0 | cAgamidae(sK109) | cCordylidae(sK110) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c143, plain, X0 | cAnomalepidae(sK111) | cLeptotyphlopidae(sK112) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c144, plain, X0 | cAnomalepidae(sK111) | cXantusiidae(sK112) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c145, plain, X0 | cSphenodontidae(sK111) | cLeptotyphlopidae(sK112) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c146, plain, X0 | cSphenodontidae(sK111) | cXantusiidae(sK112) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c147, plain, X0 | cCordylidae(sK113) | cXantusiidae(sK114) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c148, plain, X0 | cCordylidae(sK113) | cAnomalepidae(sK114) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c149, plain, X0 | cCrocodylidae(sK113) | cXantusiidae(sK114) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c150, plain, X0 | cCrocodylidae(sK113) | cAnomalepidae(sK114) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c151, plain, X0 | cAnomalepidae(sK115) | cLeptotyphlopidae(sK116) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c152, plain, X0 | cAnomalepidae(sK115) | cAnomalepidae(sK116) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c153, plain, X0 | cLoxocemidae(sK115) | cLeptotyphlopidae(sK116) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c154, plain, X0 | cLoxocemidae(sK115) | cAnomalepidae(sK116) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c155, plain, X0 | cAmphisbaenidae(sK117) | cGekkonidae(sK118) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c156, plain, X0 | cAmphisbaenidae(sK117) | cLoxocemidae(sK118) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c157, plain, X0 | cAnomalepidae(sK117) | cGekkonidae(sK118) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c158, plain, X0 | cAnomalepidae(sK117) | cLoxocemidae(sK118) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c159, plain, X0 | cSphenodontidae(sK119) | cLeptotyphlopidae(sK120) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c160, plain, X0 | cSphenodontidae(sK119) | cEmydidae(sK120) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c161, plain, X0 | cLoxocemidae(sK119) | cLeptotyphlopidae(sK120) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c162, plain, X0 | cLoxocemidae(sK119) | cEmydidae(sK120) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c163, plain, X0 | cXantusiidae(sK121) | cGekkonidae(sK122) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c164, plain, X0 | cXantusiidae(sK121) | cEmydidae(sK122) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c165, plain, X0 | cAmphisbaenidae(sK121) | cGekkonidae(sK122) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c166, plain, X0 | cAmphisbaenidae(sK121) | cEmydidae(sK122) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c167, plain, X0 | cAnomalepidae(sK123) | cSphenodontidae(sK124) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c168, plain, X0 | cAnomalepidae(sK123) | cCrocodylidae(sK124) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c169, plain, X0 | cAgamidae(sK123) | cSphenodontidae(sK124) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c170, plain, X0 | cAgamidae(sK123) | cCrocodylidae(sK124) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c171, plain, X0 | cBipedidae(sK125) | cXantusiidae(sK126) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c172, plain, X0 | cBipedidae(sK125) | cCordylidae(sK126) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c173, plain, X0 | cAmphisbaenidae(sK125) | cXantusiidae(sK126) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c174, plain, X0 | cAmphisbaenidae(sK125) | cCordylidae(sK126) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c175, plain, X0 | cGekkonidae(sK127) | cBipedidae(sK128) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c176, plain, X0 | cGekkonidae(sK127) | cCordylidae(sK128) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c177, plain, X0 | cAnomalepidae(sK127) | cBipedidae(sK128) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c178, plain, X0 | cAnomalepidae(sK127) | cCordylidae(sK128) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c179, plain, X0 | cSphenodontidae(sK129) | cLeptotyphlopidae(sK130) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c180, plain, X0 | cSphenodontidae(sK129) | cCordylidae(sK130) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c181, plain, X0 | cEmydidae(sK129) | cLeptotyphlopidae(sK130) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c182, plain, X0 | cEmydidae(sK129) | cCordylidae(sK130) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c183, plain, X0 | cXantusiidae(sK131) | cLeptotyphlopidae(sK132) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c184, plain, X0 | cXantusiidae(sK131) | cAmphisbaenidae(sK132) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c185, plain, X0 | cSphenodontidae(sK131) | cLeptotyphlopidae(sK132) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c186, plain, X0 | cSphenodontidae(sK131) | cAmphisbaenidae(sK132) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c187, plain, X0 | cXantusiidae(sK133) | cAnomalepidae(sK134) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c188, plain, X0 | cXantusiidae(sK133) | cEmydidae(sK134) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c189, plain, X0 | cBipedidae(sK133) | cAnomalepidae(sK134) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c190, plain, X0 | cBipedidae(sK133) | cEmydidae(sK134) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c191, plain, X0 | cAgamidae(sK135) | cXantusiidae(sK136) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c192, plain, X0 | cAgamidae(sK135) | cGekkonidae(sK136) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c193, plain, X0 | cLoxocemidae(sK135) | cXantusiidae(sK136) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c194, plain, X0 | cLoxocemidae(sK135) | cGekkonidae(sK136) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c195, plain, X0 | cAgamidae(sK137) | cCordylidae(sK138) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c196, plain, X0 | cAgamidae(sK137) | cEmydidae(sK138) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c197, plain, X0 | cEmydidae(sK137) | cCordylidae(sK138) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c198, plain, X0 | cEmydidae(sK137) | cEmydidae(sK138) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c199, plain, X0 | cXantusiidae(sK139) | cAnomalepidae(sK140) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c200, plain, X0 | cXantusiidae(sK139) | cCordylidae(sK140) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c201, plain, X0 | cAgamidae(sK139) | cAnomalepidae(sK140) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c202, plain, X0 | cAgamidae(sK139) | cCordylidae(sK140) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c203, plain, X0 | cCordylidae(sK141) | cGekkonidae(sK142) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c204, plain, X0 | cCordylidae(sK141) | cCordylidae(sK142) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c205, plain, X0 | cLoxocemidae(sK141) | cGekkonidae(sK142) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c206, plain, X0 | cLoxocemidae(sK141) | cCordylidae(sK142) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c207, plain, X0 | cSphenodontidae(sK143) | cAmphisbaenidae(sK144) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c208, plain, X0 | cSphenodontidae(sK143) | cCordylidae(sK144) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c209, plain, X0 | cCordylidae(sK143) | cAmphisbaenidae(sK144) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c210, plain, X0 | cCordylidae(sK143) | cCordylidae(sK144) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c211, plain, X0 | cGekkonidae(sK145) | cLeptotyphlopidae(sK146) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c212, plain, X0 | cGekkonidae(sK145) | cCrocodylidae(sK146) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c213, plain, X0 | cAmphisbaenidae(sK145) | cLeptotyphlopidae(sK146) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c214, plain, X0 | cAmphisbaenidae(sK145) | cCrocodylidae(sK146) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c215, plain, X0 | cBipedidae(sK147) | cBipedidae(sK148) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c216, plain, X0 | cBipedidae(sK147) | cAgamidae(sK148) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c217, plain, X0 | cLoxocemidae(sK147) | cBipedidae(sK148) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c218, plain, X0 | cLoxocemidae(sK147) | cAgamidae(sK148) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c219, plain, X0 | cXantusiidae(sK149) | cXantusiidae(sK150) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c220, plain, X0 | cXantusiidae(sK149) | cEmydidae(sK150) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c221, plain, X0 | cLoxocemidae(sK149) | cXantusiidae(sK150) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c222, plain, X0 | cLoxocemidae(sK149) | cEmydidae(sK150) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c223, plain, X0 | cAmphisbaenidae(sK151) | cAgamidae(sK152) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c224, plain, X0 | cAmphisbaenidae(sK151) | cCrocodylidae(sK152) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c225, plain, X0 | cEmydidae(sK151) | cAgamidae(sK152) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c226, plain, X0 | cEmydidae(sK151) | cCrocodylidae(sK152) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c227, plain, X0 | cXantusiidae(sK153) | cBipedidae(sK154) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c228, plain, X0 | cXantusiidae(sK153) | cEmydidae(sK154) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c229, plain, X0 | cCrocodylidae(sK153) | cBipedidae(sK154) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c230, plain, X0 | cCrocodylidae(sK153) | cEmydidae(sK154) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c231, plain, X0 | cAmphisbaenidae(sK155) | cCrocodylidae(sK156) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c232, plain, X0 | cAmphisbaenidae(sK155) | cLoxocemidae(sK156) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c233, plain, X0 | cCrocodylidae(sK155) | cCrocodylidae(sK156) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c234, plain, X0 | cCrocodylidae(sK155) | cLoxocemidae(sK156) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c235, plain, X0 | cAmphisbaenidae(sK157) | cLeptotyphlopidae(sK158) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c236, plain, X0 | cAmphisbaenidae(sK157) | cAgamidae(sK158) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c237, plain, X0 | cLoxocemidae(sK157) | cLeptotyphlopidae(sK158) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c238, plain, X0 | cLoxocemidae(sK157) | cAgamidae(sK158) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c239, plain, X0 | cAnomalepidae(sK159) | cCrocodylidae(sK160) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c240, plain, X0 | cAnomalepidae(sK159) | cEmydidae(sK160) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c241, plain, X0 | cCrocodylidae(sK159) | cCrocodylidae(sK160) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c242, plain, X0 | cCrocodylidae(sK159) | cEmydidae(sK160) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c243, plain, X0 | cGekkonidae(sK161) | cAgamidae(sK162) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c244, plain, X0 | cGekkonidae(sK161) | cSphenodontidae(sK162) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c245, plain, X0 | cSphenodontidae(sK161) | cAgamidae(sK162) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c246, plain, X0 | cSphenodontidae(sK161) | cSphenodontidae(sK162) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c247, plain, X0 | cBipedidae(sK163) | cGekkonidae(sK164) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c248, plain, X0 | cBipedidae(sK163) | cCrocodylidae(sK164) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c249, plain, X0 | cSphenodontidae(sK163) | cGekkonidae(sK164) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c250, plain, X0 | cSphenodontidae(sK163) | cCrocodylidae(sK164) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c251, plain, X0 | cBipedidae(sK165) | cBipedidae(sK166) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c252, plain, X0 | cBipedidae(sK165) | cGekkonidae(sK166) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c253, plain, X0 | cCrocodylidae(sK165) | cBipedidae(sK166) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c254, plain, X0 | cCrocodylidae(sK165) | cGekkonidae(sK166) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c255, plain, X0 | cLeptotyphlopidae(sK167) | cAmphisbaenidae(sK168) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c256, plain, X0 | cLeptotyphlopidae(sK167) | cSphenodontidae(sK168) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c257, plain, X0 | cGekkonidae(sK167) | cAmphisbaenidae(sK168) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c258, plain, X0 | cGekkonidae(sK167) | cSphenodontidae(sK168) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c259, plain, X0 | cLeptotyphlopidae(sK169) | cBipedidae(sK170) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c260, plain, X0 | cLeptotyphlopidae(sK169) | cAnomalepidae(sK170) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c261, plain, X0 | cBipedidae(sK169) | cBipedidae(sK170) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(c262, plain, X0 | cBipedidae(sK169) | cAnomalepidae(sK170) | ~X1, inference(clausification, [status(esa)], [negated_conjecture])).
% 29.86/29.19  cnf(d0, plain, 'xsd$ustring$u2' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cAnomalepidae(X1), inference(resolution, [status(thm)], [c54,c30])).
% 29.86/29.19  cnf(d1, plain, 'xsd$ustring$u2' = 'xsd$ustring$u4' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cCordylidae(X0), inference(resolution, [status(thm)], [d0,c36])).
% 29.86/29.19  cnf(d2, plain, ~cAnomalepidae(X0) | ~cCordylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c83,d1])).
% 29.86/29.19  cnf(d3, plain, cCordylidae(sK140) | ~'Ts86' | 'Ts87' | cReptile(sK139), inference(resolution, [status(thm)], [c200,c60])).
% 29.86/29.19  cnf(d4, plain, 'xsd$ustring$u0' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cAgamidae(X1), inference(resolution, [status(thm)], [c54,c24])).
% 29.86/29.19  cnf(d5, plain, 'xsd$ustring$u0' = 'xsd$ustring$u11' | ~cAgamidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d4,c59])).
% 29.86/29.19  cnf(d6, plain, ~cAgamidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c71,d5])).
% 29.86/29.19  cnf(d7, plain, ~cAgamidae(sK139) | ~cReptile(sK139) | cCordylidae(sK140) | ~'Ts86' | 'Ts87', inference(resolution, [status(thm)], [d6,c200])).
% 29.86/29.19  cnf(d8, plain, ~cAgamidae(sK139) | cCordylidae(sK140) | ~'Ts86' | 'Ts87' | cCordylidae(sK140) | ~'Ts86' | 'Ts87', inference(resolution, [status(thm)], [d7,d3])).
% 29.86/29.19  cnf(d9, plain, cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90' | cReptile(sK146), inference(resolution, [status(thm)], [c213,c49])).
% 29.86/29.19  cnf(d10, plain, 'xsd$ustring$u5' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cCrocodylidae(X1), inference(resolution, [status(thm)], [c54,c39])).
% 29.86/29.19  cnf(d11, plain, 'xsd$ustring$u5' = 'xsd$ustring$u8' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d10,c48])).
% 29.86/29.19  cnf(d12, plain, ~cCrocodylidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c108,d11])).
% 29.86/29.19  cnf(d13, plain, ~cCrocodylidae(sK146) | ~cLeptotyphlopidae(sK146) | cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d12,d9])).
% 29.86/29.19  cnf(d14, plain, cAmphisbaenidae(sK145) | ~cCrocodylidae(sK146) | ~'Ts89' | 'Ts90' | cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d13,c213])).
% 29.86/29.19  cnf(d15, plain, cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90' | cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d14,c214])).
% 29.86/29.19  cnf(d16, plain, 'xsd$ustring$u1' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cAmphisbaenidae(X1), inference(resolution, [status(thm)], [c54,c27])).
% 29.86/29.19  cnf(d17, plain, 'xsd$ustring$u1' = 'xsd$ustring$u7' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d16,c45])).
% 29.86/29.19  cnf(d18, plain, ~cAmphisbaenidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c77,d17])).
% 29.86/29.19  cnf(d19, plain, ~'Ts89' | 'Ts90' | cReptile(sK145), inference(resolution, [status(thm)], [d15,c28])).
% 29.86/29.19  cnf(d20, plain, ~'Ts89' | 'Ts90' | ~cAmphisbaenidae(sK145) | ~cGekkonidae(sK145), inference(resolution, [status(thm)], [d19,d18])).
% 29.86/29.19  cnf(d21, plain, cGekkonidae(sK145) | ~'Ts89' | 'Ts90' | cReptile(sK146), inference(resolution, [status(thm)], [c211,c49])).
% 29.86/29.19  cnf(d22, plain, ~cCrocodylidae(sK146) | ~cLeptotyphlopidae(sK146) | cGekkonidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d12,d21])).
% 29.86/29.20  cnf(d23, plain, ~cCrocodylidae(sK146) | cGekkonidae(sK145) | ~'Ts89' | 'Ts90' | cGekkonidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d22,c211])).
% 29.86/29.20  cnf(d24, plain, ~cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90' | cCrocodylidae(sK146) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d20,c212])).
% 29.86/29.20  cnf(d25, plain, cCrocodylidae(sK146) | ~'Ts89' | 'Ts90' | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d24,d15])).
% 29.86/29.20  cnf(d26, plain, ~'Ts89' | 'Ts90' | cGekkonidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d25,d23])).
% 29.86/29.20  cnf(d27, plain, ~'Ts89' | 'Ts90' | ~cAmphisbaenidae(sK145) | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d26,d20])).
% 29.86/29.20  cnf(d28, plain, ~'Ts89' | 'Ts90' | ~'Ts89' | 'Ts90', inference(resolution, [status(thm)], [d27,d15])).
% 29.86/29.20  cnf(d29, plain, cEmydidae(sK150) | ~'Ts91' | 'Ts92' | cReptile(sK149), inference(resolution, [status(thm)], [c220,c60])).
% 29.86/29.20  cnf(d30, plain, 'xsd$ustring$u9' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cLoxocemidae(X1), inference(resolution, [status(thm)], [c54,c51])).
% 29.86/29.20  cnf(d31, plain, 'xsd$ustring$u9' = 'xsd$ustring$u11' | ~cLoxocemidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d30,c59])).
% 29.86/29.20  cnf(d32, plain, ~cLoxocemidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c125,d31])).
% 29.86/29.20  cnf(d33, plain, ~cLoxocemidae(sK149) | ~cReptile(sK149) | cEmydidae(sK150) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d32,c220])).
% 29.86/29.20  cnf(d34, plain, cEmydidae(sK150) | ~cLoxocemidae(sK149) | ~'Ts91' | 'Ts92' | cEmydidae(sK150) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d33,d29])).
% 29.86/29.20  cnf(d35, plain, cEmydidae(sK150) | ~'Ts91' | 'Ts92' | cEmydidae(sK150) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d34,c222])).
% 29.86/29.20  cnf(d36, plain, ~'Ts91' | 'Ts92' | cReptile(sK150), inference(resolution, [status(thm)], [d35,c43])).
% 29.86/29.20  cnf(d37, plain, 'xsd$ustring$u6' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cEmydidae(X1), inference(resolution, [status(thm)], [c54,c42])).
% 29.86/29.20  cnf(d38, plain, 'xsd$ustring$u6' = 'xsd$ustring$u11' | ~cEmydidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d37,c59])).
% 29.86/29.20  cnf(d39, plain, ~cEmydidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c116,d38])).
% 29.86/29.20  cnf(d40, plain, cLoxocemidae(sK149) | ~'Ts91' | 'Ts92' | cReptile(sK150), inference(resolution, [status(thm)], [c221,c60])).
% 29.86/29.20  cnf(d41, plain, ~cEmydidae(sK150) | ~cReptile(sK150) | cLoxocemidae(sK149) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d39,c221])).
% 29.86/29.20  cnf(d42, plain, ~cEmydidae(sK150) | cLoxocemidae(sK149) | ~'Ts91' | 'Ts92' | cLoxocemidae(sK149) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d41,d40])).
% 29.86/29.20  cnf(d43, plain, ~'Ts91' | 'Ts92' | cLoxocemidae(sK149) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d35,d42])).
% 29.86/29.20  cnf(d44, plain, cXantusiidae(sK150) | ~'Ts91' | 'Ts92' | cReptile(sK149), inference(resolution, [status(thm)], [c219,c60])).
% 29.86/29.20  cnf(d45, plain, ~cLoxocemidae(sK149) | ~cReptile(sK149) | cXantusiidae(sK150) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d32,c219])).
% 29.86/29.20  cnf(d46, plain, ~cLoxocemidae(sK149) | cXantusiidae(sK150) | ~'Ts91' | 'Ts92' | cXantusiidae(sK150) | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d45,d44])).
% 29.86/29.20  cnf(d47, plain, cXantusiidae(sK150) | ~'Ts91' | 'Ts92' | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d46,d43])).
% 29.86/29.20  cnf(d48, plain, ~'Ts91' | 'Ts92' | ~cEmydidae(sK150) | ~cReptile(sK150), inference(resolution, [status(thm)], [d47,d39])).
% 29.86/29.20  cnf(d49, plain, ~cEmydidae(sK150) | ~'Ts91' | 'Ts92' | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d48,d36])).
% 29.86/29.20  cnf(d50, plain, ~'Ts91' | 'Ts92' | ~'Ts91' | 'Ts92', inference(resolution, [status(thm)], [d49,d35])).
% 29.86/29.20  cnf(d51, plain, cBipedidae(sK154) | ~'Ts93' | 'Ts94' | cReptile(sK153), inference(resolution, [status(thm)], [c227,c60])).
% 29.86/29.20  cnf(d52, plain, 'xsd$ustring$u5' = 'xsd$ustring$u11' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d10,c59])).
% 29.86/29.20  cnf(d53, plain, ~cCrocodylidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c111,d52])).
% 29.86/29.20  cnf(d54, plain, ~cCrocodylidae(sK153) | ~cReptile(sK153) | cBipedidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d53,c227])).
% 29.86/29.20  cnf(d55, plain, cBipedidae(sK154) | ~cCrocodylidae(sK153) | ~'Ts93' | 'Ts94' | cBipedidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d54,d51])).
% 29.86/29.20  cnf(d56, plain, cBipedidae(sK154) | ~'Ts93' | 'Ts94' | cBipedidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d55,c229])).
% 29.86/29.20  cnf(d57, plain, 'xsd$ustring$u3' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cBipedidae(X1), inference(resolution, [status(thm)], [c54,c33])).
% 29.86/29.20  cnf(d58, plain, 'xsd$ustring$u3' = 'xsd$ustring$u6' | ~cBipedidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d57,c42])).
% 29.86/29.20  cnf(d59, plain, ~cBipedidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c93,d58])).
% 29.86/29.20  cnf(d60, plain, ~'Ts93' | 'Ts94' | cReptile(sK154), inference(resolution, [status(thm)], [d56,c34])).
% 29.86/29.20  cnf(d61, plain, ~'Ts93' | 'Ts94' | ~cBipedidae(sK154) | ~cEmydidae(sK154), inference(resolution, [status(thm)], [d60,d59])).
% 29.86/29.20  cnf(d62, plain, cEmydidae(sK154) | ~'Ts93' | 'Ts94' | cReptile(sK153), inference(resolution, [status(thm)], [c228,c60])).
% 29.86/29.20  cnf(d63, plain, ~cCrocodylidae(sK153) | ~cReptile(sK153) | cEmydidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d53,c228])).
% 29.86/29.20  cnf(d64, plain, ~cCrocodylidae(sK153) | cEmydidae(sK154) | ~'Ts93' | 'Ts94' | cEmydidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d63,d62])).
% 29.86/29.20  cnf(d65, plain, ~cBipedidae(sK154) | ~'Ts93' | 'Ts94' | cCrocodylidae(sK153) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d61,c230])).
% 29.86/29.20  cnf(d66, plain, cCrocodylidae(sK153) | ~'Ts93' | 'Ts94' | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d65,d56])).
% 29.86/29.20  cnf(d67, plain, ~'Ts93' | 'Ts94' | cEmydidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d66,d64])).
% 29.86/29.20  cnf(d68, plain, ~'Ts93' | 'Ts94' | ~cBipedidae(sK154) | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d67,d61])).
% 29.86/29.20  cnf(d69, plain, ~'Ts93' | 'Ts94' | ~'Ts93' | 'Ts94', inference(resolution, [status(thm)], [d68,d56])).
% 29.86/29.20  cnf(d70, plain, cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95' | cReptile(sK156), inference(resolution, [status(thm)], [c231,c40])).
% 29.86/29.20  cnf(d71, plain, 'xsd$ustring$u5' = 'xsd$ustring$u9' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d10,c51])).
% 29.86/29.20  cnf(d72, plain, ~cCrocodylidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c109,d71])).
% 29.86/29.20  cnf(d73, plain, ~cCrocodylidae(sK156) | ~cLoxocemidae(sK156) | cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d72,d70])).
% 29.86/29.20  cnf(d74, plain, cAmphisbaenidae(sK155) | ~cCrocodylidae(sK156) | ~'Ts94' | 'Ts95' | cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d73,c232])).
% 29.86/29.20  cnf(d75, plain, cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95' | cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d74,c231])).
% 29.86/29.20  cnf(d76, plain, 'xsd$ustring$u1' = 'xsd$ustring$u5' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cCrocodylidae(X0), inference(resolution, [status(thm)], [d16,c39])).
% 29.86/29.20  cnf(d77, plain, ~cAmphisbaenidae(X0) | ~cCrocodylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c75,d76])).
% 29.86/29.20  cnf(d78, plain, ~'Ts94' | 'Ts95' | cReptile(sK155), inference(resolution, [status(thm)], [d75,c28])).
% 29.86/29.20  cnf(d79, plain, ~'Ts94' | 'Ts95' | ~cAmphisbaenidae(sK155) | ~cCrocodylidae(sK155), inference(resolution, [status(thm)], [d78,d77])).
% 29.86/29.20  cnf(d80, plain, cCrocodylidae(sK155) | ~'Ts94' | 'Ts95' | cReptile(sK156), inference(resolution, [status(thm)], [c234,c52])).
% 29.86/29.20  cnf(d81, plain, ~cCrocodylidae(sK156) | ~cLoxocemidae(sK156) | cCrocodylidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d72,d80])).
% 29.86/29.20  cnf(d82, plain, ~cCrocodylidae(sK156) | cCrocodylidae(sK155) | ~'Ts94' | 'Ts95' | cCrocodylidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d81,c234])).
% 29.86/29.20  cnf(d83, plain, ~cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95' | cCrocodylidae(sK156) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d79,c233])).
% 29.86/29.20  cnf(d84, plain, cCrocodylidae(sK156) | ~'Ts94' | 'Ts95' | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d83,d75])).
% 29.86/29.20  cnf(d85, plain, ~'Ts94' | 'Ts95' | cCrocodylidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d84,d82])).
% 29.86/29.20  cnf(d86, plain, ~'Ts94' | 'Ts95' | ~cAmphisbaenidae(sK155) | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d85,d79])).
% 29.86/29.20  cnf(d87, plain, ~'Ts94' | 'Ts95' | ~'Ts94' | 'Ts95', inference(resolution, [status(thm)], [d86,d75])).
% 29.86/29.20  cnf(d88, plain, cCrocodylidae(sK164) | ~'Ts98' | 'Ts99' | cReptile(sK163), inference(resolution, [status(thm)], [c250,c57])).
% 29.86/29.20  cnf(d89, plain, cGekkonidae(sK167) | ~'Ts100' | 'Ts101' | cReptile(sK168), inference(resolution, [status(thm)], [c258,c57])).
% 29.86/29.20  cnf(d90, plain, cowlNothing(sK103) | ~'xsd$uinteger'(sK104) | 'xsd$ustring'(sK104) | ~'Ts102', inference(resolution, [status(thm)], [c19,c128])).
% 29.86/29.20  cnf(d91, plain, ~'xsd$uinteger'(sK104) | 'xsd$ustring'(sK104) | ~'Ts102', inference(resolution, [status(thm)], [c20,d90])).
% 29.86/29.20  cnf(d92, plain, 'xsd$ustring'(sK104) | ~'Ts102' | 'xsd$ustring'(sK104), inference(resolution, [status(thm)], [d91,c22])).
% 29.86/29.20  cnf(d93, plain, ~'Ts102' | ~'xsd$uinteger'(sK104), inference(resolution, [status(thm)], [d92,c21])).
% 29.86/29.20  cnf(d94, plain, cowlNothing(sK103) | 'xsd$uinteger'(sK104) | ~'xsd$ustring'(sK104) | ~'Ts102', inference(resolution, [status(thm)], [c19,c129])).
% 29.86/29.20  cnf(d95, plain, 'xsd$uinteger'(sK104) | ~'xsd$ustring'(sK104) | ~'Ts102', inference(resolution, [status(thm)], [c20,d94])).
% 29.86/29.20  cnf(d96, plain, 'xsd$uinteger'(sK104) | ~'Ts102' | ~'Ts102', inference(resolution, [status(thm)], [d95,d92])).
% 29.86/29.20  cnf(d97, plain, ~'Ts102' | ~'Ts102', inference(resolution, [status(thm)], [d96,d93])).
% 29.86/29.20  cnf(d98, plain, cBipedidae(sK170) | cBipedidae(sK169) | ~'Ts101', inference(resolution, [status(thm)], [d97,c261])).
% 29.86/29.20  cnf(d99, plain, cBipedidae(sK170) | cLeptotyphlopidae(sK169) | ~'Ts101', inference(resolution, [status(thm)], [d97,c259])).
% 29.86/29.20  cnf(d100, plain, cBipedidae(sK170) | ~'Ts101' | cReptile(sK169), inference(resolution, [status(thm)], [d99,c49])).
% 29.86/29.20  cnf(d101, plain, 'xsd$ustring$u3' = 'xsd$ustring$u8' | ~cBipedidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d57,c48])).
% 29.86/29.20  cnf(d102, plain, ~cBipedidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c95,d101])).
% 29.86/29.20  cnf(d103, plain, ~cBipedidae(sK169) | ~cLeptotyphlopidae(sK169) | cBipedidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d102,d100])).
% 29.86/29.20  cnf(d104, plain, cBipedidae(sK170) | ~cBipedidae(sK169) | ~'Ts101' | cBipedidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d103,d99])).
% 29.86/29.20  cnf(d105, plain, cBipedidae(sK170) | ~'Ts101' | cBipedidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d104,d98])).
% 29.86/29.20  cnf(d106, plain, 'xsd$ustring$u2' = 'xsd$ustring$u3' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cBipedidae(X0), inference(resolution, [status(thm)], [d0,c33])).
% 29.86/29.20  cnf(d107, plain, ~cAnomalepidae(X0) | ~cBipedidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c82,d106])).
% 29.86/29.20  cnf(d108, plain, ~'Ts101' | cReptile(sK170), inference(resolution, [status(thm)], [d105,c34])).
% 29.86/29.20  cnf(d109, plain, ~'Ts101' | ~cAnomalepidae(sK170) | ~cBipedidae(sK170), inference(resolution, [status(thm)], [d108,d107])).
% 29.86/29.20  cnf(d110, plain, ~cAnomalepidae(sK170) | ~'Ts101' | ~'Ts101', inference(resolution, [status(thm)], [d109,d105])).
% 29.86/29.20  cnf(d111, plain, cAnomalepidae(sK170) | cBipedidae(sK169) | ~'Ts101', inference(resolution, [status(thm)], [d97,c262])).
% 29.86/29.20  cnf(d112, plain, cAnomalepidae(sK170) | cLeptotyphlopidae(sK169) | ~'Ts101', inference(resolution, [status(thm)], [d97,c260])).
% 29.86/29.20  cnf(d113, plain, cAnomalepidae(sK170) | ~'Ts101' | cReptile(sK169), inference(resolution, [status(thm)], [d112,c49])).
% 29.86/29.20  cnf(d114, plain, ~cBipedidae(sK169) | ~cLeptotyphlopidae(sK169) | cAnomalepidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d102,d113])).
% 29.86/29.20  cnf(d115, plain, cAnomalepidae(sK170) | ~cBipedidae(sK169) | ~'Ts101' | cAnomalepidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d114,d112])).
% 29.86/29.20  cnf(d116, plain, cAnomalepidae(sK170) | ~'Ts101' | cAnomalepidae(sK170) | ~'Ts101', inference(resolution, [status(thm)], [d115,d111])).
% 29.86/29.20  cnf(d117, plain, ~'Ts101' | ~'Ts101', inference(resolution, [status(thm)], [d116,d110])).
% 29.86/29.20  cnf(d118, plain, cGekkonidae(sK167) | cReptile(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d117,d89])).
% 29.86/29.20  cnf(d119, plain, 'xsd$ustring$u1' = 'xsd$ustring$u10' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d16,c56])).
% 29.86/29.20  cnf(d120, plain, ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c80,d119])).
% 29.86/29.20  cnf(d121, plain, cGekkonidae(sK167) | cSphenodontidae(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d117,c258])).
% 29.86/29.20  cnf(d122, plain, cGekkonidae(sK167) | ~'Ts100' | ~cAmphisbaenidae(sK168) | ~cReptile(sK168), inference(resolution, [status(thm)], [d121,d120])).
% 29.86/29.20  cnf(d123, plain, ~cAmphisbaenidae(sK168) | cGekkonidae(sK167) | ~'Ts100' | cGekkonidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d122,d118])).
% 29.86/29.20  cnf(d124, plain, cAmphisbaenidae(sK168) | cGekkonidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d117,c257])).
% 29.86/29.20  cnf(d125, plain, cAmphisbaenidae(sK168) | cLeptotyphlopidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d117,c255])).
% 29.86/29.20  cnf(d126, plain, 'xsd$ustring$u7' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cGekkonidae(X1), inference(resolution, [status(thm)], [c54,c45])).
% 29.86/29.20  cnf(d127, plain, 'xsd$ustring$u7' = 'xsd$ustring$u8' | ~cGekkonidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d126,c48])).
% 29.86/29.20  cnf(d128, plain, ~cGekkonidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c117,d127])).
% 29.86/29.20  cnf(d129, plain, cAmphisbaenidae(sK168) | ~'Ts100' | 'Ts101' | cReptile(sK167), inference(resolution, [status(thm)], [c255,c49])).
% 29.86/29.20  cnf(d130, plain, cAmphisbaenidae(sK168) | cReptile(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d117,d129])).
% 29.86/29.20  cnf(d131, plain, cAmphisbaenidae(sK168) | ~'Ts100' | ~cGekkonidae(sK167) | ~cLeptotyphlopidae(sK167), inference(resolution, [status(thm)], [d130,d128])).
% 29.86/29.20  cnf(d132, plain, cAmphisbaenidae(sK168) | ~cGekkonidae(sK167) | ~'Ts100' | cAmphisbaenidae(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d131,d125])).
% 29.86/29.20  cnf(d133, plain, cAmphisbaenidae(sK168) | ~'Ts100' | cAmphisbaenidae(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d132,d124])).
% 29.86/29.20  cnf(d134, plain, ~'Ts100' | cGekkonidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d133,d123])).
% 29.86/29.20  cnf(d135, plain, cLeptotyphlopidae(sK167) | ~'Ts100' | 'Ts101' | cReptile(sK168), inference(resolution, [status(thm)], [c256,c57])).
% 29.86/29.20  cnf(d136, plain, cLeptotyphlopidae(sK167) | cReptile(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d117,d135])).
% 29.86/29.20  cnf(d137, plain, cLeptotyphlopidae(sK167) | cSphenodontidae(sK168) | ~'Ts100', inference(resolution, [status(thm)], [d117,c256])).
% 29.86/29.20  cnf(d138, plain, cLeptotyphlopidae(sK167) | ~'Ts100' | ~cAmphisbaenidae(sK168) | ~cReptile(sK168), inference(resolution, [status(thm)], [d137,d120])).
% 29.86/29.20  cnf(d139, plain, ~cAmphisbaenidae(sK168) | cLeptotyphlopidae(sK167) | ~'Ts100' | cLeptotyphlopidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d138,d136])).
% 29.86/29.20  cnf(d140, plain, ~'Ts100' | cLeptotyphlopidae(sK167) | ~'Ts100', inference(resolution, [status(thm)], [d133,d139])).
% 29.86/29.20  cnf(d141, plain, ~'Ts100' | cReptile(sK167), inference(resolution, [status(thm)], [d140,c49])).
% 29.86/29.20  cnf(d142, plain, ~'Ts100' | ~cGekkonidae(sK167) | ~cLeptotyphlopidae(sK167), inference(resolution, [status(thm)], [d141,d128])).
% 29.86/29.20  cnf(d143, plain, ~cGekkonidae(sK167) | ~'Ts100' | ~'Ts100', inference(resolution, [status(thm)], [d142,d140])).
% 29.86/29.20  cnf(d144, plain, ~'Ts100' | ~'Ts100', inference(resolution, [status(thm)], [d143,d134])).
% 29.86/29.20  cnf(d145, plain, cBipedidae(sK166) | cBipedidae(sK165) | ~'Ts99', inference(resolution, [status(thm)], [d144,c251])).
% 29.86/29.20  cnf(d146, plain, cBipedidae(sK166) | cCrocodylidae(sK165) | ~'Ts99', inference(resolution, [status(thm)], [d144,c253])).
% 29.86/29.20  cnf(d147, plain, 'xsd$ustring$u3' = 'xsd$ustring$u5' | ~cBipedidae(X0) | ~cReptile(X0) | ~cCrocodylidae(X0), inference(resolution, [status(thm)], [d57,c39])).
% 29.86/29.20  cnf(d148, plain, ~cBipedidae(X0) | ~cCrocodylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c92,d147])).
% 29.86/29.20  cnf(d149, plain, cBipedidae(sK166) | ~'Ts99' | 'Ts100' | cReptile(sK165), inference(resolution, [status(thm)], [c251,c34])).
% 29.86/29.20  cnf(d150, plain, cBipedidae(sK166) | cReptile(sK165) | ~'Ts99', inference(resolution, [status(thm)], [d144,d149])).
% 29.86/29.20  cnf(d151, plain, cBipedidae(sK166) | ~'Ts99' | ~cBipedidae(sK165) | ~cCrocodylidae(sK165), inference(resolution, [status(thm)], [d150,d148])).
% 29.86/29.20  cnf(d152, plain, cBipedidae(sK166) | ~cBipedidae(sK165) | ~'Ts99' | cBipedidae(sK166) | ~'Ts99', inference(resolution, [status(thm)], [d151,d146])).
% 29.86/29.20  cnf(d153, plain, cBipedidae(sK166) | ~'Ts99' | cBipedidae(sK166) | ~'Ts99', inference(resolution, [status(thm)], [d152,d145])).
% 29.86/29.20  cnf(d154, plain, cBipedidae(sK165) | cGekkonidae(sK166) | ~'Ts99', inference(resolution, [status(thm)], [d144,c252])).
% 29.86/29.20  cnf(d155, plain, 'xsd$ustring$u3' = 'xsd$ustring$u7' | ~cBipedidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d57,c45])).
% 29.86/29.20  cnf(d156, plain, ~cBipedidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c94,d155])).
% 29.86/29.20  cnf(d157, plain, ~'Ts99' | cReptile(sK166), inference(resolution, [status(thm)], [d153,c34])).
% 29.86/29.20  cnf(d158, plain, ~'Ts99' | ~cBipedidae(sK166) | ~cGekkonidae(sK166), inference(resolution, [status(thm)], [d157,d156])).
% 29.86/29.20  cnf(d159, plain, ~cBipedidae(sK166) | ~'Ts99' | cBipedidae(sK165) | ~'Ts99', inference(resolution, [status(thm)], [d158,d154])).
% 29.86/29.20  cnf(d160, plain, cBipedidae(sK165) | ~'Ts99' | ~'Ts99', inference(resolution, [status(thm)], [d159,d153])).
% 29.86/29.20  cnf(d161, plain, cCrocodylidae(sK165) | cGekkonidae(sK166) | ~'Ts99', inference(resolution, [status(thm)], [d144,c254])).
% 29.86/29.20  cnf(d162, plain, ~cBipedidae(sK166) | ~'Ts99' | cCrocodylidae(sK165) | ~'Ts99', inference(resolution, [status(thm)], [d158,d161])).
% 29.86/29.20  cnf(d163, plain, cCrocodylidae(sK165) | ~'Ts99' | ~'Ts99', inference(resolution, [status(thm)], [d162,d153])).
% 29.86/29.20  cnf(d164, plain, ~'Ts99' | cReptile(sK165), inference(resolution, [status(thm)], [d163,c40])).
% 29.86/29.20  cnf(d165, plain, ~'Ts99' | ~cBipedidae(sK165) | ~cCrocodylidae(sK165), inference(resolution, [status(thm)], [d164,d148])).
% 29.86/29.20  cnf(d166, plain, ~cBipedidae(sK165) | ~'Ts99' | ~'Ts99', inference(resolution, [status(thm)], [d165,d163])).
% 29.86/29.20  cnf(d167, plain, ~'Ts99' | ~'Ts99', inference(resolution, [status(thm)], [d166,d160])).
% 29.86/29.20  cnf(d168, plain, cCrocodylidae(sK164) | cReptile(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d167,d88])).
% 29.86/29.20  cnf(d169, plain, 'xsd$ustring$u3' = 'xsd$ustring$u10' | ~cBipedidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d57,c56])).
% 29.86/29.20  cnf(d170, plain, ~cBipedidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c97,d169])).
% 29.86/29.20  cnf(d171, plain, cCrocodylidae(sK164) | cSphenodontidae(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d167,c250])).
% 29.86/29.20  cnf(d172, plain, cCrocodylidae(sK164) | ~'Ts98' | ~cBipedidae(sK163) | ~cReptile(sK163), inference(resolution, [status(thm)], [d171,d170])).
% 29.86/29.20  cnf(d173, plain, ~cBipedidae(sK163) | cCrocodylidae(sK164) | ~'Ts98' | cCrocodylidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d172,d168])).
% 29.86/29.20  cnf(d174, plain, cBipedidae(sK163) | cCrocodylidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d167,c248])).
% 29.86/29.20  cnf(d175, plain, cBipedidae(sK163) | cGekkonidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d167,c247])).
% 29.86/29.20  cnf(d176, plain, 'xsd$ustring$u5' = 'xsd$ustring$u7' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d10,c45])).
% 29.86/29.20  cnf(d177, plain, ~cCrocodylidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c107,d176])).
% 29.86/29.20  cnf(d178, plain, cBipedidae(sK163) | ~'Ts98' | 'Ts99' | cReptile(sK164), inference(resolution, [status(thm)], [c247,c46])).
% 29.86/29.20  cnf(d179, plain, cBipedidae(sK163) | cReptile(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d167,d178])).
% 29.86/29.20  cnf(d180, plain, cBipedidae(sK163) | ~'Ts98' | ~cCrocodylidae(sK164) | ~cGekkonidae(sK164), inference(resolution, [status(thm)], [d179,d177])).
% 29.86/29.20  cnf(d181, plain, cBipedidae(sK163) | ~cCrocodylidae(sK164) | ~'Ts98' | cBipedidae(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d180,d175])).
% 29.86/29.20  cnf(d182, plain, cBipedidae(sK163) | ~'Ts98' | cBipedidae(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d181,d174])).
% 29.86/29.20  cnf(d183, plain, ~'Ts98' | cCrocodylidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d182,d173])).
% 29.86/29.20  cnf(d184, plain, cGekkonidae(sK164) | ~'Ts98' | 'Ts99' | cReptile(sK163), inference(resolution, [status(thm)], [c249,c57])).
% 29.86/29.20  cnf(d185, plain, cGekkonidae(sK164) | cReptile(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d167,d184])).
% 29.86/29.20  cnf(d186, plain, cGekkonidae(sK164) | cSphenodontidae(sK163) | ~'Ts98', inference(resolution, [status(thm)], [d167,c249])).
% 29.86/29.20  cnf(d187, plain, cGekkonidae(sK164) | ~'Ts98' | ~cBipedidae(sK163) | ~cReptile(sK163), inference(resolution, [status(thm)], [d186,d170])).
% 29.86/29.20  cnf(d188, plain, ~cBipedidae(sK163) | cGekkonidae(sK164) | ~'Ts98' | cGekkonidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d187,d185])).
% 29.86/29.20  cnf(d189, plain, ~'Ts98' | cGekkonidae(sK164) | ~'Ts98', inference(resolution, [status(thm)], [d182,d188])).
% 29.86/29.20  cnf(d190, plain, ~'Ts98' | cReptile(sK164), inference(resolution, [status(thm)], [d183,c40])).
% 29.86/29.20  cnf(d191, plain, ~'Ts98' | ~cCrocodylidae(sK164) | ~cGekkonidae(sK164), inference(resolution, [status(thm)], [d190,d177])).
% 29.86/29.20  cnf(d192, plain, ~cCrocodylidae(sK164) | ~'Ts98' | ~'Ts98', inference(resolution, [status(thm)], [d191,d189])).
% 29.86/29.20  cnf(d193, plain, ~'Ts98' | ~'Ts98', inference(resolution, [status(thm)], [d192,d183])).
% 29.86/29.20  cnf(d194, plain, cAgamidae(sK162) | cGekkonidae(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d193,c243])).
% 29.86/29.20  cnf(d195, plain, cAgamidae(sK162) | ~'Ts97' | 'Ts98' | cReptile(sK161), inference(resolution, [status(thm)], [c243,c46])).
% 29.86/29.20  cnf(d196, plain, cAgamidae(sK162) | cReptile(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d193,d195])).
% 29.86/29.20  cnf(d197, plain, 'xsd$ustring$u7' = 'xsd$ustring$u10' | ~cGekkonidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d126,c56])).
% 29.86/29.20  cnf(d198, plain, ~cGekkonidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c119,d197])).
% 29.86/29.20  cnf(d199, plain, cAgamidae(sK162) | cSphenodontidae(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d193,c245])).
% 29.86/29.20  cnf(d200, plain, cAgamidae(sK162) | ~'Ts97' | ~cGekkonidae(sK161) | ~cReptile(sK161), inference(resolution, [status(thm)], [d199,d198])).
% 29.86/29.20  cnf(d201, plain, cAgamidae(sK162) | ~cGekkonidae(sK161) | ~'Ts97' | cAgamidae(sK162) | ~'Ts97', inference(resolution, [status(thm)], [d200,d196])).
% 29.86/29.20  cnf(d202, plain, cAgamidae(sK162) | ~'Ts97' | cAgamidae(sK162) | ~'Ts97', inference(resolution, [status(thm)], [d201,d194])).
% 29.86/29.20  cnf(d203, plain, ~'Ts97' | cReptile(sK162), inference(resolution, [status(thm)], [d202,c25])).
% 29.86/29.20  cnf(d204, plain, 'xsd$ustring$u0' = 'xsd$ustring$u10' | ~cAgamidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d4,c56])).
% 29.86/29.20  cnf(d205, plain, ~cAgamidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c70,d204])).
% 29.86/29.20  cnf(d206, plain, cGekkonidae(sK161) | ~'Ts97' | 'Ts98' | cReptile(sK162), inference(resolution, [status(thm)], [c244,c57])).
% 29.86/29.20  cnf(d207, plain, cGekkonidae(sK161) | cReptile(sK162) | ~'Ts97', inference(resolution, [status(thm)], [d193,d206])).
% 29.86/29.20  cnf(d208, plain, cGekkonidae(sK161) | cSphenodontidae(sK162) | ~'Ts97', inference(resolution, [status(thm)], [d193,c244])).
% 29.86/29.20  cnf(d209, plain, cGekkonidae(sK161) | ~'Ts97' | ~cAgamidae(sK162) | ~cReptile(sK162), inference(resolution, [status(thm)], [d208,d205])).
% 29.86/29.20  cnf(d210, plain, ~cAgamidae(sK162) | cGekkonidae(sK161) | ~'Ts97' | cGekkonidae(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d209,d207])).
% 29.86/29.20  cnf(d211, plain, ~'Ts97' | cGekkonidae(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d202,d210])).
% 29.86/29.20  cnf(d212, plain, ~'Ts97' | cReptile(sK161), inference(resolution, [status(thm)], [d211,c46])).
% 29.86/29.20  cnf(d213, plain, cSphenodontidae(sK162) | cSphenodontidae(sK161) | ~'Ts97', inference(resolution, [status(thm)], [d193,c246])).
% 29.86/29.20  cnf(d214, plain, cSphenodontidae(sK162) | ~'Ts97' | ~cGekkonidae(sK161) | ~cReptile(sK161), inference(resolution, [status(thm)], [d213,d198])).
% 29.86/29.20  cnf(d215, plain, ~cGekkonidae(sK161) | cSphenodontidae(sK162) | ~'Ts97' | ~'Ts97', inference(resolution, [status(thm)], [d214,d212])).
% 29.86/29.20  cnf(d216, plain, cSphenodontidae(sK162) | ~'Ts97' | ~'Ts97', inference(resolution, [status(thm)], [d215,d211])).
% 29.86/29.20  cnf(d217, plain, ~'Ts97' | ~cAgamidae(sK162) | ~cReptile(sK162), inference(resolution, [status(thm)], [d216,d205])).
% 29.86/29.20  cnf(d218, plain, ~cAgamidae(sK162) | ~'Ts97' | ~'Ts97', inference(resolution, [status(thm)], [d217,d203])).
% 29.86/29.20  cnf(d219, plain, ~'Ts97' | ~'Ts97', inference(resolution, [status(thm)], [d218,d202])).
% 29.86/29.20  cnf(d220, plain, cAnomalepidae(sK159) | cCrocodylidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d219,c239])).
% 29.86/29.20  cnf(d221, plain, cAnomalepidae(sK159) | cEmydidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d219,c240])).
% 29.86/29.20  cnf(d222, plain, cAnomalepidae(sK159) | ~'Ts96' | 'Ts97' | cReptile(sK160), inference(resolution, [status(thm)], [c239,c40])).
% 29.86/29.20  cnf(d223, plain, 'xsd$ustring$u5' = 'xsd$ustring$u6' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d10,c42])).
% 29.86/29.20  cnf(d224, plain, ~cCrocodylidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c106,d223])).
% 29.86/29.20  cnf(d225, plain, ~cCrocodylidae(sK160) | ~cEmydidae(sK160) | cAnomalepidae(sK159) | ~'Ts96' | 'Ts97', inference(resolution, [status(thm)], [d224,d222])).
% 29.86/29.20  cnf(d226, plain, cAnomalepidae(sK159) | ~cCrocodylidae(sK160) | ~cEmydidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d219,d225])).
% 29.86/29.20  cnf(d227, plain, cAnomalepidae(sK159) | ~cCrocodylidae(sK160) | ~'Ts96' | cAnomalepidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d226,d221])).
% 29.86/29.20  cnf(d228, plain, cAnomalepidae(sK159) | ~'Ts96' | cAnomalepidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d227,d220])).
% 29.86/29.20  cnf(d229, plain, 'xsd$ustring$u2' = 'xsd$ustring$u5' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cCrocodylidae(X0), inference(resolution, [status(thm)], [d0,c39])).
% 29.86/29.20  cnf(d230, plain, ~cAnomalepidae(X0) | ~cCrocodylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c84,d229])).
% 29.86/29.20  cnf(d231, plain, ~'Ts96' | cReptile(sK159), inference(resolution, [status(thm)], [d228,c31])).
% 29.86/29.20  cnf(d232, plain, ~'Ts96' | ~cAnomalepidae(sK159) | ~cCrocodylidae(sK159), inference(resolution, [status(thm)], [d231,d230])).
% 29.86/29.20  cnf(d233, plain, cCrocodylidae(sK159) | cEmydidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d219,c242])).
% 29.86/29.20  cnf(d234, plain, cCrocodylidae(sK159) | ~'Ts96' | 'Ts97' | cReptile(sK160), inference(resolution, [status(thm)], [c242,c43])).
% 29.86/29.20  cnf(d235, plain, ~cCrocodylidae(sK160) | ~cEmydidae(sK160) | cCrocodylidae(sK159) | ~'Ts96' | 'Ts97', inference(resolution, [status(thm)], [d224,d234])).
% 29.86/29.20  cnf(d236, plain, ~cCrocodylidae(sK160) | cCrocodylidae(sK159) | ~cEmydidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d219,d235])).
% 29.86/29.20  cnf(d237, plain, ~cCrocodylidae(sK160) | cCrocodylidae(sK159) | ~'Ts96' | cCrocodylidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d236,d233])).
% 29.86/29.20  cnf(d238, plain, cCrocodylidae(sK160) | cCrocodylidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d219,c241])).
% 29.86/29.20  cnf(d239, plain, ~cAnomalepidae(sK159) | ~'Ts96' | cCrocodylidae(sK160) | ~'Ts96', inference(resolution, [status(thm)], [d232,d238])).
% 29.86/29.20  cnf(d240, plain, cCrocodylidae(sK160) | ~'Ts96' | ~'Ts96', inference(resolution, [status(thm)], [d239,d228])).
% 29.86/29.20  cnf(d241, plain, ~'Ts96' | cCrocodylidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d240,d237])).
% 29.86/29.20  cnf(d242, plain, ~'Ts96' | ~cAnomalepidae(sK159) | ~'Ts96', inference(resolution, [status(thm)], [d241,d232])).
% 29.86/29.20  cnf(d243, plain, ~'Ts96' | ~'Ts96', inference(resolution, [status(thm)], [d242,d228])).
% 29.86/29.20  cnf(d244, plain, cAgamidae(sK158) | cAmphisbaenidae(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d243,c236])).
% 29.86/29.20  cnf(d245, plain, cAgamidae(sK158) | cLoxocemidae(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d243,c238])).
% 29.86/29.20  cnf(d246, plain, 'xsd$ustring$u1' = 'xsd$ustring$u9' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d16,c51])).
% 29.86/29.20  cnf(d247, plain, ~cAmphisbaenidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c79,d246])).
% 29.86/29.20  cnf(d248, plain, cAgamidae(sK158) | ~'Ts95' | 'Ts96' | cReptile(sK157), inference(resolution, [status(thm)], [c236,c28])).
% 29.86/29.20  cnf(d249, plain, cAgamidae(sK158) | cReptile(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d243,d248])).
% 29.86/29.20  cnf(d250, plain, cAgamidae(sK158) | ~'Ts95' | ~cAmphisbaenidae(sK157) | ~cLoxocemidae(sK157), inference(resolution, [status(thm)], [d249,d247])).
% 29.86/29.20  cnf(d251, plain, cAgamidae(sK158) | ~cAmphisbaenidae(sK157) | ~'Ts95' | cAgamidae(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d250,d245])).
% 29.86/29.20  cnf(d252, plain, cAgamidae(sK158) | ~'Ts95' | cAgamidae(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d251,d244])).
% 29.86/29.20  cnf(d253, plain, 'xsd$ustring$u0' = 'xsd$ustring$u8' | ~cAgamidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d4,c48])).
% 29.86/29.20  cnf(d254, plain, ~cAgamidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c68,d253])).
% 29.86/29.20  cnf(d255, plain, ~'Ts95' | cReptile(sK158), inference(resolution, [status(thm)], [d252,c25])).
% 29.86/29.20  cnf(d256, plain, ~'Ts95' | ~cAgamidae(sK158) | ~cLeptotyphlopidae(sK158), inference(resolution, [status(thm)], [d255,d254])).
% 29.86/29.20  cnf(d257, plain, cAmphisbaenidae(sK157) | cLeptotyphlopidae(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d243,c235])).
% 29.86/29.20  cnf(d258, plain, cAmphisbaenidae(sK157) | ~'Ts95' | 'Ts96' | cReptile(sK158), inference(resolution, [status(thm)], [c235,c49])).
% 29.86/29.20  cnf(d259, plain, cAmphisbaenidae(sK157) | cReptile(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d243,d258])).
% 29.86/29.20  cnf(d260, plain, cAmphisbaenidae(sK157) | ~'Ts95' | ~cAgamidae(sK158) | ~cLeptotyphlopidae(sK158), inference(resolution, [status(thm)], [d259,d254])).
% 29.86/29.20  cnf(d261, plain, ~cAgamidae(sK158) | cAmphisbaenidae(sK157) | ~'Ts95' | cAmphisbaenidae(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d260,d257])).
% 29.86/29.20  cnf(d262, plain, ~'Ts95' | cAmphisbaenidae(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d252,d261])).
% 29.86/29.20  cnf(d263, plain, cLeptotyphlopidae(sK158) | cLoxocemidae(sK157) | ~'Ts95', inference(resolution, [status(thm)], [d243,c237])).
% 29.86/29.20  cnf(d264, plain, ~'Ts95' | cReptile(sK157), inference(resolution, [status(thm)], [d262,c28])).
% 29.86/29.20  cnf(d265, plain, ~'Ts95' | ~cAmphisbaenidae(sK157) | ~cLoxocemidae(sK157), inference(resolution, [status(thm)], [d264,d247])).
% 29.86/29.20  cnf(d266, plain, ~cAmphisbaenidae(sK157) | ~'Ts95' | cLeptotyphlopidae(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d265,d263])).
% 29.86/29.20  cnf(d267, plain, cLeptotyphlopidae(sK158) | ~'Ts95' | ~'Ts95', inference(resolution, [status(thm)], [d266,d262])).
% 29.86/29.20  cnf(d268, plain, ~'Ts95' | ~cAgamidae(sK158) | ~'Ts95', inference(resolution, [status(thm)], [d267,d256])).
% 29.86/29.20  cnf(d269, plain, ~'Ts95' | ~'Ts95', inference(resolution, [status(thm)], [d268,d252])).
% 29.86/29.20  cnf(d270, plain, ~'Ts94', inference(resolution, [status(thm)], [d269,d87])).
% 29.86/29.20  cnf(d271, plain, ~'Ts93', inference(resolution, [status(thm)], [d270,d69])).
% 29.86/29.20  cnf(d272, plain, cAgamidae(sK152) | cAmphisbaenidae(sK151) | ~'Ts92', inference(resolution, [status(thm)], [d271,c223])).
% 29.86/29.20  cnf(d273, plain, cAgamidae(sK152) | cEmydidae(sK151) | ~'Ts92', inference(resolution, [status(thm)], [d271,c225])).
% 29.86/29.20  cnf(d274, plain, 'xsd$ustring$u1' = 'xsd$ustring$u6' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d16,c42])).
% 29.86/29.20  cnf(d275, plain, ~cAmphisbaenidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c76,d274])).
% 29.86/29.20  cnf(d276, plain, cAgamidae(sK152) | ~'Ts92' | 'Ts93' | cReptile(sK151), inference(resolution, [status(thm)], [c223,c28])).
% 29.86/29.20  cnf(d277, plain, cAgamidae(sK152) | cReptile(sK151) | ~'Ts92', inference(resolution, [status(thm)], [d271,d276])).
% 29.86/29.20  cnf(d278, plain, cAgamidae(sK152) | ~'Ts92' | ~cAmphisbaenidae(sK151) | ~cEmydidae(sK151), inference(resolution, [status(thm)], [d277,d275])).
% 29.86/29.20  cnf(d279, plain, cAgamidae(sK152) | ~cAmphisbaenidae(sK151) | ~'Ts92' | cAgamidae(sK152) | ~'Ts92', inference(resolution, [status(thm)], [d278,d273])).
% 29.86/29.20  cnf(d280, plain, cAgamidae(sK152) | ~'Ts92' | cAgamidae(sK152) | ~'Ts92', inference(resolution, [status(thm)], [d279,d272])).
% 29.86/29.20  cnf(d281, plain, 'xsd$ustring$u0' = 'xsd$ustring$u5' | ~cAgamidae(X0) | ~cReptile(X0) | ~cCrocodylidae(X0), inference(resolution, [status(thm)], [d4,c39])).
% 29.86/29.20  cnf(d282, plain, ~cAgamidae(X0) | ~cCrocodylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c65,d281])).
% 29.86/29.20  cnf(d283, plain, ~'Ts92' | cReptile(sK152), inference(resolution, [status(thm)], [d280,c25])).
% 29.86/29.20  cnf(d284, plain, ~'Ts92' | ~cAgamidae(sK152) | ~cCrocodylidae(sK152), inference(resolution, [status(thm)], [d283,d282])).
% 29.86/29.20  cnf(d285, plain, cAmphisbaenidae(sK151) | cCrocodylidae(sK152) | ~'Ts92', inference(resolution, [status(thm)], [d271,c224])).
% 29.86/29.20  cnf(d286, plain, ~cAgamidae(sK152) | ~'Ts92' | cAmphisbaenidae(sK151) | ~'Ts92', inference(resolution, [status(thm)], [d284,d285])).
% 29.86/29.20  cnf(d287, plain, cAmphisbaenidae(sK151) | ~'Ts92' | ~'Ts92', inference(resolution, [status(thm)], [d286,d280])).
% 29.86/29.20  cnf(d288, plain, cCrocodylidae(sK152) | cEmydidae(sK151) | ~'Ts92', inference(resolution, [status(thm)], [d271,c226])).
% 29.86/29.20  cnf(d289, plain, ~'Ts92' | cReptile(sK151), inference(resolution, [status(thm)], [d287,c28])).
% 29.86/29.20  cnf(d290, plain, ~'Ts92' | ~cAmphisbaenidae(sK151) | ~cEmydidae(sK151), inference(resolution, [status(thm)], [d289,d275])).
% 29.86/29.20  cnf(d291, plain, ~cAmphisbaenidae(sK151) | ~'Ts92' | cCrocodylidae(sK152) | ~'Ts92', inference(resolution, [status(thm)], [d290,d288])).
% 29.86/29.20  cnf(d292, plain, cCrocodylidae(sK152) | ~'Ts92' | ~'Ts92', inference(resolution, [status(thm)], [d291,d287])).
% 29.86/29.20  cnf(d293, plain, ~'Ts92' | ~cAgamidae(sK152) | ~'Ts92', inference(resolution, [status(thm)], [d292,d284])).
% 29.86/29.20  cnf(d294, plain, ~'Ts92' | ~'Ts92', inference(resolution, [status(thm)], [d293,d280])).
% 29.86/29.20  cnf(d295, plain, ~'Ts91', inference(resolution, [status(thm)], [d294,d50])).
% 29.86/29.20  cnf(d296, plain, cBipedidae(sK148) | cBipedidae(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,c215])).
% 29.86/29.20  cnf(d297, plain, cBipedidae(sK148) | cLoxocemidae(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,c217])).
% 29.86/29.20  cnf(d298, plain, 'xsd$ustring$u3' = 'xsd$ustring$u9' | ~cBipedidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d57,c51])).
% 29.86/29.20  cnf(d299, plain, ~cBipedidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c96,d298])).
% 29.86/29.20  cnf(d300, plain, cBipedidae(sK148) | ~'Ts90' | 'Ts91' | cReptile(sK147), inference(resolution, [status(thm)], [c215,c34])).
% 29.86/29.20  cnf(d301, plain, cBipedidae(sK148) | cReptile(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,d300])).
% 29.86/29.20  cnf(d302, plain, cBipedidae(sK148) | ~'Ts90' | ~cBipedidae(sK147) | ~cLoxocemidae(sK147), inference(resolution, [status(thm)], [d301,d299])).
% 29.86/29.20  cnf(d303, plain, cBipedidae(sK148) | ~cBipedidae(sK147) | ~'Ts90' | cBipedidae(sK148) | ~'Ts90', inference(resolution, [status(thm)], [d302,d297])).
% 29.86/29.20  cnf(d304, plain, cBipedidae(sK148) | ~'Ts90' | cBipedidae(sK148) | ~'Ts90', inference(resolution, [status(thm)], [d303,d296])).
% 29.86/29.20  cnf(d305, plain, 'xsd$ustring$u0' = 'xsd$ustring$u3' | ~cAgamidae(X0) | ~cReptile(X0) | ~cBipedidae(X0), inference(resolution, [status(thm)], [d4,c33])).
% 29.86/29.20  cnf(d306, plain, ~cAgamidae(X0) | ~cBipedidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c63,d305])).
% 29.86/29.20  cnf(d307, plain, ~'Ts90' | cReptile(sK148), inference(resolution, [status(thm)], [d304,c34])).
% 29.86/29.20  cnf(d308, plain, ~'Ts90' | ~cAgamidae(sK148) | ~cBipedidae(sK148), inference(resolution, [status(thm)], [d307,d306])).
% 29.92/29.20  cnf(d309, plain, ~cAgamidae(sK148) | ~'Ts90' | ~'Ts90', inference(resolution, [status(thm)], [d308,d304])).
% 29.92/29.20  cnf(d310, plain, cAgamidae(sK148) | cBipedidae(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,c216])).
% 29.92/29.20  cnf(d311, plain, cAgamidae(sK148) | cLoxocemidae(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,c218])).
% 29.92/29.20  cnf(d312, plain, cAgamidae(sK148) | ~'Ts90' | 'Ts91' | cReptile(sK147), inference(resolution, [status(thm)], [c216,c34])).
% 29.92/29.20  cnf(d313, plain, cAgamidae(sK148) | cReptile(sK147) | ~'Ts90', inference(resolution, [status(thm)], [d295,d312])).
% 29.92/29.20  cnf(d314, plain, cAgamidae(sK148) | ~'Ts90' | ~cBipedidae(sK147) | ~cLoxocemidae(sK147), inference(resolution, [status(thm)], [d313,d299])).
% 29.92/29.20  cnf(d315, plain, cAgamidae(sK148) | ~cBipedidae(sK147) | ~'Ts90' | cAgamidae(sK148) | ~'Ts90', inference(resolution, [status(thm)], [d314,d311])).
% 29.92/29.20  cnf(d316, plain, cAgamidae(sK148) | ~'Ts90' | cAgamidae(sK148) | ~'Ts90', inference(resolution, [status(thm)], [d315,d310])).
% 29.92/29.20  cnf(d317, plain, ~'Ts90' | ~'Ts90', inference(resolution, [status(thm)], [d316,d309])).
% 29.92/29.20  cnf(d318, plain, ~'Ts89', inference(resolution, [status(thm)], [d317,d28])).
% 29.92/29.20  cnf(d319, plain, cAmphisbaenidae(sK144) | cCordylidae(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,c209])).
% 29.92/29.20  cnf(d320, plain, cAmphisbaenidae(sK144) | ~'Ts88' | 'Ts89' | cReptile(sK143), inference(resolution, [status(thm)], [c207,c57])).
% 29.92/29.20  cnf(d321, plain, cAmphisbaenidae(sK144) | cReptile(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,d320])).
% 29.92/29.20  cnf(d322, plain, 'xsd$ustring$u4' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cCordylidae(X1), inference(resolution, [status(thm)], [c54,c36])).
% 29.92/29.20  cnf(d323, plain, 'xsd$ustring$u4' = 'xsd$ustring$u10' | ~cCordylidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d322,c56])).
% 29.92/29.20  cnf(d324, plain, ~cCordylidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c104,d323])).
% 29.92/29.20  cnf(d325, plain, ~cCordylidae(sK143) | ~cReptile(sK143) | cAmphisbaenidae(sK144) | ~'Ts88' | 'Ts89', inference(resolution, [status(thm)], [d324,c207])).
% 29.92/29.20  cnf(d326, plain, cAmphisbaenidae(sK144) | ~cCordylidae(sK143) | ~cReptile(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,d325])).
% 29.92/29.20  cnf(d327, plain, cAmphisbaenidae(sK144) | ~cCordylidae(sK143) | ~'Ts88' | cAmphisbaenidae(sK144) | ~'Ts88', inference(resolution, [status(thm)], [d326,d321])).
% 29.92/29.20  cnf(d328, plain, cAmphisbaenidae(sK144) | ~'Ts88' | cAmphisbaenidae(sK144) | ~'Ts88', inference(resolution, [status(thm)], [d327,d319])).
% 29.92/29.20  cnf(d329, plain, cCordylidae(sK144) | cCordylidae(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,c210])).
% 29.92/29.20  cnf(d330, plain, cCordylidae(sK144) | ~'Ts88' | 'Ts89' | cReptile(sK143), inference(resolution, [status(thm)], [c208,c57])).
% 29.92/29.20  cnf(d331, plain, cCordylidae(sK144) | cReptile(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,d330])).
% 29.92/29.20  cnf(d332, plain, ~cCordylidae(sK143) | ~cReptile(sK143) | cCordylidae(sK144) | ~'Ts88' | 'Ts89', inference(resolution, [status(thm)], [d324,c208])).
% 29.92/29.20  cnf(d333, plain, cCordylidae(sK144) | ~cCordylidae(sK143) | ~cReptile(sK143) | ~'Ts88', inference(resolution, [status(thm)], [d318,d332])).
% 29.92/29.20  cnf(d334, plain, cCordylidae(sK144) | ~cCordylidae(sK143) | ~'Ts88' | cCordylidae(sK144) | ~'Ts88', inference(resolution, [status(thm)], [d333,d331])).
% 29.92/29.20  cnf(d335, plain, cCordylidae(sK144) | ~'Ts88' | cCordylidae(sK144) | ~'Ts88', inference(resolution, [status(thm)], [d334,d329])).
% 29.92/29.20  cnf(d336, plain, 'xsd$ustring$u1' = 'xsd$ustring$u4' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cCordylidae(X0), inference(resolution, [status(thm)], [d16,c36])).
% 29.92/29.20  cnf(d337, plain, ~cAmphisbaenidae(X0) | ~cCordylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c74,d336])).
% 29.92/29.20  cnf(d338, plain, ~'Ts88' | cReptile(sK144), inference(resolution, [status(thm)], [d335,c37])).
% 29.92/29.20  cnf(d339, plain, ~'Ts88' | ~cAmphisbaenidae(sK144) | ~cCordylidae(sK144), inference(resolution, [status(thm)], [d338,d337])).
% 29.92/29.20  cnf(d340, plain, ~cAmphisbaenidae(sK144) | ~'Ts88' | ~'Ts88', inference(resolution, [status(thm)], [d339,d335])).
% 29.92/29.20  cnf(d341, plain, ~'Ts88' | ~'Ts88', inference(resolution, [status(thm)], [d340,d328])).
% 29.92/29.20  cnf(d342, plain, cCordylidae(sK142) | cCordylidae(sK141) | ~'Ts87', inference(resolution, [status(thm)], [d341,c204])).
% 29.92/29.20  cnf(d343, plain, cCordylidae(sK142) | ~'Ts87' | 'Ts88' | cReptile(sK141), inference(resolution, [status(thm)], [c204,c37])).
% 29.92/29.20  cnf(d344, plain, 'xsd$ustring$u4' = 'xsd$ustring$u9' | ~cCordylidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d322,c51])).
% 29.92/29.20  cnf(d345, plain, ~cCordylidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c103,d344])).
% 29.92/29.20  cnf(d346, plain, ~cCordylidae(sK141) | ~cLoxocemidae(sK141) | cCordylidae(sK142) | ~'Ts87' | 'Ts88', inference(resolution, [status(thm)], [d345,d343])).
% 29.92/29.20  cnf(d347, plain, cCordylidae(sK142) | ~cCordylidae(sK141) | ~'Ts87' | 'Ts88' | cCordylidae(sK142) | ~'Ts87' | 'Ts88', inference(resolution, [status(thm)], [d346,c206])).
% 29.92/29.20  cnf(d348, plain, cCordylidae(sK142) | ~cCordylidae(sK141) | ~'Ts87', inference(resolution, [status(thm)], [d341,d347])).
% 29.92/29.20  cnf(d349, plain, cCordylidae(sK142) | ~'Ts87' | cCordylidae(sK142) | ~'Ts87', inference(resolution, [status(thm)], [d348,d342])).
% 29.92/29.20  cnf(d350, plain, 'xsd$ustring$u4' = 'xsd$ustring$u7' | ~cCordylidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d322,c45])).
% 29.92/29.20  cnf(d351, plain, ~cCordylidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c101,d350])).
% 29.92/29.20  cnf(d352, plain, ~'Ts87' | cReptile(sK142), inference(resolution, [status(thm)], [d349,c37])).
% 29.92/29.20  cnf(d353, plain, ~'Ts87' | ~cCordylidae(sK142) | ~cGekkonidae(sK142), inference(resolution, [status(thm)], [d352,d351])).
% 29.92/29.20  cnf(d354, plain, cGekkonidae(sK142) | ~'Ts87' | 'Ts88' | cReptile(sK141), inference(resolution, [status(thm)], [c205,c52])).
% 29.92/29.20  cnf(d355, plain, ~cCordylidae(sK141) | ~cLoxocemidae(sK141) | cGekkonidae(sK142) | ~'Ts87' | 'Ts88', inference(resolution, [status(thm)], [d345,d354])).
% 29.92/29.20  cnf(d356, plain, ~cCordylidae(sK141) | cGekkonidae(sK142) | ~'Ts87' | 'Ts88' | cGekkonidae(sK142) | ~'Ts87' | 'Ts88', inference(resolution, [status(thm)], [d355,c205])).
% 29.92/29.20  cnf(d357, plain, ~cCordylidae(sK141) | cGekkonidae(sK142) | ~'Ts87', inference(resolution, [status(thm)], [d341,d356])).
% 29.92/29.20  cnf(d358, plain, cCordylidae(sK141) | cGekkonidae(sK142) | ~'Ts87', inference(resolution, [status(thm)], [d341,c203])).
% 29.92/29.20  cnf(d359, plain, ~cCordylidae(sK142) | ~'Ts87' | cCordylidae(sK141) | ~'Ts87', inference(resolution, [status(thm)], [d353,d358])).
% 29.92/29.20  cnf(d360, plain, cCordylidae(sK141) | ~'Ts87' | ~'Ts87', inference(resolution, [status(thm)], [d359,d349])).
% 29.92/29.20  cnf(d361, plain, ~'Ts87' | cGekkonidae(sK142) | ~'Ts87', inference(resolution, [status(thm)], [d360,d357])).
% 29.92/29.20  cnf(d362, plain, ~'Ts87' | ~cCordylidae(sK142) | ~'Ts87', inference(resolution, [status(thm)], [d361,d353])).
% 29.92/29.20  cnf(d363, plain, ~'Ts87' | ~'Ts87', inference(resolution, [status(thm)], [d362,d349])).
% 29.92/29.20  cnf(d364, plain, ~cAgamidae(sK139) | cCordylidae(sK140) | ~'Ts86', inference(resolution, [status(thm)], [d363,d8])).
% 29.92/29.20  cnf(d365, plain, cCordylidae(sK138) | ~'Ts85' | 'Ts86' | cReptile(sK137), inference(resolution, [status(thm)], [c197,c43])).
% 29.92/29.20  cnf(d366, plain, 'xsd$ustring$u0' = 'xsd$ustring$u6' | ~cAgamidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d4,c42])).
% 29.92/29.20  cnf(d367, plain, ~cAgamidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c66,d366])).
% 29.92/29.20  cnf(d368, plain, ~cAgamidae(sK137) | ~cEmydidae(sK137) | cCordylidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d367,d365])).
% 29.92/29.20  cnf(d369, plain, ~cAgamidae(sK137) | cCordylidae(sK138) | ~'Ts85' | 'Ts86' | cCordylidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d368,c197])).
% 29.92/29.20  cnf(d370, plain, cAgamidae(sK137) | ~'Ts85' | 'Ts86' | cReptile(sK138), inference(resolution, [status(thm)], [c195,c37])).
% 29.92/29.20  cnf(d371, plain, 'xsd$ustring$u4' = 'xsd$ustring$u6' | ~cCordylidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d322,c42])).
% 29.92/29.20  cnf(d372, plain, ~cCordylidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c100,d371])).
% 29.92/29.20  cnf(d373, plain, ~cCordylidae(sK138) | ~cEmydidae(sK138) | cAgamidae(sK137) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d372,d370])).
% 29.92/29.20  cnf(d374, plain, cAgamidae(sK137) | ~cCordylidae(sK138) | ~'Ts85' | 'Ts86' | cAgamidae(sK137) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d373,c196])).
% 29.92/29.20  cnf(d375, plain, cAgamidae(sK137) | ~'Ts85' | 'Ts86' | cAgamidae(sK137) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d374,c195])).
% 29.92/29.20  cnf(d376, plain, ~'Ts85' | 'Ts86' | cCordylidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d375,d369])).
% 29.92/29.20  cnf(d377, plain, cEmydidae(sK138) | ~'Ts85' | 'Ts86' | cReptile(sK137), inference(resolution, [status(thm)], [c198,c43])).
% 29.92/29.20  cnf(d378, plain, ~cAgamidae(sK137) | ~cEmydidae(sK137) | cEmydidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d367,d377])).
% 29.92/29.20  cnf(d379, plain, ~cAgamidae(sK137) | cEmydidae(sK138) | ~'Ts85' | 'Ts86' | cEmydidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d378,c198])).
% 29.92/29.20  cnf(d380, plain, ~'Ts85' | 'Ts86' | cEmydidae(sK138) | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d375,d379])).
% 29.92/29.20  cnf(d381, plain, ~'Ts85' | 'Ts86' | cReptile(sK138), inference(resolution, [status(thm)], [d376,c37])).
% 29.92/29.20  cnf(d382, plain, ~'Ts85' | 'Ts86' | ~cCordylidae(sK138) | ~cEmydidae(sK138), inference(resolution, [status(thm)], [d381,d372])).
% 29.92/29.20  cnf(d383, plain, ~cCordylidae(sK138) | ~'Ts85' | 'Ts86' | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d382,d380])).
% 29.92/29.20  cnf(d384, plain, ~'Ts85' | 'Ts86' | ~'Ts85' | 'Ts86', inference(resolution, [status(thm)], [d383,d376])).
% 29.92/29.20  cnf(d385, plain, cAgamidae(sK135) | ~'Ts84' | 'Ts85' | cReptile(sK136), inference(resolution, [status(thm)], [c191,c60])).
% 29.92/29.20  cnf(d386, plain, 'xsd$ustring$u7' = 'xsd$ustring$u11' | ~cGekkonidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d126,c59])).
% 29.92/29.20  cnf(d387, plain, ~cGekkonidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c120,d386])).
% 29.92/29.20  cnf(d388, plain, ~cGekkonidae(sK136) | ~cReptile(sK136) | cAgamidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d387,c191])).
% 29.92/29.20  cnf(d389, plain, cAgamidae(sK135) | ~cGekkonidae(sK136) | ~'Ts84' | 'Ts85' | cAgamidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d388,d385])).
% 29.92/29.20  cnf(d390, plain, cAgamidae(sK135) | ~'Ts84' | 'Ts85' | cAgamidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d389,c192])).
% 29.92/29.20  cnf(d391, plain, 'xsd$ustring$u0' = 'xsd$ustring$u9' | ~cAgamidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d4,c51])).
% 29.92/29.20  cnf(d392, plain, ~cAgamidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c69,d391])).
% 29.92/29.20  cnf(d393, plain, ~'Ts84' | 'Ts85' | cReptile(sK135), inference(resolution, [status(thm)], [d390,c25])).
% 29.92/29.20  cnf(d394, plain, ~'Ts84' | 'Ts85' | ~cAgamidae(sK135) | ~cLoxocemidae(sK135), inference(resolution, [status(thm)], [d393,d392])).
% 29.92/29.20  cnf(d395, plain, cLoxocemidae(sK135) | ~'Ts84' | 'Ts85' | cReptile(sK136), inference(resolution, [status(thm)], [c193,c60])).
% 29.92/29.20  cnf(d396, plain, ~cGekkonidae(sK136) | ~cReptile(sK136) | cLoxocemidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d387,c193])).
% 29.92/29.20  cnf(d397, plain, ~cGekkonidae(sK136) | cLoxocemidae(sK135) | ~'Ts84' | 'Ts85' | cLoxocemidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d396,d395])).
% 29.92/29.20  cnf(d398, plain, ~cAgamidae(sK135) | ~'Ts84' | 'Ts85' | cGekkonidae(sK136) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d394,c194])).
% 29.92/29.20  cnf(d399, plain, cGekkonidae(sK136) | ~'Ts84' | 'Ts85' | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d398,d390])).
% 29.92/29.20  cnf(d400, plain, ~'Ts84' | 'Ts85' | cLoxocemidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d399,d397])).
% 29.92/29.20  cnf(d401, plain, ~'Ts84' | 'Ts85' | ~cAgamidae(sK135) | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d400,d394])).
% 29.92/29.20  cnf(d402, plain, ~'Ts84' | 'Ts85' | ~'Ts84' | 'Ts85', inference(resolution, [status(thm)], [d401,d390])).
% 29.92/29.20  cnf(d403, plain, cReptile(sK131) | cLeptotyphlopidae(sK132) | ~'Ts82' | 'Ts83', inference(resolution, [status(thm)], [c57,c185])).
% 29.92/29.20  cnf(d404, plain, cCordylidae(sK130) | ~'Ts81' | 'Ts82' | cReptile(sK129), inference(resolution, [status(thm)], [c182,c43])).
% 29.92/29.20  cnf(d405, plain, 'xsd$ustring$u6' = 'xsd$ustring$u10' | ~cEmydidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d37,c56])).
% 29.92/29.20  cnf(d406, plain, ~cEmydidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c115,d405])).
% 29.92/29.20  cnf(d407, plain, ~cEmydidae(sK129) | ~cReptile(sK129) | cCordylidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d406,c180])).
% 29.92/29.20  cnf(d408, plain, cCordylidae(sK130) | ~cEmydidae(sK129) | ~'Ts81' | 'Ts82' | cCordylidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d407,d404])).
% 29.92/29.20  cnf(d409, plain, cCordylidae(sK130) | ~'Ts81' | 'Ts82' | cCordylidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d408,c182])).
% 29.92/29.20  cnf(d410, plain, 'xsd$ustring$u4' = 'xsd$ustring$u8' | ~cCordylidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d322,c48])).
% 29.92/29.20  cnf(d411, plain, ~cCordylidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c102,d410])).
% 29.92/29.20  cnf(d412, plain, ~'Ts81' | 'Ts82' | cReptile(sK130), inference(resolution, [status(thm)], [d409,c37])).
% 29.92/29.20  cnf(d413, plain, ~'Ts81' | 'Ts82' | ~cCordylidae(sK130) | ~cLeptotyphlopidae(sK130), inference(resolution, [status(thm)], [d412,d411])).
% 29.92/29.20  cnf(d414, plain, cReptile(sK129) | cLeptotyphlopidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [c57,c179])).
% 29.92/29.20  cnf(d415, plain, ~cEmydidae(sK129) | ~cReptile(sK129) | cLeptotyphlopidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d406,c179])).
% 29.92/29.20  cnf(d416, plain, ~cEmydidae(sK129) | cLeptotyphlopidae(sK130) | ~'Ts81' | 'Ts82' | cLeptotyphlopidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d415,d414])).
% 29.92/29.20  cnf(d417, plain, ~cCordylidae(sK130) | ~'Ts81' | 'Ts82' | cEmydidae(sK129) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d413,c181])).
% 29.92/29.20  cnf(d418, plain, cEmydidae(sK129) | ~'Ts81' | 'Ts82' | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d417,d409])).
% 29.92/29.20  cnf(d419, plain, ~'Ts81' | 'Ts82' | cLeptotyphlopidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d418,d416])).
% 29.92/29.20  cnf(d420, plain, ~'Ts81' | 'Ts82' | ~cCordylidae(sK130) | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d419,d413])).
% 29.92/29.20  cnf(d421, plain, ~'Ts81' | 'Ts82' | ~'Ts81' | 'Ts82', inference(resolution, [status(thm)], [d420,d409])).
% 29.92/29.20  cnf(d422, plain, cReptile(sK124) | cAgamidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [c40,c170])).
% 29.92/29.20  cnf(d423, plain, 'xsd$ustring$u5' = 'xsd$ustring$u10' | ~cCrocodylidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d10,c56])).
% 29.92/29.20  cnf(d424, plain, ~cCrocodylidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c110,d423])).
% 29.92/29.20  cnf(d425, plain, ~cCrocodylidae(sK124) | ~cReptile(sK124) | cAgamidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d424,c169])).
% 29.92/29.20  cnf(d426, plain, cAgamidae(sK123) | ~cCrocodylidae(sK124) | ~'Ts78' | 'Ts79' | cAgamidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d425,d422])).
% 29.92/29.20  cnf(d427, plain, cAgamidae(sK123) | ~'Ts78' | 'Ts79' | cAgamidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d426,c170])).
% 29.92/29.20  cnf(d428, plain, cReptile(sK124) | cAnomalepidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [c40,c168])).
% 29.92/29.20  cnf(d429, plain, ~cCrocodylidae(sK124) | ~cReptile(sK124) | cAnomalepidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d424,c167])).
% 29.92/29.20  cnf(d430, plain, cAnomalepidae(sK123) | ~cCrocodylidae(sK124) | ~'Ts78' | 'Ts79' | cAnomalepidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d429,d428])).
% 29.92/29.20  cnf(d431, plain, cAnomalepidae(sK123) | ~'Ts78' | 'Ts79' | cAnomalepidae(sK123) | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d430,c168])).
% 29.92/29.20  cnf(d432, plain, 'xsd$ustring$u0' = 'xsd$ustring$u2' | ~cAgamidae(X0) | ~cReptile(X0) | ~cAnomalepidae(X0), inference(resolution, [status(thm)], [d4,c30])).
% 29.92/29.20  cnf(d433, plain, ~cAgamidae(X0) | ~cAnomalepidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c62,d432])).
% 29.92/29.20  cnf(d434, plain, ~'Ts78' | 'Ts79' | cReptile(sK123), inference(resolution, [status(thm)], [d427,c25])).
% 29.92/29.20  cnf(d435, plain, ~'Ts78' | 'Ts79' | ~cAgamidae(sK123) | ~cAnomalepidae(sK123), inference(resolution, [status(thm)], [d434,d433])).
% 29.92/29.20  cnf(d436, plain, ~cAgamidae(sK123) | ~'Ts78' | 'Ts79' | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d435,d431])).
% 29.92/29.20  cnf(d437, plain, ~'Ts78' | 'Ts79' | ~'Ts78' | 'Ts79', inference(resolution, [status(thm)], [d436,d427])).
% 29.92/29.20  cnf(d438, plain, cReptile(sK122) | cAmphisbaenidae(sK121) | ~'Ts77' | 'Ts78', inference(resolution, [status(thm)], [c43,c166])).
% 29.92/29.20  cnf(d439, plain, 'xsd$ustring$u6' = 'xsd$ustring$u7' | ~cEmydidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d37,c45])).
% 29.92/29.20  cnf(d440, plain, ~cEmydidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c112,d439])).
% 29.92/29.20  cnf(d441, plain, ~cEmydidae(sK122) | ~cGekkonidae(sK122) | cAmphisbaenidae(sK121) | ~'Ts77' | 'Ts78', inference(resolution, [status(thm)], [d440,d438])).
% 29.92/29.20  cnf(d442, plain, cAmphisbaenidae(sK121) | ~cEmydidae(sK122) | ~'Ts77' | 'Ts78' | cAmphisbaenidae(sK121) | ~'Ts77' | 'Ts78', inference(resolution, [status(thm)], [d441,c165])).
% 29.92/29.20  cnf(d443, plain, cAmphisbaenidae(sK121) | ~'Ts77' | 'Ts78' | cAmphisbaenidae(sK121) | ~'Ts77' | 'Ts78', inference(resolution, [status(thm)], [d442,c166])).
% 29.92/29.20  cnf(d444, plain, cReptile(sK119) | cEmydidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [c52,c162])).
% 29.92/29.20  cnf(d445, plain, 'xsd$ustring$u9' = 'xsd$ustring$u10' | ~cLoxocemidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d30,c56])).
% 29.92/29.20  cnf(d446, plain, ~cLoxocemidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c124,d445])).
% 29.92/29.20  cnf(d447, plain, ~cLoxocemidae(sK119) | ~cReptile(sK119) | cEmydidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d446,c160])).
% 29.92/29.20  cnf(d448, plain, cEmydidae(sK120) | ~cLoxocemidae(sK119) | ~'Ts76' | 'Ts77' | cEmydidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d447,d444])).
% 29.92/29.20  cnf(d449, plain, cEmydidae(sK120) | ~'Ts76' | 'Ts77' | cEmydidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d448,c162])).
% 29.92/29.20  cnf(d450, plain, cReptile(sK119) | cLeptotyphlopidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [c52,c161])).
% 29.92/29.20  cnf(d451, plain, ~cLoxocemidae(sK119) | ~cReptile(sK119) | cLeptotyphlopidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d446,c159])).
% 29.92/29.20  cnf(d452, plain, cLeptotyphlopidae(sK120) | ~cLoxocemidae(sK119) | ~'Ts76' | 'Ts77' | cLeptotyphlopidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d451,d450])).
% 29.92/29.20  cnf(d453, plain, cLeptotyphlopidae(sK120) | ~'Ts76' | 'Ts77' | cLeptotyphlopidae(sK120) | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d452,c161])).
% 29.92/29.20  cnf(d454, plain, 'xsd$ustring$u6' = 'xsd$ustring$u8' | ~cEmydidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d37,c48])).
% 29.92/29.20  cnf(d455, plain, ~cEmydidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c113,d454])).
% 29.92/29.20  cnf(d456, plain, ~'Ts76' | 'Ts77' | cReptile(sK120), inference(resolution, [status(thm)], [d449,c43])).
% 29.92/29.20  cnf(d457, plain, ~'Ts76' | 'Ts77' | ~cEmydidae(sK120) | ~cLeptotyphlopidae(sK120), inference(resolution, [status(thm)], [d456,d455])).
% 29.92/29.20  cnf(d458, plain, ~cEmydidae(sK120) | ~'Ts76' | 'Ts77' | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d457,d453])).
% 29.92/29.20  cnf(d459, plain, ~'Ts76' | 'Ts77' | ~'Ts76' | 'Ts77', inference(resolution, [status(thm)], [d458,d449])).
% 29.92/29.20  cnf(d460, plain, cReptile(sK114) | cCordylidae(sK113) | ~'Ts73' | 'Ts74', inference(resolution, [status(thm)], [c60,c147])).
% 29.92/29.20  cnf(d461, plain, cReptile(sK105) | cAgamidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [c49,c132])).
% 29.92/29.20  cnf(d462, plain, 'xsd$ustring$u8' = X0 | ~cReptile(X1) | ~'rfamily$uname'(X1,X0) | ~cLeptotyphlopidae(X1), inference(resolution, [status(thm)], [c54,c48])).
% 29.92/29.20  cnf(d463, plain, 'xsd$ustring$u8' = 'xsd$ustring$u10' | ~cLeptotyphlopidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d462,c56])).
% 29.92/29.20  cnf(d464, plain, ~cLeptotyphlopidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c122,d463])).
% 29.92/29.20  cnf(d465, plain, ~cLeptotyphlopidae(sK105) | ~cReptile(sK105) | cAgamidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d464,c134])).
% 29.92/29.20  cnf(d466, plain, cAgamidae(sK106) | ~cLeptotyphlopidae(sK105) | 'Ts70' | cAgamidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d465,d461])).
% 29.92/29.20  cnf(d467, plain, cAgamidae(sK106) | 'Ts70' | cAgamidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d466,c132])).
% 29.92/29.20  cnf(d468, plain, cReptile(sK105) | cAmphisbaenidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [c49,c131])).
% 29.92/29.20  cnf(d469, plain, ~cLeptotyphlopidae(sK105) | ~cReptile(sK105) | cAmphisbaenidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d464,c133])).
% 29.92/29.20  cnf(d470, plain, cAmphisbaenidae(sK106) | ~cLeptotyphlopidae(sK105) | 'Ts70' | cAmphisbaenidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d469,d468])).
% 29.92/29.20  cnf(d471, plain, cAmphisbaenidae(sK106) | 'Ts70' | cAmphisbaenidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d470,c131])).
% 29.92/29.20  cnf(d472, plain, 'Ts70' | cReptile(sK106), inference(resolution, [status(thm)], [d467,c25])).
% 29.92/29.20  cnf(d473, plain, 'xsd$ustring$u0' = 'xsd$ustring$u1' | ~cAgamidae(X0) | ~cReptile(X0) | ~cAmphisbaenidae(X0), inference(resolution, [status(thm)], [d4,c27])).
% 29.92/29.20  cnf(d474, plain, ~cAgamidae(X0) | ~cAmphisbaenidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c61,d473])).
% 29.92/29.20  cnf(d475, plain, ~cAgamidae(sK106) | ~cAmphisbaenidae(sK106) | 'Ts70', inference(resolution, [status(thm)], [d474,d472])).
% 29.92/29.20  cnf(d476, plain, ~cAgamidae(sK106) | 'Ts70' | 'Ts70', inference(resolution, [status(thm)], [d475,d471])).
% 29.92/29.20  cnf(d477, plain, 'Ts70' | 'Ts70', inference(resolution, [status(thm)], [d476,d467])).
% 29.92/29.20  cnf(d478, plain, cEmydidae(sK108) | cLeptotyphlopidae(sK107) | 'Ts71', inference(resolution, [status(thm)], [d477,c135])).
% 29.92/29.20  cnf(d479, plain, cEmydidae(sK108) | cLoxocemidae(sK107) | 'Ts71', inference(resolution, [status(thm)], [d477,c137])).
% 29.92/29.20  cnf(d480, plain, 'xsd$ustring$u8' = 'xsd$ustring$u9' | ~cLeptotyphlopidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d462,c51])).
% 29.92/29.20  cnf(d481, plain, ~cLeptotyphlopidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c121,d480])).
% 29.92/29.20  cnf(d482, plain, cReptile(sK107) | cEmydidae(sK108) | ~'Ts70' | 'Ts71', inference(resolution, [status(thm)], [c49,c135])).
% 29.92/29.20  cnf(d483, plain, cEmydidae(sK108) | cReptile(sK107) | 'Ts71', inference(resolution, [status(thm)], [d477,d482])).
% 29.92/29.20  cnf(d484, plain, cEmydidae(sK108) | 'Ts71' | ~cLeptotyphlopidae(sK107) | ~cLoxocemidae(sK107), inference(resolution, [status(thm)], [d483,d481])).
% 29.92/29.20  cnf(d485, plain, cEmydidae(sK108) | ~cLeptotyphlopidae(sK107) | 'Ts71' | cEmydidae(sK108) | 'Ts71', inference(resolution, [status(thm)], [d484,d479])).
% 29.92/29.20  cnf(d486, plain, cEmydidae(sK108) | 'Ts71' | cEmydidae(sK108) | 'Ts71', inference(resolution, [status(thm)], [d485,d478])).
% 29.92/29.20  cnf(d487, plain, 'xsd$ustring$u6' = 'xsd$ustring$u9' | ~cEmydidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d37,c51])).
% 29.92/29.20  cnf(d488, plain, ~cEmydidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c114,d487])).
% 29.92/29.20  cnf(d489, plain, 'Ts71' | cReptile(sK108), inference(resolution, [status(thm)], [d486,c43])).
% 29.92/29.20  cnf(d490, plain, 'Ts71' | ~cEmydidae(sK108) | ~cLoxocemidae(sK108), inference(resolution, [status(thm)], [d489,d488])).
% 29.92/29.20  cnf(d491, plain, cLeptotyphlopidae(sK107) | cLoxocemidae(sK108) | 'Ts71', inference(resolution, [status(thm)], [d477,c136])).
% 29.92/29.20  cnf(d492, plain, ~cEmydidae(sK108) | 'Ts71' | cLeptotyphlopidae(sK107) | 'Ts71', inference(resolution, [status(thm)], [d490,d491])).
% 29.92/29.20  cnf(d493, plain, cLeptotyphlopidae(sK107) | 'Ts71' | 'Ts71', inference(resolution, [status(thm)], [d492,d486])).
% 29.92/29.20  cnf(d494, plain, cLoxocemidae(sK108) | cLoxocemidae(sK107) | 'Ts71', inference(resolution, [status(thm)], [d477,c138])).
% 29.92/29.20  cnf(d495, plain, 'Ts71' | cReptile(sK107), inference(resolution, [status(thm)], [d493,c49])).
% 29.92/29.20  cnf(d496, plain, 'Ts71' | ~cLeptotyphlopidae(sK107) | ~cLoxocemidae(sK107), inference(resolution, [status(thm)], [d495,d481])).
% 29.92/29.20  cnf(d497, plain, ~cLeptotyphlopidae(sK107) | 'Ts71' | cLoxocemidae(sK108) | 'Ts71', inference(resolution, [status(thm)], [d496,d494])).
% 29.92/29.20  cnf(d498, plain, cLoxocemidae(sK108) | 'Ts71' | 'Ts71', inference(resolution, [status(thm)], [d497,d493])).
% 29.92/29.20  cnf(d499, plain, 'Ts71' | ~cEmydidae(sK108) | 'Ts71', inference(resolution, [status(thm)], [d498,d490])).
% 29.92/29.20  cnf(d500, plain, 'Ts71' | 'Ts71', inference(resolution, [status(thm)], [d499,d486])).
% 29.92/29.20  cnf(d501, plain, cAgamidae(sK109) | cAgamidae(sK110) | 'Ts72', inference(resolution, [status(thm)], [d500,c141])).
% 29.92/29.20  cnf(d502, plain, cAgamidae(sK109) | cCordylidae(sK110) | 'Ts72', inference(resolution, [status(thm)], [d500,c142])).
% 29.92/29.20  cnf(d503, plain, 'xsd$ustring$u0' = 'xsd$ustring$u4' | ~cAgamidae(X0) | ~cReptile(X0) | ~cCordylidae(X0), inference(resolution, [status(thm)], [d4,c36])).
% 29.92/29.20  cnf(d504, plain, ~cAgamidae(X0) | ~cCordylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c64,d503])).
% 29.92/29.20  cnf(d505, plain, cReptile(sK110) | cAgamidae(sK109) | ~'Ts71' | 'Ts72', inference(resolution, [status(thm)], [c25,c141])).
% 29.92/29.20  cnf(d506, plain, cAgamidae(sK109) | cReptile(sK110) | 'Ts72', inference(resolution, [status(thm)], [d500,d505])).
% 29.92/29.20  cnf(d507, plain, cAgamidae(sK109) | 'Ts72' | ~cAgamidae(sK110) | ~cCordylidae(sK110), inference(resolution, [status(thm)], [d506,d504])).
% 29.92/29.20  cnf(d508, plain, cAgamidae(sK109) | ~cAgamidae(sK110) | 'Ts72' | cAgamidae(sK109) | 'Ts72', inference(resolution, [status(thm)], [d507,d502])).
% 29.92/29.20  cnf(d509, plain, cAgamidae(sK109) | 'Ts72' | cAgamidae(sK109) | 'Ts72', inference(resolution, [status(thm)], [d508,d501])).
% 29.92/29.20  cnf(d510, plain, cAgamidae(sK110) | cGekkonidae(sK109) | 'Ts72', inference(resolution, [status(thm)], [d500,c139])).
% 29.92/29.20  cnf(d511, plain, 'xsd$ustring$u0' = 'xsd$ustring$u7' | ~cAgamidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d4,c45])).
% 29.92/29.20  cnf(d512, plain, ~cAgamidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c67,d511])).
% 29.92/29.20  cnf(d513, plain, 'Ts72' | cReptile(sK109), inference(resolution, [status(thm)], [d509,c25])).
% 29.92/29.20  cnf(d514, plain, 'Ts72' | ~cAgamidae(sK109) | ~cGekkonidae(sK109), inference(resolution, [status(thm)], [d513,d512])).
% 29.92/29.20  cnf(d515, plain, ~cAgamidae(sK109) | 'Ts72' | cAgamidae(sK110) | 'Ts72', inference(resolution, [status(thm)], [d514,d510])).
% 29.92/29.20  cnf(d516, plain, cAgamidae(sK110) | 'Ts72' | 'Ts72', inference(resolution, [status(thm)], [d515,d509])).
% 29.92/29.20  cnf(d517, plain, cCordylidae(sK110) | cGekkonidae(sK109) | 'Ts72', inference(resolution, [status(thm)], [d500,c140])).
% 29.92/29.20  cnf(d518, plain, ~cAgamidae(sK109) | 'Ts72' | cCordylidae(sK110) | 'Ts72', inference(resolution, [status(thm)], [d514,d517])).
% 29.92/29.20  cnf(d519, plain, cCordylidae(sK110) | 'Ts72' | 'Ts72', inference(resolution, [status(thm)], [d518,d509])).
% 29.92/29.20  cnf(d520, plain, 'Ts72' | cReptile(sK110), inference(resolution, [status(thm)], [d519,c37])).
% 29.92/29.20  cnf(d521, plain, 'Ts72' | ~cAgamidae(sK110) | ~cCordylidae(sK110), inference(resolution, [status(thm)], [d520,d504])).
% 29.92/29.20  cnf(d522, plain, ~cAgamidae(sK110) | 'Ts72' | 'Ts72', inference(resolution, [status(thm)], [d521,d519])).
% 29.92/29.20  cnf(d523, plain, 'Ts72' | 'Ts72', inference(resolution, [status(thm)], [d522,d516])).
% 29.92/29.20  cnf(d524, plain, cAnomalepidae(sK111) | cLeptotyphlopidae(sK112) | 'Ts73', inference(resolution, [status(thm)], [d523,c143])).
% 29.92/29.20  cnf(d525, plain, cReptile(sK112) | cAnomalepidae(sK111) | ~'Ts72' | 'Ts73', inference(resolution, [status(thm)], [c49,c143])).
% 29.92/29.20  cnf(d526, plain, cAnomalepidae(sK111) | cReptile(sK112) | 'Ts73', inference(resolution, [status(thm)], [d523,d525])).
% 29.92/29.20  cnf(d527, plain, 'xsd$ustring$u8' = 'xsd$ustring$u11' | ~cLeptotyphlopidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d462,c59])).
% 29.92/29.20  cnf(d528, plain, ~cLeptotyphlopidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c123,d527])).
% 29.92/29.20  cnf(d529, plain, cAnomalepidae(sK111) | cXantusiidae(sK112) | 'Ts73', inference(resolution, [status(thm)], [d523,c144])).
% 29.92/29.20  cnf(d530, plain, cAnomalepidae(sK111) | 'Ts73' | ~cLeptotyphlopidae(sK112) | ~cReptile(sK112), inference(resolution, [status(thm)], [d529,d528])).
% 29.92/29.20  cnf(d531, plain, cAnomalepidae(sK111) | ~cLeptotyphlopidae(sK112) | 'Ts73' | cAnomalepidae(sK111) | 'Ts73', inference(resolution, [status(thm)], [d530,d526])).
% 29.92/29.20  cnf(d532, plain, cAnomalepidae(sK111) | 'Ts73' | cAnomalepidae(sK111) | 'Ts73', inference(resolution, [status(thm)], [d531,d524])).
% 29.92/29.20  cnf(d533, plain, 'Ts73' | cReptile(sK111), inference(resolution, [status(thm)], [d532,c31])).
% 29.92/29.20  cnf(d534, plain, 'xsd$ustring$u2' = 'xsd$ustring$u10' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [d0,c56])).
% 29.92/29.20  cnf(d535, plain, ~cAnomalepidae(X0) | ~cReptile(X0) | ~cSphenodontidae(X0), inference(resolution, [status(thm)], [c89,d534])).
% 29.92/29.20  cnf(d536, plain, cLeptotyphlopidae(sK112) | cSphenodontidae(sK111) | 'Ts73', inference(resolution, [status(thm)], [d523,c145])).
% 29.92/29.20  cnf(d537, plain, cLeptotyphlopidae(sK112) | 'Ts73' | ~cAnomalepidae(sK111) | ~cReptile(sK111), inference(resolution, [status(thm)], [d536,d535])).
% 29.92/29.20  cnf(d538, plain, ~cAnomalepidae(sK111) | cLeptotyphlopidae(sK112) | 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d537,d533])).
% 29.92/29.20  cnf(d539, plain, cLeptotyphlopidae(sK112) | 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d538,d532])).
% 29.92/29.20  cnf(d540, plain, 'Ts73' | cReptile(sK112), inference(resolution, [status(thm)], [d539,c49])).
% 29.92/29.20  cnf(d541, plain, cSphenodontidae(sK111) | cXantusiidae(sK112) | 'Ts73', inference(resolution, [status(thm)], [d523,c146])).
% 29.92/29.20  cnf(d542, plain, cSphenodontidae(sK111) | 'Ts73' | ~cLeptotyphlopidae(sK112) | ~cReptile(sK112), inference(resolution, [status(thm)], [d541,d528])).
% 29.92/29.20  cnf(d543, plain, ~cLeptotyphlopidae(sK112) | cSphenodontidae(sK111) | 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d542,d540])).
% 29.92/29.20  cnf(d544, plain, cSphenodontidae(sK111) | 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d543,d539])).
% 29.92/29.20  cnf(d545, plain, 'Ts73' | ~cAnomalepidae(sK111) | ~cReptile(sK111), inference(resolution, [status(thm)], [d544,d535])).
% 29.92/29.20  cnf(d546, plain, ~cAnomalepidae(sK111) | 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d545,d533])).
% 29.92/29.20  cnf(d547, plain, 'Ts73' | 'Ts73', inference(resolution, [status(thm)], [d546,d532])).
% 29.92/29.20  cnf(d548, plain, cCordylidae(sK113) | cReptile(sK114) | 'Ts74', inference(resolution, [status(thm)], [d547,d460])).
% 29.92/29.20  cnf(d549, plain, 'xsd$ustring$u2' = 'xsd$ustring$u11' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d0,c59])).
% 29.92/29.20  cnf(d550, plain, ~cAnomalepidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c90,d549])).
% 29.92/29.20  cnf(d551, plain, cCordylidae(sK113) | cXantusiidae(sK114) | 'Ts74', inference(resolution, [status(thm)], [d547,c147])).
% 29.92/29.20  cnf(d552, plain, cCordylidae(sK113) | 'Ts74' | ~cAnomalepidae(sK114) | ~cReptile(sK114), inference(resolution, [status(thm)], [d551,d550])).
% 29.92/29.20  cnf(d553, plain, ~cAnomalepidae(sK114) | cCordylidae(sK113) | 'Ts74' | cCordylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d552,d548])).
% 29.92/29.20  cnf(d554, plain, cAnomalepidae(sK114) | cCordylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d547,c148])).
% 29.92/29.20  cnf(d555, plain, cAnomalepidae(sK114) | cCrocodylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d547,c150])).
% 29.92/29.20  cnf(d556, plain, 'xsd$ustring$u4' = 'xsd$ustring$u5' | ~cCordylidae(X0) | ~cReptile(X0) | ~cCrocodylidae(X0), inference(resolution, [status(thm)], [d322,c39])).
% 29.92/29.20  cnf(d557, plain, ~cCordylidae(X0) | ~cCrocodylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c99,d556])).
% 29.92/29.20  cnf(d558, plain, cReptile(sK113) | cAnomalepidae(sK114) | ~'Ts73' | 'Ts74', inference(resolution, [status(thm)], [c37,c148])).
% 29.92/29.20  cnf(d559, plain, cAnomalepidae(sK114) | cReptile(sK113) | 'Ts74', inference(resolution, [status(thm)], [d547,d558])).
% 29.92/29.20  cnf(d560, plain, cAnomalepidae(sK114) | 'Ts74' | ~cCordylidae(sK113) | ~cCrocodylidae(sK113), inference(resolution, [status(thm)], [d559,d557])).
% 29.92/29.20  cnf(d561, plain, cAnomalepidae(sK114) | ~cCordylidae(sK113) | 'Ts74' | cAnomalepidae(sK114) | 'Ts74', inference(resolution, [status(thm)], [d560,d555])).
% 29.92/29.20  cnf(d562, plain, cAnomalepidae(sK114) | 'Ts74' | cAnomalepidae(sK114) | 'Ts74', inference(resolution, [status(thm)], [d561,d554])).
% 29.92/29.20  cnf(d563, plain, 'Ts74' | cCordylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d562,d553])).
% 29.92/29.20  cnf(d564, plain, cReptile(sK114) | cCrocodylidae(sK113) | ~'Ts73' | 'Ts74', inference(resolution, [status(thm)], [c60,c149])).
% 29.92/29.20  cnf(d565, plain, cCrocodylidae(sK113) | cReptile(sK114) | 'Ts74', inference(resolution, [status(thm)], [d547,d564])).
% 29.92/29.20  cnf(d566, plain, cCrocodylidae(sK113) | cXantusiidae(sK114) | 'Ts74', inference(resolution, [status(thm)], [d547,c149])).
% 29.92/29.20  cnf(d567, plain, cCrocodylidae(sK113) | 'Ts74' | ~cAnomalepidae(sK114) | ~cReptile(sK114), inference(resolution, [status(thm)], [d566,d550])).
% 29.92/29.20  cnf(d568, plain, ~cAnomalepidae(sK114) | cCrocodylidae(sK113) | 'Ts74' | cCrocodylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d567,d565])).
% 29.92/29.20  cnf(d569, plain, 'Ts74' | cCrocodylidae(sK113) | 'Ts74', inference(resolution, [status(thm)], [d562,d568])).
% 29.92/29.20  cnf(d570, plain, 'Ts74' | cReptile(sK113), inference(resolution, [status(thm)], [d563,c37])).
% 29.92/29.20  cnf(d571, plain, 'Ts74' | ~cCordylidae(sK113) | ~cCrocodylidae(sK113), inference(resolution, [status(thm)], [d570,d557])).
% 29.92/29.20  cnf(d572, plain, ~cCordylidae(sK113) | 'Ts74' | 'Ts74', inference(resolution, [status(thm)], [d571,d569])).
% 29.92/29.20  cnf(d573, plain, 'Ts74' | 'Ts74', inference(resolution, [status(thm)], [d572,d563])).
% 29.92/29.20  cnf(d574, plain, cAnomalepidae(sK116) | cAnomalepidae(sK115) | 'Ts75', inference(resolution, [status(thm)], [d573,c152])).
% 29.92/29.20  cnf(d575, plain, cAnomalepidae(sK116) | cLoxocemidae(sK115) | 'Ts75', inference(resolution, [status(thm)], [d573,c154])).
% 29.92/29.20  cnf(d576, plain, 'xsd$ustring$u2' = 'xsd$ustring$u9' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d0,c51])).
% 29.92/29.20  cnf(d577, plain, ~cAnomalepidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c88,d576])).
% 29.92/29.20  cnf(d578, plain, cReptile(sK115) | cAnomalepidae(sK116) | ~'Ts74' | 'Ts75', inference(resolution, [status(thm)], [c31,c152])).
% 29.92/29.20  cnf(d579, plain, cAnomalepidae(sK116) | cReptile(sK115) | 'Ts75', inference(resolution, [status(thm)], [d573,d578])).
% 29.92/29.20  cnf(d580, plain, cAnomalepidae(sK116) | 'Ts75' | ~cAnomalepidae(sK115) | ~cLoxocemidae(sK115), inference(resolution, [status(thm)], [d579,d577])).
% 29.92/29.20  cnf(d581, plain, cAnomalepidae(sK116) | ~cAnomalepidae(sK115) | 'Ts75' | cAnomalepidae(sK116) | 'Ts75', inference(resolution, [status(thm)], [d580,d575])).
% 29.92/29.20  cnf(d582, plain, cAnomalepidae(sK116) | 'Ts75' | cAnomalepidae(sK116) | 'Ts75', inference(resolution, [status(thm)], [d581,d574])).
% 29.92/29.20  cnf(d583, plain, 'xsd$ustring$u2' = 'xsd$ustring$u8' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d0,c48])).
% 29.92/29.20  cnf(d584, plain, ~cAnomalepidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c87,d583])).
% 29.92/29.20  cnf(d585, plain, 'Ts75' | cReptile(sK116), inference(resolution, [status(thm)], [d582,c31])).
% 29.92/29.20  cnf(d586, plain, 'Ts75' | ~cAnomalepidae(sK116) | ~cLeptotyphlopidae(sK116), inference(resolution, [status(thm)], [d585,d584])).
% 29.92/29.20  cnf(d587, plain, cAnomalepidae(sK115) | cLeptotyphlopidae(sK116) | 'Ts75', inference(resolution, [status(thm)], [d573,c151])).
% 29.92/29.20  cnf(d588, plain, ~cAnomalepidae(sK116) | 'Ts75' | cAnomalepidae(sK115) | 'Ts75', inference(resolution, [status(thm)], [d586,d587])).
% 29.92/29.20  cnf(d589, plain, cAnomalepidae(sK115) | 'Ts75' | 'Ts75', inference(resolution, [status(thm)], [d588,d582])).
% 29.92/29.20  cnf(d590, plain, cLeptotyphlopidae(sK116) | cLoxocemidae(sK115) | 'Ts75', inference(resolution, [status(thm)], [d573,c153])).
% 29.92/29.20  cnf(d591, plain, 'Ts75' | cReptile(sK115), inference(resolution, [status(thm)], [d589,c31])).
% 29.92/29.20  cnf(d592, plain, 'Ts75' | ~cAnomalepidae(sK115) | ~cLoxocemidae(sK115), inference(resolution, [status(thm)], [d591,d577])).
% 29.92/29.20  cnf(d593, plain, ~cAnomalepidae(sK115) | 'Ts75' | cLeptotyphlopidae(sK116) | 'Ts75', inference(resolution, [status(thm)], [d592,d590])).
% 29.92/29.20  cnf(d594, plain, cLeptotyphlopidae(sK116) | 'Ts75' | 'Ts75', inference(resolution, [status(thm)], [d593,d589])).
% 29.92/29.20  cnf(d595, plain, 'Ts75' | ~cAnomalepidae(sK116) | 'Ts75', inference(resolution, [status(thm)], [d594,d586])).
% 29.92/29.20  cnf(d596, plain, 'Ts75' | 'Ts75', inference(resolution, [status(thm)], [d595,d582])).
% 29.92/29.20  cnf(d597, plain, cAnomalepidae(sK117) | cGekkonidae(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,c157])).
% 29.92/29.20  cnf(d598, plain, cAnomalepidae(sK117) | cLoxocemidae(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,c158])).
% 29.92/29.20  cnf(d599, plain, 'xsd$ustring$u7' = 'xsd$ustring$u9' | ~cGekkonidae(X0) | ~cReptile(X0) | ~cLoxocemidae(X0), inference(resolution, [status(thm)], [d126,c51])).
% 29.92/29.20  cnf(d600, plain, ~cGekkonidae(X0) | ~cLoxocemidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c118,d599])).
% 29.92/29.20  cnf(d601, plain, cReptile(sK118) | cAnomalepidae(sK117) | ~'Ts75' | 'Ts76', inference(resolution, [status(thm)], [c46,c157])).
% 29.92/29.20  cnf(d602, plain, cAnomalepidae(sK117) | cReptile(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,d601])).
% 29.92/29.20  cnf(d603, plain, cAnomalepidae(sK117) | 'Ts76' | ~cGekkonidae(sK118) | ~cLoxocemidae(sK118), inference(resolution, [status(thm)], [d602,d600])).
% 29.92/29.20  cnf(d604, plain, cAnomalepidae(sK117) | ~cGekkonidae(sK118) | 'Ts76' | cAnomalepidae(sK117) | 'Ts76', inference(resolution, [status(thm)], [d603,d598])).
% 29.92/29.20  cnf(d605, plain, cAnomalepidae(sK117) | 'Ts76' | cAnomalepidae(sK117) | 'Ts76', inference(resolution, [status(thm)], [d604,d597])).
% 29.92/29.20  cnf(d606, plain, 'xsd$ustring$u1' = 'xsd$ustring$u2' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cAnomalepidae(X0), inference(resolution, [status(thm)], [d16,c30])).
% 29.92/29.20  cnf(d607, plain, ~cAmphisbaenidae(X0) | ~cAnomalepidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c72,d606])).
% 29.92/29.20  cnf(d608, plain, 'Ts76' | cReptile(sK117), inference(resolution, [status(thm)], [d605,c31])).
% 29.92/29.20  cnf(d609, plain, 'Ts76' | ~cAmphisbaenidae(sK117) | ~cAnomalepidae(sK117), inference(resolution, [status(thm)], [d608,d607])).
% 29.92/29.20  cnf(d610, plain, ~cAmphisbaenidae(sK117) | 'Ts76' | 'Ts76', inference(resolution, [status(thm)], [d609,d605])).
% 29.92/29.20  cnf(d611, plain, cAmphisbaenidae(sK117) | cGekkonidae(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,c155])).
% 29.92/29.20  cnf(d612, plain, cAmphisbaenidae(sK117) | cLoxocemidae(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,c156])).
% 29.92/29.20  cnf(d613, plain, cReptile(sK118) | cAmphisbaenidae(sK117) | ~'Ts75' | 'Ts76', inference(resolution, [status(thm)], [c46,c155])).
% 29.92/29.20  cnf(d614, plain, cAmphisbaenidae(sK117) | cReptile(sK118) | 'Ts76', inference(resolution, [status(thm)], [d596,d613])).
% 29.92/29.20  cnf(d615, plain, cAmphisbaenidae(sK117) | 'Ts76' | ~cGekkonidae(sK118) | ~cLoxocemidae(sK118), inference(resolution, [status(thm)], [d614,d600])).
% 29.92/29.20  cnf(d616, plain, cAmphisbaenidae(sK117) | ~cGekkonidae(sK118) | 'Ts76' | cAmphisbaenidae(sK117) | 'Ts76', inference(resolution, [status(thm)], [d615,d612])).
% 29.92/29.20  cnf(d617, plain, cAmphisbaenidae(sK117) | 'Ts76' | cAmphisbaenidae(sK117) | 'Ts76', inference(resolution, [status(thm)], [d616,d611])).
% 29.92/29.20  cnf(d618, plain, 'Ts76' | 'Ts76', inference(resolution, [status(thm)], [d617,d610])).
% 29.92/29.20  cnf(d619, plain, 'Ts77', inference(resolution, [status(thm)], [d618,d459])).
% 29.92/29.20  cnf(d620, plain, cAmphisbaenidae(sK121) | 'Ts78', inference(resolution, [status(thm)], [d619,d443])).
% 29.92/29.20  cnf(d621, plain, ~'Ts77' | 'Ts78' | cReptile(sK121), inference(resolution, [status(thm)], [d443,c28])).
% 29.92/29.20  cnf(d622, plain, cReptile(sK121) | 'Ts78', inference(resolution, [status(thm)], [d619,d621])).
% 29.92/29.20  cnf(d623, plain, 'xsd$ustring$u1' = 'xsd$ustring$u11' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d16,c59])).
% 29.92/29.20  cnf(d624, plain, ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c81,d623])).
% 29.92/29.20  cnf(d625, plain, cGekkonidae(sK122) | cXantusiidae(sK121) | 'Ts78', inference(resolution, [status(thm)], [d619,c163])).
% 29.92/29.20  cnf(d626, plain, cGekkonidae(sK122) | 'Ts78' | ~cAmphisbaenidae(sK121) | ~cReptile(sK121), inference(resolution, [status(thm)], [d625,d624])).
% 29.92/29.20  cnf(d627, plain, ~cAmphisbaenidae(sK121) | cGekkonidae(sK122) | 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d626,d622])).
% 29.92/29.20  cnf(d628, plain, cGekkonidae(sK122) | 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d627,d620])).
% 29.92/29.20  cnf(d629, plain, 'Ts78' | cReptile(sK122), inference(resolution, [status(thm)], [d628,c46])).
% 29.92/29.20  cnf(d630, plain, 'Ts78' | ~cEmydidae(sK122) | ~cGekkonidae(sK122), inference(resolution, [status(thm)], [d629,d440])).
% 29.92/29.20  cnf(d631, plain, ~cEmydidae(sK122) | 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d630,d628])).
% 29.92/29.20  cnf(d632, plain, cEmydidae(sK122) | cXantusiidae(sK121) | 'Ts78', inference(resolution, [status(thm)], [d619,c164])).
% 29.92/29.20  cnf(d633, plain, cEmydidae(sK122) | 'Ts78' | ~cAmphisbaenidae(sK121) | ~cReptile(sK121), inference(resolution, [status(thm)], [d632,d624])).
% 29.92/29.20  cnf(d634, plain, ~cAmphisbaenidae(sK121) | cEmydidae(sK122) | 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d633,d622])).
% 29.92/29.20  cnf(d635, plain, cEmydidae(sK122) | 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d634,d620])).
% 29.92/29.20  cnf(d636, plain, 'Ts78' | 'Ts78', inference(resolution, [status(thm)], [d635,d631])).
% 29.92/29.20  cnf(d637, plain, 'Ts79', inference(resolution, [status(thm)], [d636,d437])).
% 29.92/29.20  cnf(d638, plain, cBipedidae(sK125) | cCordylidae(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,c172])).
% 29.92/29.20  cnf(d639, plain, cBipedidae(sK125) | ~'Ts79' | 'Ts80' | cReptile(sK126), inference(resolution, [status(thm)], [c172,c37])).
% 29.92/29.20  cnf(d640, plain, cBipedidae(sK125) | cReptile(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,d639])).
% 29.92/29.20  cnf(d641, plain, 'xsd$ustring$u4' = 'xsd$ustring$u11' | ~cCordylidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d322,c59])).
% 29.92/29.20  cnf(d642, plain, ~cCordylidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c105,d641])).
% 29.92/29.20  cnf(d643, plain, cBipedidae(sK125) | cXantusiidae(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,c171])).
% 29.92/29.20  cnf(d644, plain, cBipedidae(sK125) | 'Ts80' | ~cCordylidae(sK126) | ~cReptile(sK126), inference(resolution, [status(thm)], [d643,d642])).
% 29.92/29.20  cnf(d645, plain, cBipedidae(sK125) | ~cCordylidae(sK126) | 'Ts80' | cBipedidae(sK125) | 'Ts80', inference(resolution, [status(thm)], [d644,d640])).
% 29.92/29.20  cnf(d646, plain, cBipedidae(sK125) | 'Ts80' | cBipedidae(sK125) | 'Ts80', inference(resolution, [status(thm)], [d645,d638])).
% 29.92/29.20  cnf(d647, plain, 'xsd$ustring$u1' = 'xsd$ustring$u3' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cBipedidae(X0), inference(resolution, [status(thm)], [d16,c33])).
% 29.92/29.20  cnf(d648, plain, ~cAmphisbaenidae(X0) | ~cBipedidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c73,d647])).
% 29.92/29.20  cnf(d649, plain, 'Ts80' | cReptile(sK125), inference(resolution, [status(thm)], [d646,c34])).
% 29.92/29.20  cnf(d650, plain, 'Ts80' | ~cAmphisbaenidae(sK125) | ~cBipedidae(sK125), inference(resolution, [status(thm)], [d649,d648])).
% 29.92/29.20  cnf(d651, plain, ~cAmphisbaenidae(sK125) | 'Ts80' | 'Ts80', inference(resolution, [status(thm)], [d650,d646])).
% 29.92/29.20  cnf(d652, plain, cAmphisbaenidae(sK125) | cCordylidae(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,c174])).
% 29.92/29.20  cnf(d653, plain, cAmphisbaenidae(sK125) | ~'Ts79' | 'Ts80' | cReptile(sK126), inference(resolution, [status(thm)], [c174,c37])).
% 29.92/29.20  cnf(d654, plain, cAmphisbaenidae(sK125) | cReptile(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,d653])).
% 29.92/29.20  cnf(d655, plain, cAmphisbaenidae(sK125) | cXantusiidae(sK126) | 'Ts80', inference(resolution, [status(thm)], [d637,c173])).
% 29.92/29.20  cnf(d656, plain, cAmphisbaenidae(sK125) | 'Ts80' | ~cCordylidae(sK126) | ~cReptile(sK126), inference(resolution, [status(thm)], [d655,d642])).
% 29.92/29.20  cnf(d657, plain, cAmphisbaenidae(sK125) | ~cCordylidae(sK126) | 'Ts80' | cAmphisbaenidae(sK125) | 'Ts80', inference(resolution, [status(thm)], [d656,d654])).
% 29.92/29.20  cnf(d658, plain, cAmphisbaenidae(sK125) | 'Ts80' | cAmphisbaenidae(sK125) | 'Ts80', inference(resolution, [status(thm)], [d657,d652])).
% 29.92/29.20  cnf(d659, plain, 'Ts80' | 'Ts80', inference(resolution, [status(thm)], [d658,d651])).
% 29.92/29.20  cnf(d660, plain, cAnomalepidae(sK127) | cBipedidae(sK128) | 'Ts81', inference(resolution, [status(thm)], [d659,c177])).
% 29.92/29.20  cnf(d661, plain, cAnomalepidae(sK127) | cCordylidae(sK128) | 'Ts81', inference(resolution, [status(thm)], [d659,c178])).
% 29.92/29.20  cnf(d662, plain, 'xsd$ustring$u3' = 'xsd$ustring$u4' | ~cBipedidae(X0) | ~cReptile(X0) | ~cCordylidae(X0), inference(resolution, [status(thm)], [d57,c36])).
% 29.92/29.20  cnf(d663, plain, ~cBipedidae(X0) | ~cCordylidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c91,d662])).
% 29.92/29.20  cnf(d664, plain, cAnomalepidae(sK127) | ~'Ts80' | 'Ts81' | cReptile(sK128), inference(resolution, [status(thm)], [c177,c34])).
% 29.92/29.20  cnf(d665, plain, cAnomalepidae(sK127) | cReptile(sK128) | 'Ts81', inference(resolution, [status(thm)], [d659,d664])).
% 29.92/29.20  cnf(d666, plain, cAnomalepidae(sK127) | 'Ts81' | ~cBipedidae(sK128) | ~cCordylidae(sK128), inference(resolution, [status(thm)], [d665,d663])).
% 29.92/29.20  cnf(d667, plain, cAnomalepidae(sK127) | ~cBipedidae(sK128) | 'Ts81' | cAnomalepidae(sK127) | 'Ts81', inference(resolution, [status(thm)], [d666,d661])).
% 29.92/29.20  cnf(d668, plain, cAnomalepidae(sK127) | 'Ts81' | cAnomalepidae(sK127) | 'Ts81', inference(resolution, [status(thm)], [d667,d660])).
% 29.92/29.20  cnf(d669, plain, cBipedidae(sK128) | cGekkonidae(sK127) | 'Ts81', inference(resolution, [status(thm)], [d659,c175])).
% 29.92/29.20  cnf(d670, plain, 'xsd$ustring$u2' = 'xsd$ustring$u7' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cGekkonidae(X0), inference(resolution, [status(thm)], [d0,c45])).
% 29.92/29.20  cnf(d671, plain, ~cAnomalepidae(X0) | ~cGekkonidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c86,d670])).
% 29.92/29.20  cnf(d672, plain, 'Ts81' | cReptile(sK127), inference(resolution, [status(thm)], [d668,c31])).
% 29.92/29.20  cnf(d673, plain, 'Ts81' | ~cAnomalepidae(sK127) | ~cGekkonidae(sK127), inference(resolution, [status(thm)], [d672,d671])).
% 29.92/29.20  cnf(d674, plain, ~cAnomalepidae(sK127) | 'Ts81' | cBipedidae(sK128) | 'Ts81', inference(resolution, [status(thm)], [d673,d669])).
% 29.92/29.20  cnf(d675, plain, cBipedidae(sK128) | 'Ts81' | 'Ts81', inference(resolution, [status(thm)], [d674,d668])).
% 29.92/29.20  cnf(d676, plain, cCordylidae(sK128) | cGekkonidae(sK127) | 'Ts81', inference(resolution, [status(thm)], [d659,c176])).
% 29.92/29.20  cnf(d677, plain, ~cAnomalepidae(sK127) | 'Ts81' | cCordylidae(sK128) | 'Ts81', inference(resolution, [status(thm)], [d673,d676])).
% 29.92/29.20  cnf(d678, plain, cCordylidae(sK128) | 'Ts81' | 'Ts81', inference(resolution, [status(thm)], [d677,d668])).
% 29.92/29.20  cnf(d679, plain, 'Ts81' | cReptile(sK128), inference(resolution, [status(thm)], [d675,c34])).
% 29.92/29.20  cnf(d680, plain, 'Ts81' | ~cBipedidae(sK128) | ~cCordylidae(sK128), inference(resolution, [status(thm)], [d679,d663])).
% 29.92/29.20  cnf(d681, plain, ~cBipedidae(sK128) | 'Ts81' | 'Ts81', inference(resolution, [status(thm)], [d680,d678])).
% 29.92/29.20  cnf(d682, plain, 'Ts81' | 'Ts81', inference(resolution, [status(thm)], [d681,d675])).
% 29.92/29.20  cnf(d683, plain, 'Ts82', inference(resolution, [status(thm)], [d682,d421])).
% 29.92/29.20  cnf(d684, plain, cLeptotyphlopidae(sK132) | cReptile(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,d403])).
% 29.92/29.20  cnf(d685, plain, cLeptotyphlopidae(sK132) | cSphenodontidae(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,c185])).
% 29.92/29.20  cnf(d686, plain, ~cSphenodontidae(X0) | 'xsd$ustring$u10' = X1 | ~cReptile(X0) | ~'rfamily$uname'(X0,X1), inference(resolution, [status(thm)], [c56,c54])).
% 29.92/29.20  cnf(d687, plain, 'xsd$ustring$u10' = 'xsd$ustring$u11' | ~cReptile(X0) | ~cSphenodontidae(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d686,c59])).
% 29.92/29.20  cnf(d688, plain, ~cReptile(X0) | ~cSphenodontidae(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c126,d687])).
% 29.92/29.20  cnf(d689, plain, cLeptotyphlopidae(sK132) | cXantusiidae(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,c183])).
% 29.92/29.20  cnf(d690, plain, cLeptotyphlopidae(sK132) | 'Ts83' | ~cReptile(sK131) | ~cSphenodontidae(sK131), inference(resolution, [status(thm)], [d689,d688])).
% 29.92/29.20  cnf(d691, plain, cLeptotyphlopidae(sK132) | ~cReptile(sK131) | 'Ts83' | cLeptotyphlopidae(sK132) | 'Ts83', inference(resolution, [status(thm)], [d690,d685])).
% 29.92/29.20  cnf(d692, plain, cLeptotyphlopidae(sK132) | 'Ts83' | cLeptotyphlopidae(sK132) | 'Ts83', inference(resolution, [status(thm)], [d691,d684])).
% 29.92/29.20  cnf(d693, plain, 'xsd$ustring$u1' = 'xsd$ustring$u8' | ~cAmphisbaenidae(X0) | ~cReptile(X0) | ~cLeptotyphlopidae(X0), inference(resolution, [status(thm)], [d16,c48])).
% 29.92/29.20  cnf(d694, plain, ~cAmphisbaenidae(X0) | ~cLeptotyphlopidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c78,d693])).
% 29.92/29.20  cnf(d695, plain, 'Ts83' | cReptile(sK132), inference(resolution, [status(thm)], [d692,c49])).
% 29.92/29.20  cnf(d696, plain, 'Ts83' | ~cAmphisbaenidae(sK132) | ~cLeptotyphlopidae(sK132), inference(resolution, [status(thm)], [d695,d694])).
% 29.92/29.20  cnf(d697, plain, ~cAmphisbaenidae(sK132) | 'Ts83' | 'Ts83', inference(resolution, [status(thm)], [d696,d692])).
% 29.92/29.20  cnf(d698, plain, cReptile(sK131) | cAmphisbaenidae(sK132) | ~'Ts82' | 'Ts83', inference(resolution, [status(thm)], [c57,c186])).
% 29.92/29.20  cnf(d699, plain, cAmphisbaenidae(sK132) | cReptile(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,d698])).
% 29.92/29.20  cnf(d700, plain, cAmphisbaenidae(sK132) | cSphenodontidae(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,c186])).
% 29.92/29.20  cnf(d701, plain, cAmphisbaenidae(sK132) | cXantusiidae(sK131) | 'Ts83', inference(resolution, [status(thm)], [d683,c184])).
% 29.92/29.20  cnf(d702, plain, cAmphisbaenidae(sK132) | 'Ts83' | ~cReptile(sK131) | ~cSphenodontidae(sK131), inference(resolution, [status(thm)], [d701,d688])).
% 29.92/29.20  cnf(d703, plain, cAmphisbaenidae(sK132) | ~cReptile(sK131) | 'Ts83' | cAmphisbaenidae(sK132) | 'Ts83', inference(resolution, [status(thm)], [d702,d700])).
% 29.92/29.20  cnf(d704, plain, cAmphisbaenidae(sK132) | 'Ts83' | cAmphisbaenidae(sK132) | 'Ts83', inference(resolution, [status(thm)], [d703,d699])).
% 29.92/29.20  cnf(d705, plain, 'Ts83' | 'Ts83', inference(resolution, [status(thm)], [d704,d697])).
% 29.92/29.20  cnf(d706, plain, cAnomalepidae(sK134) | cBipedidae(sK133) | 'Ts84', inference(resolution, [status(thm)], [d705,c189])).
% 29.92/29.20  cnf(d707, plain, cReptile(sK133) | cAnomalepidae(sK134) | ~'Ts83' | 'Ts84', inference(resolution, [status(thm)], [c60,c187])).
% 29.92/29.20  cnf(d708, plain, cAnomalepidae(sK134) | cReptile(sK133) | 'Ts84', inference(resolution, [status(thm)], [d705,d707])).
% 29.92/29.20  cnf(d709, plain, 'xsd$ustring$u3' = 'xsd$ustring$u11' | ~cBipedidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [d57,c59])).
% 29.92/29.20  cnf(d710, plain, ~cBipedidae(X0) | ~cReptile(X0) | ~cXantusiidae(X0), inference(resolution, [status(thm)], [c98,d709])).
% 29.92/29.20  cnf(d711, plain, ~cBipedidae(sK133) | ~cReptile(sK133) | cAnomalepidae(sK134) | ~'Ts83' | 'Ts84', inference(resolution, [status(thm)], [d710,c187])).
% 29.92/29.20  cnf(d712, plain, cAnomalepidae(sK134) | ~cBipedidae(sK133) | ~cReptile(sK133) | 'Ts84', inference(resolution, [status(thm)], [d705,d711])).
% 29.92/29.20  cnf(d713, plain, cAnomalepidae(sK134) | ~cBipedidae(sK133) | 'Ts84' | cAnomalepidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d712,d708])).
% 29.92/29.20  cnf(d714, plain, cAnomalepidae(sK134) | 'Ts84' | cAnomalepidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d713,d706])).
% 29.92/29.20  cnf(d715, plain, 'xsd$ustring$u2' = 'xsd$ustring$u6' | ~cAnomalepidae(X0) | ~cReptile(X0) | ~cEmydidae(X0), inference(resolution, [status(thm)], [d0,c42])).
% 29.92/29.20  cnf(d716, plain, ~cAnomalepidae(X0) | ~cEmydidae(X0) | ~cReptile(X0), inference(resolution, [status(thm)], [c85,d715])).
% 29.92/29.20  cnf(d717, plain, 'Ts84' | cReptile(sK134), inference(resolution, [status(thm)], [d714,c31])).
% 29.92/29.20  cnf(d718, plain, 'Ts84' | ~cAnomalepidae(sK134) | ~cEmydidae(sK134), inference(resolution, [status(thm)], [d717,d716])).
% 29.92/29.20  cnf(d719, plain, cEmydidae(sK134) | ~'Ts83' | 'Ts84' | cReptile(sK133), inference(resolution, [status(thm)], [c188,c60])).
% 29.92/29.20  cnf(d720, plain, cEmydidae(sK134) | cReptile(sK133) | 'Ts84', inference(resolution, [status(thm)], [d705,d719])).
% 29.92/29.20  cnf(d721, plain, ~cBipedidae(sK133) | ~cReptile(sK133) | cEmydidae(sK134) | ~'Ts83' | 'Ts84', inference(resolution, [status(thm)], [d710,c188])).
% 29.92/29.20  cnf(d722, plain, ~cBipedidae(sK133) | cEmydidae(sK134) | ~cReptile(sK133) | 'Ts84', inference(resolution, [status(thm)], [d705,d721])).
% 29.92/29.20  cnf(d723, plain, ~cBipedidae(sK133) | cEmydidae(sK134) | 'Ts84' | cEmydidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d722,d720])).
% 29.92/29.20  cnf(d724, plain, cBipedidae(sK133) | cEmydidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d705,c190])).
% 29.92/29.20  cnf(d725, plain, ~cAnomalepidae(sK134) | 'Ts84' | cBipedidae(sK133) | 'Ts84', inference(resolution, [status(thm)], [d718,d724])).
% 29.92/29.20  cnf(d726, plain, cBipedidae(sK133) | 'Ts84' | 'Ts84', inference(resolution, [status(thm)], [d725,d714])).
% 29.92/29.20  cnf(d727, plain, 'Ts84' | cEmydidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d726,d723])).
% 29.92/29.20  cnf(d728, plain, 'Ts84' | ~cAnomalepidae(sK134) | 'Ts84', inference(resolution, [status(thm)], [d727,d718])).
% 29.92/29.20  cnf(d729, plain, 'Ts84' | 'Ts84', inference(resolution, [status(thm)], [d728,d714])).
% 29.92/29.20  cnf(d730, plain, 'Ts85', inference(resolution, [status(thm)], [d729,d402])).
% 29.92/29.20  cnf(d731, plain, 'Ts86', inference(resolution, [status(thm)], [d730,d384])).
% 29.92/29.20  cnf(d732, plain, ~cAgamidae(sK139) | cCordylidae(sK140), inference(resolution, [status(thm)], [d731,d364])).
% 29.92/29.20  cnf(d733, plain, cAgamidae(sK139) | cAnomalepidae(sK140) | ~'Ts86', inference(resolution, [status(thm)], [d363,c201])).
% 29.92/29.20  cnf(d734, plain, cAgamidae(sK139) | cAnomalepidae(sK140), inference(resolution, [status(thm)], [d731,d733])).
% 29.92/29.20  cnf(d735, plain, cAgamidae(sK139) | cCordylidae(sK140) | ~'Ts86', inference(resolution, [status(thm)], [d363,c202])).
% 29.92/29.20  cnf(d736, plain, cAgamidae(sK139) | cCordylidae(sK140), inference(resolution, [status(thm)], [d731,d735])).
% 29.92/29.20  cnf(d737, plain, cAgamidae(sK139) | ~'Ts86' | 'Ts87' | cReptile(sK140), inference(resolution, [status(thm)], [c201,c31])).
% 29.92/29.20  cnf(d738, plain, cAgamidae(sK139) | cReptile(sK140) | ~'Ts86', inference(resolution, [status(thm)], [d363,d737])).
% 29.92/29.20  cnf(d739, plain, cAgamidae(sK139) | cReptile(sK140), inference(resolution, [status(thm)], [d731,d738])).
% 29.92/29.20  cnf(d740, plain, cAgamidae(sK139) | ~cAnomalepidae(sK140) | ~cCordylidae(sK140), inference(resolution, [status(thm)], [d739,d2])).
% 29.92/29.20  cnf(d741, plain, cAgamidae(sK139) | ~cAnomalepidae(sK140) | cAgamidae(sK139), inference(resolution, [status(thm)], [d740,d736])).
% 29.92/29.20  cnf(d742, plain, cAgamidae(sK139) | cAgamidae(sK139), inference(resolution, [status(thm)], [d741,d734])).
% 29.92/29.20  cnf(d743, plain, cCordylidae(sK140), inference(resolution, [status(thm)], [d742,d732])).
% 29.92/29.20  cnf(d744, plain, cReptile(sK140), inference(resolution, [status(thm)], [d743,c37])).
% 29.92/29.20  cnf(d745, plain, ~cAnomalepidae(sK140) | ~cCordylidae(sK140), inference(resolution, [status(thm)], [d744,d2])).
% 29.92/29.20  cnf(d746, plain, ~cAnomalepidae(sK140), inference(resolution, [status(thm)], [d743,d745])).
% 29.92/29.20  cnf(d747, plain, cAnomalepidae(sK140) | ~'Ts86' | 'Ts87' | cReptile(sK139), inference(resolution, [status(thm)], [c199,c60])).
% 29.92/29.20  cnf(d748, plain, ~cAgamidae(sK139) | ~cReptile(sK139) | cAnomalepidae(sK140) | ~'Ts86' | 'Ts87', inference(resolution, [status(thm)], [d6,c199])).
% 29.92/29.20  cnf(d749, plain, ~cAgamidae(sK139) | cAnomalepidae(sK140) | ~'Ts86' | 'Ts87' | cAnomalepidae(sK140) | ~'Ts86' | 'Ts87', inference(resolution, [status(thm)], [d748,d747])).
% 29.92/29.20  cnf(d750, plain, ~cAgamidae(sK139) | cAnomalepidae(sK140) | ~'Ts86', inference(resolution, [status(thm)], [d363,d749])).
% 29.92/29.20  cnf(d751, plain, ~cAgamidae(sK139) | cAnomalepidae(sK140), inference(resolution, [status(thm)], [d731,d750])).
% 29.92/29.20  cnf(d752, plain, cAnomalepidae(sK140), inference(resolution, [status(thm)], [d742,d751])).
% 29.92/29.20  cnf(d753, plain, $false, inference(resolution, [status(thm)], [d752,d746])).
% 29.92/29.20  % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------