%------------------------------------------------------------------------------
% File : Waldmeister---710
% Problem : DAT436-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : woody %s
% Computer : n013.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 184.39s 184.86s
% Output : CNFRefutation 184.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : DAT436-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : woody %s
% 0.16/0.33 % Computer : n013.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 20:56:11 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.52/0.93 ********************************************************************************
% 0.52/0.93 * W A L D M E I S T E R \| \ / \|/ *
% 0.52/0.93 * |/ | \/ | *
% 0.52/0.93 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / *
% 0.52/0.93 * A. Jaeger and B. Loechner | | *
% 0.52/0.93 * <waldmeister@informatik.uni-kl.de> | *
% 0.52/0.93 ********************************************************************************
% 0.52/0.93
% 0.52/0.93
% 0.52/0.93 Goals:
% 0.52/0.93 ------
% 0.52/0.93
% 0.52/0.93 ( 1) cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?=? selsort(cons(s^3(zero),cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil))))))
% 0.52/0.93
% 0.52/0.93 Detected structure: Orkus
% 0.52/0.93 ********************************************************************************
% 0.52/0.93 ****************************** COMPLETION - PROOF ******************************
% 0.52/0.93 ********************************************************************************
% 0.52/0.93
% 184.39/184.86 joined goal: 1 cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?= selsort(cons(s^3(zero),cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil)))))) to cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil)))))
% 184.39/184.86 goal joined
% 184.39/184.86 % SZS status Unsatisfiable
% 184.39/184.86 #START OF PROOF
% 184.39/184.86 % SZS output start CNFRefutation
% 184.39/184.86 cnf('0.1.0.0',axiom,
% 184.39/184.86 ( cons(X1,X2) = ifrepl(true,X3,X1,cons(X4,X2)) ),
% 184.39/184.86 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.86 cnf('0.1.1.0',plain,
% 184.39/184.86 ( cons(X1,X2) = ifrepl(true,X3,X1,cons(X4,X2)) ),
% 184.39/184.86 inference(weigh,[status(thm)],['0.1.0.0']),
% 184.39/184.86 [weight('<0,0,0,[0,0,0,1]>')]).
% 184.39/184.86 cnf('0.1.2.0',plain,
% 184.39/184.86 ( ifrepl(true,X1,X2,cons(X3,X4)) = cons(X2,X4) ),
% 184.39/184.86 inference(orient,[status(thm)],['0.1.1.0',theory(equality)]),
% 184.39/184.86 [x,rule_1]).
% 184.39/184.86 cnf('0.2.0.0',axiom,
% 184.39/184.86 ( cons(X1,selsort(X2)) = ifselsort(true,cons(X1,X2)) ),
% 184.39/184.86 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.86 cnf('0.2.1.0',plain,
% 184.39/184.86 ( cons(X1,selsort(X2)) = ifselsort(true,cons(X1,X2)) ),
% 184.39/184.86 inference(weigh,[status(thm)],['0.2.0.0']),
% 184.39/184.86 [weight('<1,0,0,[0,0,0,2]>')]).
% 184.39/184.86 cnf('0.2.2.0',plain,
% 184.39/184.86 ( ifselsort(true,cons(X1,X2)) = cons(X1,selsort(X2)) ),
% 184.39/184.86 inference(orient,[status(thm)],['0.2.1.0',theory(equality)]),
% 184.39/184.86 [x,rule_2]).
% 184.39/184.86 cnf('0.3.0.0',axiom,
% 184.39/184.86 ( cons(X1,replace(X2,X3,X4)) = ifrepl(false,X2,X3,cons(X1,X4)) ),
% 184.39/184.86 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.86 cnf('0.3.1.0',plain,
% 184.39/184.87 ( cons(X1,replace(X2,X3,X4)) = ifrepl(false,X2,X3,cons(X1,X4)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.3.0.0']),
% 184.39/184.87 [weight('<2,0,0,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.3.2.0',plain,
% 184.39/184.87 ( ifrepl(false,X1,X2,cons(X3,X4)) = cons(X3,replace(X1,X2,X4)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.3.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_3]).
% 184.39/184.87 cnf('0.4.0.0',axiom,
% 184.39/184.87 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.4.1.0',plain,
% 184.39/184.87 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.4.0.0']),
% 184.39/184.87 [weight('<3,0,0,[0,0,0,4]>')]).
% 184.39/184.87 cnf('0.4.2.0',plain,
% 184.39/184.87 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.4.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_4]).
% 184.39/184.87 cnf('0.5.0.0',axiom,
% 184.39/184.87 ( s(X1) = min(cons(s(X1),nil)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.5.1.0',plain,
% 184.39/184.87 ( s(X1) = min(cons(s(X1),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.5.0.0']),
% 184.39/184.87 [weight('<4,0,0,[0,0,0,5]>')]).
% 184.39/184.87 cnf('0.5.2.0',plain,
% 184.39/184.87 ( min(cons(s(X1),nil)) = s(X1) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.5.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_5]).
% 184.39/184.87 cnf('0.6.0.0',axiom,
% 184.39/184.87 ( zero = min(cons(zero,nil)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.6.1.0',plain,
% 184.39/184.87 ( zero = min(cons(zero,nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.6.0.0']),
% 184.39/184.87 [weight('<5,0,0,[0,0,0,6]>')]).
% 184.39/184.87 cnf('0.6.2.0',plain,
% 184.39/184.87 ( min(cons(zero,nil)) = zero ),
% 184.39/184.87 inference(orient,[status(thm)],['0.6.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_6]).
% 184.39/184.87 cnf('0.7.0.0',axiom,
% 184.39/184.87 ( min(cons(X1,X2)) = ifmin(false,cons(X3,cons(X1,X2))) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.7.1.0',plain,
% 184.39/184.87 ( min(cons(X1,X2)) = ifmin(false,cons(X3,cons(X1,X2))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.7.0.0']),
% 184.39/184.87 [weight('<6,0,0,[0,0,0,7]>')]).
% 184.39/184.87 cnf('0.7.2.0',plain,
% 184.39/184.87 ( ifmin(false,cons(X1,cons(X2,X3))) = min(cons(X2,X3)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.7.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_7]).
% 184.39/184.87 cnf('0.8.0.0',axiom,
% 184.39/184.87 ( min(cons(X1,X2)) = ifmin(true,cons(X1,cons(X3,X2))) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.8.1.0',plain,
% 184.39/184.87 ( min(cons(X1,X2)) = ifmin(true,cons(X1,cons(X3,X2))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.8.0.0']),
% 184.39/184.87 [weight('<7,0,0,[0,0,0,8]>')]).
% 184.39/184.87 cnf('0.8.2.0',plain,
% 184.39/184.87 ( ifmin(true,cons(X1,cons(X2,X3))) = min(cons(X1,X3)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.8.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_8]).
% 184.39/184.87 cnf('0.9.0.0',axiom,
% 184.39/184.87 ( min(cons(X1,cons(X2,X3))) = ifmin(le(X1,X2),cons(X1,cons(X2,X3))) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.9.1.0',plain,
% 184.39/184.87 ( min(cons(X1,cons(X2,X3))) = ifmin(le(X1,X2),cons(X1,cons(X2,X3))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.9.0.0']),
% 184.39/184.87 [weight('<8,0,0,[0,0,0,9]>')]).
% 184.39/184.87 cnf('0.9.2.0',plain,
% 184.39/184.87 ( ifmin(le(X1,X2),cons(X1,cons(X2,X3))) = min(cons(X1,cons(X2,X3))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.9.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_9]).
% 184.39/184.87 cnf('0.10.0.0',axiom,
% 184.39/184.87 ( eq(X1,X2) = eq(s(X1),s(X2)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.10.1.0',plain,
% 184.39/184.87 ( eq(X1,X2) = eq(s(X1),s(X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.10.0.0']),
% 184.39/184.87 [weight('<9,0,0,[0,0,0,10]>')]).
% 184.39/184.87 cnf('0.10.2.0',plain,
% 184.39/184.87 ( eq(s(X1),s(X2)) = eq(X1,X2) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.10.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_10]).
% 184.39/184.87 cnf('0.11.0.0',axiom,
% 184.39/184.87 ( eq(s(X1),zero) = false ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.11.1.0',plain,
% 184.39/184.87 ( eq(s(X1),zero) = false ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.11.0.0']),
% 184.39/184.87 [weight('<10,0,0,[0,0,0,11]>')]).
% 184.39/184.87 cnf('0.11.2.0',plain,
% 184.39/184.87 ( eq(s(X1),zero) = false ),
% 184.39/184.87 inference(orient,[status(thm)],['0.11.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_11]).
% 184.39/184.87 cnf('0.12.0.0',axiom,
% 184.39/184.87 ( eq(zero,s(X1)) = false ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.12.1.0',plain,
% 184.39/184.87 ( eq(zero,s(X1)) = false ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.12.0.0']),
% 184.39/184.87 [weight('<11,0,0,[0,0,0,12]>')]).
% 184.39/184.87 cnf('0.12.2.0',plain,
% 184.39/184.87 ( eq(zero,s(X1)) = false ),
% 184.39/184.87 inference(orient,[status(thm)],['0.12.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_12]).
% 184.39/184.87 cnf('0.13.0.0',axiom,
% 184.39/184.87 ( eq(zero,zero) = true ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.13.1.0',plain,
% 184.39/184.87 ( eq(zero,zero) = true ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13.0.0']),
% 184.39/184.87 [weight('<12,0,0,[0,0,0,13]>')]).
% 184.39/184.87 cnf('0.13.2.0',plain,
% 184.39/184.87 ( eq(zero,zero) = true ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_13]).
% 184.39/184.87 cnf('0.14.0.0',axiom,
% 184.39/184.87 ( false = le(s(X1),zero) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.14.1.0',plain,
% 184.39/184.87 ( false = le(s(X1),zero) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.14.0.0']),
% 184.39/184.87 [weight('<13,0,0,[0,0,0,14]>')]).
% 184.39/184.87 cnf('0.14.2.0',plain,
% 184.39/184.87 ( le(s(X1),zero) = false ),
% 184.39/184.87 inference(orient,[status(thm)],['0.14.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_14]).
% 184.39/184.87 cnf('0.15.0.0',axiom,
% 184.39/184.87 ( nil = selsort(nil) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.15.1.0',plain,
% 184.39/184.87 ( nil = selsort(nil) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.15.0.0']),
% 184.39/184.87 [weight('<14,0,0,[0,0,0,15]>')]).
% 184.39/184.87 cnf('0.15.2.0',plain,
% 184.39/184.87 ( selsort(nil) = nil ),
% 184.39/184.87 inference(orient,[status(thm)],['0.15.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_15]).
% 184.39/184.87 cnf('0.16.0.0',axiom,
% 184.39/184.87 ( nil = replace(X1,X2,nil) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.16.1.0',plain,
% 184.39/184.87 ( nil = replace(X1,X2,nil) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.16.0.0']),
% 184.39/184.87 [weight('<15,0,0,[0,0,0,16]>')]).
% 184.39/184.87 cnf('0.16.2.0',plain,
% 184.39/184.87 ( replace(X1,X2,nil) = nil ),
% 184.39/184.87 inference(orient,[status(thm)],['0.16.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_16]).
% 184.39/184.87 cnf('0.17.0.0',axiom,
% 184.39/184.87 ( true = le(zero,X1) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.17.1.0',plain,
% 184.39/184.87 ( true = le(zero,X1) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.17.0.0']),
% 184.39/184.87 [weight('<16,0,0,[0,0,0,17]>')]).
% 184.39/184.87 cnf('0.17.2.0',plain,
% 184.39/184.87 ( le(zero,X1) = true ),
% 184.39/184.87 inference(orient,[status(thm)],['0.17.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_17]).
% 184.39/184.87 cnf('0.18.0.0',axiom,
% 184.39/184.87 ( le(X1,X2) = le(s(X1),s(X2)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.18.1.0',plain,
% 184.39/184.87 ( le(X1,X2) = le(s(X1),s(X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.18.0.0']),
% 184.39/184.87 [weight('<17,0,0,[0,0,0,18]>')]).
% 184.39/184.87 cnf('0.18.2.0',plain,
% 184.39/184.87 ( le(s(X1),s(X2)) = le(X1,X2) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.18.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_18]).
% 184.39/184.87 cnf('0.19.0.0',axiom,
% 184.39/184.87 ( selsort(cons(X1,X2)) = ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.19.1.0',plain,
% 184.39/184.87 ( selsort(cons(X1,X2)) = ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.19.0.0']),
% 184.39/184.87 [weight('<18,0,0,[0,0,0,19]>')]).
% 184.39/184.87 cnf('0.19.2.0',plain,
% 184.39/184.87 ( ifselsort(eq(X1,min(cons(X1,X2))),cons(X1,X2)) = selsort(cons(X1,X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.19.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_19]).
% 184.39/184.87 cnf('0.20.0.0',axiom,
% 184.39/184.87 ( replace(X1,X2,cons(X3,X4)) = ifrepl(eq(X1,X3),X1,X2,cons(X3,X4)) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013')).
% 184.39/184.87 cnf('0.20.1.0',plain,
% 184.39/184.87 ( replace(X1,X2,cons(X3,X4)) = ifrepl(eq(X1,X3),X1,X2,cons(X3,X4)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.20.0.0']),
% 184.39/184.87 [weight('<19,0,0,[0,0,0,20]>')]).
% 184.39/184.87 cnf('0.20.2.0',plain,
% 184.39/184.87 ( ifrepl(eq(X1,X2),X1,X3,cons(X2,X4)) = replace(X1,X3,cons(X2,X4)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.20.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_20]).
% 184.39/184.87 cnf('0.22.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(zero,X2)) = ifrepl(true,zero,X1,cons(zero,X2)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.20.2.0','0.13.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.22.0.1',plain,
% 184.39/184.87 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.22.0.0','0.1.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.22.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.22.0.1']),
% 184.39/184.87 [weight('<69,20,13,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.22.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(zero,X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.22.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_22]).
% 184.39/184.87 cnf('0.28.0.0',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(zero,X2))) = ifmin(false,cons(s(X1),cons(zero,X2))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.9.2.0','0.14.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.28.0.1',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.28.0.0','0.7.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.28.1.0',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.28.0.1']),
% 184.39/184.87 [weight('<95,14,9,[0,0,0,1]>')]).
% 184.39/184.87 cnf('0.28.2.0',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(zero,X2))) = min(cons(zero,X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.28.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_28]).
% 184.39/184.87 cnf('0.32.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),X3)) = ifrepl(false,zero,X1,cons(s(X2),X3)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.20.2.0','0.12.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.32.0.1',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),X3)) = cons(s(X2),replace(zero,X1,X3)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.32.0.0','0.3.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.32.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),X3)) = cons(s(X2),replace(zero,X1,X3)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.32.0.1']),
% 184.39/184.87 [weight('<119,20,12,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.32.2.0',plain,
% 184.39/184.87 ( cons(s(X1),replace(zero,X2,X3)) = replace(zero,X2,cons(s(X1),X3)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.32.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_32]).
% 184.39/184.87 cnf('0.33.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.16.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.33.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.33.0.0']),
% 184.39/184.87 [weight('<95,32,16,[1,0,0,3]>')]).
% 184.39/184.87 cnf('0.33.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),nil)) = cons(s(X2),nil) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.33.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_33]).
% 184.39/184.87 cnf('0.34.0.0',plain,
% 184.39/184.87 ( selsort(cons(s(X1),nil)) = ifselsort(eq(s(X1),s(X1)),cons(s(X1),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.19.2.0','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.34.0.1',plain,
% 184.39/184.87 ( selsort(cons(s(X1),nil)) = ifselsort(eq(X1,X1),cons(s(X1),nil)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.34.0.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.34.1.0',plain,
% 184.39/184.87 ( selsort(cons(s(X1),nil)) = ifselsort(eq(X1,X1),cons(s(X1),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.34.0.1']),
% 184.39/184.87 [weight('<125,19,5,[1,0,0,3]>')]).
% 184.39/184.87 cnf('0.34.2.0',plain,
% 184.39/184.87 ( ifselsort(eq(X1,X1),cons(s(X1),nil)) = selsort(cons(s(X1),nil)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.34.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_34]).
% 184.39/184.87 cnf('0.46.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.22.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.46.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.46.0.0']),
% 184.39/184.87 [weight('<159,32,22,[1,0,0,3]>')]).
% 184.39/184.87 cnf('0.46.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(zero,X3))) = cons(s(X2),cons(X1,X3)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.46.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_46]).
% 184.39/184.87 cnf('0.47.0.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(X1)),nil)) = ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.34.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.47.1.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(X1)),nil)) = ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.47.0.0']),
% 184.39/184.87 [weight('<159,34,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.47.2.0',plain,
% 184.39/184.87 ( ifselsort(eq(X1,X1),cons(s(s(X1)),nil)) = selsort(cons(s(s(X1)),nil)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.47.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_47]).
% 184.39/184.87 cnf('0.51.0.0',plain,
% 184.39/184.87 ( cons(s(X1),selsort(replace(zero,X2,X3))) = ifselsort(true,replace(zero,X2,cons(s(X1),X3))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.2.2.0','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.51.1.0',plain,
% 184.39/184.87 ( cons(s(X1),selsort(replace(zero,X2,X3))) = ifselsort(true,replace(zero,X2,cons(s(X1),X3))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.51.0.0']),
% 184.39/184.87 [weight('<179,32,2,[0,0,0,2]>')]).
% 184.39/184.87 cnf('0.51.2.0',plain,
% 184.39/184.87 ( ifselsort(true,replace(zero,X1,cons(s(X2),X3))) = cons(s(X2),selsort(replace(zero,X1,X3))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.51.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_51]).
% 184.39/184.87 cnf('0.57.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.33.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.57.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.57.0.0']),
% 184.39/184.87 [weight('<197,33,32,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.57.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),nil))) = cons(s(X2),cons(s(X3),nil)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.57.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_57]).
% 184.39/184.87 cnf('0.58.0.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(X1))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.47.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.58.1.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(X1))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.58.0.0']),
% 184.39/184.87 [weight('<197,47,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.58.2.0',plain,
% 184.39/184.87 ( ifselsort(eq(X1,X1),cons(s(s(s(X1))),nil)) = selsort(cons(s(s(s(X1))),nil)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.58.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_58]).
% 184.39/184.87 cnf('0.62.0.0',plain,
% 184.39/184.87 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.1.2.0','0.4.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.4','L')]).
% 184.39/184.87 cnf('0.62.1.0',plain,
% 184.39/184.87 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.62.0.0']),
% 184.39/184.87 [weight('<?,4,1,[0,0,0,4]>')]).
% 184.39/184.87 cnf('0.62.2.0',plain,
% 184.39/184.87 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,X4,X1,ifselsort(false,cons(X2,X3))) ),
% 184.39/184.87 inference(activate,[status(thm)],['0.62.1.0']),
% 184.39/184.87 [equation_1]).
% 184.39/184.87 cnf('0.62.2.1',plain,
% 184.39/184.87 ( cons(X1,selsort(replace(min(cons(X2,X3)),X2,X3))) = ifrepl(true,const2,X1,ifselsort(false,cons(X2,X3))) ),
% 184.39/184.87 inference(instr,[status(thm)],['0.62.2.0',theory(equality)])).
% 184.39/184.87 cnf('0.70.0.0',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(s(X2),X3))) = ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.9.2.0','0.18.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.70.1.0',plain,
% 184.39/184.87 ( min(cons(s(X1),cons(s(X2),X3))) = ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.70.0.0']),
% 184.39/184.87 [weight('<239,18,9,[0,0,0,1]>')]).
% 184.39/184.87 cnf('0.70.2.0',plain,
% 184.39/184.87 ( ifmin(le(X1,X2),cons(s(X1),cons(s(X2),X3))) = min(cons(s(X1),cons(s(X2),X3))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.70.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_69]).
% 184.39/184.87 cnf('0.71.0.0',plain,
% 184.39/184.87 ( min(cons(s(zero),cons(s(X1),X2))) = ifmin(true,cons(s(zero),cons(s(X1),X2))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.70.2.0','0.17.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.71.0.1',plain,
% 184.39/184.87 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.71.0.0','0.8.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.71.1.0',plain,
% 184.39/184.87 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.71.0.1']),
% 184.39/184.87 [weight('<125,70,17,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.71.2.0',plain,
% 184.39/184.87 ( min(cons(s(zero),cons(s(X1),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.71.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_70]).
% 184.39/184.87 cnf('0.72.0.0',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(zero),X2))) = ifmin(false,cons(s(s(X1)),cons(s(zero),X2))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.70.2.0','0.14.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.72.0.1',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.72.0.0','0.7.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.72.1.0',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.72.0.1']),
% 184.39/184.87 [weight('<149,70,14,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.72.2.0',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(zero),X2))) = min(cons(s(zero),X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.72.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_71]).
% 184.39/184.87 cnf('0.73.0.0',plain,
% 184.39/184.87 ( replace(s(X1),X2,cons(s(X3),X4)) = ifrepl(eq(X1,X3),s(X1),X2,cons(s(X3),X4)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.20.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.73.1.0',plain,
% 184.39/184.87 ( replace(s(X1),X2,cons(s(X3),X4)) = ifrepl(eq(X1,X3),s(X1),X2,cons(s(X3),X4)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.73.0.0']),
% 184.39/184.87 [weight('<239,20,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.73.2.0',plain,
% 184.39/184.87 ( ifrepl(eq(X1,X2),s(X1),X3,cons(s(X2),X4)) = replace(s(X1),X3,cons(s(X2),X4)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.73.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_72]).
% 184.39/184.87 cnf('0.91.0.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(X1)))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.58.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.91.1.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(X1)))),nil)) = ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.91.0.0']),
% 184.39/184.87 [weight('<239,58,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.91.2.0',plain,
% 184.39/184.87 ( ifselsort(eq(X1,X1),cons(s(s(s(s(X1)))),nil)) = selsort(cons(s(s(s(s(X1)))),nil)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.91.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_90]).
% 184.39/184.87 cnf('0.92.0.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(zero)))),nil)) = ifselsort(true,cons(s(s(s(s(zero)))),nil)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.91.2.0','0.13.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.92.0.1',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),selsort(nil)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.92.0.0','0.2.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.92.0.2',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.92.0.1','0.15.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2','L')]).
% 184.39/184.87 cnf('0.92.1.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.92.0.2']),
% 184.39/184.87 [weight('<143,91,13,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.92.2.0',plain,
% 184.39/184.87 ( selsort(cons(s(s(s(s(zero)))),nil)) = cons(s(s(s(s(zero)))),nil) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.92.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_91]).
% 184.39/184.87 cnf('0.93.0.0',plain,
% 184.39/184.87 ( min(cons(s(zero),replace(zero,X1,X2))) = min(cons(s(zero),replace(zero,X1,cons(s(X3),X2)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.71.2.0','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.93.0.1',plain,
% 184.39/184.87 ( min(replace(zero,X1,cons(s(zero),X2))) = min(cons(s(zero),replace(zero,X1,cons(s(X3),X2)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.93.0.0','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.93.0.2',plain,
% 184.39/184.87 ( min(replace(zero,X1,cons(s(zero),X2))) = min(replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.93.0.1','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.93.1.0',plain,
% 184.39/184.87 ( min(replace(zero,X1,cons(s(zero),X2))) = min(replace(zero,X1,cons(s(zero),cons(s(X3),X2)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.93.0.2']),
% 184.39/184.87 [weight('<239,71,32,[1,0,0,4]>')]).
% 184.39/184.87 cnf('0.93.2.0',plain,
% 184.39/184.87 ( min(replace(zero,X1,cons(s(zero),cons(s(X2),X3)))) = min(replace(zero,X1,cons(s(zero),X3))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.93.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_92]).
% 184.39/184.87 cnf('0.110.0.0',plain,
% 184.39/184.87 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(interreduction_right,[status(thm)],['0.4.2.0'])).
% 184.39/184.87 cnf('0.110.1.0',plain,
% 184.39/184.87 ( cons(min(cons(X1,X2)),selsort(replace(min(cons(X1,X2)),X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.110.0.0']),
% 184.39/184.87 [weight('<265,4,62,[0,0,0,0]>')]).
% 184.39/184.87 cnf('0.110.1.1',plain,
% 184.39/184.87 ( ifrepl(true,const2,min(cons(X1,X2)),ifselsort(false,cons(X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.110.1.0','0.62.2.1',theory(equality)]),
% 184.39/184.87 [pos('L','L')]).
% 184.39/184.87 cnf('0.110.2.0',plain,
% 184.39/184.87 ( ifrepl(true,const2,min(cons(X1,X2)),ifselsort(false,cons(X1,X2))) = ifselsort(false,cons(X1,X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.110.1.1',theory(equality)]),
% 184.39/184.87 [u,rule_109]).
% 184.39/184.87 cnf('0.117.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.46.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.117.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.117.0.0']),
% 184.39/184.87 [weight('<285,46,32,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.117.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(zero,X4)))) = cons(s(X2),cons(s(X3),cons(X1,X4))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.117.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_116]).
% 184.39/184.87 cnf('0.173.0.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.57.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.173.1.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.173.0.0']),
% 184.39/184.87 [weight('<335,57,32,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.173.2.0',plain,
% 184.39/184.87 ( replace(zero,X1,cons(s(X2),cons(s(X3),cons(s(X4),nil)))) = cons(s(X2),cons(s(X3),cons(s(X4),nil))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.173.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_172]).
% 184.39/184.87 cnf('0.174.0.0',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(s(X2)),X3))) = ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.70.2.0','0.18.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.174.1.0',plain,
% 184.39/184.87 ( min(cons(s(s(X1)),cons(s(s(X2)),X3))) = ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.174.0.0']),
% 184.39/184.87 [weight('<335,70,18,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.174.2.0',plain,
% 184.39/184.87 ( ifmin(le(X1,X2),cons(s(s(X1)),cons(s(s(X2)),X3))) = min(cons(s(s(X1)),cons(s(s(X2)),X3))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.174.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_173]).
% 184.39/184.87 cnf('0.175.0.0',plain,
% 184.39/184.87 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = ifmin(true,cons(s(s(zero)),cons(s(s(X1)),X2))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.174.2.0','0.17.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.175.0.1',plain,
% 184.39/184.87 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.175.0.0','0.8.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.175.1.0',plain,
% 184.39/184.87 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.175.0.1']),
% 184.39/184.87 [weight('<186,174,17,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.175.2.0',plain,
% 184.39/184.87 ( min(cons(s(s(zero)),cons(s(s(X1)),X2))) = min(cons(s(s(zero)),X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.175.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_174]).
% 184.39/184.87 cnf('0.178.0.0',plain,
% 184.39/184.87 ( replace(s(s(X1)),X2,cons(s(s(X3)),X4)) = ifrepl(eq(X1,X3),s(s(X1)),X2,cons(s(s(X3)),X4)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.73.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.178.1.0',plain,
% 184.39/184.87 ( replace(s(s(X1)),X2,cons(s(s(X3)),X4)) = ifrepl(eq(X1,X3),s(s(X1)),X2,cons(s(s(X3)),X4)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.178.0.0']),
% 184.39/184.87 [weight('<335,73,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.178.2.0',plain,
% 184.39/184.87 ( ifrepl(eq(X1,X2),s(s(X1)),X3,cons(s(s(X2)),X4)) = replace(s(s(X1)),X3,cons(s(s(X2)),X4)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.178.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_177]).
% 184.39/184.87 cnf('0.235.0.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.62.2.0','0.62.2.0',theory(equality)]),
% 184.39/184.87 [pos('L','L')]).
% 184.39/184.87 cnf('0.235.1.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.235.0.0']),
% 184.39/184.87 [weight('<360,62,62,[1,0,0,0]>')]).
% 184.39/184.87 cnf('0.235.2.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X5,X2,ifselsort(false,cons(X3,X4))) ),
% 184.39/184.87 inference(activate,[status(thm)],['0.235.1.0']),
% 184.39/184.87 [equation_2]).
% 184.39/184.87 cnf('0.235.2.1',plain,
% 184.39/184.87 ( ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,const2,X2,ifselsort(false,cons(X3,X4))) ),
% 184.39/184.87 inference(instr,[status(thm)],['0.235.2.0',theory(equality)])).
% 184.39/184.87 cnf('0.235.2.2',plain,
% 184.39/184.87 ( ifrepl(true,const2,X2,ifselsort(false,cons(X3,X4))) = ifrepl(true,X1,X2,ifselsort(false,cons(X3,X4))) ),
% 184.39/184.87 inference(instl,[status(thm)],['0.235.2.0',theory(equality)])).
% 184.39/184.87 cnf('0.241.0.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.235.2.0','0.110.2.0',theory(equality)]),
% 184.39/184.87 [pos('L','L')]).
% 184.39/184.87 cnf('0.241.1.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.241.0.0']),
% 184.39/184.87 [weight('<233,235,110,[1,0,0,0]>')]).
% 184.39/184.87 cnf('0.241.2.0',plain,
% 184.39/184.87 ( ifrepl(true,X1,min(cons(X2,X3)),ifselsort(false,cons(X2,X3))) = ifselsort(false,cons(X2,X3)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.241.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_239]).
% 184.39/184.87 cnf('0.317.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.19.2.0','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2.1','L')]).
% 184.39/184.87 cnf('0.317.0.1',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.317.0.0','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.317.0.2',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.317.0.1','0.32.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2','L')]).
% 184.39/184.87 cnf('0.317.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.317.0.2']),
% 184.39/184.87 [weight('<?,32,19,[0,0,0,4]>')]).
% 184.39/184.87 cnf('0.317.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.317.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_315]).
% 184.39/184.87 cnf('0.469.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.117.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.469.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.469.0.0']),
% 184.39/184.87 [weight('<447,117,32,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.469.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.469.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_467]).
% 184.39/184.87 cnf('0.472.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.174.2.0','0.18.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.472.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.472.0.0']),
% 184.39/184.87 [weight('<447,174,18,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.472.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.472.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_470]).
% 184.39/184.87 cnf('0.474.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.472.2.0','0.14.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.474.0.1',plain,
% 184.39/184.87 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.474.0.0','0.7.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.474.1.0',plain,
% 184.39/184.87 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.474.0.1']),
% 184.39/184.87 [weight('<293,472,14,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.474.2.0',plain,
% 184.39/184.87 ( min(cons(s(s(s(s(X1)))),cons(s(s(s(zero))),X2))) = min(cons(s(s(s(zero))),X2)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.474.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_472]).
% 184.39/184.87 cnf('0.476.0.0',plain,
% 184.39/184.87 ( 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)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.178.2.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.476.1.0',plain,
% 184.39/184.87 ( 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)) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.476.0.0']),
% 184.39/184.87 [weight('<447,178,10,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.476.2.0',plain,
% 184.39/184.87 ( 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)) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.476.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_474]).
% 184.39/184.87 cnf('0.477.0.0',plain,
% 184.39/184.87 ( 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)) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.476.2.0','0.13.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.477.0.1',plain,
% 184.39/184.87 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.477.0.0','0.1.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.477.1.0',plain,
% 184.39/184.87 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.477.0.1']),
% 184.39/184.87 [weight('<207,476,13,[1,0,0,1]>')]).
% 184.39/184.87 cnf('0.477.2.0',plain,
% 184.39/184.87 ( replace(s(s(s(zero))),X1,cons(s(s(s(zero))),X2)) = cons(X1,X2) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.477.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_475]).
% 184.39/184.87 cnf('0.756.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.32.2.0','0.173.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.756.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.756.0.0']),
% 184.39/184.87 [weight('<509,173,32,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.756.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.756.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_752]).
% 184.39/184.87 cnf('0.882.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.19.2.0','0.72.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.882.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.882.0.0']),
% 184.39/184.87 [weight('<531,72,19,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.882.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.882.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_878]).
% 184.39/184.87 cnf('0.1884.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.19.2.0','0.175.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.1884.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.1884.0.0']),
% 184.39/184.87 [weight('<650,175,19,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.1884.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.1884.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_1867]).
% 184.39/184.87 cnf('0.3855.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.882.2.0','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.3855.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.3855.0.0']),
% 184.39/184.87 [weight('<747,882,71,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.3855.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.3855.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_3815]).
% 184.39/184.87 cnf('0.4641.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.317.2.0','0.93.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.4641.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.4641.0.0']),
% 184.39/184.87 [weight('<781,317,93,[1,0,0,4]>')]).
% 184.39/184.87 cnf('0.4641.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.4641.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_4599]).
% 184.39/184.87 cnf('0.4642.0.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.4641.2.0','0.173.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2.1','L')]).
% 184.39/184.87 cnf('0.4642.0.1',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.0','0.756.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1','L')]).
% 184.39/184.87 cnf('0.4642.0.2',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.1','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1.2','L')]).
% 184.39/184.87 cnf('0.4642.0.3',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.2','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1.2','L')]).
% 184.39/184.87 cnf('0.4642.0.4',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.3','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1.2','L')]).
% 184.39/184.87 cnf('0.4642.0.5',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.4','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.4642.0.6',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.5','0.13.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.4642.0.7',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.6','0.51.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.4642.0.8',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.4642.0.7','0.173.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.1','L')]).
% 184.39/184.87 cnf('0.4642.1.0',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.4642.0.8']),
% 184.39/184.87 [weight('<434,4641,173,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.4642.2.0',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.4642.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_4600]).
% 184.39/184.87 cnf('0.13132.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.241.2.0','0.474.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.3','L')]).
% 184.39/184.87 cnf('0.13132.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13132.0.0']),
% 184.39/184.87 [weight('<974,474,241,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.13132.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13132.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_13012]).
% 184.39/184.87 cnf('0.13133.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.13132.2.0','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.3','L')]).
% 184.39/184.87 cnf('0.13133.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13133.0.0']),
% 184.39/184.87 [weight('<791,13132,5,[1,0,0,3]>')]).
% 184.39/184.87 cnf('0.13133.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13133.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_13013]).
% 184.39/184.87 cnf('0.13134.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.13133.2.0','0.62.2.0',theory(equality)]),
% 184.39/184.87 [pos('L','R')]).
% 184.39/184.87 cnf('0.13134.0.1',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13134.0.0','0.474.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.1.1','L')]).
% 184.39/184.87 cnf('0.13134.0.2',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13134.0.1','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.1.1','L')]).
% 184.39/184.87 cnf('0.13134.0.3',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13134.0.2','0.477.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.1','L')]).
% 184.39/184.87 cnf('0.13134.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13134.0.3']),
% 184.39/184.87 [weight('<419,13133,62,[1,0,1,0]>')]).
% 184.39/184.87 cnf('0.13134.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13134.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_13014]).
% 184.39/184.87 cnf('0.13159.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.1884.2.0','0.175.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.13159.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13159.0.0']),
% 184.39/184.87 [weight('<974,1884,175,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.13159.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13159.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_13039]).
% 184.39/184.87 cnf('0.13160.0.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.13159.2.0','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.13160.0.1',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13160.0.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.13160.0.2',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13160.0.1','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.13160.0.3',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13160.0.2','0.13.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.13160.0.4',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.13160.0.3','0.2.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.13160.1.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.13160.0.4']),
% 184.39/184.87 [weight('<434,13159,5,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.13160.2.0',plain,
% 184.39/184.87 ( 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)))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.13160.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_13040]).
% 184.39/184.87 cnf('0.14126.0.0',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.3855.2.0','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.14126.1.0',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.14126.0.0']),
% 184.39/184.87 [weight('<999,3855,71,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.14126.2.0',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.14126.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_14005]).
% 184.39/184.87 cnf('0.21511.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.19.2.0','0.474.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.21511.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.21511.0.0']),
% 184.39/184.87 [weight('<1079,474,19,[0,0,0,3]>')]).
% 184.39/184.87 cnf('0.21511.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.21511.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_21366]).
% 184.39/184.87 cnf('0.21512.0.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.21511.2.0','0.5.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.21512.0.1',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.21512.0.0','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.21512.0.2',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.21512.0.1','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.21512.0.3',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.21512.0.2','0.10.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.21512.0.4',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.21512.0.3','0.11.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.21512.0.5',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.21512.0.4','0.13134.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.21512.1.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.21512.0.5']),
% 184.39/184.87 [weight('<377,21511,5,[1,0,0,7]>')]).
% 184.39/184.87 cnf('0.21512.2.0',plain,
% 184.39/184.87 ( 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))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.21512.1.0',theory(equality)]),
% 184.39/184.87 [u,rule_21367]).
% 184.39/184.87 cnf('0.27243.0.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.14126.2.0','0.28.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.27243.1.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.27243.0.0']),
% 184.39/184.87 [weight('<1117,14126,28,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.27243.2.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.27243.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_27066]).
% 184.39/184.87 cnf('0.27244.0.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.27243.2.0','0.6.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.1.2','L')]).
% 184.39/184.87 cnf('0.27244.0.1',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27244.0.0','0.11.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.1','L')]).
% 184.39/184.87 cnf('0.27244.1.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.27244.0.1']),
% 184.39/184.87 [weight('<683,27243,6,[1,0,0,5]>')]).
% 184.39/184.87 cnf('0.27244.2.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.27244.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_27067]).
% 184.39/184.87 cnf('0.27246.0.0',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.62.2.0','0.27244.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.4','L')]).
% 184.39/184.87 cnf('0.27246.0.1',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.0','0.72.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1.1','L')]).
% 184.39/184.87 cnf('0.27246.0.2',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.1','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1.1','L')]).
% 184.39/184.87 cnf('0.27246.0.3',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.2','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1.1','L')]).
% 184.39/184.87 cnf('0.27246.0.4',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.3','0.28.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1.1','L')]).
% 184.39/184.87 cnf('0.27246.0.5',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.4','0.6.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1.1','L')]).
% 184.39/184.87 cnf('0.27246.0.6',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.5','0.469.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2.1','L')]).
% 184.39/184.87 cnf('0.27246.0.7',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27246.0.6','0.4642.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.2','L')]).
% 184.39/184.87 cnf('0.27246.1.0',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.27246.0.7']),
% 184.39/184.87 [weight('<857,27244,62,[0,0,1,4]>')]).
% 184.39/184.87 cnf('0.27246.2.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.27246.1.0',theory(equality)]),
% 184.39/184.87 [x,rule_27069]).
% 184.39/184.87 cnf('0.27247.0.0',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(cp,[status(thm)],['0.241.2.0','0.27244.2.0',theory(equality)]),
% 184.39/184.87 [pos('L.4','L')]).
% 184.39/184.87 cnf('0.27247.0.1',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.0','0.27244.2.0',theory(equality)]),
% 184.39/184.87 [pos('L','L')]).
% 184.39/184.87 cnf('0.27247.0.2',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.1','0.72.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.3','L')]).
% 184.39/184.87 cnf('0.27247.0.3',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.2','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.3','L')]).
% 184.39/184.87 cnf('0.27247.0.4',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.3','0.71.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.3','L')]).
% 184.39/184.87 cnf('0.27247.0.5',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.4','0.28.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.3','L')]).
% 184.39/184.87 cnf('0.27247.0.6',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.0.5','0.6.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.3','L')]).
% 184.39/184.87 cnf('0.27247.1.0',plain,
% 184.39/184.87 ( 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))))))) ),
% 184.39/184.87 inference(weigh,[status(thm)],['0.27247.0.6']),
% 184.39/184.87 [weight('<857,27244,241,[0,0,0,7]>')]).
% 184.39/184.87 cnf('0.27247.1.1',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['0.27247.1.0','0.27246.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('0.27247.2.0',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(orient,[status(thm)],['0.27247.1.1',theory(equality)]),
% 184.39/184.87 [u,rule_27070]).
% 184.39/184.87 cnf('1.0.0.0',conjecture,
% 184.39/184.87 ( cons(zero,cons(s(zero),cons(s(s(zero)),cons(s(s(s(zero))),cons(s(s(s(s(zero)))),nil))))) = selsort(cons(s(s(s(zero))),cons(s(zero),cons(s(s(zero)),cons(s(s(s(s(zero)))),cons(zero,nil)))))) ),
% 184.39/184.87 file('/tmp/WALDMEISTER_7837_n013',conjecture_1)).
% 184.39/184.87 cnf('1.0.0.1',plain,
% 184.39/184.87 ( 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(s(zero))),nil)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['1.0.0.0','0.27247.2.0',theory(equality)]),
% 184.39/184.87 [pos('R','L')]).
% 184.39/184.87 cnf('1.0.0.2',plain,
% 184.39/184.87 ( 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(s(zero))),nil)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['1.0.0.1','0.13160.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.2','L')]).
% 184.39/184.87 cnf('1.0.0.3',plain,
% 184.39/184.87 ( 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)))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['1.0.0.2','0.21512.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.2.2','L')]).
% 184.39/184.87 cnf('1.0.0.4',plain,
% 184.39/184.87 ( 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))))) ),
% 184.39/184.87 inference(reduction,[status(thm)],['1.0.0.3','0.92.2.0',theory(equality)]),
% 184.39/184.87 [pos('R.2.2.2.2','L')]).
% 184.39/184.87 cnf('1.0.0.5',plain,
% 184.39/184.87 ( $true ),
% 184.39/184.87 inference(trivial,[status(thm)],['1.0.0.4',theory(equality)]),
% 184.39/184.87 [conjecture_1]).
% 184.39/184.87
% 184.39/184.87 Proved Goals:
% 184.39/184.87 No. 1: cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) ?= selsort(cons(s^3(zero),cons(s(zero),cons(s(s(zero)),cons(s^4(zero),cons(zero,nil)))))) joined, current: cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil))))) = cons(zero,cons(s(zero),cons(s(s(zero)),cons(s^3(zero),cons(s^4(zero),nil)))))
% 184.39/184.87 1 goal was specified, which was proved.
% 184.39/184.87 % SZS output end CNFRefutation
% 184.39/184.87 #END OF PROOF
% 184.39/184.87
% 184.39/184.87 Problem WALDMEISTER_7837_n013
% 184.39/184.87 CPs.gen 17767022
% 184.39/184.87 CPs.reexp 0
% 184.39/184.87 Select 63808
% 184.39/184.87 R 27070
% 184.39/184.87 E 177
% 184.39/184.87 vsize 41.8M
% 184.39/184.87 rss 38.8M
% 184.39/184.87 process.time 183.913s
% 184.39/184.87 wallclock.time 183.942s
% 184.39/184.87 status S
% 184.39/184.87
% 184.39/184.87
% 184.39/184.87 Waldmeister states: Goal proved.
% 184.39/184.87 % SZS status Unsatisfiable
%------------------------------------------------------------------------------