%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU272+2 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Thu Dec 30 02:52:49 EST 2010
% Result : Theorem 100.60s
% Output : Solution 249.54s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP16601/SEU272+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~s1_xboole_0__e8_6__wellord2__1:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... antisymmetry_r2_hidden:
% CSA axiom antisymmetry_r2_hidden found
% Looking for CSA axiom ... s1_tarski__e8_6__wellord2__1:
% CSA axiom s1_tarski__e8_6__wellord2__1 found
% Looking for CSA axiom ... t10_ordinal1:
% CSA axiom t10_ordinal1 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :t10_ordinal1:s1_tarski__e8_6__wellord2__1:antisymmetry_r2_hidden (3)
% Unselected axioms are ... :t23_ordinal1:t24_ordinal1:t2_tarski:t3_ordinal1:t7_tarski:t33_ordinal1:t41_ordinal1:t42_ordinal1:t31_ordinal1:d1_xboole_0:d1_tarski:d2_xboole_0:d3_xboole_0:d4_xboole_0:d1_enumset1:d2_tarski:d3_ordinal1:d4_tarski:fc1_ordinal1:antisymmetry_r2_xboole_0:existence_m1_subset_1:irreflexivity_r2_xboole_0:rc1_xboole_0:rc2_xboole_0:reflexivity_r1_tarski:t1_xboole_1:connectedness_r1_ordinal1:reflexivity_r1_ordinal1:d1_relat_1:d2_relat_1:d1_ordinal1:d3_tarski:t21_ordinal1:t32_ordinal1:t7_boole:d10_xboole_0:d1_zfmisc_1:t1_subset:t3_xboole_0:d1_setfam_1:d2_zfmisc_1:l23_zfmisc_1:t33_zfmisc_1:t46_zfmisc_1:t65_zfmisc_1:t8_boole:fc3_ordinal1:t35_funct_1:commutativity_k2_xboole_0:commutativity_k3_xboole_0:idempotence_k2_xboole_0:idempotence_k3_xboole_0:commutativity_k2_tarski:d4_subset_1:t10_zfmisc_1:d4_relat_1:d10_relat_1:d11_relat_1:d12_relat_1:d13_relat_1:d14_relat_1:d1_wellord1:d4_relat_2:d5_relat_1:d6_relat_2:d7_relat_1:d8_relat_1:l3_wellord1:redefinition_r1_ordinal1:t30_relat_1:d1_relat_2:d8_relat_2:l2_wellord1:cc1_ordinal1:cc2_ordinal1:d4_ordinal1:existence_m2_relset_1:rc1_ordinal1:symmetry_r1_xboole_0:t12_xboole_1:t28_xboole_1:t3_subset:t3_xboole_1:t6_zfmisc_1:d2_subset_1:l3_subset_1:l71_subset_1:t2_subset:t4_subset:t4_wellord2:t6_boole:t99_zfmisc_1:d6_ordinal1:dt_k6_relat_1:fc1_relat_1:fc2_relat_1:fc3_relat_1:l1_zfmisc_1:l25_zfmisc_1:l28_zfmisc_1:l2_zfmisc_1:l55_zfmisc_1:t106_zfmisc_1:t1_boole:t25_wellord1:t2_boole:t37_zfmisc_1:t39_xboole_1:t3_boole:t40_xboole_1:t48_xboole_1:t4_boole:t4_xboole_0:t69_enumset1:t83_xboole_1:t8_zfmisc_1:t9_zfmisc_1:cc1_relat_1:d1_mcart_1:d2_mcart_1:d2_ordinal1:fc13_relat_1:l50_zfmisc_1:rc1_relat_1:rc2_ordinal1:rc2_relat_1:t38_zfmisc_1:t56_relat_1:t92_zfmisc_1:t9_tarski:d8_xboole_0:l4_wellord1:t34_funct_1:t60_xboole_1:t72_funct_1:involutiveness_k4_relat_1:l82_funct_1:t143_relat_1:t166_relat_1:t17_xboole_1:t19_xboole_1:t20_relat_1:t26_xboole_1:t2_xboole_1:t33_xboole_1:t36_xboole_1:t7_xboole_1:t8_xboole_1:fc2_subset_1:fc2_xboole_0:fc3_subset_1:fc3_xboole_0:l1_wellord1:t146_relat_1:t160_relat_1:t16_wellord1:t17_wellord1:t18_wellord1:t22_relset_1:t23_relset_1:t37_relat_1:t74_relat_1:cc1_funct_1:cc3_ordinal1:d1_wellord2:d3_relat_1:dt_k5_setfam_1:existence_m1_relset_1:fc1_subset_1:fc1_xboole_0:fc1_zfmisc_1:fc4_ordinal1:rc3_ordinal1:t8_funct_1:d14_relat_2:d9_relat_2:fc4_subset_1:l32_xboole_1:l3_zfmisc_1:l4_zfmisc_1:t136_zfmisc_1:t174_relat_1:t20_wellord1:t21_wellord1:t37_xboole_1:t39_zfmisc_1:t45_xboole_1:t71_relat_1:d3_wellord1:d5_tarski:d7_xboole_0:fc2_ordinal1:fc3_funct_1:l29_wellord1:t116_relat_1:t118_relat_1:t118_zfmisc_1:t119_zfmisc_1:t144_relat_1:t167_relat_1:t1_zfmisc_1:t25_relat_1:t44_relat_1:t45_relat_1:t54_subset_1:t5_subset:t60_relat_1:t63_xboole_1:t99_relat_1:d12_relat_2:d4_funct_1:d8_setfam_1:d9_funct_1:involutiveness_k3_subset_1:involutiveness_k7_setfam_1:rc1_subset_1:rc2_subset_1:redefinition_k4_relset_1:redefinition_k5_relset_1:t16_relset_1:t21_funct_1:t46_relat_1:t47_relat_1:t50_subset_1:d6_relat_1:fc4_relat_1:fc5_relat_1:fc6_relat_1:fc7_relat_1:fc8_relat_1:rc2_funct_1:t14_relset_1:t22_wellord1:t23_wellord1:t24_wellord1:t68_funct_1:t7_mcart_1:d12_funct_1:d13_funct_1:d2_wellord1:d5_funct_1:d7_wellord1:d8_funct_1:dt_k2_funct_1:fc10_relat_1:fc11_relat_1:fc1_funct_1:fc2_funct_1:fc4_funct_1:fc5_funct_1:fc9_relat_1:rc1_funct_1:rc3_funct_1:rc4_funct_1:t115_relat_1:t117_relat_1:t145_relat_1:t178_relat_1:t19_wellord1:t22_funct_1:t23_funct_1:t31_wellord1:t32_wellord1:t39_wellord1:t70_funct_1:t86_relat_1:t88_relat_1:t90_relat_1:d6_wellord1:dt_k1_wellord2:dt_k2_wellord1:dt_k4_relat_1:dt_k5_relat_1:dt_k7_relat_1:dt_k8_relat_1:rc3_relat_1:redefinition_k5_setfam_1:t119_relat_1:t140_relat_1:t146_funct_1:t43_subset_1:t54_funct_1:t94_relat_1:cc1_relset_1:cc2_funct_1:d1_relset_1:d5_subset_1:dt_k2_subset_1:fc12_relat_1:redefinition_k6_setfam_1:redefinition_k6_subset_1:t145_funct_1:t147_funct_1:t21_relat_1:t46_setfam_1:t55_funct_1:t57_funct_1:t64_relat_1:t65_relat_1:redefinition_m2_relset_1:t12_relset_1:t2_wellord2:t3_wellord2:t5_wellord2:dt_k3_subset_1:dt_k4_relset_1:dt_k5_relset_1:dt_k6_setfam_1:dt_k6_subset_1:dt_k7_setfam_1:dt_m2_relset_1:d16_relat_2:t5_wellord1:t8_wellord1:t47_setfam_1:t48_setfam_1:t49_wellord1:t54_wellord1:t62_funct_1:d4_wellord1:d5_wellord1:t53_wellord1:dt_k10_relat_1:dt_k1_enumset1:dt_k1_funct_1:dt_k1_mcart_1:dt_k1_ordinal1:dt_k1_relat_1:dt_k1_setfam_1:dt_k1_tarski:dt_k1_wellord1:dt_k1_xboole_0:dt_k1_zfmisc_1:dt_k2_mcart_1:dt_k2_relat_1:dt_k2_tarski:dt_k2_xboole_0:dt_k2_zfmisc_1:dt_k3_relat_1:dt_k3_tarski:dt_k3_xboole_0:dt_k4_tarski:dt_k4_xboole_0:dt_k9_relat_1:dt_m1_relset_1:dt_m1_subset_1 (346)
% SZS status THM for /tmp/SystemOnTPTP16601/SEU272+2.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP16601/SEU272+2.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 17879
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.95 CPU 2.03 WC
% PrfWatch: 3.94 CPU 4.03 WC
% PrfWatch: 5.94 CPU 6.04 WC
% PrfWatch: 7.93 CPU 8.05 WC
% PrfWatch: 9.92 CPU 10.05 WC
% PrfWatch: 11.92 CPU 12.06 WC
% PrfWatch: 13.91 CPU 14.07 WC
% PrfWatch: 15.90 CPU 16.07 WC
% PrfWatch: 17.90 CPU 18.08 WC
% PrfWatch: 19.72 CPU 20.09 WC
% PrfWatch: 21.57 CPU 22.09 WC
% PrfWatch: 23.56 CPU 24.10 WC
% PrfWatch: 25.55 CPU 26.11 WC
% PrfWatch: 27.55 CPU 28.11 WC
% PrfWatch: 29.55 CPU 30.12 WC
% PrfWatch: 31.53 CPU 32.13 WC
% PrfWatch: 33.50 CPU 34.13 WC
% PrfWatch: 35.50 CPU 36.14 WC
% PrfWatch: 37.45 CPU 38.15 WC
% PrfWatch: 39.45 CPU 40.15 WC
% PrfWatch: 41.38 CPU 42.17 WC
% PrfWatch: 43.20 CPU 44.18 WC
% PrfWatch: 45.05 CPU 46.19 WC
% PrfWatch: 47.04 CPU 48.20 WC
% PrfWatch: 49.04 CPU 50.21 WC
% PrfWatch: 51.04 CPU 52.23 WC
% PrfWatch: 53.04 CPU 54.24 WC
% PrfWatch: 55.04 CPU 56.25 WC
% PrfWatch: 57.04 CPU 58.26 WC
% PrfWatch: 59.03 CPU 60.28 WC
% PrfWatch: 61.04 CPU 62.29 WC
% PrfWatch: 63.04 CPU 64.30 WC
% PrfWatch: 65.04 CPU 66.32 WC
% PrfWatch: 67.04 CPU 68.33 WC
% PrfWatch: 69.04 CPU 70.34 WC
% PrfWatch: 71.03 CPU 72.35 WC
% PrfWatch: 73.03 CPU 74.37 WC
% PrfWatch: 75.03 CPU 76.38 WC
% PrfWatch: 76.96 CPU 78.41 WC
% PrfWatch: 78.96 CPU 80.41 WC
% PrfWatch: 80.94 CPU 82.42 WC
% PrfWatch: 82.93 CPU 84.43 WC
% PrfWatch: 84.92 CPU 86.43 WC
% PrfWatch: 86.90 CPU 88.44 WC
% PrfWatch: 88.90 CPU 90.45 WC
% PrfWatch: 90.88 CPU 92.45 WC
% PrfWatch: 92.87 CPU 94.46 WC
% PrfWatch: 94.72 CPU 96.47 WC
% PrfWatch: 96.55 CPU 98.48 WC
% PrfWatch: 98.55 CPU 100.49 WC
% PrfWatch: 100.55 CPU 102.51 WC
% PrfWatch: 102.54 CPU 104.52 WC
% PrfWatch: 104.55 CPU 106.53 WC
% # Preprocessing time : 0.012 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 106.54 CPU 108.55 WC
% PrfWatch: 108.54 CPU 110.56 WC
% PrfWatch: 110.54 CPU 112.57 WC
% PrfWatch: 112.54 CPU 114.58 WC
% PrfWatch: 114.54 CPU 116.60 WC
% PrfWatch: 116.54 CPU 118.61 WC
% PrfWatch: 118.54 CPU 120.62 WC
% PrfWatch: 120.53 CPU 122.63 WC
% PrfWatch: 122.54 CPU 124.65 WC
% PrfWatch: 124.53 CPU 126.66 WC
% PrfWatch: 126.54 CPU 128.67 WC
% PrfWatch: 128.54 CPU 130.68 WC
% PrfWatch: 130.53 CPU 132.70 WC
% PrfWatch: 132.53 CPU 134.71 WC
% PrfWatch: 134.54 CPU 136.72 WC
% PrfWatch: 136.53 CPU 138.73 WC
% PrfWatch: 138.36 CPU 140.75 WC
% PrfWatch: 140.22 CPU 142.76 WC
% PrfWatch: 142.23 CPU 144.77 WC
% PrfWatch: 144.23 CPU 146.79 WC
% PrfWatch: 146.23 CPU 148.80 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:![X2]:(ordinal(X2)=>(![X3]:![X4]:![X5]:((((X3=X4&?[X6]:((ordinal(X6)&X4=X6)&in(X6,X1)))&X3=X5)&?[X7]:((ordinal(X7)&X5=X7)&in(X7,X1)))=>X4=X5)=>?[X3]:![X4]:(in(X4,X3)<=>?[X5]:((in(X5,succ(X2))&X5=X4)&?[X8]:((ordinal(X8)&X4=X8)&in(X8,X1)))))),file('/tmp/SRASS.s.p', s1_tarski__e8_6__wellord2__1)).
% fof(4, conjecture,![X1]:![X2]:(ordinal(X2)=>?[X3]:![X4]:(in(X4,X3)<=>(in(X4,succ(X2))&?[X5]:((ordinal(X5)&X4=X5)&in(X5,X1))))),file('/tmp/SRASS.s.p', s1_xboole_0__e8_6__wellord2__1)).
% fof(5, negated_conjecture,~(![X1]:![X2]:(ordinal(X2)=>?[X3]:![X4]:(in(X4,X3)<=>(in(X4,succ(X2))&?[X5]:((ordinal(X5)&X4=X5)&in(X5,X1)))))),inference(assume_negation,[status(cth)],[4])).
% fof(9, plain,![X1]:![X2]:(~(ordinal(X2))|(?[X3]:?[X4]:?[X5]:((((X3=X4&?[X6]:((ordinal(X6)&X4=X6)&in(X6,X1)))&X3=X5)&?[X7]:((ordinal(X7)&X5=X7)&in(X7,X1)))&~(X4=X5))|?[X3]:![X4]:((~(in(X4,X3))|?[X5]:((in(X5,succ(X2))&X5=X4)&?[X8]:((ordinal(X8)&X4=X8)&in(X8,X1))))&(![X5]:((~(in(X5,succ(X2)))|~(X5=X4))|![X8]:((~(ordinal(X8))|~(X4=X8))|~(in(X8,X1))))|in(X4,X3))))),inference(fof_nnf,[status(thm)],[2])).
% fof(10, plain,![X9]:![X10]:(~(ordinal(X10))|(?[X11]:?[X12]:?[X13]:((((X11=X12&?[X14]:((ordinal(X14)&X12=X14)&in(X14,X9)))&X11=X13)&?[X15]:((ordinal(X15)&X13=X15)&in(X15,X9)))&~(X12=X13))|?[X16]:![X17]:((~(in(X17,X16))|?[X18]:((in(X18,succ(X10))&X18=X17)&?[X19]:((ordinal(X19)&X17=X19)&in(X19,X9))))&(![X20]:((~(in(X20,succ(X10)))|~(X20=X17))|![X21]:((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9))))|in(X17,X16))))),inference(variable_rename,[status(thm)],[9])).
% fof(11, plain,![X9]:![X10]:(~(ordinal(X10))|(((((esk1_2(X9,X10)=esk2_2(X9,X10)&((ordinal(esk4_2(X9,X10))&esk2_2(X9,X10)=esk4_2(X9,X10))&in(esk4_2(X9,X10),X9)))&esk1_2(X9,X10)=esk3_2(X9,X10))&((ordinal(esk5_2(X9,X10))&esk3_2(X9,X10)=esk5_2(X9,X10))&in(esk5_2(X9,X10),X9)))&~(esk2_2(X9,X10)=esk3_2(X9,X10)))|![X17]:((~(in(X17,esk6_2(X9,X10)))|((in(esk7_3(X9,X10,X17),succ(X10))&esk7_3(X9,X10,X17)=X17)&((ordinal(esk8_3(X9,X10,X17))&X17=esk8_3(X9,X10,X17))&in(esk8_3(X9,X10,X17),X9))))&(![X20]:((~(in(X20,succ(X10)))|~(X20=X17))|![X21]:((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9))))|in(X17,esk6_2(X9,X10)))))),inference(skolemize,[status(esa)],[10])).
% fof(12, plain,![X9]:![X10]:![X17]:![X20]:![X21]:(((((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10)))&(~(in(X17,esk6_2(X9,X10)))|((in(esk7_3(X9,X10,X17),succ(X10))&esk7_3(X9,X10,X17)=X17)&((ordinal(esk8_3(X9,X10,X17))&X17=esk8_3(X9,X10,X17))&in(esk8_3(X9,X10,X17),X9)))))|((((esk1_2(X9,X10)=esk2_2(X9,X10)&((ordinal(esk4_2(X9,X10))&esk2_2(X9,X10)=esk4_2(X9,X10))&in(esk4_2(X9,X10),X9)))&esk1_2(X9,X10)=esk3_2(X9,X10))&((ordinal(esk5_2(X9,X10))&esk3_2(X9,X10)=esk5_2(X9,X10))&in(esk5_2(X9,X10),X9)))&~(esk2_2(X9,X10)=esk3_2(X9,X10))))|~(ordinal(X10))),inference(shift_quantors,[status(thm)],[11])).
% fof(13, plain,![X9]:![X10]:![X17]:![X20]:![X21]:(((((((esk1_2(X9,X10)=esk2_2(X9,X10)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|((((~(ordinal(X21))|~(X17=X21))|~(in(X21,X9)))|(~(in(X20,succ(X10)))|~(X20=X17)))|in(X17,esk6_2(X9,X10))))|~(ordinal(X10))))&((((((((esk1_2(X9,X10)=esk2_2(X9,X10)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|(in(esk7_3(X9,X10,X17),succ(X10))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((((esk1_2(X9,X10)=esk2_2(X9,X10)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|(esk7_3(X9,X10,X17)=X17|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((((((((esk1_2(X9,X10)=esk2_2(X9,X10)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|(ordinal(esk8_3(X9,X10,X17))|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((((esk1_2(X9,X10)=esk2_2(X9,X10)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|(X17=esk8_3(X9,X10,X17)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((((((esk1_2(X9,X10)=esk2_2(X9,X10)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((((ordinal(esk4_2(X9,X10))|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk2_2(X9,X10)=esk4_2(X9,X10)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk4_2(X9,X10),X9)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((esk1_2(X9,X10)=esk3_2(X9,X10)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((((ordinal(esk5_2(X9,X10))|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))&((esk3_2(X9,X10)=esk5_2(X9,X10)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))&((in(esk5_2(X9,X10),X9)|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10)))))&((~(esk2_2(X9,X10)=esk3_2(X9,X10))|(in(esk8_3(X9,X10,X17),X9)|~(in(X17,esk6_2(X9,X10)))))|~(ordinal(X10))))))),inference(distribute,[status(thm)],[12])).
% cnf(14,plain,(in(esk8_3(X3,X1,X2),X3)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(18,plain,(in(esk8_3(X3,X1,X2),X3)|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(22,plain,(in(esk8_3(X3,X1,X2),X3)|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(23,plain,(X2=esk8_3(X3,X1,X2)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(27,plain,(X2=esk8_3(X3,X1,X2)|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(31,plain,(X2=esk8_3(X3,X1,X2)|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(32,plain,(ordinal(esk8_3(X3,X1,X2))|~ordinal(X1)|~in(X2,esk6_2(X3,X1))|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(36,plain,(ordinal(esk8_3(X3,X1,X2))|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(40,plain,(ordinal(esk8_3(X3,X1,X2))|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(41,plain,(esk7_3(X3,X1,X2)=X2|~ordinal(X1)|~in(X2,esk6_2(X3,X1))|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(45,plain,(esk7_3(X3,X1,X2)=X2|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(49,plain,(esk7_3(X3,X1,X2)=X2|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(50,plain,(in(esk7_3(X3,X1,X2),succ(X1))|~ordinal(X1)|~in(X2,esk6_2(X3,X1))|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(54,plain,(in(esk7_3(X3,X1,X2),succ(X1))|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(58,plain,(in(esk7_3(X3,X1,X2),succ(X1))|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|~in(X2,esk6_2(X3,X1))),inference(split_conjunct,[status(thm)],[13])).
% cnf(59,plain,(in(X2,esk6_2(X3,X1))|~ordinal(X1)|X4!=X2|~in(X4,succ(X1))|~in(X5,X3)|X2!=X5|~ordinal(X5)|esk2_2(X3,X1)!=esk3_2(X3,X1)),inference(split_conjunct,[status(thm)],[13])).
% cnf(63,plain,(in(X2,esk6_2(X3,X1))|esk1_2(X3,X1)=esk3_2(X3,X1)|~ordinal(X1)|X4!=X2|~in(X4,succ(X1))|~in(X5,X3)|X2!=X5|~ordinal(X5)),inference(split_conjunct,[status(thm)],[13])).
% cnf(67,plain,(in(X2,esk6_2(X3,X1))|esk1_2(X3,X1)=esk2_2(X3,X1)|~ordinal(X1)|X4!=X2|~in(X4,succ(X1))|~in(X5,X3)|X2!=X5|~ordinal(X5)),inference(split_conjunct,[status(thm)],[13])).
% fof(71, negated_conjecture,?[X1]:?[X2]:(ordinal(X2)&![X3]:?[X4]:((~(in(X4,X3))|(~(in(X4,succ(X2)))|![X5]:((~(ordinal(X5))|~(X4=X5))|~(in(X5,X1)))))&(in(X4,X3)|(in(X4,succ(X2))&?[X5]:((ordinal(X5)&X4=X5)&in(X5,X1)))))),inference(fof_nnf,[status(thm)],[5])).
% fof(72, negated_conjecture,?[X6]:?[X7]:(ordinal(X7)&![X8]:?[X9]:((~(in(X9,X8))|(~(in(X9,succ(X7)))|![X10]:((~(ordinal(X10))|~(X9=X10))|~(in(X10,X6)))))&(in(X9,X8)|(in(X9,succ(X7))&?[X11]:((ordinal(X11)&X9=X11)&in(X11,X6)))))),inference(variable_rename,[status(thm)],[71])).
% fof(73, negated_conjecture,(ordinal(esk10_0)&![X8]:((~(in(esk11_1(X8),X8))|(~(in(esk11_1(X8),succ(esk10_0)))|![X10]:((~(ordinal(X10))|~(esk11_1(X8)=X10))|~(in(X10,esk9_0)))))&(in(esk11_1(X8),X8)|(in(esk11_1(X8),succ(esk10_0))&((ordinal(esk12_1(X8))&esk11_1(X8)=esk12_1(X8))&in(esk12_1(X8),esk9_0)))))),inference(skolemize,[status(esa)],[72])).
% fof(74, negated_conjecture,![X8]:![X10]:((((((~(ordinal(X10))|~(esk11_1(X8)=X10))|~(in(X10,esk9_0)))|~(in(esk11_1(X8),succ(esk10_0))))|~(in(esk11_1(X8),X8)))&(in(esk11_1(X8),X8)|(in(esk11_1(X8),succ(esk10_0))&((ordinal(esk12_1(X8))&esk11_1(X8)=esk12_1(X8))&in(esk12_1(X8),esk9_0)))))&ordinal(esk10_0)),inference(shift_quantors,[status(thm)],[73])).
% fof(75, negated_conjecture,![X8]:![X10]:((((((~(ordinal(X10))|~(esk11_1(X8)=X10))|~(in(X10,esk9_0)))|~(in(esk11_1(X8),succ(esk10_0))))|~(in(esk11_1(X8),X8)))&((in(esk11_1(X8),succ(esk10_0))|in(esk11_1(X8),X8))&(((ordinal(esk12_1(X8))|in(esk11_1(X8),X8))&(esk11_1(X8)=esk12_1(X8)|in(esk11_1(X8),X8)))&(in(esk12_1(X8),esk9_0)|in(esk11_1(X8),X8)))))&ordinal(esk10_0)),inference(distribute,[status(thm)],[74])).
% cnf(76,negated_conjecture,(ordinal(esk10_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(77,negated_conjecture,(in(esk11_1(X1),X1)|in(esk12_1(X1),esk9_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(78,negated_conjecture,(in(esk11_1(X1),X1)|esk11_1(X1)=esk12_1(X1)),inference(split_conjunct,[status(thm)],[75])).
% cnf(79,negated_conjecture,(in(esk11_1(X1),X1)|ordinal(esk12_1(X1))),inference(split_conjunct,[status(thm)],[75])).
% cnf(80,negated_conjecture,(in(esk11_1(X1),X1)|in(esk11_1(X1),succ(esk10_0))),inference(split_conjunct,[status(thm)],[75])).
% cnf(81,negated_conjecture,(~in(esk11_1(X1),X1)|~in(esk11_1(X1),succ(esk10_0))|~in(X2,esk9_0)|esk11_1(X1)!=X2|~ordinal(X2)),inference(split_conjunct,[status(thm)],[75])).
% cnf(82,plain,(esk1_2(X1,X2)=esk2_2(X1,X2)|in(X3,esk6_2(X1,X2))|X3!=X4|~ordinal(X3)|~ordinal(X2)|~in(X4,succ(X2))|~in(X3,X1)),inference(er,[status(thm)],[67,theory(equality)])).
% cnf(83,plain,(esk1_2(X1,X2)=esk2_2(X1,X2)|in(X3,esk6_2(X1,X2))|~ordinal(X3)|~ordinal(X2)|~in(X3,succ(X2))|~in(X3,X1)),inference(er,[status(thm)],[82,theory(equality)])).
% cnf(84,plain,(esk1_2(X1,X2)=esk3_2(X1,X2)|in(X3,esk6_2(X1,X2))|X3!=X4|~ordinal(X3)|~ordinal(X2)|~in(X4,succ(X2))|~in(X3,X1)),inference(er,[status(thm)],[63,theory(equality)])).
% cnf(85,plain,(esk1_2(X1,X2)=esk3_2(X1,X2)|in(X3,esk6_2(X1,X2))|~ordinal(X3)|~ordinal(X2)|~in(X3,succ(X2))|~in(X3,X1)),inference(er,[status(thm)],[84,theory(equality)])).
% cnf(98,plain,(in(X1,esk6_2(X2,X3))|esk3_2(X2,X3)!=esk2_2(X2,X3)|X1!=X4|~ordinal(X1)|~ordinal(X3)|~in(X4,succ(X3))|~in(X1,X2)),inference(er,[status(thm)],[59,theory(equality)])).
% cnf(99,plain,(in(X1,esk6_2(X2,X3))|esk3_2(X2,X3)!=esk2_2(X2,X3)|~ordinal(X1)|~ordinal(X3)|~in(X1,succ(X3))|~in(X1,X2)),inference(er,[status(thm)],[98,theory(equality)])).
% cnf(124,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|esk7_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk11_1(esk6_2(X1,X2)),succ(esk10_0))|~ordinal(X2)),inference(spm,[status(thm)],[49,80,theory(equality)])).
% cnf(128,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|esk7_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk11_1(esk6_2(X1,X2)),succ(esk10_0))|~ordinal(X2)),inference(spm,[status(thm)],[45,80,theory(equality)])).
% cnf(147,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)),inference(spm,[status(thm)],[31,78,theory(equality)])).
% cnf(148,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|ordinal(esk12_1(esk6_2(X1,X2)))|~ordinal(X2)),inference(spm,[status(thm)],[31,79,theory(equality)])).
% cnf(149,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk12_1(esk6_2(X1,X2)),esk9_0)|~ordinal(X2)),inference(spm,[status(thm)],[31,77,theory(equality)])).
% cnf(151,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)),inference(spm,[status(thm)],[27,78,theory(equality)])).
% cnf(152,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|ordinal(esk12_1(esk6_2(X1,X2)))|~ordinal(X2)),inference(spm,[status(thm)],[27,79,theory(equality)])).
% cnf(153,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk12_1(esk6_2(X1,X2)),esk9_0)|~ordinal(X2)),inference(spm,[status(thm)],[27,77,theory(equality)])).
% cnf(174,negated_conjecture,(esk7_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk11_1(esk6_2(X1,X2)),succ(esk10_0))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(spm,[status(thm)],[41,80,theory(equality)])).
% cnf(175,negated_conjecture,(esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(spm,[status(thm)],[23,78,theory(equality)])).
% cnf(177,negated_conjecture,(esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk12_1(esk6_2(X1,X2)),esk9_0)|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(spm,[status(thm)],[23,77,theory(equality)])).
% cnf(178,negated_conjecture,(esk8_3(X1,X2,esk11_1(esk6_2(X1,X2)))=esk11_1(esk6_2(X1,X2))|in(esk11_1(esk6_2(X1,X2)),succ(esk10_0))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(spm,[status(thm)],[23,80,theory(equality)])).
% cnf(382,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|~ordinal(esk10_0)|~in(esk11_1(X2),X1)),inference(spm,[status(thm)],[83,80,theory(equality)])).
% cnf(395,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|$false|~in(esk11_1(X2),X1)),inference(rw,[status(thm)],[382,76,theory(equality)])).
% cnf(396,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|~in(esk11_1(X2),X1)),inference(cn,[status(thm)],[395,theory(equality)])).
% cnf(401,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|~ordinal(esk10_0)|~in(esk11_1(X2),X1)),inference(spm,[status(thm)],[85,80,theory(equality)])).
% cnf(414,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|$false|~in(esk11_1(X2),X1)),inference(rw,[status(thm)],[401,76,theory(equality)])).
% cnf(415,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(X2),esk6_2(X1,esk10_0))|in(esk11_1(X2),X2)|~ordinal(esk11_1(X2))|~in(esk11_1(X2),X1)),inference(cn,[status(thm)],[414,theory(equality)])).
% cnf(501,negated_conjecture,(in(esk11_1(X1),esk6_2(X2,esk10_0))|in(esk11_1(X1),X1)|esk3_2(X2,esk10_0)!=esk2_2(X2,esk10_0)|~ordinal(esk11_1(X1))|~ordinal(esk10_0)|~in(esk11_1(X1),X2)),inference(spm,[status(thm)],[99,80,theory(equality)])).
% cnf(515,negated_conjecture,(in(esk11_1(X1),esk6_2(X2,esk10_0))|in(esk11_1(X1),X1)|esk3_2(X2,esk10_0)!=esk2_2(X2,esk10_0)|~ordinal(esk11_1(X1))|$false|~in(esk11_1(X1),X2)),inference(rw,[status(thm)],[501,76,theory(equality)])).
% cnf(516,negated_conjecture,(in(esk11_1(X1),esk6_2(X2,esk10_0))|in(esk11_1(X1),X1)|esk3_2(X2,esk10_0)!=esk2_2(X2,esk10_0)|~ordinal(esk11_1(X1))|~in(esk11_1(X1),X2)),inference(cn,[status(thm)],[515,theory(equality)])).
% cnf(1692,negated_conjecture,(esk7_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))),inference(spm,[status(thm)],[124,76,theory(equality)])).
% cnf(2241,negated_conjecture,(esk7_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))),inference(spm,[status(thm)],[128,76,theory(equality)])).
% cnf(4857,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|ordinal(esk11_1(esk6_2(X1,X2)))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[40,147,theory(equality)])).
% cnf(4861,negated_conjecture,(esk1_2(X1,X2)=esk2_2(X1,X2)|in(esk11_1(esk6_2(X1,X2)),X1)|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[22,147,theory(equality)])).
% cnf(4949,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|ordinal(esk12_1(esk6_2(X1,esk10_0)))),inference(spm,[status(thm)],[148,76,theory(equality)])).
% cnf(5036,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)),inference(spm,[status(thm)],[149,76,theory(equality)])).
% cnf(5339,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|ordinal(esk11_1(esk6_2(X1,X2)))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[36,151,theory(equality)])).
% cnf(5343,negated_conjecture,(esk1_2(X1,X2)=esk3_2(X1,X2)|in(esk11_1(esk6_2(X1,X2)),X1)|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[18,151,theory(equality)])).
% cnf(5591,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|ordinal(esk12_1(esk6_2(X1,esk10_0)))),inference(spm,[status(thm)],[152,76,theory(equality)])).
% cnf(5758,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)),inference(spm,[status(thm)],[153,76,theory(equality)])).
% cnf(9214,negated_conjecture,(esk7_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|esk3_2(X1,esk10_0)!=esk2_2(X1,esk10_0)),inference(spm,[status(thm)],[174,76,theory(equality)])).
% cnf(9438,negated_conjecture,(ordinal(esk11_1(esk6_2(X1,X2)))|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[32,175,theory(equality)])).
% cnf(9439,negated_conjecture,(in(esk11_1(esk6_2(X1,X2)),X1)|esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)|~in(esk11_1(esk6_2(X1,X2)),esk6_2(X1,X2))),inference(spm,[status(thm)],[14,175,theory(equality)])).
% cnf(9763,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|esk3_2(X1,esk10_0)!=esk2_2(X1,esk10_0)),inference(spm,[status(thm)],[177,76,theory(equality)])).
% cnf(9954,negated_conjecture,(esk8_3(X1,esk10_0,esk11_1(esk6_2(X1,esk10_0)))=esk11_1(esk6_2(X1,esk10_0))|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|esk3_2(X1,esk10_0)!=esk2_2(X1,esk10_0)),inference(spm,[status(thm)],[178,76,theory(equality)])).
% cnf(18014,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[40,4949,theory(equality)])).
% cnf(18075,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[18014,76,theory(equality)])).
% cnf(18076,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[18075,theory(equality)])).
% cnf(18300,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[36,5591,theory(equality)])).
% cnf(18362,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[18300,76,theory(equality)])).
% cnf(18363,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[18362,theory(equality)])).
% cnf(29535,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[22,5036,theory(equality)])).
% cnf(29628,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[29535,76,theory(equality)])).
% cnf(29629,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[29628,theory(equality)])).
% cnf(29861,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[18,5758,theory(equality)])).
% cnf(29955,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[29861,76,theory(equality)])).
% cnf(29956,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[29955,theory(equality)])).
% cnf(38176,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[58,1692,theory(equality)])).
% cnf(38212,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[38176,76,theory(equality)])).
% cnf(38213,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[38212,theory(equality)])).
% cnf(38529,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|~ordinal(esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(spm,[status(thm)],[54,2241,theory(equality)])).
% cnf(38566,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|$false|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(rw,[status(thm)],[38529,76,theory(equality)])).
% cnf(38567,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))),inference(cn,[status(thm)],[38566,theory(equality)])).
% cnf(42452,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))),inference(csr,[status(thm)],[38213,80])).
% cnf(42511,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|esk11_1(esk6_2(X1,esk10_0))!=X2|~ordinal(X2)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))|~in(X2,esk9_0)),inference(spm,[status(thm)],[81,42452,theory(equality)])).
% cnf(42849,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk11_1(esk6_2(X1,esk10_0)),succ(esk10_0))),inference(csr,[status(thm)],[38567,80])).
% cnf(42908,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|esk11_1(esk6_2(X1,esk10_0))!=X2|~ordinal(X2)|~in(esk11_1(esk6_2(X1,esk10_0)),esk6_2(X1,esk10_0))|~in(X2,esk9_0)),inference(spm,[status(thm)],[81,42849,theory(equality)])).
% cnf(45283,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk11_1(esk6_2(X1,esk10_0))!=X2|~ordinal(X2)|~in(X2,esk9_0)),inference(spm,[status(thm)],[42511,78,theory(equality)])).
% cnf(46016,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|~ordinal(esk11_1(esk6_2(X1,esk10_0)))|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)),inference(er,[status(thm)],[45283,theory(equality)])).
% cnf(49475,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk11_1(esk6_2(X1,esk10_0))!=X2|~ordinal(X2)|~in(X2,esk9_0)),inference(spm,[status(thm)],[42908,78,theory(equality)])).
% cnf(50018,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|~ordinal(esk11_1(esk6_2(X1,esk10_0)))|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)),inference(er,[status(thm)],[49475,theory(equality)])).
% cnf(168250,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))),inference(csr,[status(thm)],[18076,79])).
% cnf(168639,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|ordinal(esk11_1(esk6_2(X1,esk10_0)))|ordinal(esk12_1(esk6_2(X1,esk10_0)))),inference(csr,[status(thm)],[18363,79])).
% cnf(273650,negated_conjecture,(esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)),inference(csr,[status(thm)],[29629,77])).
% cnf(275225,negated_conjecture,(esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|in(esk12_1(esk6_2(X1,esk10_0)),esk9_0)|in(esk11_1(esk6_2(X1,esk10_0)),X1)),inference(csr,[status(thm)],[29956,77])).
% cnf(1077713,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk1_2(X1,X2)=esk2_2(X1,X2)|ordinal(esk11_1(esk6_2(X1,X2)))|~ordinal(X2)),inference(csr,[status(thm)],[4857,78])).
% cnf(1077933,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[46016,1077713,theory(equality)])).
% cnf(1077957,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)|$false),inference(rw,[status(thm)],[1077933,76,theory(equality)])).
% cnf(1077958,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk2_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)),inference(cn,[status(thm)],[1077957,theory(equality)])).
% cnf(1080317,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk1_2(X1,X2)=esk3_2(X1,X2)|ordinal(esk11_1(esk6_2(X1,X2)))|~ordinal(X2)),inference(csr,[status(thm)],[5339,78])).
% cnf(1080531,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[50018,1080317,theory(equality)])).
% cnf(1080550,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)|$false),inference(rw,[status(thm)],[1080531,76,theory(equality)])).
% cnf(1080551,negated_conjecture,(esk12_1(esk6_2(X1,esk10_0))=esk11_1(esk6_2(X1,esk10_0))|esk1_2(X1,esk10_0)=esk3_2(X1,esk10_0)|~in(esk11_1(esk6_2(X1,esk10_0)),esk9_0)),inference(cn,[status(thm)],[1080550,theory(equality)])).
% cnf(1144067,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|ordinal(esk11_1(esk6_2(X1,X2)))|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(csr,[status(thm)],[9438,78])).
% cnf(1691365,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk1_2(X1,X2)=esk2_2(X1,X2)|in(esk11_1(esk6_2(X1,X2)),X1)|~ordinal(X2)),inference(csr,[status(thm)],[4861,78])).
% cnf(1691837,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1077958,1691365,theory(equality)])).
% cnf(1691908,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|$false),inference(rw,[status(thm)],[1691837,76,theory(equality)])).
% cnf(1691909,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(cn,[status(thm)],[1691908,theory(equality)])).
% cnf(1692750,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(spm,[status(thm)],[168250,1691909,theory(equality)])).
% cnf(1692764,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(spm,[status(thm)],[273650,1691909,theory(equality)])).
% cnf(1693241,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(spm,[status(thm)],[396,1692764,theory(equality)])).
% cnf(1695005,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(csr,[status(thm)],[1693241,1692750])).
% cnf(1695418,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(spm,[status(thm)],[42511,1695005,theory(equality)])).
% cnf(1698160,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[1695418,theory(equality)])).
% cnf(1698485,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(csr,[status(thm)],[1698160,1692764])).
% cnf(1698486,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(csr,[status(thm)],[1698485,1692750])).
% cnf(1780345,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|esk1_2(X1,X2)=esk3_2(X1,X2)|in(esk11_1(esk6_2(X1,X2)),X1)|~ordinal(X2)),inference(csr,[status(thm)],[5343,78])).
% cnf(1780814,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk1_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1080551,1780345,theory(equality)])).
% cnf(1780888,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(rw,[status(thm)],[1780814,1698486,theory(equality)])).
% cnf(1780889,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|$false),inference(rw,[status(thm)],[1780888,76,theory(equality)])).
% cnf(1780890,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)),inference(cn,[status(thm)],[1780889,theory(equality)])).
% cnf(1781749,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(spm,[status(thm)],[168639,1780890,theory(equality)])).
% cnf(1781764,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(spm,[status(thm)],[275225,1780890,theory(equality)])).
% cnf(1781822,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(rw,[status(thm)],[1781749,1698486,theory(equality)])).
% cnf(1781823,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(cn,[status(thm)],[1781822,theory(equality)])).
% cnf(1781836,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(rw,[status(thm)],[1781764,1698486,theory(equality)])).
% cnf(1781837,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(cn,[status(thm)],[1781836,theory(equality)])).
% cnf(1782290,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(spm,[status(thm)],[415,1781837,theory(equality)])).
% cnf(1782349,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(rw,[status(thm)],[1782290,1698486,theory(equality)])).
% cnf(1782350,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(cn,[status(thm)],[1782349,theory(equality)])).
% cnf(1783348,negated_conjecture,(esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(csr,[status(thm)],[1782350,1781823])).
% cnf(1783762,negated_conjecture,(esk1_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(spm,[status(thm)],[42908,1783348,theory(equality)])).
% cnf(1784302,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(rw,[status(thm)],[1783762,1698486,theory(equality)])).
% cnf(1784303,negated_conjecture,(esk2_2(esk9_0,esk10_0)=esk3_2(esk9_0,esk10_0)|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(cn,[status(thm)],[1784302,theory(equality)])).
% cnf(1786244,negated_conjecture,(esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[1784303,theory(equality)])).
% cnf(1787295,negated_conjecture,(esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(csr,[status(thm)],[1786244,1781837])).
% cnf(1787296,negated_conjecture,(esk3_2(esk9_0,esk10_0)=esk2_2(esk9_0,esk10_0)),inference(csr,[status(thm)],[1787295,1781823])).
% cnf(1787300,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))),inference(spm,[status(thm)],[9214,1787296,theory(equality)])).
% cnf(1787301,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk12_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(spm,[status(thm)],[9763,1787296,theory(equality)])).
% cnf(1787302,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))),inference(spm,[status(thm)],[9954,1787296,theory(equality)])).
% cnf(1788387,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~in(X1,esk9_0)),inference(spm,[status(thm)],[81,1787300,theory(equality)])).
% cnf(1788615,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~in(X1,esk9_0)),inference(spm,[status(thm)],[81,1787302,theory(equality)])).
% cnf(1803127,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(spm,[status(thm)],[1788387,78,theory(equality)])).
% cnf(1803892,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[1803127,theory(equality)])).
% cnf(1803903,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1803892,1144067,theory(equality)])).
% cnf(1803996,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[1803903,1787296,theory(equality)])).
% cnf(1803997,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|$false),inference(rw,[status(thm)],[1803996,76,theory(equality)])).
% cnf(1803998,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(cn,[status(thm)],[1803997,theory(equality)])).
% cnf(1804403,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(spm,[status(thm)],[1788615,78,theory(equality)])).
% cnf(1804689,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[1804403,theory(equality)])).
% cnf(1804700,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1804689,1144067,theory(equality)])).
% cnf(1804793,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[1804700,1787296,theory(equality)])).
% cnf(1804794,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|$false),inference(rw,[status(thm)],[1804793,76,theory(equality)])).
% cnf(1804795,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(cn,[status(thm)],[1804794,theory(equality)])).
% cnf(2494888,negated_conjecture,(esk12_1(esk6_2(X1,X2))=esk11_1(esk6_2(X1,X2))|in(esk11_1(esk6_2(X1,X2)),X1)|esk3_2(X1,X2)!=esk2_2(X1,X2)|~ordinal(X2)),inference(csr,[status(thm)],[9439,78])).
% cnf(2495383,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1804795,2494888,theory(equality)])).
% cnf(2495384,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[1803998,2494888,theory(equality)])).
% cnf(2495485,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[2495383,1787296,theory(equality)])).
% cnf(2495486,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false),inference(rw,[status(thm)],[2495485,76,theory(equality)])).
% cnf(2495487,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2495486,theory(equality)])).
% cnf(2495488,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[2495384,1787296,theory(equality)])).
% cnf(2495489,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false),inference(rw,[status(thm)],[2495488,76,theory(equality)])).
% cnf(2495490,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2495489,theory(equality)])).
% cnf(2496239,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[32,2495487,theory(equality)])).
% cnf(2496240,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[14,2495487,theory(equality)])).
% cnf(2496636,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2496239,1787296,theory(equality)])).
% cnf(2496637,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2496636,76,theory(equality)])).
% cnf(2496638,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2496637,theory(equality)])).
% cnf(2496639,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2496240,1787296,theory(equality)])).
% cnf(2496640,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2496639,76,theory(equality)])).
% cnf(2496641,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2496640,theory(equality)])).
% cnf(2497500,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[50,2495490,theory(equality)])).
% cnf(2497707,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2497500,1787296,theory(equality)])).
% cnf(2497708,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2497707,76,theory(equality)])).
% cnf(2497709,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2497708,theory(equality)])).
% cnf(2498315,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(csr,[status(thm)],[2496638,78])).
% cnf(2499329,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))),inference(csr,[status(thm)],[2497709,78])).
% cnf(2499531,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~in(X1,esk9_0)),inference(spm,[status(thm)],[81,2499329,theory(equality)])).
% cnf(2499593,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(csr,[status(thm)],[2496641,78])).
% cnf(2500603,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(csr,[status(thm)],[2499531,78])).
% cnf(2500604,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[2500603,theory(equality)])).
% cnf(2501266,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(csr,[status(thm)],[2500604,2499593])).
% cnf(2501267,negated_conjecture,(esk12_1(esk6_2(esk9_0,esk10_0))=esk11_1(esk6_2(esk9_0,esk10_0))),inference(csr,[status(thm)],[2501266,2498315])).
% cnf(2501268,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[79,2501267,theory(equality)])).
% cnf(2501269,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[77,2501267,theory(equality)])).
% cnf(2502034,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(rw,[status(thm)],[1787301,2501267,theory(equality)])).
% cnf(2504542,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(spm,[status(thm)],[516,2502034,theory(equality)])).
% cnf(2504605,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(rw,[status(thm)],[2504542,1787296,theory(equality)])).
% cnf(2504606,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(cn,[status(thm)],[2504605,theory(equality)])).
% cnf(2509611,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(csr,[status(thm)],[2504606,2501268])).
% cnf(2509774,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[23,2509611,theory(equality)])).
% cnf(2510121,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[2509774,1787296,theory(equality)])).
% cnf(2510122,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false),inference(rw,[status(thm)],[2510121,76,theory(equality)])).
% cnf(2510123,negated_conjecture,(esk8_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2510122,theory(equality)])).
% cnf(2510942,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[32,2510123,theory(equality)])).
% cnf(2510943,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[14,2510123,theory(equality)])).
% cnf(2511363,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2510942,1787296,theory(equality)])).
% cnf(2511364,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2511363,76,theory(equality)])).
% cnf(2511365,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2511364,theory(equality)])).
% cnf(2511366,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2510943,1787296,theory(equality)])).
% cnf(2511367,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2511366,76,theory(equality)])).
% cnf(2511368,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2511367,theory(equality)])).
% cnf(2512403,negated_conjecture,(ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(csr,[status(thm)],[2511365,2501268])).
% cnf(2512855,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(csr,[status(thm)],[2511368,2501269])).
% cnf(2513007,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(spm,[status(thm)],[516,2512855,theory(equality)])).
% cnf(2513372,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))),inference(rw,[status(thm)],[2513007,1787296,theory(equality)])).
% cnf(2513373,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|$false|$false),inference(rw,[status(thm)],[2513372,2512403,theory(equality)])).
% cnf(2513374,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2513373,theory(equality)])).
% cnf(2513744,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)),inference(spm,[status(thm)],[41,2513374,theory(equality)])).
% cnf(2514385,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|~ordinal(esk10_0)),inference(rw,[status(thm)],[2513744,1787296,theory(equality)])).
% cnf(2514386,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))|$false|$false),inference(rw,[status(thm)],[2514385,76,theory(equality)])).
% cnf(2514387,negated_conjecture,(esk7_3(esk9_0,esk10_0,esk11_1(esk6_2(esk9_0,esk10_0)))=esk11_1(esk6_2(esk9_0,esk10_0))),inference(cn,[status(thm)],[2514386,theory(equality)])).
% cnf(2516277,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|esk3_2(esk9_0,esk10_0)!=esk2_2(esk9_0,esk10_0)|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(spm,[status(thm)],[50,2514387,theory(equality)])).
% cnf(2516496,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|$false|~ordinal(esk10_0)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2516277,1787296,theory(equality)])).
% cnf(2516497,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|$false|$false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))),inference(rw,[status(thm)],[2516496,76,theory(equality)])).
% cnf(2516498,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))|$false|$false|$false),inference(rw,[status(thm)],[2516497,2513374,theory(equality)])).
% cnf(2516499,negated_conjecture,(in(esk11_1(esk6_2(esk9_0,esk10_0)),succ(esk10_0))),inference(cn,[status(thm)],[2516498,theory(equality)])).
% cnf(2517642,negated_conjecture,(esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk6_2(esk9_0,esk10_0))|~in(X1,esk9_0)),inference(spm,[status(thm)],[81,2516499,theory(equality)])).
% cnf(2518103,negated_conjecture,(esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|$false|~in(X1,esk9_0)),inference(rw,[status(thm)],[2517642,2513374,theory(equality)])).
% cnf(2518104,negated_conjecture,(esk11_1(esk6_2(esk9_0,esk10_0))!=X1|~ordinal(X1)|~in(X1,esk9_0)),inference(cn,[status(thm)],[2518103,theory(equality)])).
% cnf(2519446,negated_conjecture,(~ordinal(esk11_1(esk6_2(esk9_0,esk10_0)))|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(er,[status(thm)],[2518104,theory(equality)])).
% cnf(2519447,negated_conjecture,($false|~in(esk11_1(esk6_2(esk9_0,esk10_0)),esk9_0)),inference(rw,[status(thm)],[2519446,2512403,theory(equality)])).
% cnf(2519448,negated_conjecture,($false|$false),inference(rw,[status(thm)],[2519447,2512855,theory(equality)])).
% cnf(2519449,negated_conjecture,($false),inference(cn,[status(thm)],[2519448,theory(equality)])).
% cnf(2519450,negated_conjecture,($false),2519449,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 30163
% # ...of these trivial : 353
% # ...subsumed : 20231
% # ...remaining for further processing: 9579
% # Other redundant clauses eliminated : 18
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1596
% # Backward-rewritten : 1113
% # Generated clauses : 1906672
% # ...of the previous two non-trivial : 1838807
% # Contextual simplify-reflections : 41653
% # Paramodulations : 1906585
% # Factorizations : 38
% # Equation resolutions : 58
% # Current number of processed clauses: 6799
% # Positive orientable unit clauses: 18
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 6
% # Non-unit-clauses : 6775
% # Current number of unprocessed clauses: 1259199
% # ...number of literals in the above : 9769464
% # Clause-clause subsumption calls (NU) : 711226
% # Rec. Clause-clause subsumption calls : 161403
% # Unit Clause-clause subsumption calls : 2298
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 54
% # Indexed BW rewrite successes : 15
% # Backwards rewriting index: 916 leaves, 1.89+/-2.212 terms/leaf
% # Paramod-from index: 297 leaves, 1.65+/-1.643 terms/leaf
% # Paramod-into index: 602 leaves, 1.64+/-1.645 terms/leaf
% # -------------------------------------------------
% # User time : 102.990 s
% # System time : 2.600 s
% # Total time : 105.590 s
% # Maximum resident set size: 0 pages
% PrfWatch: 148.20 CPU 150.81 WC
% PrfWatch: 148.28 CPU 150.89 WC
% FINAL PrfWatch: 148.28 CPU 150.89 WC
% SZS output end Solution for /tmp/SystemOnTPTP16601/SEU272+2.tptp
%
%------------------------------------------------------------------------------