%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : LCL643+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n031.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:34:13 PM UTC 2026 % Result : Unknown 1.64s 1.90s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL643+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_zenon_modulo %d %s % 0.07/0.34 % Computer : n031.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sat Sep 5 02:41:24 UTC 2026 % 0.07/0.34 % CPUTime : % 1.64/1.90 Zenon error: exhausted search space without finding a proof % 1.64/1.90 (* Current branch: % 1.64/1.90 (-. (p3 zenon_Vrh)) % 1.64/1.90 (zenon_Vq != zenon_Vpg) % 1.64/1.90 (-. (p3 zenon_Vgh)) % 1.64/1.90 (-. (p4 zenon_Vqd)) % 1.64/1.90 (r1 zenon_Vjb zenon_Vkb) % 1.64/1.90 (zenon_Vq != zenon_Veh) % 1.64/1.90 (-. (p1 zenon_Vgi)) % 1.64/1.90 (-. (p4 zenon_Vfi)) % 1.64/1.90 (r1 zenon_Vyd zenon_Vzd) % 1.64/1.90 (zenon_Vo != zenon_Vic) % 1.64/1.90 (zenon_Vq != Tau_16) % 1.64/1.90 (r1 zenon_Vyb zenon_Vzb) % 1.64/1.90 (-. (p2 Tau_1)) % 1.64/1.90 (r1 zenon_Vwd zenon_Vxd) % 1.64/1.90 (zenon_Vm != Tau_0) % 1.64/1.90 (zenon_Vo != Tau_0) % 1.64/1.90 (zenon_Vq != Tau_0) % 1.64/1.90 (-. (p4 zenon_Vyi)) % 1.64/1.90 (zenon_Vq != zenon_Vic) % 1.64/1.90 (-. (p4 zenon_Vmh)) % 1.64/1.90 (-. (p1 Tau_3)) % 1.64/1.90 (-. (p2 zenon_Vag)) % 1.64/1.90 (zenon_Vq != zenon_Vkg) % 1.64/1.90 (-. (p1 zenon_Vgd)) % 1.64/1.90 (-. (p4 zenon_Vpe)) % 1.64/1.90 (zenon_Vo != zenon_Vgi) % 1.64/1.90 (zenon_Vo != zenon_Vfc) % 1.64/1.90 (-. (p3 zenon_Vbd)) % 1.64/1.90 (zenon_Vo != zenon_Vgc) % 1.64/1.90 (r1 zenon_Vrf zenon_Vsf) % 1.64/1.90 (-. (p3 zenon_Vgi)) % 1.64/1.90 (-. (p4 zenon_Vcj)) % 1.64/1.90 (-. (p3 zenon_Vnd)) % 1.64/1.90 (zenon_Vq != zenon_Vze) % 1.64/1.90 (-. (p2 zenon_Vsk)) % 1.64/1.90 (-. (p3 zenon_Vij)) % 1.64/1.90 (zenon_Vm != zenon_Vmk) % 1.64/1.90 (zenon_Vm != Tau_6) % 1.64/1.90 (zenon_Vo != Tau_6) % 1.64/1.90 (zenon_Vq != Tau_6) % 1.64/1.90 (-. (p1 zenon_Voi)) % 1.64/1.90 (-. (p3 zenon_Vlb)) % 1.64/1.90 (-. (p2 zenon_Vwj)) % 1.64/1.90 (zenon_Vm != zenon_Vod) % 1.64/1.90 (r1 zenon_Vse zenon_Vye) % 1.64/1.90 (zenon_Vm != zenon_Vgk) % 1.64/1.90 (zenon_Vo != zenon_Vuh) % 1.64/1.90 (-. (p2 Tau_0)) % 1.64/1.90 (-. (p1 zenon_Vlb)) % 1.64/1.90 (r1 zenon_Vfi zenon_Vgi) % 1.64/1.90 (zenon_Vm != zenon_Vge) % 1.64/1.90 (-. (p2 zenon_Vsi)) % 1.64/1.90 (-. (p2 zenon_Vob)) % 1.64/1.90 (zenon_Vm != Tau_5) % 1.64/1.90 (zenon_Vo != Tau_5) % 1.64/1.90 (zenon_Vq != Tau_5) % 1.64/1.90 (-. (p3 Tau_17)) % 1.64/1.90 (r1 Tau_0 Tau_15) % 1.64/1.90 (zenon_Vo != zenon_Vpe) % 1.64/1.90 (zenon_Vm != zenon_Vwj) % 1.64/1.90 (zenon_Vm != zenon_Vn) % 1.64/1.90 (zenon_Vo != zenon_Vrh) % 1.64/1.90 (-. (p1 zenon_Vyk)) % 1.64/1.90 (zenon_Vq != zenon_Vie) % 1.64/1.90 (r1 zenon_Ved zenon_Vfd) % 1.64/1.90 (-. (p1 zenon_Vyg)) % 1.64/1.90 (zenon_Vq != zenon_Vck) % 1.64/1.90 (-. (p1 zenon_Vsk)) % 1.64/1.90 (-. (p1 zenon_Vkc)) % 1.64/1.90 (r1 Tau_0 Tau_1) % 1.64/1.90 (-. (p2 zenon_Vjg)) % 1.64/1.90 (zenon_Vm != Tau_13) % 1.64/1.90 (zenon_Vo != Tau_13) % 1.64/1.90 (zenon_Vq != Tau_13) % 1.64/1.90 (zenon_Vq != zenon_Vrh) % 1.64/1.90 (-. (p2 zenon_Vlh)) % 1.64/1.90 (zenon_Vo != zenon_Vxg) % 1.64/1.90 (-. (p1 zenon_Vxd)) % 1.64/1.90 (-. (p4 zenon_Vzh)) % 1.64/1.90 (-. (p1 Tau_6)) % 1.64/1.90 (-. (p4 zenon_Vtc)) % 1.64/1.90 (-. (p1 zenon_Vrf)) % 1.64/1.90 (-. (p1 Tau_17)) % 1.64/1.90 (zenon_Vo != zenon_Vwb) % 1.64/1.90 (-. (p3 zenon_Ved)) % 1.64/1.90 (-. (p3 zenon_Vfi)) % 1.64/1.90 (-. (p2 zenon_Vgk)) % 1.64/1.90 (-. (p1 zenon_Vyb)) % 1.64/1.90 (-. (p3 zenon_Vkb)) % 1.64/1.90 (r1 zenon_X24 zenon_Vdl) % 1.64/1.90 (zenon_Vq != zenon_Voi) % 1.64/1.90 (-. (p1 zenon_Vmh)) % 1.64/1.90 (zenon_Vm != zenon_Vnd) % 1.64/1.90 (-. (p3 zenon_Vhc)) % 1.64/1.90 (-. (p3 zenon_Vmk)) % 1.64/1.90 (-. (p1 zenon_Vae)) % 1.64/1.90 (zenon_Vo != zenon_Vai) % 1.64/1.90 (zenon_Vq != zenon_Vgk) % 1.64/1.90 (-. (p2 Tau_6)) % 1.64/1.90 (zenon_Vq != zenon_Vhf) % 1.64/1.90 (-. (p1 zenon_Vhf)) % 1.64/1.90 (zenon_Vo != zenon_Vsj) % 1.64/1.90 (zenon_Vo != zenon_Voe) % 1.64/1.90 (zenon_Vm != zenon_Vzf) % 1.64/1.90 (-. (p4 zenon_Vqe)) % 1.64/1.90 (-. (p3 Tau_10)) % 1.64/1.90 (-. (p1 Tau_20)) % 1.64/1.90 (-. (p4 zenon_Vmb)) % 1.64/1.90 (-. (p1 zenon_Vpe)) % 1.64/1.90 (-. (p3 zenon_Vyg)) % 1.64/1.90 (zenon_Vq != zenon_Vgi) % 1.64/1.90 (r1 Tau_0 Tau_9) % 1.64/1.90 (zenon_Vo != zenon_Vsg) % 1.64/1.90 (zenon_Vo != zenon_Vbd) % 1.64/1.90 (-. (p1 zenon_Vmk)) % 1.64/1.90 (zenon_Vq != zenon_Vxd) % 1.64/1.90 (-. (p1 zenon_Vwj)) % 1.64/1.90 (r1 zenon_Vsk zenon_Vvk) % 1.64/1.90 (zenon_Vo != zenon_Vkc) % 1.64/1.90 (-. (p1 zenon_Ved)) % 1.64/1.90 (-. (p4 zenon_Vzf)) % 1.64/1.90 (-. (p3 zenon_Vig)) % 1.64/1.90 (-. (p1 zenon_Vzh)) % 1.64/1.90 (-. (p1 zenon_Vyi)) % 1.64/1.90 (-. (p4 zenon_Vyg)) % 1.64/1.90 (-. (p2 Tau_17)) % 1.64/1.90 (r1 Tau_10 zenon_Vdh) % 1.64/1.90 (r1 zenon_Vui zenon_Vyi) % 1.64/1.90 (-. (p4 zenon_Vae)) % 1.64/1.90 (zenon_Vm != zenon_Vie) % 1.64/1.90 (zenon_Vo != zenon_Vp) % 1.64/1.90 (-. (p1 zenon_Vze)) % 1.64/1.90 (-. (p4 zenon_Vod)) % 1.64/1.90 (zenon_Vo != zenon_Vdh) % 1.64/1.90 (zenon_Vo != zenon_Veh) % 1.64/1.90 (-. (p2 Tau_5)) % 1.64/1.90 (zenon_Vq != zenon_Vyf) % 1.64/1.90 (-. (p1 Tau_10)) % 1.64/1.90 (-. (p4 zenon_Vsc)) % 1.64/1.90 (r1 Tau_9 zenon_Vpg) % 1.64/1.90 (-. (p2 zenon_Vij)) % 1.64/1.90 (r1 zenon_Vcg zenon_Vig) % 1.64/1.90 (zenon_Vo != zenon_Vkf) % 1.64/1.90 (zenon_Vq != zenon_Vsg) % 1.64/1.90 (-. (p1 zenon_Vpd)) % 1.64/1.90 (r1 Tau_13 zenon_Vsi) % 1.64/1.90 (-. (p1 zenon_Vlh)) % 1.64/1.90 (-. (p4 zenon_Veh)) % 1.64/1.90 (zenon_Vq != zenon_Vpe) % 1.64/1.90 (-. (p4 zenon_Vck)) % 1.64/1.90 (r1 zenon_Vyj zenon_Vck) % 1.64/1.90 (zenon_Vm != zenon_Vck) % 1.64/1.90 (-. (p1 zenon_Vdd)) % 1.64/1.90 (-. (p2 zenon_Vye)) % 1.64/1.90 (zenon_Vm != zenon_Vjb) % 1.64/1.90 (-. (p2 Tau_14)) % 1.64/1.90 (-. (p1 zenon_Vdh)) % 1.64/1.90 (-. (p3 zenon_Vej)) % 1.64/1.90 (-. (p2 zenon_Voe)) % 1.64/1.90 (-. (p1 Tau_2)) % 1.64/1.90 (zenon_Vq != zenon_Vmb) % 1.64/1.90 (r1 zenon_Vgc zenon_Vhc) % 1.64/1.90 (-. (p3 zenon_Vaf)) % 1.64/1.90 (zenon_Vm != zenon_Vkb) % 1.64/1.90 (zenon_Vo != zenon_Voj) % 1.64/1.90 (-. (p1 zenon_Vaf)) % 1.64/1.90 (zenon_Vq != zenon_Vrc) % 1.64/1.90 (-. (p4 zenon_Vbd)) % 1.64/1.90 (-. (p1 zenon_Vsh)) % 1.64/1.90 (zenon_Vo != Tau_3) % 1.64/1.90 (zenon_Vq != Tau_3) % 1.64/1.90 (r1 zenon_X23 zenon_Vq) % 1.64/1.90 (-. (p4 zenon_Vif)) % 1.64/1.90 (r1 Tau_0 Tau_13) % 1.64/1.90 (r1 Tau_0 Tau_11) % 1.64/1.90 (zenon_Vq != zenon_Vig) % 1.64/1.90 (r1 zenon_Voe zenon_Vpe) % 1.64/1.90 (r1 zenon_Voi zenon_Vpi) % 1.64/1.90 (r1 zenon_Vo zenon_Vp) % 1.64/1.90 (-. (p1 zenon_Vmj)) % 1.64/1.90 (-. (p1 zenon_Vxb)) % 1.64/1.90 (zenon_Vm != zenon_Vuc) % 1.64/1.90 (zenon_Vo != zenon_Vgk) % 1.64/1.90 (zenon_Vo != zenon_Vyb) % 1.64/1.90 (zenon_Vq != zenon_Vwb) % 1.64/1.90 (-. (p4 zenon_Vgk)) % 1.64/1.90 (-. (p2 zenon_Vyi)) % 1.64/1.90 (-. (p2 Tau_2)) % 1.64/1.90 (zenon_Vo != zenon_Vui) % 1.64/1.90 (-. (p3 zenon_Vtc)) % 1.64/1.90 (-. (p2 zenon_Voj)) % 1.64/1.90 (zenon_Vo != zenon_Vsk) % 1.64/1.90 (zenon_Vq != zenon_Vrf) % 1.64/1.90 (-. (p3 zenon_Vze)) % 1.64/1.90 (-. (p1 zenon_Vai)) % 1.64/1.90 (-. (p3 zenon_Vgf)) % 1.64/1.90 (-. (p4 zenon_Vhe)) % 1.64/1.90 (zenon_Vo != zenon_Vcd) % 1.64/1.90 (r1 Tau_0 Tau_3) % 1.64/1.90 (zenon_Vq != zenon_Vsj) % 1.64/1.90 (-. (p3 zenon_Vye)) % 1.64/1.90 (zenon_Vm != zenon_Vkg) % 1.64/1.90 (-. (p3 zenon_Vpe)) % 1.64/1.90 (-. (p3 zenon_Vic)) % 1.64/1.90 (-. (p1 zenon_Vrh)) % 1.64/1.90 (r1 zenon_Vmj zenon_Vnj) % 1.64/1.90 (-. (p4 zenon_Vgi)) % 1.64/1.90 (-. (p2 zenon_Vze)) % 1.64/1.90 (-. (p2 zenon_Vrh)) % 1.64/1.90 (-. (p3 zenon_Vxg)) % 1.64/1.90 (-. (p3 zenon_Vqe)) % 1.64/1.90 (r1 zenon_Vdd zenon_Ved) % 1.64/1.90 (-. (p3 zenon_Vxb)) % 1.64/1.90 (-. (p3 Tau_0)) % 1.64/1.90 (-. (p2 zenon_Vkg)) % 1.64/1.90 (r1 zenon_Vni zenon_Voi) % 1.64/1.90 (zenon_Vo != zenon_Vuc) % 1.64/1.90 (-. (p2 Tau_9)) % 1.64/1.90 (zenon_Vq != zenon_Vai) % 1.64/1.90 (-. (p1 zenon_Vsc)) % 1.64/1.90 (-. (p3 zenon_Vob)) % 1.64/1.90 (-. (p4 zenon_Vyd)) % 1.64/1.90 (r1 zenon_Vsf zenon_Vtf) % 1.64/1.90 (-. (p3 zenon_Vge)) % 1.64/1.90 (-. (p4 zenon_Vag)) % 1.64/1.90 (-. (p3 zenon_Vyd)) % 1.64/1.90 (-. (p2 zenon_Vrf)) % 1.64/1.90 (-. (p2 zenon_Veh)) % 1.64/1.90 (-. (p2 zenon_Vni)) % 1.64/1.90 (r1 zenon_Vyf zenon_Vzf) % 1.64/1.90 (r1 zenon_Vgi zenon_Vhi) % 1.64/1.90 (-. (p2 zenon_Vka)) % 1.64/1.90 (-. (p2 zenon_Vaf)) % 1.64/1.90 (zenon_Vm != zenon_Vmj) % 1.64/1.90 (r1 zenon_Vqg zenon_Vrg) % 1.64/1.90 (-. (p1 zenon_Vcg)) % 1.64/1.90 (-. (p3 zenon_Vhe)) % 1.64/1.90 (zenon_Vm != zenon_Vsh) % 1.64/1.90 (zenon_Vq != zenon_Vnd) % 1.64/1.90 (r1 zenon_Vsg zenon_Vxg) % 1.64/1.90 (-. (p1 zenon_Vkf)) % 1.64/1.90 (zenon_Vq != zenon_Vzh) % 1.64/1.90 (zenon_Vq != zenon_Vlh) % 1.64/1.90 (zenon_Vm != zenon_Voi) % 1.64/1.90 (zenon_Vo != zenon_Vmk) % 1.64/1.90 (-. (p4 Tau_5)) % 1.64/1.90 (r1 zenon_Vai zenon_Vbi) % 1.64/1.90 (-. (p4 zenon_Voe)) % 1.64/1.90 (-. (p1 zenon_Vcd)) % 1.64/1.90 (zenon_Vo != zenon_Vgh) % 1.64/1.90 (zenon_Vo != zenon_Voi) % 1.64/1.90 (r1 zenon_Vxb zenon_Vyb) % 1.64/1.90 (zenon_Vq != zenon_Vsi) % 1.64/1.90 (-. (p1 Tau_4)) % 1.64/1.90 (r1 zenon_Vsc zenon_Vtc) % 1.64/1.90 (zenon_Vm != zenon_Vrc) % 1.64/1.90 (r1 zenon_Vii zenon_Vni) % 1.64/1.90 (zenon_Vm != zenon_Vyi) % 1.64/1.90 (zenon_Vo != zenon_Vyi) % 1.64/1.90 (zenon_Vo != zenon_Vsi) % 1.64/1.90 (-. (p3 Tau_9)) % 1.64/1.90 (r1 zenon_Vae zenon_Vge) % 1.64/1.90 (zenon_Vq != zenon_Vyg) % 1.64/1.90 (-. (p3 zenon_Vck)) % 1.64/1.90 (r1 zenon_Vgd zenon_Vnd) % 1.64/1.90 (zenon_Vm != zenon_Vsi) % 1.64/1.90 (zenon_Vo != zenon_Vse) % 1.64/1.90 (zenon_Vo != Tau_15) % 1.64/1.90 (zenon_Vq != Tau_15) % 1.64/1.90 (-. (p2 zenon_Vmb)) % 1.64/1.90 (zenon_Vo != zenon_Vka) % 1.64/1.90 (-. (p1 zenon_Vhc)) % 1.64/1.90 (-. (p3 zenon_Vsi)) % 1.64/1.90 (-. (p4 zenon_Vsg)) % 1.64/1.90 (-. (p3 zenon_Voi)) % 1.64/1.90 (-. (p4 zenon_Vhc)) % 1.64/1.90 (zenon_Vo != zenon_Vaf) % 1.64/1.90 (-. (p3 Tau_13)) % 1.64/1.90 (zenon_Vo != zenon_Ved) % 1.64/1.90 (-. (p1 zenon_Vyd)) % 1.64/1.90 (zenon_Vm != zenon_Vob) % 1.64/1.90 (zenon_Vq != zenon_Vyj) % 1.64/1.90 (r1 Tau_4 zenon_Vbd) % 1.64/1.90 (zenon_Vo != zenon_Vdl) % 1.64/1.90 (r1 zenon_Vgf zenon_Vhf) % 1.64/1.90 (r1 Tau_0 Tau_14) % 1.64/1.90 (-. (p2 zenon_Vbd)) % 1.64/1.90 (-. (p3 zenon_Vrf)) % 1.64/1.90 (-. (p1 zenon_Vqf)) % 1.64/1.90 (-. (p1 zenon_Vhe)) % 1.64/1.90 (-. (p4 zenon_Vsf)) % 1.64/1.90 (-. (p2 zenon_Vcd)) % 1.64/1.90 (-. (p4 zenon_Vxg)) % 1.64/1.90 (-. (p4 zenon_Vjb)) % 1.64/1.90 (-. (p2 zenon_Vcb)) % 1.64/1.90 (-. (p4 zenon_Vhf)) % 1.64/1.90 (-. (p1 zenon_Vck)) % 1.64/1.90 (r1 Tau_2 zenon_Vjb) % 1.64/1.90 (zenon_Vm != zenon_Vhf) % 1.64/1.90 (-. (p3 zenon_Vdh)) % 1.64/1.90 (zenon_Vq != zenon_Vaf) % 1.64/1.90 (zenon_Vq != Tau_4) % 1.64/1.90 (zenon_Vq != zenon_Vhe) % 1.64/1.90 (zenon_Vo != zenon_Vij) % 1.64/1.90 (zenon_Vq != zenon_Vob) % 1.64/1.90 (r1 zenon_Vnd zenon_Vod) % 1.64/1.90 (-. (p1 zenon_Vse)) % 1.64/1.90 (r1 Tau_0 Tau_7) % 1.64/1.90 (-. (p2 zenon_Vkf)) % 1.64/1.90 (-. (p4 zenon_Vze)) % 1.64/1.90 (-. (p3 zenon_Vpd)) % 1.64/1.90 (zenon_Vq != zenon_Vif) % 1.64/1.90 (-. (p1 zenon_Vnd)) % 1.64/1.90 (zenon_Vo != zenon_Vsh) % 1.64/1.90 (r1 Tau_0 Tau_19) % 1.64/1.90 (-. (p4 zenon_Vge)) % 1.64/1.90 (zenon_Vm != zenon_Vyd) % 1.64/1.90 (-. (p4 Tau_9)) % 1.64/1.90 (zenon_Vm != zenon_Vaf) % 1.64/1.90 (zenon_Vq != zenon_Vod) % 1.64/1.90 (r1 zenon_Vpg zenon_Vqg) % 1.64/1.90 (r1 zenon_Vsi zenon_Vti) % 1.64/1.90 (-. (p3 zenon_Vui)) % 1.64/1.90 (p1 zenon_Vq) % 1.64/1.90 (zenon_Vo != zenon_Vge) % 1.64/1.90 (r1 Tau_0 Tau_10) % 1.64/1.90 (-. (p2 Tau_19)) % 1.64/1.90 (zenon_Vq != zenon_Vsf) % 1.64/1.90 (r1 zenon_Vdh zenon_Veh) % 1.64/1.90 (-. (p1 Tau_19)) % 1.64/1.90 (-. (p1 zenon_Veh)) % 1.64/1.90 (-. (p4 zenon_Vrf)) % 1.64/1.90 (zenon_Vm != zenon_Vtc) % 1.64/1.90 (-. (p4 zenon_Vwb)) % 1.64/1.90 (zenon_Vo != zenon_Vmb) % 1.64/1.90 (zenon_Vm != Tau_18) % 1.64/1.90 (zenon_Vo != Tau_18) % 1.64/1.90 (zenon_Vq != Tau_18) % 1.64/1.90 (-. (p4 zenon_Vui)) % 1.64/1.90 (zenon_Vo != zenon_Vod) % 1.64/1.90 (r1 Tau_0 Tau_20) % 1.64/1.90 (zenon_Vo != zenon_Vzh) % 1.64/1.90 (-. (p3 zenon_Vxd)) % 1.64/1.90 (zenon_Vo != zenon_Vkb) % 1.64/1.90 (zenon_Vq != zenon_Vmj) % 1.64/1.90 (-. (p3 zenon_Vwd)) % 1.64/1.90 (zenon_Vm != Tau_14) % 1.64/1.90 (zenon_Vo != Tau_14) % 1.64/1.90 (zenon_Vq != Tau_14) % 1.64/1.90 (-. (p1 Tau_5)) % 1.64/1.90 (-. (p3 zenon_Vyb)) % 1.64/1.90 (-. (p1 Tau_8)) % 1.64/1.90 (zenon_Vq != zenon_Vcd) % 1.64/1.90 (-. (p3 zenon_Vmj)) % 1.64/1.90 (-. (p3 zenon_Vjg)) % 1.64/1.90 (r1 zenon_Vkb zenon_Vlb) % 1.64/1.90 (-. (p2 Tau_15)) % 1.64/1.90 (r1 zenon_Veh zenon_Vfh) % 1.64/1.90 (zenon_Vq != zenon_Vfc) % 1.64/1.90 (-. (p4 zenon_Vye)) % 1.64/1.90 (r1 zenon_Vq zenon_Vr) % 1.64/1.90 (-. (p2 zenon_Vyg)) % 1.64/1.90 (zenon_Vm != zenon_Vgc) % 1.64/1.90 (-. (p4 zenon_Vgc)) % 1.64/1.90 (zenon_Vq != zenon_Vlb) % 1.64/1.90 (-. (p1 zenon_Vkg)) % 1.64/1.90 (-. (p2 zenon_Vej)) % 1.64/1.90 (-. (p4 zenon_Vqg)) % 1.64/1.90 (zenon_Vo != zenon_Vye) % 1.64/1.90 (zenon_Vq != zenon_Ved) % 1.64/1.90 (-. (p2 Tau_10)) % 1.64/1.90 (r1 zenon_Vij zenon_Vjj) % 1.64/1.90 (-. (p4 zenon_Ved)) % 1.64/1.90 (-. (p1 Tau_13)) % 1.64/1.90 (r1 zenon_X21 zenon_Vm) % 1.64/1.90 (-. (p1 Tau_18)) % 1.64/1.90 (r1 Tau_6 zenon_Voe) % 1.64/1.90 (zenon_Vo != zenon_Vqd) % 1.64/1.90 (zenon_Vq != zenon_Vxg) % 1.64/1.90 (zenon_Vq != zenon_Vhc) % 1.64/1.90 (-. (p3 zenon_Vhf)) % 1.64/1.90 (-. (p3 zenon_Vlh)) % 1.64/1.90 (-. (p4 zenon_Vcd)) % 1.64/1.90 (r1 zenon_Vhf zenon_Vif) % 1.64/1.90 (zenon_Vo != zenon_Vag) % 1.64/1.90 (r1 Tau_0 Tau_17) % 1.64/1.90 (r1 Tau_0 Tau_2) % 1.64/1.90 (-. (p1 zenon_Vfi)) % 1.64/1.90 (r1 zenon_Vcj zenon_Vdj) % 1.64/1.90 (zenon_Vo != zenon_Vqe) % 1.64/1.90 (-. (p2 zenon_Vqe)) % 1.64/1.90 (r1 zenon_Vwj zenon_Vxj) % 1.64/1.90 (-. (p3 zenon_Vsf)) % 1.64/1.90 (zenon_Vo != zenon_Vgf) % 1.64/1.90 (-. (p1 Tau_15)) % 1.64/1.90 (-. (p2 zenon_Vui)) % 1.64/1.90 (zenon_Vo != zenon_Vlh) % 1.64/1.90 (-. (p3 zenon_Vse)) % 1.64/1.90 (-. (p2 zenon_Vqg)) % 1.64/1.90 (zenon_Vm != zenon_Vsf) % 1.64/1.90 (zenon_Vq != zenon_Vui) % 1.64/1.90 (zenon_Vm != zenon_Vlb) % 1.64/1.90 (-. (p1 Tau_12)) % 1.64/1.90 (zenon_Vq != zenon_Voj) % 1.64/1.90 (-. (p3 zenon_Vdd)) % 1.64/1.90 (-. (p4 zenon_Vfc)) % 1.64/1.90 (-. (p1 zenon_Vob)) % 1.64/1.90 (-. (p3 zenon_Vcj)) % 1.64/1.90 (-. (p3 Tau_6)) % 1.64/1.90 (r1 zenon_Vvb zenon_Vwb) % 1.64/1.90 (-. (p2 zenon_Vpe)) % 1.64/1.90 (-. (p3 zenon_Vod)) % 1.64/1.90 (r1 zenon_Vkf zenon_Vqf) % 1.64/1.90 (zenon_Vq != zenon_Vwj) % 1.64/1.90 (zenon_Vm != zenon_Vsc) % 1.64/1.90 (zenon_Vo != zenon_Vck) % 1.64/1.90 (r1 zenon_Vsh zenon_Vth) % 1.64/1.90 (-. (p2 zenon_Voi)) % 1.64/1.90 (r1 zenon_Vig zenon_Vjg) % 1.64/1.90 (-. (p3 zenon_Vuc)) % 1.64/1.90 (-. (p1 zenon_Vej)) % 1.64/1.90 (-. (p2 zenon_Vtc)) % 1.64/1.90 (zenon_Vo != zenon_Vcj) % 1.64/1.90 (r1 zenon_Vaf zenon_Vbf) % 1.64/1.90 (r1 zenon_Vlh zenon_Vmh) % 1.64/1.90 (r1 zenon_Voj zenon_Vsj) % 1.64/1.90 (-. (p2 zenon_Vyf)) % 1.64/1.90 (-. (p4 zenon_Vxd)) % 1.64/1.90 (-. (p2 zenon_Vkb)) % 1.64/1.90 (zenon_Vo != zenon_Vsc) % 1.64/1.90 (r1 zenon_Vkc zenon_Vrc) % 1.64/1.90 (-. (p2 Tau_7)) % 1.64/1.90 (-. (p4 zenon_Vnd)) % 1.64/1.90 (-. (p2 zenon_Vyd)) % 1.64/1.90 (-. (p2 Tau_11)) % 1.64/1.90 (zenon_Vq != zenon_Vxb) % 1.64/1.90 (-. (p4 zenon_Vvb)) % 1.64/1.90 (-. (p3 zenon_Vmb)) % 1.64/1.90 (-. (p1 zenon_Vgf)) % 1.64/1.90 (r1 zenon_Vuh zenon_Vzh) % 1.64/1.90 (r1 zenon_Vkg zenon_Vlg) % 1.64/1.90 (-. (p3 zenon_Vyf)) % 1.64/1.90 (-. (p1 zenon_Vye)) % 1.64/1.90 (zenon_Vq != zenon_Vbd) % 1.64/1.90 (zenon_Vm != zenon_Vye) % 1.64/1.90 (zenon_Vo != zenon_Vqg) % 1.64/1.90 (zenon_Vq != zenon_Vcg) % 1.64/1.90 (r1 zenon_Vzh zenon_Vai) % 1.64/1.90 (zenon_Vm != zenon_Vqg) % 1.64/1.90 (-. (p3 zenon_Vsh)) % 1.64/1.90 (zenon_Vq != zenon_Vsh) % 1.64/1.90 (zenon_Vq != zenon_Vgf) % 1.64/1.90 (zenon_Vq != zenon_Vjb) % 1.64/1.90 (-. (p1 zenon_Vqe)) % 1.64/1.90 (zenon_Vm != zenon_Vdh) % 1.64/1.90 (zenon_Vq != Tau_8) % 1.64/1.90 (-. (p1 zenon_Vvb)) % 1.64/1.90 (-. (p1 zenon_Vzf)) % 1.64/1.90 (r1 zenon_Vze zenon_Vaf) % 1.64/1.90 (zenon_Vm != zenon_Vxg) % 1.64/1.90 (zenon_Vo != zenon_Vae) % 1.64/1.90 (r1 zenon_Vsj zenon_Vtj) % 1.64/1.90 (-. (p3 zenon_Vai)) % 1.64/1.90 (-. (p2 zenon_Vpd)) % 1.64/1.90 (zenon_Vm != zenon_Vhe) % 1.64/1.90 (zenon_Vq != zenon_Vuc) % 1.64/1.90 (zenon_Vq != zenon_Voe) % 1.64/1.90 (zenon_Vq != zenon_Vzf) % 1.64/1.90 (-. (p4 zenon_Vpg)) % 1.64/1.90 (r1 Tau_0 Tau_4) % 1.64/1.90 (-. (p1 zenon_Vsj)) % 1.64/1.90 (zenon_Vq != zenon_Vag) % 1.64/1.90 (-. (p3 zenon_Vpg)) % 1.64/1.90 (zenon_Vq != zenon_Vsk) % 1.64/1.90 (-. (p2 zenon_Vjb)) % 1.64/1.90 (-. (p1 zenon_Vwd)) % 1.64/1.90 (-. (p3 Tau_5)) % 1.64/1.90 (r1 zenon_Vcd zenon_Vdd) % 1.64/1.90 (-. (p3 zenon_Veh)) % 1.64/1.90 (zenon_Vm != zenon_Vfi) % 1.64/1.90 (zenon_Vq != zenon_Vmk) % 1.64/1.90 (-. (p2 zenon_Vhe)) % 1.64/1.90 (zenon_Vm != zenon_Vpd) % 1.64/1.90 (-. (p1 zenon_Voe)) % 1.64/1.90 (zenon_Vm != zenon_Vxd) % 1.64/1.90 (-. (p1 Tau_14)) % 1.64/1.90 (zenon_Vo != zenon_Vig) % 1.64/1.90 (-. (p2 zenon_Vse)) % 1.64/1.90 (r1 zenon_Vxd zenon_Vyd) % 1.64/1.90 (zenon_Vq != zenon_Vfi) % 1.64/1.90 (r1 zenon_Vpd zenon_Vqd) % 1.64/1.90 (zenon_Vo != Tau_1) % 1.64/1.90 (-. (p4 zenon_Vwj)) % 1.64/1.90 (-. (p2 zenon_Vkc)) % 1.64/1.90 (r1 zenon_Vzf zenon_Vag) % 1.64/1.90 (-. (p4 zenon_Vsj)) % 1.64/1.90 (zenon_Vm != zenon_Vui) % 1.64/1.90 (-. (p3 zenon_Vsj)) % 1.64/1.90 (zenon_Vo != zenon_Vie) % 1.64/1.90 (zenon_Vq != zenon_Vae) % 1.64/1.90 (-. (p1 zenon_Vyj)) % 1.64/1.90 (-. (p1 zenon_Vii)) % 1.64/1.90 (zenon_Vo != zenon_Vnd) % 1.64/1.90 (zenon_Vo != zenon_Vhf) % 1.64/1.90 (-. (p4 zenon_Vsh)) % 1.64/1.90 (-. (p4 Tau_13)) % 1.64/1.90 (r1 Tau_20 zenon_Vxk) % 1.64/1.90 (-. (p4 zenon_Vdd)) % 1.64/1.90 (zenon_Vo != zenon_Vxb) % 1.64/1.90 (r1 zenon_Vic zenon_Vjc) % 1.64/1.90 (zenon_Vq != Tau_12) % 1.64/1.90 (zenon_Vo != zenon_Vmh) % 1.64/1.90 (-. (p2 zenon_Vae)) % 1.64/1.90 (-. (p3 zenon_Vie)) % 1.64/1.90 (r1 zenon_Vrc zenon_Vsc) % 1.64/1.90 (-. (p1 zenon_Vuc)) % 1.64/1.90 (-. (p1 zenon_Vxg)) % 1.64/1.90 (zenon_Vm != zenon_Vyf) % 1.64/1.90 (zenon_Vq != zenon_Vyd) % 1.64/1.90 (zenon_Vm != zenon_Vze) % 1.64/1.90 (-. (p4 zenon_Vsi)) % 1.64/1.90 (zenon_Vm != zenon_Vdd) % 1.64/1.90 (-. (p2 zenon_Vgc)) % 1.64/1.90 (-. (p2 zenon_Via)) % 1.64/1.90 (zenon_Vq != zenon_Vdh) % 1.64/1.90 (zenon_Vo != zenon_Vrf) % 1.64/1.90 (zenon_Vo != zenon_Vyg) % 1.64/1.90 (-. (p2 zenon_Vcj)) % 1.64/1.90 (-. (p2 zenon_Vgi)) % 1.64/1.90 (-. (p3 zenon_Vsg)) % 1.64/1.90 (r1 zenon_Vyi zenon_Vzi) % 1.64/1.90 (r1 zenon_Vgk zenon_Vjk) % 1.64/1.90 (r1 zenon_Vif zenon_Vjf) % 1.64/1.90 (zenon_Vo != zenon_Vtc) % 1.64/1.90 (zenon_Vm != zenon_Vxb) % 1.64/1.90 (zenon_Vo != zenon_Vrc) % 1.64/1.90 (r1 Tau_0 Tau_8) % 1.64/1.90 (r1 zenon_Vck zenon_Vdk) % 1.64/1.90 (-. (p4 zenon_Vyb)) % 1.64/1.90 (-. (p4 zenon_Vig)) % 1.64/1.90 (-. (p4 zenon_Vkb)) % 1.64/1.90 (zenon_Vm != zenon_Vfc) % 1.64/1.90 (-. (p1 zenon_Vsg)) % 1.64/1.90 (-. (p4 zenon_Vxb)) % 1.64/1.90 (-. (p2 zenon_Vvb)) % 1.64/1.90 (-. (p4 zenon_Vai)) % 1.64/1.90 (-. (p1 zenon_Vmb)) % 1.64/1.90 (r1 Tau_8 zenon_Vyf) % 1.64/1.90 (-. (p3 zenon_Vcd)) % 1.64/1.90 (r1 Tau_16 zenon_Vwj) % 1.64/1.90 (zenon_Vm != Tau_17) % 1.64/1.90 (zenon_Vo != Tau_17) % 1.64/1.90 (zenon_Vq != Tau_17) % 1.64/1.90 (-. (p2 zenon_Vic)) % 1.64/1.90 (zenon_Vm != Tau_2) % 1.64/1.90 (zenon_Vo != Tau_2) % 1.64/1.90 (zenon_Vq != Tau_2) % 1.64/1.90 (-. (p1 zenon_Vge)) % 1.64/1.90 (-. (p2 zenon_Vai)) % 1.64/1.90 (r1 Tau_0 Tau_18) % 1.64/1.90 (zenon_Vq != zenon_Vmh) % 1.64/1.90 (-. (p2 zenon_Vuh)) % 1.64/1.90 (r1 Tau_15 zenon_Vmj) % 1.64/1.90 (zenon_Vm != zenon_Vic) % 1.64/1.90 (zenon_Vm != zenon_Vgh) % 1.64/1.90 (-. (p2 zenon_Ved)) % 1.64/1.90 (-. (p2 Tau_13)) % 1.64/1.90 (-. (p2 zenon_Vfc)) % 1.64/1.90 (-. (p3 zenon_Voe)) % 1.64/1.90 (p3 zenon_Vm) % 1.64/1.90 (-. (p1 zenon_Vqg)) % 1.64/1.90 (r1 zenon_Vye zenon_Vze) % 1.64/1.90 (zenon_Vm != zenon_Vse) % 1.64/1.90 (-. (p2 zenon_Vif)) % 1.64/1.90 (zenon_Vm != zenon_Vgi) % 1.64/1.90 (zenon_Vq != zenon_Vye) % 1.64/1.90 (-. (p2 zenon_Vig)) % 1.64/1.90 (-. (p1 zenon_Vgk)) % 1.64/1.90 (-. (p1 zenon_Vtc)) % 1.64/1.90 (-. (p2 Tau_3)) % 1.64/1.90 (-. (p1 zenon_Vic)) % 1.64/1.90 (-. (p4 zenon_Vij)) % 1.64/1.90 (r1 zenon_Vwb zenon_Vxb) % 1.64/1.90 (-. (p2 zenon_Vdd)) % 1.64/1.90 (-. (p4 zenon_Vqf)) % 1.64/1.90 (-. (p2 zenon_Vlb)) % 1.64/1.90 (-. (p3 zenon_Vfc)) % 1.64/1.90 (-. (p2 zenon_Vsj)) % 1.64/1.90 (-. (p3 zenon_Vn)) % 1.64/1.90 (zenon_Vq != zenon_Vkc) % 1.64/1.90 (-. (p3 zenon_Vwb)) % 1.64/1.90 (-. (p1 zenon_Vif)) % 1.64/1.90 (zenon_Vq != zenon_Vqd) % 1.64/1.90 (-. (p2 zenon_Vge)) % 1.64/1.90 (zenon_Vo != zenon_Vni) % 1.64/1.90 (zenon_Vo != zenon_Vhc) % 1.64/1.90 (-. (p3 zenon_Vwj)) % 1.64/1.90 (zenon_Vo != zenon_Vzf) % 1.64/1.90 (-. (p3 zenon_Vgk)) % 1.64/1.90 (zenon_Vq != zenon_Vgh) % 1.64/1.90 (-. (p2 zenon_Vgf)) % 1.64/1.90 (-. (p1 zenon_Vie)) % 1.64/1.90 (r1 zenon_Vqe zenon_Vre) % 1.64/1.90 (zenon_Vm != zenon_Vzh) % 1.64/1.90 (zenon_Vo != zenon_Vhe) % 1.64/1.90 (-. (p1 zenon_Vgh)) % 1.64/1.90 (zenon_Vq != zenon_Vpd) % 1.64/1.90 (zenon_Vq != zenon_Vgc) % 1.64/1.90 (zenon_Vm != zenon_Vpe) % 1.64/1.90 (r1 Tau_3 zenon_Vfc) % 1.64/1.90 (-. (p2 zenon_Vsf)) % 1.64/1.90 (-. (p3 zenon_Vrc)) % 1.64/1.90 (zenon_Vm != zenon_Vwb) % 1.64/1.90 (-. (p2 zenon_Vsc)) % 1.64/1.90 (-. (p4 zenon_Vmj)) % 1.64/1.90 (zenon_Vm != zenon_Vsg) % 1.64/1.90 (-. (p4 zenon_Vuc)) % 1.64/1.90 (zenon_Vm != zenon_Vrf) % 1.64/1.90 (zenon_Vq != zenon_Vyi) % 1.64/1.90 (-. (p1 zenon_Vsi)) % 1.64/1.90 (-. (p3 zenon_Vzh)) % 1.64/1.90 (r1 Tau_11 zenon_Vrh) % 1.64/1.90 (zenon_Vq != zenon_Vjg) % 1.64/1.90 (zenon_Vm != zenon_Vcd) % 1.64/1.90 (-. (p2 zenon_Vdh)) % 1.64/1.90 (-. (p2 zenon_Vdl)) % 1.64/1.90 (zenon_Vo != zenon_Vmj) % 1.64/1.90 (zenon_Vm != zenon_Vbd) % 1.64/1.90 (zenon_Vo != zenon_Vpd) % 1.64/1.90 (-. (p3 Tau_18)) % 1.64/1.90 (-. (p2 zenon_Vmh)) % 1.64/1.90 (-. (p2 zenon_Vnd)) % 1.64/1.90 (-. (p2 zenon_Vxb)) % 1.64/1.90 (zenon_Vo != zenon_Vel) % 1.64/1.90 (-. (p1 Tau_11)) % 1.64/1.90 (-. (p3 zenon_Vjb)) % 1.64/1.90 (-. (p2 zenon_Vyb)) % 1.64/1.90 (zenon_Vm != zenon_Vqf) % 1.64/1.90 (zenon_Vm != zenon_Vhc) % 1.64/1.90 (zenon_Vo != zenon_Vze) % 1.64/1.90 (zenon_Vm != zenon_Vyb) % 1.64/1.90 (zenon_Vq != zenon_Vqe) % 1.64/1.90 (-. (p1 zenon_Vij)) % 1.64/1.90 (zenon_Vo != zenon_Vsf) % 1.64/1.90 (r1 zenon_Vfc zenon_Vgc) % 1.64/1.90 (r1 zenon_X22 zenon_Vo) % 1.64/1.90 (zenon_Vm != zenon_Voe) % 1.64/1.90 (-. (p1 zenon_Vag)) % 1.64/1.90 (-. (p4 zenon_Vic)) % 1.64/1.90 (-. (p1 zenon_Vcj)) % 1.64/1.90 (-. (p2 zenon_Vp)) % 1.64/1.90 (-. (p2 zenon_Vgh)) % 1.64/1.90 (r1 Tau_5 zenon_Vwd) % 1.64/1.90 (r1 zenon_Vob zenon_Vvb) % 1.64/1.90 (zenon_Vo != zenon_Vqf) % 1.64/1.90 (-. (p3 Tau_2)) % 1.64/1.90 (-. (p3 Tau_14)) % 1.64/1.90 (r1 zenon_Vqd zenon_Vrd) % 1.64/1.90 (zenon_Vq != zenon_Vse) % 1.64/1.90 (zenon_Vq != zenon_Vuh) % 1.64/1.90 (r1 zenon_Vxg zenon_Vyg) % 1.64/1.90 (-. (p3 zenon_Vag)) % 1.64/1.90 (-. (p2 zenon_Vpg)) % 1.64/1.90 (-. (p2 zenon_Vck)) % 1.64/1.90 (r1 zenon_Vhe zenon_Vie) % 1.64/1.90 (zenon_Vq != zenon_Vqg) % 1.64/1.90 (zenon_Vo != Tau_11) % 1.64/1.90 (zenon_Vq != Tau_11) % 1.64/1.90 (zenon_Vo != Tau_7) % 1.64/1.90 (zenon_Vq != Tau_7) % 1.64/1.90 (-. (p2 zenon_Vfi)) % 1.64/1.90 (zenon_Vq != zenon_Vyk) % 1.64/1.90 (zenon_Vm != zenon_Vrh) % 1.64/1.90 (-. (p2 zenon_Vhf)) % 1.64/1.90 (-. (p1 zenon_Vjb)) % 1.64/1.90 (r1 zenon_Vyk zenon_Vbl) % 1.64/1.90 (zenon_Vq != zenon_Vkf) % 1.64/1.90 (-. (p1 Tau_9)) % 1.64/1.90 (-. (p4 zenon_Vrh)) % 1.64/1.90 (-. (p2 zenon_Vqd)) % 1.64/1.90 (-. (p4 zenon_Vjg)) % 1.64/1.90 (-. (p1 zenon_Vui)) % 1.64/1.90 (r1 zenon_Vmb zenon_Vnb) % 1.64/1.90 (r1 Tau_0 Tau_6) % 1.64/1.90 (-. (p3 zenon_Vyi)) % 1.64/1.90 (-. (p4 zenon_Vaf)) % 1.64/1.90 (zenon_Vm != zenon_Vmb) % 1.64/1.90 (-. (p2 zenon_Vhc)) % 1.64/1.90 (zenon_Vo != zenon_Vwj) % 1.64/1.90 (-. (p2 zenon_Vsg)) % 1.64/1.90 (zenon_Vm != zenon_Vvb) % 1.64/1.90 (r1 zenon_Vej zenon_Vij) % 1.64/1.90 (-. (p3 zenon_Vqf)) % 1.64/1.90 (zenon_Vq != zenon_Vqf) % 1.64/1.90 (-. (p1 zenon_Vfc)) % 1.64/1.90 (r1 zenon_Vge zenon_Vhe) % 1.64/1.90 (zenon_Vm != zenon_Vai) % 1.64/1.90 (-. (p1 Tau_7)) % 1.64/1.90 (-. (p1 zenon_Vsf)) % 1.64/1.90 (-. (p2 zenon_Vel)) % 1.64/1.90 (-. (p3 zenon_Vmh)) % 1.64/1.90 (-. (p3 zenon_Vae)) % 1.64/1.90 (-. (p4 zenon_Vlb)) % 1.64/1.90 (zenon_Vq != zenon_Vdd) % 1.64/1.90 (r1 zenon_Vrh zenon_Vsh) % 1.64/1.90 (-. (p3 zenon_Vkg)) % 1.64/1.90 (-. (p3 zenon_Vvb)) % 1.64/1.90 (zenon_Vo != zenon_Vpg) % 1.64/1.90 (-. (p1 zenon_Vig)) % 1.64/1.90 (-. (p1 zenon_Vyf)) % 1.64/1.90 (zenon_Vm != zenon_Vpg) % 1.64/1.90 (r1 Tau_0 Tau_12) % 1.64/1.90 (r1 Tau_14 zenon_Vcj) % 1.64/1.90 (zenon_Vm != zenon_Vae) % 1.64/1.90 (zenon_Vm != Tau_9) % 1.64/1.90 (zenon_Vo != Tau_9) % 1.64/1.90 (zenon_Vq != Tau_9) % 1.64/1.90 (-. (p1 zenon_Vwb)) % 1.64/1.90 (zenon_Vq != zenon_Vtc) % 1.64/1.90 (r1 zenon_Vqf zenon_Vrf) % 1.64/1.90 (zenon_Vo != zenon_Vob) % 1.64/1.90 (zenon_Vq != zenon_Vsc) % 1.64/1.90 (-. (p1 zenon_Vkb)) % 1.64/1.90 (r1 zenon_Vmk zenon_Vpk) % 1.64/1.90 (-. (p1 zenon_Vni)) % 1.64/1.90 (zenon_Vo != zenon_Vif) % 1.64/1.90 (zenon_Vq != zenon_Vii) % 1.64/1.90 (r1 Tau_12 zenon_Vfi) % 1.64/1.90 (-. (p2 zenon_Vod)) % 1.64/1.90 (-. (p3 zenon_Vgc)) % 1.64/1.90 (zenon_Vq != zenon_Vkb) % 1.64/1.90 (-. (p4 zenon_Vdh)) % 1.64/1.90 (r1 zenon_Vgh zenon_Vlh) % 1.64/1.90 (zenon_Vo != Tau_19) % 1.64/1.90 (zenon_Vq != Tau_19) % 1.64/1.90 (zenon_Vm != zenon_Vqe) % 1.64/1.90 (-. (p2 zenon_Vqf)) % 1.64/1.90 (-. (p2 zenon_Vuc)) % 1.64/1.90 (r1 zenon_Vtc zenon_Vuc) % 1.64/1.90 (zenon_Vq != Tau_20) % 1.64/1.90 (zenon_Vm != zenon_Vmh) % 1.64/1.90 (zenon_Vo != zenon_Vcb) % 1.64/1.90 (-. (p2 zenon_Vrc)) % 1.64/1.90 (-. (p1 zenon_Vr)) % 1.64/1.90 (zenon_Vo != zenon_Vdd) % 1.64/1.90 (-. (p3 zenon_Vsc)) % 1.64/1.90 (zenon_Vo != zenon_Vwd) % 1.64/1.90 (zenon_Vq != zenon_Vr) % 1.64/1.90 (zenon_Vo != zenon_Vlb) % 1.64/1.90 (-. (p2 zenon_Vmk)) % 1.64/1.90 (r1 zenon_Vm zenon_Vn) % 1.64/1.90 (-. (p4 zenon_Vyf)) % 1.64/1.90 (zenon_Vm != zenon_Vqd) % 1.64/1.90 (-. (p2 zenon_Vwd)) % 1.64/1.90 (-. (p1 zenon_Vjg)) % 1.64/1.90 (zenon_Vq != zenon_Vej) % 1.64/1.90 (zenon_Vm != zenon_Vjg) % 1.64/1.90 (zenon_Vo != zenon_Vkg) % 1.64/1.90 (zenon_Vo != zenon_Vej) % 1.64/1.90 (-. (p2 zenon_Vmj)) % 1.64/1.90 (-. (p4 Tau_17)) % 1.64/1.90 (-. (p2 zenon_Vwb)) % 1.64/1.90 (-. (p1 zenon_Vgc)) % 1.64/1.90 (zenon_Vm != zenon_Vwd) % 1.64/1.90 (-. (p3 zenon_Vzf)) % 1.64/1.90 (-. (p4 zenon_Vni)) % 1.64/1.90 (r1 zenon_Vod zenon_Vpd) % 1.64/1.90 (r1 Tau_0 Tau_5) % 1.64/1.90 (r1 zenon_Vlb zenon_Vmb) % 1.64/1.90 (zenon_Vo != zenon_Vvb) % 1.64/1.90 (r1 zenon_Vie zenon_Vje) % 1.64/1.90 (zenon_Vq != zenon_Vni) % 1.64/1.90 (-. (p4 zenon_Vgf)) % 1.64/1.90 (-. (p4 zenon_Vie)) % 1.64/1.90 (r1 Tau_18 zenon_Vlk) % 1.64/1.90 (-. (p2 zenon_Vxg)) % 1.64/1.90 (r1 Tau_19 zenon_Vrk) % 1.64/1.90 (r1 zenon_Vpe zenon_Vqe) % 1.64/1.90 (r1 zenon_Vmh zenon_Vnh) % 1.64/1.90 (r1 zenon_Vuc zenon_Vvc) % 1.64/1.90 (zenon_Vm != zenon_Vlh) % 1.64/1.90 (-. (p2 Tau_18)) % 1.64/1.90 (zenon_Vm != zenon_Vcj) % 1.64/1.90 (zenon_Vq != zenon_Vvb) % 1.64/1.90 (-. (p1 Tau_0)) % 1.64/1.90 (zenon_Vm != zenon_Vej) % 1.64/1.90 (r1 zenon_Vag zenon_Vbg) % 1.64/1.90 (-. (p2 zenon_Vxd)) % 1.64/1.90 (-. (p1 zenon_Vuh)) % 1.64/1.90 (zenon_Vm != Tau_10) % 1.64/1.90 (zenon_Vo != Tau_10) % 1.64/1.90 (zenon_Vq != Tau_10) % 1.64/1.90 (r1 Tau_17 zenon_Vfk) % 1.64/1.90 (zenon_Vo != zenon_Vjg) % 1.64/1.90 (zenon_Vo != zenon_Vyf) % 1.64/1.90 (zenon_Vq != zenon_Vij) % 1.64/1.90 (-. (p3 zenon_Vqg)) % 1.64/1.90 (r1 Tau_0 Tau_16) % 1.64/1.90 (zenon_Vo != zenon_Vxd) % 1.64/1.90 (zenon_Vm != zenon_Vig) % 1.64/1.90 (zenon_Vq != zenon_Vgd) % 1.64/1.90 (zenon_Vm != zenon_Vgf) % 1.64/1.90 (zenon_Vo != zenon_Vjb) % 1.64/1.90 (zenon_Vm != zenon_Vij) % 1.64/1.90 (zenon_Vm != zenon_Vyg) % 1.64/1.90 (-. (p2 zenon_Vzf)) % 1.64/1.90 (zenon_Vm != zenon_Ved) % 1.64/1.90 (-. (p1 zenon_Vrc)) % 1.64/1.90 (p2 zenon_Vo) % 1.64/1.90 (zenon_Vm != zenon_Vag) % 1.64/1.90 (r1 zenon_Vyg zenon_Vzg) % 1.64/1.90 (zenon_Vm != zenon_Veh) % 1.64/1.90 (zenon_Vq != zenon_Vge) % 1.64/1.90 (r1 zenon_Vjg zenon_Vkg) % 1.64/1.90 (-. (p3 zenon_Vqd)) % 1.64/1.90 (-. (p3 zenon_Vif)) % 1.64/1.90 (zenon_Vm != zenon_Vsj) % 1.64/1.90 (-. (p2 zenon_Vsh)) % 1.64/1.90 (-. (p4 zenon_Vpd)) % 1.64/1.90 (-. (p1 Tau_16)) % 1.64/1.90 (zenon_Vo != zenon_Via) % 1.64/1.90 (-. (p3 zenon_Vni)) % 1.64/1.90 (zenon_Vq != zenon_Vwd) % 1.64/1.90 (-. (p2 zenon_Vzh)) % 1.64/1.90 (zenon_Vq != zenon_Vyb) % 1.64/1.90 (-. (p1 zenon_Vpg)) % 1.64/1.90 (-. (p2 zenon_Vie)) % 1.64/1.90 (zenon_Vm != zenon_Vni) % 1.64/1.90 (-. (p4 zenon_Vlh)) % 1.64/1.90 (-. (p4 zenon_Vrc)) % 1.64/1.90 (-. (p4 zenon_Voi)) % 1.64/1.90 (zenon_Vo != zenon_Vfi) % 1.64/1.90 (zenon_Vm != zenon_Vif) % 1.64/1.90 (r1 zenon_Vbd zenon_Vcd) % 1.64/1.90 (-. (p1 zenon_Voj)) % 1.64/1.90 (-. (p4 zenon_Vwd)) % 1.64/1.90 (-. (p4 zenon_Vkg)) % 1.64/1.90 (zenon_Vo != zenon_Vyd) % 1.64/1.90 (-. (p1 zenon_Vbd)) % 1.64/1.90 (-. (p1 zenon_Vod)) % 1.64/1.90 (zenon_Vq != zenon_Vcj) % 1.64/1.90 (-. (p1 zenon_Vqd)) % 1.64/1.90 (r1 zenon_Vhc zenon_Vic) % 1.64/1.90 (r1 Tau_7 zenon_Vgf) % 1.64/1.90 *) % 1.64/1.90 (* NO-PROOF *) % 1.64/1.90 % SZS status GaveUp % 1.64/1.90 Number of rewrites on terms: 0 % 1.64/1.90 Number of rewrites on props: 0 % 1.64/1.90 nodes searched: 729 % 1.64/1.90 max branch formulas: 1260 % 1.64/1.90 proof nodes created: 0 % 1.64/1.90 formulas created: 7682 % 1.64/1.90 %------------------------------------------------------------------------------