%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : PUZ039-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n027.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 : 600s % DateTime : Mon Jul 18 18:11:32 EDT 2022 % Result : Unsatisfiable 20.33s 20.78s % Output : CNFRefutation 20.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ039-10 : TPTP v8.1.0. Released v7.5.0. % 0.11/0.12 % Command : fiesta-wrapper %s % 0.13/0.33 % Computer : n027.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun May 29 00:44:29 EDT 2022 % 0.13/0.33 % CPUTime : % 20.33/20.78 Theorem Proved. % 20.33/20.78 % SZS status Unsatisfiable % 20.33/20.78 % SZS output start CNFRefutation % 20.33/20.78 [1=axiom,[], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true]. % 20.33/20.78 [2=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,e1(X110,X111),e2(X112,X113)),true,state(X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,e1(X112,X113),e2(X110,X111)),true) = true]. % 20.33/20.78 [8=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,h(X15,X16),X17,X18,X19,X110,e1(s(X15),X16),e2(s(X15),s(X16))),true,state(X10,X11,X12,X13,X14,h(s(X15),X16),X17,X18,X19,X110,e1(X15,X16),e2(X15,s(X16))),true) = true]. % 20.33/20.78 [9=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,h(X15,s(X16)),X17,X18,X19,X110,e1(X15,X16),X111),true,state(X10,X11,X12,X13,X14,h(X15,X16),X17,X18,X19,X110,e1(X15,s(s(X16))),X111),true) = true]. % 20.33/20.78 [10=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,h(X15,X16),X17,X18,X19,X110,e1(X15,s(s(X16))),X111),true,state(X10,X11,X12,X13,X14,h(X15,s(X16)),X17,X18,X19,X110,e1(X15,X16),X111),true) = true]. % 20.33/20.78 [11=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,v4(s(X14),X15),X16,X17,X18,X19,X110,e1(X14,X15),X111),true,state(X10,X11,X12,X13,v4(X14,X15),X16,X17,X18,X19,X110,e1(s(s(X14)),X15),X111),true) = true]. % 20.33/20.78 [12=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,v4(X14,X15),X16,X17,X18,X19,X110,e1(s(s(X14)),X15),X111),true,state(X10,X11,X12,X13,v4(s(X14),X15),X16,X17,X18,X19,X110,e1(X14,X15),X111),true) = true]. % 20.33/20.78 [13=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,v4(X14,s(X15)),X16,X17,X18,X19,X110,e1(X14,X15),e2(s(X14),X15)),true,state(X10,X11,X12,X13,v4(X14,X15),X16,X17,X18,X19,X110,e1(X14,s(X15)),e2(s(X14),s(X15))),true) = true]. % 20.33/20.78 [15=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,v3(s(X13),X14),X15,X16,X17,X18,X19,X110,e1(X13,X14),X111),true,state(X10,X11,X12,v3(X13,X14),X15,X16,X17,X18,X19,X110,e1(s(s(X13)),X14),X111),true) = true]. % 20.33/20.78 [16=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,v3(X13,X14),X15,X16,X17,X18,X19,X110,e1(s(s(X13)),X14),X111),true,state(X10,X11,X12,v3(s(X13),X14),X15,X16,X17,X18,X19,X110,e1(X13,X14),X111),true) = true]. % 20.33/20.78 [17=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,v3(X13,s(X14)),X15,X16,X17,X18,X19,X110,e1(X13,X14),e2(s(X13),X14)),true,state(X10,X11,X12,v3(X13,X14),X15,X16,X17,X18,X19,X110,e1(X13,s(X14)),e2(s(X13),s(X14))),true) = true]. % 20.33/20.78 [18=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,v3(X13,X14),X15,X16,X17,X18,X19,X110,e1(X13,s(X14)),e2(s(X13),s(X14))),true,state(X10,X11,X12,v3(X13,s(X14)),X15,X16,X17,X18,X19,X110,e1(X13,X14),e2(s(X13),X14)),true) = true]. % 20.33/20.78 [19=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,v2(s(X12),X13),X14,X15,X16,X17,X18,X19,X110,e1(X12,X13),X111),true,state(X10,X11,v2(X12,X13),X14,X15,X16,X17,X18,X19,X110,e1(s(s(X12)),X13),X111),true) = true]. % 20.33/20.78 [20=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,v2(X12,X13),X14,X15,X16,X17,X18,X19,X110,e1(s(s(X12)),X13),X111),true,state(X10,X11,v2(s(X12),X13),X14,X15,X16,X17,X18,X19,X110,e1(X12,X13),X111),true) = true]. % 20.33/20.78 [23=axiom,[], % 20.33/20.78 ifeq(state(X10,v1(s(X11),X12),X13,X14,X15,X16,X17,X18,X19,X110,e1(X11,X12),X111),true,state(X10,v1(X11,X12),X13,X14,X15,X16,X17,X18,X19,X110,e1(s(s(X11)),X12),X111),true) = true]. % 20.33/20.78 [24=axiom,[], % 20.33/20.78 ifeq(state(X10,v1(X11,X12),X13,X14,X15,X16,X17,X18,X19,X110,e1(s(s(X11)),X12),X111),true,state(X10,v1(s(X11),X12),X13,X14,X15,X16,X17,X18,X19,X110,e1(X11,X12),X111),true) = true]. % 20.33/20.78 [27=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(s(X19),X110),e1(X19,X110),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,X110),e1(s(X19),X110),X111),true) = true]. % 20.33/20.78 [28=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,X110),e1(s(X19),X110),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(s(X19),X110),e1(X19,X110),X111),true) = true]. % 20.33/20.78 [29=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,s(X110)),e1(X19,X110),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,X110),e1(X19,s(X110)),X111),true) = true]. % 20.33/20.78 [30=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,X110),e1(X19,s(X110)),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,X18,s4(X19,s(X110)),e1(X19,X110),X111),true) = true]. % 20.33/20.78 [31=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,s3(s(X18),X19),X110,e1(X18,X19),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,X19),X110,e1(s(X18),X19),X111),true) = true]. % 20.33/20.78 [32=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,X19),X110,e1(s(X18),X19),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,s3(s(X18),X19),X110,e1(X18,X19),X111),true) = true]. % 20.33/20.78 [33=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,s(X19)),X110,e1(X18,X19),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,X19),X110,e1(X18,s(X19)),X111),true) = true]. % 20.33/20.78 [34=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,X19),X110,e1(X18,s(X19)),X111),true,state(X10,X11,X12,X13,X14,X15,X16,X17,s3(X18,s(X19)),X110,e1(X18,X19),X111),true) = true]. % 20.33/20.78 [35=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,s2(s(X17),X18),X19,X110,e1(X17,X18),X111),true,state(X10,X11,X12,X13,X14,X15,X16,s2(X17,X18),X19,X110,e1(s(X17),X18),X111),true) = true]. % 20.33/20.78 [36=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,s2(X17,X18),X19,X110,e1(s(X17),X18),X111),true,state(X10,X11,X12,X13,X14,X15,X16,s2(s(X17),X18),X19,X110,e1(X17,X18),X111),true) = true]. % 20.33/20.78 [37=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,s2(X17,s(X18)),X19,X110,e1(X17,X18),X111),true,state(X10,X11,X12,X13,X14,X15,X16,s2(X17,X18),X19,X110,e1(X17,s(X18)),X111),true) = true]. % 20.33/20.78 [38=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,X16,s2(X17,X18),X19,X110,e1(X17,s(X18)),X111),true,state(X10,X11,X12,X13,X14,X15,X16,s2(X17,s(X18)),X19,X110,e1(X17,X18),X111),true) = true]. % 20.33/20.78 [39=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,s1(s(X16),X17),X18,X19,X110,e1(X16,X17),X111),true,state(X10,X11,X12,X13,X14,X15,s1(X16,X17),X18,X19,X110,e1(s(X16),X17),X111),true) = true]. % 20.33/20.78 [40=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,s1(X16,X17),X18,X19,X110,e1(s(X16),X17),X111),true,state(X10,X11,X12,X13,X14,X15,s1(s(X16),X17),X18,X19,X110,e1(X16,X17),X111),true) = true]. % 20.33/20.78 [41=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,s1(X16,s(X17)),X18,X19,X110,e1(X16,X17),X111),true,state(X10,X11,X12,X13,X14,X15,s1(X16,X17),X18,X19,X110,e1(X16,s(X17)),X111),true) = true]. % 20.33/20.78 [42=axiom,[], % 20.33/20.78 ifeq(state(X10,X11,X12,X13,X14,X15,s1(X16,X17),X18,X19,X110,e1(X16,s(X17)),X111),true,state(X10,X11,X12,X13,X14,X15,s1(X16,s(X17)),X18,X19,X110,e1(X16,X17),X111),true) = true]. % 20.33/20.78 [43=axiom,[], % 20.33/20.78 ifeq(X10,X10,X11,X12) = X11]. % 20.33/20.78 [44=axiom,[], % 20.33/20.78 thtop(X10,X10) = thmfalse]. % 20.33/20.78 [45=axiom,[], % 20.33/20.78 thtop(state(X10,X11,X12,X13,v4(s(s(o)),s(s(o))),X14,X15,X16,X17,X18,X19,X110),true) = thmtrue]. % 20.33/20.78 [46=param(16,1),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),s(s(s(o))))) = true]. % 20.33/20.78 [48=param(24,46),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(o,o),e2(s(s(s(s(o)))),s(s(s(o))))) = true]. % 20.33/20.78 [49=param(2,48),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(o)),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(s(o)))),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [56=param(12,49),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [59=param(10,56),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(o)),s(o)),e2(o,o)) = true]. % 20.33/20.78 [66=param(39,59),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [71=param(37,66),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(o)),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(s(o)))),s(s(o))),e1(s(s(s(o))),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [73=param(27,71),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(o)),s3(s(s(s(s(o)))),s(o)),s4(s(s(s(o))),s(s(o))),e1(s(s(s(s(o)))),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [77=param(34,73),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(s(o)))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [79=param(36,77),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [83=param(29,79),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(o))),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [92=param(31,83),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(o))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(s(o)))),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [94=param(38,92),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(s(o)))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [96=param(28,94),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(s(o)))),s(o)),e1(s(s(s(o))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [97=param(2,96),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(s(o)))),s(o)),e1(o,o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [112=param(23,97),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(s(o)))),s(o)),e1(s(s(o)),o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [209=param(41,112),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(s(o)))),s(o)),e1(s(s(o)),s(o)),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [210=param(2,209),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(s(o)))),s(o)),e1(s(s(s(o))),s(o)),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [212=param(27,210),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(s(o)))),s(o)),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [214=param(37,212),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(o))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [216=param(32,214),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(o)),e1(s(s(s(o))),s(s(o))),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [221=param(30,216),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),s(o)),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [223=param(35,221),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(s(o)))),s(o)),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [225=param(2,223),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),s(o)),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [546=param(35,225),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),o),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),s(o)),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [1135=param(18,546),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),o),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [1137=param(40,1135),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [1140=param(24,1137),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(o,o),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [1143=param(2,1140),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(o))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(s(o)))),o),e2(o,o)) = true]. % 20.33/20.78 [1145=param(40,1143),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),o),e2(o,o)) = true]. % 20.33/20.78 [1146=param(2,1145),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(o,o),e2(s(s(s(o))),o)) = true]. % 20.33/20.78 [1153=param(23,1146),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),o),e2(s(s(s(o))),o)) = true]. % 20.33/20.78 [1156=param(37,1153),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(o)),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),s(o)),e2(s(s(s(o))),o)) = true]. % 20.33/20.78 [1157=param(2,1156),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(o)),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(s(o))),o),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [1160=param(36,1157),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),o),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [1165=param(24,1160),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(o,o),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [1166=param(2,1165),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(s(o))),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),s(o)),e2(o,o)) = true]. % 20.33/20.78 [1167=param(9,1166),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [1196=param(20,1167),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(o,s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [1197=param(2,1196),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(o,o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [1198=param(23,1197),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),s(o)),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [1203=param(9,1198),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(s(o))),s(s(o))),e1(s(s(o)),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [1312=param(27,1203),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(s(o)))),s(s(o))),s4(s(s(o)),s(s(o))),e1(s(s(s(o))),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [1315=param(31,1312),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(o))),s(s(o))),s4(s(s(o)),s(s(o))),e1(s(s(s(s(o)))),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [1316=param(2,1315),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(o))),s(s(o))),s4(s(s(o)),s(s(o))),e1(o,s(s(s(o)))),e2(s(s(s(s(o)))),s(s(o)))) = true]. % 20.33/20.78 [1319=param(19,1316),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(o))),s(s(o))),s4(s(s(o)),s(s(o))),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(s(o)))),s(s(o)))) = true]. % 20.33/20.78 [2163=param(30,1319),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(s(o))),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(o)),s(s(o))),e2(s(s(s(s(o)))),s(s(o)))) = true]. % 20.33/20.78 [3635=param(31,2163),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(o))),s(s(o))),e2(s(s(s(s(o)))),s(s(o)))) = true]. % 20.33/20.78 [6027=param(18,3635),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),o),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(o))),s(o)),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [6029=param(38,6027),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(o))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(o))),o),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [6031=param(39,6029),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),o),s2(s(s(s(o))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [6032=param(2,6031),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),o),s2(s(s(s(o))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(s(o)))),s(o)),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [6033=param(36,6032),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(o))),s(o)),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [6036=param(2,6033),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(o))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(s(o)))),o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [6164=param(40,6036),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(o)),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(s(o))),o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [6167=param(8,6164),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(o)),o),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [6170=param(24,6167),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(o,o),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [6172=param(2,6170),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(s(o))),s4(s(s(o)),s(s(s(o)))),e1(s(s(o)),s(o)),e2(o,o)) = true]. % 20.33/20.78 [6173=param(33,6172),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(o)),s4(s(s(o)),s(s(s(o)))),e1(s(s(o)),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [6178=param(29,6173),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(o)),s4(s(s(o)),s(s(o))),e1(s(s(o)),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [6182=param(20,6178),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(o)),s4(s(s(o)),s(s(o))),e1(o,s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [6184=param(2,6182),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(o)),s4(s(s(o)),s(s(o))),e1(o,o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6185=param(23,6184),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),s(o)),s4(s(s(o)),s(s(o))),e1(s(s(o)),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6189=param(33,6185),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),o),s4(s(s(o)),s(s(o))),e1(s(s(o)),s(o)),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6191=param(29,6189),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(s(o))),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(o)),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6193=param(15,6191),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(o)),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6231=param(38,6193),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),o),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),s(o)),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6233=param(42,6231),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [6235=param(2,6233),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(o,s(s(s(o)))),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [6236=param(19,6235),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [6285=param(11,6236),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),s(s(s(o)))),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [9673=param(38,6285),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(o)),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [9729=param(42,9673),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),s(o)),e2(s(s(s(s(o)))),o)) = true]. % 20.33/20.78 [9730=param(2,9729),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(o))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(s(o)))),o),e2(s(s(s(s(o)))),s(o))) = true]. % 20.33/20.78 [9731=param(8,9730),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(o)),o),s4(s(s(o)),s(o)),e1(s(s(s(o))),o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [9734=param(32,9731),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),s(o)),e1(s(s(o)),o),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [9737=param(29,9734),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(s(o))),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(o)),s(o)),e2(s(s(s(o))),s(o))) = true]. % 20.33/20.78 [9795=param(17,9737),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(o)),s(s(o))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9888=param(2,9795),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(s(o)))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(o))),s(s(o))),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9890=param(39,9888),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9894=param(10,9890),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9897=param(32,9894),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(o)),o),e1(s(s(s(o))),o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9902=param(28,9897),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9904=param(24,9902),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(o,o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [9906=param(2,9904),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(s(o))),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [9907=param(39,9906),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(s(o))),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [9908=param(2,9907),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(o,o),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9909=param(23,9908),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),o),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9913=param(27,9909),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(s(o)))),o),s4(s(s(o)),o),e1(s(s(s(o))),o),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9915=param(31,9913),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),o),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9917=param(9,9915),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(s(o)))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),s(s(o))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9923=param(37,9917),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),s(s(s(o)))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9925=param(12,9923),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9929=param(20,9925),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(o,s(s(s(o)))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [9931=param(2,9929),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(s(o)))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(o))),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9932=param(35,9931),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),o),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),s(s(o))),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9938=param(10,9932),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(o))),o),s4(s(s(o)),o),e1(s(s(s(s(o)))),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9943=param(32,9938),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(o)),o),e1(s(s(s(o))),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9946=param(28,9943),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9949=param(24,9946),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(o,o),e2(o,s(s(s(o))))) = true]. % 20.33/20.78 [9950=param(2,9949),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(s(o),s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(o,s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [9953=param(19,9950),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(s(o))),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [9955=param(11,9953),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(o)),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(s(s(o)))),s(s(s(o)))),e2(o,o)) = true]. % 20.33/20.78 [9999=param(10,9955),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(o)),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(s(s(o)))),s(o)),e2(o,o)) = true]. % 20.33/20.78 [10002=param(16,9999),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),s(s(o))),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(o)),e2(o,o)) = true]. % 20.33/20.78 [10008=param(41,10002),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(o))),e2(o,o)) = true]. % 20.33/20.78 [10009=param(2,10008),[43], % 20.33/20.78 state(bb(o,s(o)),v1(s(o),o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(o,o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [10014=param(23,10009),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),s(o)),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),o),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [10071=param(41,10014),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(o)),e2(s(s(o)),s(s(o)))) = true]. % 20.33/20.78 [10072=param(2,10071),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(s(o))),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(o))),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [10080=param(35,10072),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(s(o))),s(s(o))),e2(s(s(o)),s(o))) = true]. % 20.33/20.78 [10081=param(2,10080),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(s(o))),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(o)),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [10085=param(37,10081),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(s(o)))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(o))),e2(s(s(s(o))),s(s(o)))) = true]. % 20.33/20.78 [10087=param(13,10085),[43], % 20.33/20.78 state(bb(o,s(o)),v1(o,o),v2(o,s(s(s(o)))),v3(s(s(s(o))),s(o)),v4(s(s(o)),s(s(o))),h(s(s(s(s(o)))),s(s(o))),s1(s(s(o)),o),s2(s(s(o)),s(o)),s3(s(s(s(s(o)))),o),s4(s(s(s(o))),o),e1(s(s(o)),s(s(s(o)))),e2(s(s(s(o))),s(s(s(o))))) = true]. % 20.33/20.79 [10119=param(45,10087),[44], % 20.33/20.79 thmtrue = thmfalse]. % 20.33/20.79 % SZS output end CNFRefutation % 20.33/20.79 Space: 120875 KB %------------------------------------------------------------------------------