%------------------------------------------------------------------------------
% File : Waldmeister---710
% Problem : DAT436-2 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : woody %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:23:53 PM UTC 2026
% Result : Unsatisfiable 175.32s 175.79s
% Output : CNFRefutation 175.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : DAT436-2 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : woody %s
% 0.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 20:59:02 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.56/0.97 ********************************************************************************
% 0.56/0.97 * W A L D M E I S T E R \| \ / \|/ *
% 0.56/0.97 * |/ | \/ | *
% 0.56/0.97 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / *
% 0.56/0.97 * A. Jaeger and B. Loechner | | *
% 0.56/0.97 * <waldmeister@informatik.uni-kl.de> | *
% 0.56/0.97 ********************************************************************************
% 0.56/0.97
% 0.56/0.97
% 0.56/0.97 Goals:
% 0.56/0.97 ------
% 0.56/0.97
% 0.56/0.97 ( 1) true1 ?= false1
% 0.56/0.97 using narrowing to prove cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?= selsort(cons(x1,cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil))))))
% 0.56/0.97
% 0.56/0.97 Detected structure: Orkus
% 0.56/0.97 ********************************************************************************
% 0.56/0.97 ****************************** COMPLETION - PROOF ******************************
% 0.56/0.97 ********************************************************************************
% 0.56/0.97
% 175.32/175.79 joined goal: 1 cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?= selsort(cons(x1,cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil)))))) to false1
% 175.32/175.79 goal joined
% 175.32/175.79 % SZS status Unsatisfiable
% 175.32/175.79 #START OF PROOF
% 175.32/175.79 % SZS output start CNFRefutation
% 175.32/175.79 cnf('0.1.0.0',axiom,
% 175.32/175.79 ( cons(X1,X2) = ifrepl(true,X3,X1,cons(X4,X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.1.1.0',plain,
% 175.32/175.79 ( cons(X1,X2) = ifrepl(true,X3,X1,cons(X4,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.1.0.0']),
% 175.32/175.79 [weight('<0,0,0,[0,0,0,1]>')]).
% 175.32/175.79 cnf('0.1.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,cons(X3,X4)) = cons(X2,X4) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.1.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_1]).
% 175.32/175.79 cnf('0.2.0.0',axiom,
% 175.32/175.79 ( cons(X1,selsort(X2)) = ifselsort(true,cons(X1,X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.2.1.0',plain,
% 175.32/175.79 ( cons(X1,selsort(X2)) = ifselsort(true,cons(X1,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.2.0.0']),
% 175.32/175.79 [weight('<1,0,0,[0,0,0,2]>')]).
% 175.32/175.79 cnf('0.2.2.0',plain,
% 175.32/175.79 ( ifselsort(true,cons(X1,X2)) = cons(X1,selsort(X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.2.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_2]).
% 175.32/175.79 cnf('0.3.0.0',axiom,
% 175.32/175.79 ( cons(X1,replace(X2,X3,X4)) = ifrepl(false,X2,X3,cons(X1,X4)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.3.1.0',plain,
% 175.32/175.79 ( cons(X1,replace(X2,X3,X4)) = ifrepl(false,X2,X3,cons(X1,X4)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.3.0.0']),
% 175.32/175.79 [weight('<2,0,0,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.3.2.0',plain,
% 175.32/175.79 ( ifrepl(false,X1,X2,cons(X3,X4)) = cons(X3,replace(X1,X2,X4)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.3.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_3]).
% 175.32/175.79 cnf('0.4.0.0',axiom,
% 175.32/175.79 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.4.1.0',plain,
% 175.32/175.79 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.4.0.0']),
% 175.32/175.79 [weight('<3,0,0,[0,0,0,4]>')]).
% 175.32/175.79 cnf('0.4.2.0',plain,
% 175.32/175.79 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.4.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_4]).
% 175.32/175.79 cnf('0.5.0.0',axiom,
% 175.32/175.79 ( s(X1) = min(cons(s(X1),nil)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.5.1.0',plain,
% 175.32/175.79 ( s(X1) = min(cons(s(X1),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.5.0.0']),
% 175.32/175.79 [weight('<4,0,0,[0,0,0,5]>')]).
% 175.32/175.79 cnf('0.5.2.0',plain,
% 175.32/175.79 ( min(cons(s(X1),nil)) = s(X1) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.5.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_5]).
% 175.32/175.79 cnf('0.6.0.0',axiom,
% 175.32/175.79 ( zero = min(cons(zero,nil)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.6.1.0',plain,
% 175.32/175.79 ( zero = min(cons(zero,nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.6.0.0']),
% 175.32/175.79 [weight('<5,0,0,[0,0,0,6]>')]).
% 175.32/175.79 cnf('0.6.2.0',plain,
% 175.32/175.79 ( min(cons(zero,nil)) = zero ),
% 175.32/175.79 inference(orient,[status(thm)],['0.6.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_6]).
% 175.32/175.79 cnf('0.7.0.0',axiom,
% 175.32/175.79 ( min(cons(X1,X2)) = ifmin(false,cons(X3,cons(X1,X2))) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.7.1.0',plain,
% 175.32/175.79 ( min(cons(X1,X2)) = ifmin(false,cons(X3,cons(X1,X2))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.7.0.0']),
% 175.32/175.79 [weight('<6,0,0,[0,0,0,7]>')]).
% 175.32/175.79 cnf('0.7.2.0',plain,
% 175.32/175.79 ( ifmin(false,cons(X1,cons(X2,X3))) = min(cons(X2,X3)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.7.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_7]).
% 175.32/175.79 cnf('0.8.0.0',axiom,
% 175.32/175.79 ( min(cons(X1,X2)) = ifmin(true,cons(X1,cons(X3,X2))) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.8.1.0',plain,
% 175.32/175.79 ( min(cons(X1,X2)) = ifmin(true,cons(X1,cons(X3,X2))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.8.0.0']),
% 175.32/175.79 [weight('<7,0,0,[0,0,0,8]>')]).
% 175.32/175.79 cnf('0.8.2.0',plain,
% 175.32/175.79 ( ifmin(true,cons(X1,cons(X2,X3))) = min(cons(X1,X3)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.8.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_8]).
% 175.32/175.79 cnf('0.9.0.0',axiom,
% 175.32/175.79 ( min(cons(X1,cons(X2,X3))) = ifmin(le(X1,X2),cons(X1,cons(X2,X3))) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.9.1.0',plain,
% 175.32/175.79 ( min(cons(X1,cons(X2,X3))) = ifmin(le(X1,X2),cons(X1,cons(X2,X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.9.0.0']),
% 175.32/175.79 [weight('<8,0,0,[0,0,0,9]>')]).
% 175.32/175.79 cnf('0.9.2.0',plain,
% 175.32/175.79 ( ifmin(le(X1,X2),cons(X1,cons(X2,X3))) = min(cons(X1,cons(X2,X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.9.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_9]).
% 175.32/175.79 cnf('0.10.0.0',axiom,
% 175.32/175.79 ( eq(X1,X2) = eq(s(X1),s(X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.10.1.0',plain,
% 175.32/175.79 ( eq(X1,X2) = eq(s(X1),s(X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.10.0.0']),
% 175.32/175.79 [weight('<9,0,0,[0,0,0,10]>')]).
% 175.32/175.79 cnf('0.10.2.0',plain,
% 175.32/175.79 ( eq(s(X1),s(X2)) = eq(X1,X2) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.10.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_10]).
% 175.32/175.79 cnf('0.11.0.0',axiom,
% 175.32/175.79 ( eq(s(X1),zero) = false ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.11.1.0',plain,
% 175.32/175.79 ( eq(s(X1),zero) = false ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.11.0.0']),
% 175.32/175.79 [weight('<10,0,0,[0,0,0,11]>')]).
% 175.32/175.79 cnf('0.11.2.0',plain,
% 175.32/175.79 ( eq(s(X1),zero) = false ),
% 175.32/175.79 inference(orient,[status(thm)],['0.11.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_11]).
% 175.32/175.79 cnf('0.12.0.0',axiom,
% 175.32/175.79 ( eq(zero,s(X1)) = false ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.12.1.0',plain,
% 175.32/175.79 ( eq(zero,s(X1)) = false ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.12.0.0']),
% 175.32/175.79 [weight('<11,0,0,[0,0,0,12]>')]).
% 175.32/175.79 cnf('0.12.2.0',plain,
% 175.32/175.79 ( eq(zero,s(X1)) = false ),
% 175.32/175.79 inference(orient,[status(thm)],['0.12.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_12]).
% 175.32/175.79 cnf('0.13.0.0',axiom,
% 175.32/175.79 ( eq(zero,zero) = true ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.13.1.0',plain,
% 175.32/175.79 ( eq(zero,zero) = true ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13.0.0']),
% 175.32/175.79 [weight('<12,0,0,[0,0,0,13]>')]).
% 175.32/175.79 cnf('0.13.2.0',plain,
% 175.32/175.79 ( eq(zero,zero) = true ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_13]).
% 175.32/175.79 cnf('0.14.0.0',axiom,
% 175.32/175.79 ( false = le(s(X1),zero) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.14.1.0',plain,
% 175.32/175.79 ( false = le(s(X1),zero) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.14.0.0']),
% 175.32/175.79 [weight('<13,0,0,[0,0,0,14]>')]).
% 175.32/175.79 cnf('0.14.2.0',plain,
% 175.32/175.79 ( le(s(X1),zero) = false ),
% 175.32/175.79 inference(orient,[status(thm)],['0.14.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_14]).
% 175.32/175.79 cnf('0.15.0.0',axiom,
% 175.32/175.79 ( nil = selsort(nil) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.15.1.0',plain,
% 175.32/175.79 ( nil = selsort(nil) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.15.0.0']),
% 175.32/175.79 [weight('<14,0,0,[0,0,0,15]>')]).
% 175.32/175.79 cnf('0.15.2.0',plain,
% 175.32/175.79 ( selsort(nil) = nil ),
% 175.32/175.79 inference(orient,[status(thm)],['0.15.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_15]).
% 175.32/175.79 cnf('0.16.0.0',axiom,
% 175.32/175.79 ( nil = replace(X1,X2,nil) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.16.1.0',plain,
% 175.32/175.79 ( nil = replace(X1,X2,nil) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.16.0.0']),
% 175.32/175.79 [weight('<15,0,0,[0,0,0,16]>')]).
% 175.32/175.79 cnf('0.16.2.0',plain,
% 175.32/175.79 ( replace(X1,X2,nil) = nil ),
% 175.32/175.79 inference(orient,[status(thm)],['0.16.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_16]).
% 175.32/175.79 cnf('0.17.0.0',axiom,
% 175.32/175.79 ( true = le(zero,X1) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.17.1.0',plain,
% 175.32/175.79 ( true = le(zero,X1) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.17.0.0']),
% 175.32/175.79 [weight('<16,0,0,[0,0,0,17]>')]).
% 175.32/175.79 cnf('0.17.2.0',plain,
% 175.32/175.79 ( le(zero,X1) = true ),
% 175.32/175.79 inference(orient,[status(thm)],['0.17.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_17]).
% 175.32/175.79 cnf('0.18.0.0',axiom,
% 175.32/175.79 ( le(X1,X2) = le(s(X1),s(X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.18.1.0',plain,
% 175.32/175.79 ( le(X1,X2) = le(s(X1),s(X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.18.0.0']),
% 175.32/175.79 [weight('<17,0,0,[0,0,0,18]>')]).
% 175.32/175.79 cnf('0.18.2.0',plain,
% 175.32/175.79 ( le(s(X1),s(X2)) = le(X1,X2) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.18.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_18]).
% 175.32/175.79 cnf('0.19.0.0',axiom,
% 175.32/175.79 ( selsort(cons(X1,X2)) = ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.19.1.0',plain,
% 175.32/175.79 ( selsort(cons(X1,X2)) = ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.19.0.0']),
% 175.32/175.79 [weight('<18,0,0,[0,0,0,19]>')]).
% 175.32/175.79 cnf('0.19.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) = selsort(cons(X1,X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.19.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_19]).
% 175.32/175.79 cnf('0.20.0.0',axiom,
% 175.32/175.79 ( replace(X1,X2,cons(X3,X4)) = ifrepl(eq(X1,X3),X1,X2,cons(X3,X4)) ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.20.1.0',plain,
% 175.32/175.79 ( replace(X1,X2,cons(X3,X4)) = ifrepl(eq(X1,X3),X1,X2,cons(X3,X4)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.20.0.0']),
% 175.32/175.79 [weight('<19,0,0,[0,0,0,20]>')]).
% 175.32/175.79 cnf('0.20.2.0',plain,
% 175.32/175.79 ( ifrepl(eq(X1,X2),X1,X3,cons(X2,X4)) = replace(X1,X3,cons(X2,X4)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.20.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_20]).
% 175.32/175.79 cnf('0.21.0.0',axiom,
% 175.32/175.79 ( eq1(X1,X1) = true1 ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.21.1.0',plain,
% 175.32/175.79 ( eq1(X1,X1) = true1 ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.21.0.0']),
% 175.32/175.79 [weight('<20,0,0,[0,0,0,21]>')]).
% 175.32/175.79 cnf('0.21.2.0',plain,
% 175.32/175.79 ( eq1(X1,X1) = true1 ),
% 175.32/175.79 inference(orient,[status(thm)],['0.21.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_21]).
% 175.32/175.79 cnf('0.22.0.0',axiom,
% 175.32/175.79 ( eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),selsort(cons(X1,cons(s(zero),cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(zero,nil))))))) = false1 ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004')).
% 175.32/175.79 cnf('0.22.1.0',plain,
% 175.32/175.79 ( eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),selsort(cons(X1,cons(s(zero),cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(zero,nil))))))) = false1 ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.22.0.0']),
% 175.32/175.79 [weight('<21,0,0,[0,0,0,22]>')]).
% 175.32/175.79 cnf('0.22.2.0',plain,
% 175.32/175.79 ( eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),selsort(cons(X1,cons(s(zero),cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(zero,nil))))))) = false1 ),
% 175.32/175.79 inference(orient,[status(thm)],['0.22.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_22]).
% 175.32/175.79 cnf('0.24.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(zero,X2)) = ifrepl(true,zero,X1,cons(zero,X2)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.20.2.0','0.13.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.24.0.1',plain,
% 175.32/175.79 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.24.0.0','0.1.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.24.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.24.0.1']),
% 175.32/175.79 [weight('<69,20,13,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.24.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.24.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_24]).
% 175.32/175.79 cnf('0.30.0.0',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(zero,X2))) = ifmin(false,cons(s(X1),cons(zero,X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.9.2.0','0.14.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.30.0.1',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.30.0.0','0.7.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.30.1.0',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.30.0.1']),
% 175.32/175.79 [weight('<95,14,9,[0,0,0,1]>')]).
% 175.32/175.79 cnf('0.30.2.0',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.30.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_30]).
% 175.32/175.79 cnf('0.34.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),X3)) = ifrepl(false,zero,X1,cons(s(X2),X3)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.20.2.0','0.12.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.34.0.1',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),X3)) = cons(s(X2),replace(zero,X1,X3)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.34.0.0','0.3.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.34.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),X3)) = cons(s(X2),replace(zero,X1,X3)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.34.0.1']),
% 175.32/175.79 [weight('<119,20,12,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.34.2.0',plain,
% 175.32/175.79 ( cons(s(X1),replace(zero,X2,X3)) = replace(zero,X2,cons(s(X1),X3)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.34.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_34]).
% 175.32/175.79 cnf('0.35.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.16.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.35.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.35.0.0']),
% 175.32/175.79 [weight('<95,34,16,[1,0,0,3]>')]).
% 175.32/175.79 cnf('0.35.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.35.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_35]).
% 175.32/175.79 cnf('0.36.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(X1),nil)) = ifselsort(eq(s(X1),s(X1)),cons(s(X1),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.19.2.0','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.36.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(X1),nil)) = ifselsort(eq(X1,X1),cons(s(X1),nil)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.36.0.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.36.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(X1),nil)) = ifselsort(eq(X1,X1),cons(s(X1),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.36.0.1']),
% 175.32/175.79 [weight('<125,19,5,[1,0,0,3]>')]).
% 175.32/175.79 cnf('0.36.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(X1,X1),cons(s(X1),nil)) = selsort(cons(s(X1),nil)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.36.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_36]).
% 175.32/175.79 cnf('0.48.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.24.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.48.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.48.0.0']),
% 175.32/175.79 [weight('<159,34,24,[1,0,0,3]>')]).
% 175.32/175.79 cnf('0.48.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.48.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_48]).
% 175.32/175.79 cnf('0.49.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),nil)) = ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.36.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.49.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),nil)) = ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.49.0.0']),
% 175.32/175.79 [weight('<159,36,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.49.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) = selsort(cons(s(s(X1)),nil)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.49.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_49]).
% 175.32/175.79 cnf('0.53.0.0',plain,
% 175.32/175.79 ( cons(s(X1),selsort(replace(zero,X2,X3))) = ifselsort(true,replace(zero,X2,cons(s(X1),X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.2.2.0','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.53.1.0',plain,
% 175.32/175.79 ( cons(s(X1),selsort(replace(zero,X2,X3))) = ifselsort(true,replace(zero,X2,cons(s(X1),X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.53.0.0']),
% 175.32/175.79 [weight('<179,34,2,[0,0,0,2]>')]).
% 175.32/175.79 cnf('0.53.2.0',plain,
% 175.32/175.79 ( ifselsort(true,replace(zero,X1,cons(s(X2),X3))) = cons(s(X2),selsort(replace(zero,X1,X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.53.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_53]).
% 175.32/175.79 cnf('0.59.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.35.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.59.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.59.0.0']),
% 175.32/175.79 [weight('<197,35,34,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.59.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.59.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_59]).
% 175.32/175.79 cnf('0.60.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(X1))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.49.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.60.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(X1))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.60.0.0']),
% 175.32/175.79 [weight('<197,49,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.60.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) = selsort(cons(s(s(s(X1))),nil)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.60.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_60]).
% 175.32/175.79 cnf('0.63.0.0',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.1.2.0','0.4.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.4','L')]).
% 175.32/175.79 cnf('0.63.1.0',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.63.0.0']),
% 175.32/175.79 [weight('<?,4,1,[0,0,0,4]>')]).
% 175.32/175.79 cnf('0.63.2.0',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 175.32/175.79 inference(activate,[status(thm)],['0.63.1.0']),
% 175.32/175.79 [equation_1]).
% 175.32/175.79 cnf('0.63.2.1',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,false1,X1,ifselsort(false,cons(X2,X3))) ),
% 175.32/175.79 inference(instr,[status(thm)],['0.63.2.0',theory(equality)])).
% 175.32/175.79 cnf('0.72.0.0',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(s(X2),X3))) = ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.9.2.0','0.18.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.72.1.0',plain,
% 175.32/175.79 ( min(cons(s(X1),cons(s(X2),X3))) = ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.72.0.0']),
% 175.32/175.79 [weight('<239,18,9,[0,0,0,1]>')]).
% 175.32/175.79 cnf('0.72.2.0',plain,
% 175.32/175.79 ( ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) = min(cons(s(X1),cons(s(X2),X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.72.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_71]).
% 175.32/175.79 cnf('0.73.0.0',plain,
% 175.32/175.79 ( min(cons(s(zero),cons(s(X1),X2))) = ifmin(true,cons(s(zero),cons(s(X1),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.72.2.0','0.17.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.73.0.1',plain,
% 175.32/175.79 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.73.0.0','0.8.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.73.1.0',plain,
% 175.32/175.79 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.73.0.1']),
% 175.32/175.79 [weight('<125,72,17,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.73.2.0',plain,
% 175.32/175.79 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.73.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_72]).
% 175.32/175.79 cnf('0.74.0.0',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(zero),X2))) = ifmin(false,cons(s(s(X1)),cons(s(zero),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.72.2.0','0.14.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.74.0.1',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.74.0.0','0.7.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.74.1.0',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.74.0.1']),
% 175.32/175.79 [weight('<149,72,14,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.74.2.0',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.74.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_73]).
% 175.32/175.79 cnf('0.75.0.0',plain,
% 175.32/175.79 ( replace(s(X1),X2,cons(s(X3),X4)) = ifrepl(eq(X1,X3),s(X1),X2,cons(s(X3),X4)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.20.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.75.1.0',plain,
% 175.32/175.79 ( replace(s(X1),X2,cons(s(X3),X4)) = ifrepl(eq(X1,X3),s(X1),X2,cons(s(X3),X4)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.75.0.0']),
% 175.32/175.79 [weight('<239,20,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.75.2.0',plain,
% 175.32/175.79 ( ifrepl(eq(X1,X2),s(X1),X3,cons(s(X2),X4)) = replace(s(X1),X3,cons(s(X2),X4)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.75.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_74]).
% 175.32/175.79 cnf('0.93.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.60.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.93.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.93.0.0']),
% 175.32/175.79 [weight('<239,60,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.93.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) = selsort(cons(s(s(s(s(X1)))),nil)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.93.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_92]).
% 175.32/175.79 cnf('0.94.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(zero)))),nil)) = ifselsort(true,cons(s(s(s(s(zero)))),nil)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.93.2.0','0.13.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.94.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),selsort(nil)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.94.0.0','0.2.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.94.0.2',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.94.0.1','0.15.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2','L')]).
% 175.32/175.79 cnf('0.94.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.94.0.2']),
% 175.32/175.79 [weight('<143,93,13,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.94.2.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.94.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_93]).
% 175.32/175.79 cnf('0.95.0.0',plain,
% 175.32/175.79 ( min(cons(s(zero),replace(zero,X1,X2))) = min(cons(s(zero),replace(zero,X1,cons(s(X3),X2)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.73.2.0','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.95.0.1',plain,
% 175.32/175.79 ( min(replace(zero,X1,cons(s(zero),X2))) = min(cons(s(zero),replace(zero,X1,cons(s(X3),X2)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.95.0.0','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.95.0.2',plain,
% 175.32/175.79 ( min(replace(zero,X1,cons(s(zero),X2))) = min(replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.95.0.1','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.95.1.0',plain,
% 175.32/175.79 ( min(replace(zero,X1,cons(s(zero),X2))) = min(replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.95.0.2']),
% 175.32/175.79 [weight('<239,73,34,[1,0,0,4]>')]).
% 175.32/175.79 cnf('0.95.2.0',plain,
% 175.32/175.79 ( min(replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) = min(replace(zero,X1,cons(s(zero),X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.95.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_94]).
% 175.32/175.79 cnf('0.112.0.0',plain,
% 175.32/175.79 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(interreduction_right,[status(thm)],['0.4.2.0'])).
% 175.32/175.79 cnf('0.112.1.0',plain,
% 175.32/175.79 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.112.0.0']),
% 175.32/175.79 [weight('<265,4,63,[0,0,0,0]>')]).
% 175.32/175.79 cnf('0.112.1.1',plain,
% 175.32/175.79 ( ifrepl(true,false1,min(cons(X1,X2)),ifselsort(false,cons(X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.112.1.0','0.63.2.1',theory(equality)]),
% 175.32/175.79 [pos('L','L')]).
% 175.32/175.79 cnf('0.112.2.0',plain,
% 175.32/175.79 ( ifrepl(true,false1,min(cons(X1,X2)),ifselsort(false,cons(X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.112.1.1',theory(equality)]),
% 175.32/175.79 [u,rule_111]).
% 175.32/175.79 cnf('0.119.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.48.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.119.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.119.0.0']),
% 175.32/175.79 [weight('<285,48,34,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.119.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.119.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_118]).
% 175.32/175.79 cnf('0.175.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.59.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.175.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.175.0.0']),
% 175.32/175.79 [weight('<335,59,34,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.175.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.175.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_174]).
% 175.32/175.79 cnf('0.176.0.0',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(s(X2)),X3))) = ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.72.2.0','0.18.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.176.1.0',plain,
% 175.32/175.79 ( min(cons(s(s(X1)),cons(s(s(X2)),X3))) = ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.176.0.0']),
% 175.32/175.79 [weight('<335,72,18,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.176.2.0',plain,
% 175.32/175.79 ( ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) = min(cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.176.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_175]).
% 175.32/175.79 cnf('0.177.0.0',plain,
% 175.32/175.79 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = ifmin(true,cons(s(s(zero)),cons(s(s(X1)),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.176.2.0','0.17.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.177.0.1',plain,
% 175.32/175.79 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.177.0.0','0.8.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.177.1.0',plain,
% 175.32/175.79 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.177.0.1']),
% 175.32/175.79 [weight('<186,176,17,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.177.2.0',plain,
% 175.32/175.79 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.177.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_176]).
% 175.32/175.79 cnf('0.180.0.0',plain,
% 175.32/175.79 ( replace(s(s(X1)),X2,cons(s(s(X3)),X4)) = ifrepl(eq(X1,X3),s(s(X1)),X2,cons(s(s(X3)),X4)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.75.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.180.1.0',plain,
% 175.32/175.79 ( replace(s(s(X1)),X2,cons(s(s(X3)),X4)) = ifrepl(eq(X1,X3),s(s(X1)),X2,cons(s(s(X3)),X4)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.180.0.0']),
% 175.32/175.79 [weight('<335,75,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.180.2.0',plain,
% 175.32/175.79 ( ifrepl(eq(X1,X2),s(s(X1)),X3,cons(s(s(X2)),X4)) = replace(s(s(X1)),X3,cons(s(s(X2)),X4)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.180.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_179]).
% 175.32/175.79 cnf('0.237.0.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.63.2.0','0.63.2.0',theory(equality)]),
% 175.32/175.79 [pos('L','L')]).
% 175.32/175.79 cnf('0.237.1.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.237.0.0']),
% 175.32/175.79 [weight('<360,63,63,[1,0,0,0]>')]).
% 175.32/175.79 cnf('0.237.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 175.32/175.79 inference(activate,[status(thm)],['0.237.1.0']),
% 175.32/175.79 [equation_2]).
% 175.32/175.79 cnf('0.237.2.1',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,false1,X2,ifselsort(false,cons(X3,X4))) ),
% 175.32/175.79 inference(instr,[status(thm)],['0.237.2.0',theory(equality)])).
% 175.32/175.79 cnf('0.237.2.2',plain,
% 175.32/175.79 ( ifrepl(true,false1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) ),
% 175.32/175.79 inference(instl,[status(thm)],['0.237.2.0',theory(equality)])).
% 175.32/175.79 cnf('0.243.0.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.237.2.0','0.112.2.0',theory(equality)]),
% 175.32/175.79 [pos('L','L')]).
% 175.32/175.79 cnf('0.243.1.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.243.0.0']),
% 175.32/175.79 [weight('<233,237,112,[1,0,0,0]>')]).
% 175.32/175.79 cnf('0.243.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.243.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_241]).
% 175.32/175.79 cnf('0.318.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(X1),replace(zero,X2,X3))) = ifselsort(eq(s(X1),min(replace(zero,X2,cons(s(X1),X3)))),cons(s(X1),replace(zero,X2,X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.19.2.0','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2.1','L')]).
% 175.32/175.79 cnf('0.318.0.1',plain,
% 175.32/175.79 ( selsort(replace(zero,X2,cons(s(X1),X3))) = ifselsort(eq(s(X1),min(replace(zero,X2,cons(s(X1),X3)))),cons(s(X1),replace(zero,X2,X3))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.318.0.0','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.318.0.2',plain,
% 175.32/175.79 ( selsort(replace(zero,X2,cons(s(X1),X3))) = ifselsort(eq(s(X1),min(replace(zero,X2,cons(s(X1),X3)))),replace(zero,X2,cons(s(X1),X3))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.318.0.1','0.34.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2','L')]).
% 175.32/175.79 cnf('0.318.1.0',plain,
% 175.32/175.79 ( selsort(replace(zero,X2,cons(s(X1),X3))) = ifselsort(eq(s(X1),min(replace(zero,X2,cons(s(X1),X3)))),replace(zero,X2,cons(s(X1),X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.318.0.2']),
% 175.32/175.79 [weight('<?,34,19,[0,0,0,4]>')]).
% 175.32/175.79 cnf('0.318.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(X1),min(replace(zero,X2,cons(s(X1),X3)))),replace(zero,X2,cons(s(X1),X3))) = selsort(replace(zero,X2,cons(s(X1),X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.318.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_316]).
% 175.32/175.79 cnf('0.472.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(zero,X5))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(X1,X5)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.119.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.472.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(zero,X5))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(X1,X5)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.472.0.0']),
% 175.32/175.79 [weight('<447,119,34,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.472.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(zero,X5))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(X1,X5)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.472.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_470]).
% 175.32/175.79 cnf('0.474.0.0',plain,
% 175.32/175.79 ( min(cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) = ifmin(le(X1,X2),cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.176.2.0','0.18.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.474.1.0',plain,
% 175.32/175.79 ( min(cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) = ifmin(le(X1,X2),cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.474.0.0']),
% 175.32/175.79 [weight('<447,176,18,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.474.2.0',plain,
% 175.32/175.79 ( ifmin(le(X1,X2),cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) = min(cons(s(s(s(X1))),cons(s(s(s(X2))),X3))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.474.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_472]).
% 175.32/175.79 cnf('0.476.0.0',plain,
% 175.32/175.79 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = ifmin(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.474.2.0','0.14.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.476.0.1',plain,
% 175.32/175.79 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.476.0.0','0.7.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.476.1.0',plain,
% 175.32/175.79 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.476.0.1']),
% 175.32/175.79 [weight('<293,474,14,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.476.2.0',plain,
% 175.32/175.79 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.476.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_474]).
% 175.32/175.79 cnf('0.478.0.0',plain,
% 175.32/175.79 ( replace(s(s(s(X1))),X2,cons(s(s(s(X3))),X4)) = ifrepl(eq(X1,X3),s(s(s(X1))),X2,cons(s(s(s(X3))),X4)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.180.2.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.478.1.0',plain,
% 175.32/175.79 ( replace(s(s(s(X1))),X2,cons(s(s(s(X3))),X4)) = ifrepl(eq(X1,X3),s(s(s(X1))),X2,cons(s(s(s(X3))),X4)) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.478.0.0']),
% 175.32/175.79 [weight('<447,180,10,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.478.2.0',plain,
% 175.32/175.79 ( ifrepl(eq(X1,X2),s(s(s(X1))),X3,cons(s(s(s(X2))),X4)) = replace(s(s(s(X1))),X3,cons(s(s(s(X2))),X4)) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.478.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_476]).
% 175.32/175.79 cnf('0.479.0.0',plain,
% 175.32/175.79 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = ifrepl(true,s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.478.2.0','0.13.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.479.0.1',plain,
% 175.32/175.79 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.479.0.0','0.1.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.479.1.0',plain,
% 175.32/175.79 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.479.0.1']),
% 175.32/175.79 [weight('<207,478,13,[1,0,0,1]>')]).
% 175.32/175.79 cnf('0.479.2.0',plain,
% 175.32/175.79 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.479.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_477]).
% 175.32/175.79 cnf('0.758.0.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.34.2.0','0.175.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.758.1.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.758.0.0']),
% 175.32/175.79 [weight('<509,175,34,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.758.2.0',plain,
% 175.32/175.79 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil))))) = cons(s(X2),cons(s(X3),cons(s(X4),cons(s(X5),nil)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.758.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_754]).
% 175.32/175.79 cnf('0.884.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),X2))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X2))),cons(s(s(X1)),cons(s(zero),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.19.2.0','0.74.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.884.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),X2))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X2))),cons(s(s(X1)),cons(s(zero),X2))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.884.0.0']),
% 175.32/175.79 [weight('<531,74,19,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.884.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(X1)),min(cons(s(zero),X2))),cons(s(s(X1)),cons(s(zero),X2))) = selsort(cons(s(s(X1)),cons(s(zero),X2))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.884.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_880]).
% 175.32/175.79 cnf('0.1887.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),X2))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X2))),cons(s(s(zero)),cons(s(s(X1)),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.19.2.0','0.177.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.1887.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),X2))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X2))),cons(s(s(zero)),cons(s(s(X1)),X2))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.1887.0.0']),
% 175.32/175.79 [weight('<650,177,19,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.1887.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X1))),cons(s(s(zero)),cons(s(s(X2)),X1))) = selsort(cons(s(s(zero)),cons(s(s(X2)),X1))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.1887.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_1870]).
% 175.32/175.79 cnf('0.3859.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),X3)))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X3))),cons(s(s(X1)),cons(s(zero),cons(s(X2),X3)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.884.2.0','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.3859.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),X3)))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X3))),cons(s(s(X1)),cons(s(zero),cons(s(X2),X3)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.3859.0.0']),
% 175.32/175.79 [weight('<747,884,73,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.3859.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(X1)),min(cons(s(zero),X2))),cons(s(s(X1)),cons(s(zero),cons(s(X3),X2)))) = selsort(cons(s(s(X1)),cons(s(zero),cons(s(X3),X2)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.3859.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_3819]).
% 175.32/175.79 cnf('0.4651.0.0',plain,
% 175.32/175.79 ( selsort(replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) = ifselsort(eq(s(zero),min(replace(zero,X1,cons(s(zero),X3)))),replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.318.2.0','0.95.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.4651.1.0',plain,
% 175.32/175.79 ( selsort(replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) = ifselsort(eq(s(zero),min(replace(zero,X1,cons(s(zero),X3)))),replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.4651.0.0']),
% 175.32/175.79 [weight('<781,318,95,[1,0,0,4]>')]).
% 175.32/175.79 cnf('0.4651.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(zero),min(replace(zero,X1,cons(s(zero),X2)))),replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) = selsort(replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.4651.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_4609]).
% 175.32/175.79 cnf('0.4652.0.0',plain,
% 175.32/175.79 ( selsort(replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) = ifselsort(eq(s(zero),min(cons(s(zero),cons(s(X3),cons(s(X4),nil))))),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.4651.2.0','0.175.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2.1','L')]).
% 175.32/175.79 cnf('0.4652.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(eq(s(zero),min(cons(s(zero),cons(s(X3),cons(s(X4),nil))))),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.0','0.758.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1','L')]).
% 175.32/175.79 cnf('0.4652.0.2',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(eq(s(zero),min(cons(s(zero),cons(s(X4),nil)))),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.1','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1.2','L')]).
% 175.32/175.79 cnf('0.4652.0.3',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(eq(s(zero),min(cons(s(zero),nil))),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.2','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1.2','L')]).
% 175.32/175.79 cnf('0.4652.0.4',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(eq(s(zero),s(zero)),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.3','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1.2','L')]).
% 175.32/175.79 cnf('0.4652.0.5',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(eq(zero,zero),replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.4','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.4652.0.6',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = ifselsort(true,replace(zero,X1,cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.5','0.13.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.4652.0.7',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = cons(s(zero),selsort(replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.6','0.53.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.4652.0.8',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = cons(s(zero),selsort(cons(s(X2),cons(s(X3),cons(s(X4),nil))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.4652.0.7','0.175.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.1','L')]).
% 175.32/175.79 cnf('0.4652.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X2),cons(s(X3),cons(s(X4),nil))))) = cons(s(zero),selsort(cons(s(X2),cons(s(X3),cons(s(X4),nil))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.4652.0.8']),
% 175.32/175.79 [weight('<434,4651,175,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.4652.2.0',plain,
% 175.32/175.79 ( selsort(cons(s(zero),cons(s(X1),cons(s(X2),cons(s(X3),nil))))) = cons(s(zero),selsort(cons(s(X1),cons(s(X2),cons(s(X3),nil))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.4652.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_4610]).
% 175.32/175.79 cnf('0.13136.0.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = ifrepl(true,X3,min(cons(s(s(s(zero))),X2)),ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.243.2.0','0.476.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.3','L')]).
% 175.32/175.79 cnf('0.13136.1.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = ifrepl(true,X3,min(cons(s(s(s(zero))),X2)),ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13136.0.0']),
% 175.32/175.79 [weight('<974,476,243,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.13136.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,min(cons(s(s(s(zero))),X2)),ifselsort(false,cons(s(s(s(s(X3)))),cons(s(s(s(zero))),X2)))) = ifselsort(false,cons(s(s(s(s(X3)))),cons(s(s(s(zero))),X2))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13136.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_13016]).
% 175.32/175.79 cnf('0.13137.0.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifrepl(true,X2,s(s(s(zero))),ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.13136.2.0','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.3','L')]).
% 175.32/175.79 cnf('0.13137.1.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifrepl(true,X2,s(s(s(zero))),ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13137.0.0']),
% 175.32/175.79 [weight('<791,13136,5,[1,0,0,3]>')]).
% 175.32/175.79 cnf('0.13137.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,s(s(s(zero))),ifselsort(false,cons(s(s(s(s(X2)))),cons(s(s(s(zero))),nil)))) = ifselsort(false,cons(s(s(s(s(X2)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13137.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_13017]).
% 175.32/175.79 cnf('0.13138.0.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(replace(min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))),s(s(s(s(X1)))),cons(s(s(s(zero))),nil)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.13137.2.0','0.63.2.0',theory(equality)]),
% 175.32/175.79 [pos('L','R')]).
% 175.32/175.79 cnf('0.13138.0.1',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(replace(min(cons(s(s(s(zero))),nil)),s(s(s(s(X1)))),cons(s(s(s(zero))),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13138.0.0','0.476.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.1.1','L')]).
% 175.32/175.79 cnf('0.13138.0.2',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(replace(s(s(s(zero))),s(s(s(s(X1)))),cons(s(s(s(zero))),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13138.0.1','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.1.1','L')]).
% 175.32/175.79 cnf('0.13138.0.3',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13138.0.2','0.479.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.1','L')]).
% 175.32/175.79 cnf('0.13138.1.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13138.0.3']),
% 175.32/175.79 [weight('<419,13137,63,[1,0,1,0]>')]).
% 175.32/175.79 cnf('0.13138.2.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13138.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_13018]).
% 175.32/175.79 cnf('0.13163.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X3)))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X3))),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X3)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.1887.2.0','0.177.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.13163.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X3)))) = ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X3))),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),X3)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13163.0.0']),
% 175.32/175.79 [weight('<974,1887,177,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.13163.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(zero)),min(cons(s(s(zero)),X1))),cons(s(s(zero)),cons(s(s(X2)),cons(s(s(X3)),X1)))) = selsort(cons(s(s(zero)),cons(s(s(X2)),cons(s(s(X3)),X1)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13163.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_13043]).
% 175.32/175.79 cnf('0.13164.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = ifselsort(eq(s(s(zero)),s(s(zero))),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.13163.2.0','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.13164.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = ifselsort(eq(s(zero),s(zero)),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13164.0.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.13164.0.2',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = ifselsort(eq(zero,zero),cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13164.0.1','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.13164.0.3',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = ifselsort(true,cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13164.0.2','0.13.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.13164.0.4',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = cons(s(s(zero)),selsort(cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.13164.0.3','0.2.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.13164.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = cons(s(s(zero)),selsort(cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.13164.0.4']),
% 175.32/175.79 [weight('<434,13163,5,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.13164.2.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(zero)),cons(s(s(X1)),cons(s(s(X2)),nil)))) = cons(s(s(zero)),selsort(cons(s(s(X1)),cons(s(s(X2)),nil)))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.13164.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_13044]).
% 175.32/175.79 cnf('0.14130.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X4))))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X4))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X4))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.3859.2.0','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.14130.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X4))))) = ifselsort(eq(s(s(X1)),min(cons(s(zero),X4))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),X4))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.14130.0.0']),
% 175.32/175.79 [weight('<999,3859,73,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.14130.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(X1)),min(cons(s(zero),X2))),cons(s(s(X1)),cons(s(zero),cons(s(X3),cons(s(X4),X2))))) = selsort(cons(s(s(X1)),cons(s(zero),cons(s(X3),cons(s(X4),X2))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.14130.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_14009]).
% 175.32/175.79 cnf('0.21515.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = ifselsort(eq(s(s(s(s(X1)))),min(cons(s(s(s(zero))),X2))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.19.2.0','0.476.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.21515.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = ifselsort(eq(s(s(s(s(X1)))),min(cons(s(s(s(zero))),X2))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.21515.0.0']),
% 175.32/175.79 [weight('<1079,476,19,[0,0,0,3]>')]).
% 175.32/175.79 cnf('0.21515.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(s(s(X1)))),min(cons(s(s(s(zero))),X2))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.21515.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_21370]).
% 175.32/175.79 cnf('0.21516.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(s(s(X1)))),s(s(s(zero)))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.21515.2.0','0.5.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.21516.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(s(X1))),s(s(zero))),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.21516.0.0','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.21516.0.2',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(s(X1)),s(zero)),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.21516.0.1','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.21516.0.3',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifselsort(eq(s(X1),zero),cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.21516.0.2','0.10.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.21516.0.4',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = ifselsort(false,cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.21516.0.3','0.11.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.21516.0.5',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.21516.0.4','0.13138.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.21516.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.21516.0.5']),
% 175.32/175.79 [weight('<377,21515,5,[1,0,0,7]>')]).
% 175.32/175.79 cnf('0.21516.2.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),nil))) = cons(s(s(s(zero))),selsort(cons(s(s(s(s(X1)))),nil))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.21516.1.0',theory(equality)]),
% 175.32/175.79 [u,rule_21371]).
% 175.32/175.79 cnf('0.27248.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X4)))))) = ifselsort(eq(s(s(X1)),min(cons(zero,X4))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X4)))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.14130.2.0','0.30.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.27248.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X4)))))) = ifselsort(eq(s(s(X1)),min(cons(zero,X4))),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,X4)))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27248.0.0']),
% 175.32/175.79 [weight('<1117,14130,30,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.27248.2.0',plain,
% 175.32/175.79 ( ifselsort(eq(s(s(X1)),min(cons(zero,X2))),cons(s(s(X1)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,X2)))))) = selsort(cons(s(s(X1)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,X2)))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27248.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_27071]).
% 175.32/175.79 cnf('0.27249.0.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifselsort(eq(s(s(X1)),zero),cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.27248.2.0','0.6.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.1.2','L')]).
% 175.32/175.79 cnf('0.27249.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifselsort(false,cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27249.0.0','0.11.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.1','L')]).
% 175.32/175.79 cnf('0.27249.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifselsort(false,cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27249.0.1']),
% 175.32/175.79 [weight('<683,27248,6,[1,0,0,5]>')]).
% 175.32/175.79 cnf('0.27249.2.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27249.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_27072]).
% 175.32/175.79 cnf('0.27250.0.0',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil)))))),s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.63.2.0','0.27249.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.4','L')]).
% 175.32/175.79 cnf('0.27250.0.1',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))),s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.0','0.74.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1.1','L')]).
% 175.32/175.79 cnf('0.27250.0.2',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(s(zero),cons(s(X4),cons(zero,nil)))),s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.1','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1.1','L')]).
% 175.32/175.79 cnf('0.27250.0.3',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(s(zero),cons(zero,nil))),s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.2','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1.1','L')]).
% 175.32/175.79 cnf('0.27250.0.4',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(min(cons(zero,nil)),s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.3','0.30.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1.1','L')]).
% 175.32/175.79 cnf('0.27250.0.5',plain,
% 175.32/175.79 ( cons(X1,selsort(replace(zero,s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.4','0.6.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1.1','L')]).
% 175.32/175.79 cnf('0.27250.0.6',plain,
% 175.32/175.79 ( cons(X1,selsort(cons(s(zero),cons(s(X3),cons(s(X4),cons(s(s(X2)),nil)))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.5','0.472.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.1','L')]).
% 175.32/175.79 cnf('0.27250.0.7',plain,
% 175.32/175.79 ( cons(X1,cons(s(zero),selsort(cons(s(X3),cons(s(X4),cons(s(s(X2)),nil)))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27250.0.6','0.4652.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.27250.1.0',plain,
% 175.32/175.79 ( cons(X1,cons(s(zero),selsort(cons(s(X3),cons(s(X4),cons(s(s(X2)),nil)))))) = ifrepl(true,X5,X1,selsort(cons(s(s(X2)),cons(s(zero),cons(s(X3),cons(s(X4),cons(zero,nil))))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27250.0.7']),
% 175.32/175.79 [weight('<857,27249,63,[0,0,1,4]>')]).
% 175.32/175.79 cnf('0.27250.2.0',plain,
% 175.32/175.79 ( ifrepl(true,X1,X2,selsort(cons(s(s(X3)),cons(s(zero),cons(s(X4),cons(s(X5),cons(zero,nil))))))) = cons(X2,cons(s(zero),selsort(cons(s(X4),cons(s(X5),cons(s(s(X3)),nil)))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27250.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_27073]).
% 175.32/175.79 cnf('0.27251.0.0',plain,
% 175.32/175.79 ( ifselsort(false,cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.243.2.0','0.27249.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.4','L')]).
% 175.32/175.79 cnf('0.27251.0.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.0','0.27249.2.0',theory(equality)]),
% 175.32/175.79 [pos('L','L')]).
% 175.32/175.79 cnf('0.27251.0.2',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.1','0.74.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.3','L')]).
% 175.32/175.79 cnf('0.27251.0.3',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(s(zero),cons(s(X3),cons(zero,nil)))),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.2','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.3','L')]).
% 175.32/175.79 cnf('0.27251.0.4',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(s(zero),cons(zero,nil))),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.3','0.73.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.3','L')]).
% 175.32/175.79 cnf('0.27251.0.5',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,min(cons(zero,nil)),selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.4','0.30.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.3','L')]).
% 175.32/175.79 cnf('0.27251.0.6',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,zero,selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.0.5','0.6.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.3','L')]).
% 175.32/175.79 cnf('0.27251.1.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = ifrepl(true,X4,zero,selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil))))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27251.0.6']),
% 175.32/175.79 [weight('<857,27249,243,[0,0,0,7]>')]).
% 175.32/175.79 cnf('0.27251.1.1',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = cons(zero,cons(s(zero),selsort(cons(s(X2),cons(s(X3),cons(s(s(X1)),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27251.1.0','0.27250.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.27251.2.0',plain,
% 175.32/175.79 ( selsort(cons(s(s(X1)),cons(s(zero),cons(s(X2),cons(s(X3),cons(zero,nil)))))) = cons(zero,cons(s(zero),selsort(cons(s(X2),cons(s(X3),cons(s(s(X1)),nil)))))) ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27251.1.1',theory(equality)]),
% 175.32/175.79 [u,rule_27074]).
% 175.32/175.79 cnf('0.27252.0.0',plain,
% 175.32/175.79 ( false1 = eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),selsort(cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(s(s(X1)),nil))))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.22.2.0','0.27251.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2','L')]).
% 175.32/175.79 cnf('0.27252.0.1',plain,
% 175.32/175.79 ( false1 = eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),cons(s(s(zero)),selsort(cons(s(s(s(s(zero)))),cons(s(s(X1)),nil))))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27252.0.0','0.13164.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.2.2','L')]).
% 175.32/175.79 cnf('0.27252.1.0',plain,
% 175.32/175.79 ( false1 = eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),cons(s(s(zero)),selsort(cons(s(s(s(s(zero)))),cons(s(s(X1)),nil))))))) ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27252.0.1']),
% 175.32/175.79 [weight('<294,27251,22,[0,0,0,22]>')]).
% 175.32/175.79 cnf('0.27252.2.0',plain,
% 175.32/175.79 ( eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),cons(s(s(zero)),selsort(cons(s(s(s(s(zero)))),cons(s(s(X1)),nil))))))) = false1 ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27252.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_27075]).
% 175.32/175.79 cnf('0.27253.0.0',plain,
% 175.32/175.79 ( false1 = eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),selsort(cons(s(s(s(s(zero)))),nil))))))) ),
% 175.32/175.79 inference(cp,[status(thm)],['0.27252.2.0','0.21516.2.0',theory(equality)]),
% 175.32/175.79 [pos('L.2.2.2.2','L')]).
% 175.32/175.79 cnf('0.27253.0.1',plain,
% 175.32/175.79 ( false1 = eq1(cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))),cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil)))))) ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27253.0.0','0.94.2.0',theory(equality)]),
% 175.32/175.79 [pos('R.2.2.2.2.2','L')]).
% 175.32/175.79 cnf('0.27253.0.2',plain,
% 175.32/175.79 ( false1 = true1 ),
% 175.32/175.79 inference(reduction,[status(thm)],['0.27253.0.1','0.21.2.0',theory(equality)]),
% 175.32/175.79 [pos('R','L')]).
% 175.32/175.79 cnf('0.27253.1.0',plain,
% 175.32/175.79 ( false1 = true1 ),
% 175.32/175.79 inference(weigh,[status(thm)],['0.27253.0.2']),
% 175.32/175.79 [weight('<5,27252,21516,[1,0,0,31]>')]).
% 175.32/175.79 cnf('0.27253.2.0',plain,
% 175.32/175.79 ( true1 = false1 ),
% 175.32/175.79 inference(orient,[status(thm)],['0.27253.1.0',theory(equality)]),
% 175.32/175.79 [x,rule_27076]).
% 175.32/175.79 cnf('1.0.0.0',conjecture,
% 175.32/175.79 ( true1 = false1 ),
% 175.32/175.79 file('/tmp/WALDMEISTER_20968_n004',conjecture_1)).
% 175.32/175.79 cnf('1.0.0.1',plain,
% 175.32/175.79 ( false1 = false1 ),
% 175.32/175.79 inference(reduction,[status(thm)],['1.0.0.0','0.27253.2.0',theory(equality)]),
% 175.32/175.79 [pos('L','L')]).
% 175.32/175.79 cnf('1.0.0.2',plain,
% 175.32/175.79 ( $true ),
% 175.32/175.79 inference(trivial,[status(thm)],['1.0.0.1',theory(equality)]),
% 175.32/175.79 [conjecture_1]).
% 175.32/175.79
% 175.32/175.79 Proved Goals:
% 175.32/175.79 No. 1: true ?= false, current false1 ?= false1
% 175.32/175.79 using narrowing to prove cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?= selsort(cons(x1,cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil))))))
% 175.32/175.79
% 175.32/175.79 1 goal was specified, which was proved.
% 175.32/175.79 % SZS output end CNFRefutation
% 175.32/175.79 #END OF PROOF
% 175.32/175.79
% 175.32/175.79 Problem WALDMEISTER_20968_n004
% 175.32/175.79 CPs.gen 17767448
% 175.32/175.79 CPs.reexp 0
% 175.32/175.79 Select 63822
% 175.32/175.79 R 27076
% 175.32/175.79 E 177
% 175.32/175.79 vsize 41.6M
% 175.32/175.79 rss 39.9M
% 175.32/175.79 process.time 174.823s
% 175.32/175.79 wallclock.time 174.823s
% 175.32/175.79 status S
% 175.32/175.79
% 175.32/175.79
% 175.32/175.79 Waldmeister states: Goal proved.
% 175.32/175.79 % SZS status Unsatisfiable
%------------------------------------------------------------------------------